Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
00a054f1
Commit
00a054f1
authored
Feb 25, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Simplify f_equiv a bit.
parent
8a1a8f00
Pipeline
#166
passed with stage
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
5 additions
and
17 deletions
+5
-17
prelude/tactics.v
prelude/tactics.v
+5
-17
No files found.
prelude/tactics.v
View file @
00a054f1
...
...
@@ -233,7 +233,7 @@ Ltac setoid_subst :=
If it cannot solve an equality, it will leave that to the user. *)
Ltac
f_equiv
:
=
(* Deal with "pointwise_relation" *)
try
lazymatch
goal
with
repeat
lazymatch
goal
with
|
|-
pointwise_relation
_
_
_
_
=>
intros
?
end
;
(* Normalize away equalities. *)
...
...
@@ -249,13 +249,9 @@ Ltac f_equiv :=
destruct
x
;
f_equiv
(* First assume that the arguments need the same relation as the result *)
|
|-
?R
(
?f
?x
)
(
?f
_
)
=>
let
H
:
=
fresh
"Proper"
in
assert
(
Proper
(
R
==>
R
)
f
)
as
H
by
(
eapply
_
)
;
apply
H
;
clear
H
;
f_equiv
apply
(
_
:
Proper
(
R
==>
R
)
f
)
;
f_equiv
|
|-
?R
(
?f
?x
?y
)
(
?f
_
_
)
=>
let
H
:
=
fresh
"Proper"
in
assert
(
Proper
(
R
==>
R
==>
R
)
f
)
as
H
by
(
eapply
_
)
;
apply
H
;
clear
H
;
f_equiv
apply
(
_
:
Proper
(
R
==>
R
==>
R
)
f
)
;
f_equiv
(* Next, try to infer the relation. Unfortunately, there is an instance
of Proper for (eq ==> _), which will always be matched. *)
(* TODO: Can we exclude that instance? *)
...
...
@@ -263,17 +259,9 @@ Ltac f_equiv :=
query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *)
|
|-
?R
(
?f
?x
)
(
?f
_
)
=>
let
R1
:
=
fresh
"R"
in
let
H
:
=
fresh
"HProp"
in
let
T
:
=
type
of
x
in
evar
(
R1
:
relation
T
)
;
assert
(
Proper
(
R1
==>
R
)
f
)
as
H
by
(
subst
R1
;
eapply
_
)
;
subst
R1
;
apply
H
;
clear
H
;
f_equiv
apply
(
_
:
Proper
(
_
==>
R
)
f
)
;
f_equiv
|
|-
?R
(
?f
?x
?y
)
(
?f
_
_
)
=>
let
R1
:
=
fresh
"R"
in
let
R2
:
=
fresh
"R"
in
let
H
:
=
fresh
"HProp"
in
let
T1
:
=
type
of
x
in
evar
(
R1
:
relation
T1
)
;
let
T2
:
=
type
of
y
in
evar
(
R2
:
relation
T2
)
;
assert
(
Proper
(
R1
==>
R2
==>
R
)
f
)
as
H
by
(
subst
R1
R2
;
eapply
_
)
;
subst
R1
R2
;
apply
H
;
clear
H
;
f_equiv
apply
(
_
:
Proper
(
_
==>
_
==>
R
)
f
)
;
f_equiv
(* In case the function symbol differs, but the arguments are the same,
maybe we have a pointwise_relation in our context. *)
|
H
:
pointwise_relation
_
?R
?f
?g
|-
?R
(
?f
?x
)
(
?g
?x
)
=>
...
...
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