Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
George Pirlea
Iris
Commits
7ad02b97
Commit
7ad02b97
authored
Nov 17, 2016
by
Robbert Krebbers
Browse files
Prove that Fix_F is proper.
parent
82a63e76
Changes
1
Hide whitespace changes
Inline
Side-by-side
prelude/relations.v
View file @
7ad02b97
...
@@ -221,3 +221,13 @@ nor by conversion tests in the kernel), but in some cases we do need it for
...
@@ -221,3 +221,13 @@ nor by conversion tests in the kernel), but in some cases we do need it for
computation (that is, we cannot make it opaque). We use the [Strategy]
computation (that is, we cannot make it opaque). We use the [Strategy]
command to make its expanding behavior less eager. *)
command to make its expanding behavior less eager. *)
Strategy
100
[
wf_guard
].
Strategy
100
[
wf_guard
].
Lemma
Fix_F_proper
`
{
R
:
relation
A
}
(
B
:
A
→
Type
)
(
E
:
∀
x
,
relation
(
B
x
))
{
E_Equivalence
:
∀
x
,
Equivalence
(
E
x
)}
(
F
:
∀
x
,
(
∀
y
,
R
y
x
→
B
y
)
→
B
x
)
(
HF
:
∀
(
x
:
A
)
(
f
g
:
∀
y
,
R
y
x
→
B
y
),
(
∀
y
Hy
Hy'
,
E
_
(
f
y
Hy
)
(
g
y
Hy'
))
→
E
_
(
F
x
f
)
(
F
x
g
))
(
x
:
A
)
(
acc1
acc2
:
Acc
R
x
)
:
E
_
(
Fix_F
B
F
acc1
)
(
Fix_F
B
F
acc2
).
Proof
.
revert
x
acc1
acc2
.
fix
2
.
intros
x
[
acc1
]
[
acc2
]
;
simpl
;
auto
.
Qed
.
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