Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Adam
Iris
Commits
1d937ab3
Commit
1d937ab3
authored
Oct 02, 2021
by
Ralf Jung
Browse files
make f_contractive consistent with f_equiv
parent
9ed67339
Changes
1
Hide whitespace changes
Inline
Side-by-side
iris/algebra/ofe.v
View file @
1d937ab3
...
...
@@ -253,15 +253,17 @@ End contractive.
Ltac
f_contractive
:
=
match
goal
with
|
|-
?f
_
≡
{
_
}
≡
?f
_
=>
simple
apply
(
_
:
Proper
(
dist_later
_
==>
_
)
f
)
|
|-
?f
_
_
≡
{
_
}
≡
?f
_
_
=>
simple
apply
(
_
:
Proper
(
dist_later
_
==>
_
==>
_
)
f
)
|
|-
?f
_
_
≡
{
_
}
≡
?f
_
_
=>
simple
apply
(
_
:
Proper
(
_
==>
dist_later
_
==>
_
)
f
)
|
|-
?f
_
≡
{
_
}
≡
?f
_
=>
simple
apply
(
_
:
Proper
(
dist_later
_
==>
dist
_
)
f
)
|
|-
?f
_
_
≡
{
_
}
≡
?f
_
_
=>
simple
apply
(
_
:
Proper
(
dist_later
_
==>
_
==>
dist
_
)
f
)
|
|-
?f
_
_
≡
{
_
}
≡
?f
_
_
=>
simple
apply
(
_
:
Proper
(
_
==>
dist_later
_
==>
dist
_
)
f
)
end
;
try
match
goal
with
|
|-
@
dist_later
?A
_
?n
?x
?y
=>
destruct
n
as
[|
n
]
;
[
exact
I
|
change
(@
dist
A
_
n
x
y
)]
end
;
try
simple
apply
reflexivity
.
(* Only try reflexivity if the terms are syntactically equal. This avoids
very expensive failing unification. *)
try
match
goal
with
|-
_
?x
?x
=>
simple
apply
reflexivity
end
.
Ltac
solve_contractive
:
=
solve_proper_core
ltac
:
(
fun
_
=>
first
[
f_contractive
|
f_equiv
]).
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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