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
Rodolphe Lepigre
Iris
Commits
ffc56091
Verified
Commit
ffc56091
authored
Jun 25, 2019
by
Paolo G. Giarrusso
Browse files
Prove `existT a` is NonExpansive & Proper
One of the new proofs needs `sigTO`, so move others together.
parent
6b6c6b63
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/algebra/ofe.v
View file @
ffc56091
...
...
@@ -1325,17 +1325,6 @@ Section sigT.
Definition
sigT_dist_proj1
n
{
x
y
}
:
x
≡
{
n
}
≡
y
→
projT1
x
=
projT1
y
:
=
proj1_ex
.
Definition
sigT_equiv_proj1
x
y
:
x
≡
y
→
projT1
x
=
projT1
y
:
=
λ
H
,
proj1_ex
(
H
0
).
(** [existT] is "non-expansive". *)
Lemma
existT_ne
n
{
i1
i2
}
{
v1
:
P
i1
}
{
v2
:
P
i2
}
:
∀
(
eq
:
i1
=
i2
),
(
rew
f_equal
P
eq
in
v1
≡
{
n
}
≡
v2
)
→
existT
i1
v1
≡
{
n
}
≡
existT
i2
v2
.
Proof
.
intros
->
;
simpl
.
exists
eq_refl
=>
/=.
done
.
Qed
.
Lemma
existT_proper
{
i1
i2
}
{
v1
:
P
i1
}
{
v2
:
P
i2
}
:
∀
(
eq
:
i1
=
i2
),
(
rew
f_equal
P
eq
in
v1
≡
v2
)
→
existT
i1
v1
≡
existT
i2
v2
.
Proof
.
intros
eq
Heq
n
.
apply
(
existT_ne
n
eq
),
equiv_dist
,
Heq
.
Qed
.
Definition
sigT_ofe_mixin
:
OfeMixin
(
sigT
P
).
Proof
.
split
=>
//
n
.
...
...
@@ -1353,6 +1342,26 @@ Section sigT.
Canonical
Structure
sigTO
:
ofeT
:
=
OfeT
(
sigT
P
)
sigT_ofe_mixin
.
(** [existT] is "non-expansive" — general, dependently-typed statement. *)
Lemma
existT_ne
n
{
i1
i2
}
{
v1
:
P
i1
}
{
v2
:
P
i2
}
:
∀
(
eq
:
i1
=
i2
),
(
rew
f_equal
P
eq
in
v1
≡
{
n
}
≡
v2
)
→
existT
i1
v1
≡
{
n
}
≡
existT
i2
v2
.
Proof
.
intros
->
;
simpl
.
exists
eq_refl
=>
/=.
done
.
Qed
.
Lemma
existT_proper
{
i1
i2
}
{
v1
:
P
i1
}
{
v2
:
P
i2
}
:
∀
(
eq
:
i1
=
i2
),
(
rew
f_equal
P
eq
in
v1
≡
v2
)
→
existT
i1
v1
≡
existT
i2
v2
.
Proof
.
intros
eq
Heq
n
.
apply
(
existT_ne
n
eq
),
equiv_dist
,
Heq
.
Qed
.
(** [existT] is "non-expansive" — non-dependently-typed version. *)
Global
Instance
existT_ne_2
a
:
NonExpansive
(@
existT
A
P
a
).
Proof
.
move
=>
???
Heq
.
apply
(
existT_ne
_
eq_refl
Heq
).
Qed
.
Global
Instance
existT_proper_2
a
:
Proper
((
≡
)
==>
(
≡
))
(@
existT
A
P
a
).
Proof
.
apply
ne_proper
,
_
.
Qed
.
(* XXX Which do you prefer? *)
(* Proof. move => ?? Heq. apply (existT_proper eq_refl Heq). Qed. *)
Implicit
Types
(
c
:
chain
sigTO
).
Global
Instance
sigT_discrete
x
:
Discrete
(
projT2
x
)
→
Discrete
x
.
...
...
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