Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Lennard Gäher
stdpp
Commits
2327e1a2
Commit
2327e1a2
authored
Mar 15, 2021
by
Robbert Krebbers
Browse files
Merge branch 'msammler/f_equiv5' into 'master'
Add more underscores to f_equiv See merge request
iris/stdpp!235
parents
78c857b9
9aede26b
Changes
1
Show whitespace changes
Inline
Side-by-side
theories/tactics.v
View file @
2327e1a2
...
...
@@ -347,6 +347,7 @@ Ltac f_equiv :=
|
|-
?R
(
?f
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
==>
R
==>
R
)
f
)
|
|-
?R
(
?f
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
==>
R
==>
R
==>
R
)
f
)
|
|-
?R
(
?f
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
==>
R
==>
R
==>
R
==>
R
)
f
)
|
|-
?R
(
?f
_
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
==>
R
==>
R
==>
R
==>
R
==>
R
)
f
)
(* For the case in which R is polymorphic, or an operational type class,
like equiv. *)
|
|-
(
?R
_
)
(
?f
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
_
==>
_
)
f
)
...
...
@@ -360,7 +361,10 @@ Ltac f_equiv :=
|
|-
(
?R
_
_
_
)
(
?f
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
_
_
_
==>
R
_
_
_
R
_
_
_
==>
_
)
f
)
|
|-
(
?R
_
)
(
?f
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
_
==>
R
_
==>
R
_
==>
R
_
==>
_
)
f
)
|
|-
(
?R
_
_
)
(
?f
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
_
_
==>
R
_
_
==>
R
_
_
==>
R
_
_
==>
_
)
f
)
|
|-
(
?R
_
_
_
)
(
?f
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
_
_
_
==>
R
_
_
_
R
_
_
_
==>
R
_
_
_
==>
_
)
f
)
|
|-
(
?R
_
_
_
)
(
?f
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
_
_
_
==>
R
_
_
_
==>
R
_
_
_
==>
R
_
_
_
==>
_
)
f
)
|
|-
(
?R
_
)
(
?f
_
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
_
==>
R
_
==>
R
_
==>
R
_
==>
R
_
==>
_
)
f
)
|
|-
(
?R
_
_
)
(
?f
_
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
_
_
==>
R
_
_
==>
R
_
_
==>
R
_
_
==>
R
_
_
==>
_
)
f
)
|
|-
(
?R
_
_
_
)
(
?f
_
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
R
_
_
_
==>
R
_
_
_
==>
R
_
_
_
==>
R
_
_
_
==>
R
_
_
_
==>
_
)
f
)
(* Next, try to infer the relation. Unfortunately, very often, it will turn
the goal into a Leibniz equality so we get stuck. *)
(* TODO: Can we exclude that instance? *)
...
...
@@ -368,6 +372,7 @@ Ltac f_equiv :=
|
|-
?R
(
?f
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
_
==>
_
==>
R
)
f
)
|
|-
?R
(
?f
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
_
==>
_
==>
_
==>
R
)
f
)
|
|-
?R
(
?f
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
_
==>
_
==>
_
==>
_
==>
R
)
f
)
|
|-
?R
(
?f
_
_
_
_
_
)
_
=>
simple
apply
(
_
:
Proper
(
_
==>
_
==>
_
==>
_
==>
_
==>
R
)
f
)
(* In case the function symbol differs, but the arguments are the same,
maybe we have a pointwise_relation in our context. *)
(* TODO: If only some of the arguments are the same, we could also
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment
