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
Tej Chajed
stdpp
Commits
461bc9c9
Commit
461bc9c9
authored
Nov 16, 2017
by
Ralf Jung
Browse files
f_equiv: comments
parent
e1fff8e2
Changes
1
Hide whitespace changes
Inline
Sidebyside
theories/tactics.v
View file @
461bc9c9
...
...
@@ 304,18 +304,18 @@ Ltac f_equiv :=


(
?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
)
(* Next, try to infer the relation. Unfortunately,
there is an instance
of Proper for (eq ==> _), which will always be matched
. *)
(* 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? *)
(* TODO: If some of the arguments are the same, we could also
query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *)


?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. *)
(* 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
query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *)

H
:
pointwise_relation
_
?R
?f
?g

?R
(
?f
?x
)
(
?g
?x
)
=>
simple
apply
H
end
;
try
simple
apply
reflexivity
.
...
...
Write
Preview
Markdown
is supported
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