mirror of https://github.com/nmvdw/HITs-Examples
first step toward cons-union iso: construction of min function for FSet A, where A is Totally Ordered. To construct min, various lemmas about empty set are needed. This min function is constructed in a very inefficient way w.r.t. proofs of assoc, comm, etc.
This commit is contained in:
Leon Gondelman
parent
f8ed41e5fe
commit
0d210cae04
|
|
@ -3,3 +3,5 @@
|
||||||
definition.v
|
definition.v
|
||||||
operations.v
|
operations.v
|
||||||
properties.v
|
properties.v
|
||||||
|
empty_set.v
|
||||||
|
ordered.v
|
||||||
|
|
|
||||||
|
|
@ -190,3 +190,7 @@ Instance FSet_recursion A : HitRecursion (FSet A) := {
|
||||||
H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
|
H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
|
||||||
|
|
||||||
End FSet.
|
End FSet.
|
||||||
|
|
||||||
|
Notation "{| x |}" := (L x).
|
||||||
|
Infix "∪" := U (at level 8, right associativity).
|
||||||
|
Notation "∅" := E.
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,227 @@
|
||||||
|
Require Import HoTT.
|
||||||
|
Require Import HitTactics.
|
||||||
|
Require Import definition.
|
||||||
|
Require Import operations.
|
||||||
|
Require Import properties.
|
||||||
|
|
||||||
|
|
||||||
|
Ltac destruct_match := repeat
|
||||||
|
match goal with
|
||||||
|
| [|- match ?X with | _ => _ end ] => destruct X
|
||||||
|
end.
|
||||||
|
|
||||||
|
Ltac destruct_match_1 :=
|
||||||
|
repeat match goal with
|
||||||
|
| [|- match ?X with | _ => _ end ] => destruct X
|
||||||
|
| [|- ?X = ?Y ] => apply path_ishprop
|
||||||
|
| [ H: ?x <> E |- Empty ] => destruct H
|
||||||
|
| [ H1: ?x = E, H2: ?y = E, H3: ?w ∪ ?q = E |- ?r = E]
|
||||||
|
=> rewrite H1, H2 in H3; rewrite nl in H3; rewrite nl in H3
|
||||||
|
end.
|
||||||
|
|
||||||
|
Ltac eq_neq_tac :=
|
||||||
|
match goal with
|
||||||
|
| [ H: ?x <> E, H': ?x = E |- _ ] => destruct H; assumption
|
||||||
|
end.
|
||||||
|
|
||||||
|
Section EmptySetProperties.
|
||||||
|
|
||||||
|
Context {A : Type}.
|
||||||
|
Context {A_deceq : DecidablePaths A}.
|
||||||
|
|
||||||
|
|
||||||
|
(*Should go to properties *)
|
||||||
|
Lemma union_subset `{Funext} :
|
||||||
|
forall x y z: FSet A, x ∪ y ⊆ z = true -> x ⊆ z = true /\ y ⊆ z = true.
|
||||||
|
intros x y z Hu.
|
||||||
|
split.
|
||||||
|
- eapply subset_isIn. intros a Ha.
|
||||||
|
eapply subset_isIn in Hu.
|
||||||
|
+ instantiate (1 := a) in Hu.
|
||||||
|
assumption.
|
||||||
|
+ transitivity (a ∈ x || a ∈ y)%Bool .
|
||||||
|
apply union_isIn.
|
||||||
|
rewrite Ha. cbn; reflexivity.
|
||||||
|
- eapply subset_isIn. intros a Ha.
|
||||||
|
eapply subset_isIn in Hu.
|
||||||
|
+ instantiate (1 := a) in Hu.
|
||||||
|
assumption.
|
||||||
|
+ rewrite comm. transitivity (a ∈ y || a ∈ x)%Bool .
|
||||||
|
apply union_isIn.
|
||||||
|
rewrite Ha. cbn. reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
Lemma eset_subset_l `{Funext} : forall x: FSet A, x ⊆ ∅ = true -> x = ∅.
|
||||||
|
intros x He.
|
||||||
|
apply eq_subset.
|
||||||
|
split.
|
||||||
|
- cbn; reflexivity.
|
||||||
|
- assumption.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma eset_subset_r `{Funext} : forall x: FSet A, x = ∅ -> x ⊆ ∅ = true.
|
||||||
|
intros x He.
|
||||||
|
apply eq_subset. apply symmetry. assumption.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma subset_transitive `{Funext}:
|
||||||
|
forall x y z, x ⊆ y = true -> y ⊆ z = true -> x ⊆ z = true.
|
||||||
|
intros.
|
||||||
|
Admitted.
|
||||||
|
|
||||||
|
Lemma eset_union_l `{Funext} : forall x y: FSet A, x ∪ y = ∅ -> x = ∅ .
|
||||||
|
Proof.
|
||||||
|
intros.
|
||||||
|
assert (x ⊆ (x ∪ y) = true).
|
||||||
|
apply subset_union_equiv. rewrite assoc. rewrite (union_idem x). reflexivity.
|
||||||
|
apply eset_subset_r in X.
|
||||||
|
assert (x ⊆ ∅ = true).
|
||||||
|
apply (subset_transitive x (U x y)); assumption.
|
||||||
|
apply eset_subset_l.
|
||||||
|
assumption.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma eset_union_lr `{Funext} :
|
||||||
|
forall x y: FSet A, x ∪ y = ∅ -> ((x = ∅) /\ (y = ∅)).
|
||||||
|
Proof.
|
||||||
|
intros.
|
||||||
|
split.
|
||||||
|
apply eset_union_l in X; assumption.
|
||||||
|
rewrite comm in X.
|
||||||
|
apply eset_union_l in X. assumption.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Lemma non_empty_union_l `{Funext} :
|
||||||
|
forall x y: FSet A, x <> E -> x ∪ y <> E.
|
||||||
|
intros x y He.
|
||||||
|
intro Hu.
|
||||||
|
apply He.
|
||||||
|
apply eq_subset in Hu.
|
||||||
|
destruct Hu as [_ H1].
|
||||||
|
apply union_subset in H1.
|
||||||
|
apply eset_subset_l.
|
||||||
|
destruct H1.
|
||||||
|
assumption.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma non_empty_union_r `{Funext} :
|
||||||
|
forall x y: FSet A, y <> E -> x ∪ y <> E.
|
||||||
|
intros x y He.
|
||||||
|
intro Hu.
|
||||||
|
apply He.
|
||||||
|
apply eq_subset in Hu.
|
||||||
|
destruct Hu as [_ H1].
|
||||||
|
apply union_subset in H1.
|
||||||
|
apply eset_subset_l.
|
||||||
|
destruct H1.
|
||||||
|
assumption.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Theorem contrapositive : forall P Q : Type,
|
||||||
|
(P -> Q) -> (not Q -> not P) .
|
||||||
|
Proof.
|
||||||
|
intros p q H1 H2.
|
||||||
|
unfold "~".
|
||||||
|
intro H3.
|
||||||
|
apply H1 in H3. apply H2 in H3. assumption.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Lemma non_empty_singleton : forall a: A, L a <> E.
|
||||||
|
intros a H.
|
||||||
|
enough (false = true).
|
||||||
|
contradiction (false_ne_true X).
|
||||||
|
transitivity (isIn a E).
|
||||||
|
cbn. reflexivity.
|
||||||
|
transitivity (a ∈ (L a)).
|
||||||
|
apply (ap (fun x => a ∈ x) H^) .
|
||||||
|
cbn. destruct (dec (a = a)).
|
||||||
|
reflexivity.
|
||||||
|
destruct n.
|
||||||
|
reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
(* Lemma aux `{Funext}: forall x: FSet A, forall p q: x = ∅ -> False, p = q.
|
||||||
|
intros. apply path_forall. intro.
|
||||||
|
apply path_ishprop.
|
||||||
|
Defined.*)
|
||||||
|
|
||||||
|
|
||||||
|
Lemma fset_eset_dec `{Funext}: forall x: FSet A, x = ∅ \/ x <> ∅.
|
||||||
|
hinduction.
|
||||||
|
- left; reflexivity.
|
||||||
|
- right. apply non_empty_singleton.
|
||||||
|
- intros x y [G1 | G2] [G3 | G4].
|
||||||
|
+ left. rewrite G1, G3. apply nl.
|
||||||
|
+ right. apply non_empty_union_r; assumption.
|
||||||
|
+ right. apply non_empty_union_l; assumption.
|
||||||
|
+ right. apply non_empty_union_l; assumption.
|
||||||
|
- intros. destruct px, py, pz; apply path_sum; destruct_match_1.
|
||||||
|
+ rewrite p, p0, p1. rewrite nl. rewrite nl. reflexivity.
|
||||||
|
+ assumption.
|
||||||
|
+ rewrite p, p0 in p1. rewrite nl in p1. rewrite comm in p1. rewrite nl in p1.
|
||||||
|
assumption.
|
||||||
|
+ rewrite p in p0. rewrite nl in p0.
|
||||||
|
apply (non_empty_union_l y z) in n. eq_neq_tac.
|
||||||
|
+ rewrite p, p0 in p1. rewrite nr in p1. rewrite nr in p1. assumption.
|
||||||
|
+ rewrite p in p0. rewrite nr in p0.
|
||||||
|
apply (non_empty_union_l x z) in n. eq_neq_tac.
|
||||||
|
+ rewrite p in p0. rewrite nr in p0.
|
||||||
|
apply (non_empty_union_l x y) in n. eq_neq_tac.
|
||||||
|
+ apply (non_empty_union_l x y) in n.
|
||||||
|
apply (non_empty_union_l (x ∪ y) z) in n. eq_neq_tac.
|
||||||
|
- intros. destruct px, py; apply path_sum; destruct_match_1.
|
||||||
|
+ rewrite p, p0; apply union_idem.
|
||||||
|
+ rewrite p in p0. rewrite nr in p0. assumption.
|
||||||
|
+ rewrite p in p0. rewrite nl in p0. assumption.
|
||||||
|
+ apply (non_empty_union_r y x) in n. eq_neq_tac.
|
||||||
|
- intros x px.
|
||||||
|
destruct px. apply path_sum; destruct_match_1.
|
||||||
|
+ assumption.
|
||||||
|
+ apply path_sum; destruct_match_1. assumption.
|
||||||
|
- intros x px.
|
||||||
|
destruct px. apply path_sum; destruct_match_1.
|
||||||
|
+ assumption.
|
||||||
|
+ apply path_sum; destruct_match_1. assumption.
|
||||||
|
- intros. cbn. apply path_sum. destruct_match_1.
|
||||||
|
+ apply (non_empty_singleton x). apply p.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Lemma union_non_empty `{Funext}:
|
||||||
|
forall X1 X2: FSet A, U X1 X2 <> ∅ -> X1 <> ∅ \/ X2 <> ∅.
|
||||||
|
intros X1 X2 G.
|
||||||
|
specialize (fset_eset_dec X1).
|
||||||
|
intro. destruct X. rewrite p in G. rewrite nl in G.
|
||||||
|
right. assumption. left. apply n.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma union_non_empty' `{Funext}:
|
||||||
|
forall X1 X2: FSet A, U X1 X2 <> ∅ ->
|
||||||
|
(X1 <> ∅ /\ X2 = ∅) \/
|
||||||
|
(X1 = ∅ /\ X2 <> ∅) \/
|
||||||
|
(X1 <> ∅ /\ X2 <> ∅ ).
|
||||||
|
intros X1 X2 G.
|
||||||
|
specialize (fset_eset_dec X1).
|
||||||
|
specialize (fset_eset_dec X2).
|
||||||
|
intros H1 H2.
|
||||||
|
destruct H1, H2.
|
||||||
|
- rewrite p, p0 in G. destruct G. apply union_idem.
|
||||||
|
- left; split; assumption.
|
||||||
|
- right. left. split; assumption.
|
||||||
|
- right. right. split; assumption.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
End EmptySetProperties.
|
||||||
|
|
@ -0,0 +1,574 @@
|
||||||
|
Require Import HoTT.
|
||||||
|
Require Import HitTactics.
|
||||||
|
Require Import definition.
|
||||||
|
Require Import operations.
|
||||||
|
Require Import properties.
|
||||||
|
Require Import empty_set.
|
||||||
|
Class Antisymmetric {A} (R : relation A) :=
|
||||||
|
antisymmetry : forall x y, R x y -> R y x -> x = y.
|
||||||
|
|
||||||
|
|
||||||
|
Class Total {A} (R : relation A) :=
|
||||||
|
total : forall x y, x = y \/ R x y \/ R y x.
|
||||||
|
|
||||||
|
Class TotalOrder {A} (R : relation A) :=
|
||||||
|
{ TotalOrder_Reflexive : Reflexive R | 2 ;
|
||||||
|
TotalOrder_Antisymmetric : Antisymmetric R | 2;
|
||||||
|
TotalOrder_Transitive : Transitive R | 2;
|
||||||
|
TotalOrder_Total : Total R | 2; }.
|
||||||
|
|
||||||
|
Context {A : Type0}.
|
||||||
|
Context {A_deceq : DecidablePaths A}.
|
||||||
|
Context {R: relation A}.
|
||||||
|
Context {A_ordered : TotalOrder R}.
|
||||||
|
|
||||||
|
|
||||||
|
Ltac eq_neq_tac :=
|
||||||
|
match goal with
|
||||||
|
| [ H: ?x <> E, H': ?x = E |- _ ] => destruct H; assumption
|
||||||
|
end.
|
||||||
|
|
||||||
|
|
||||||
|
Ltac destruct_match_1 :=
|
||||||
|
repeat match goal with
|
||||||
|
| [|- match ?X with | _ => _ end ] => destruct X
|
||||||
|
| [|- ?X = ?Y ] => apply path_ishprop
|
||||||
|
| [ H: ?x <> E |- Empty ] => destruct H
|
||||||
|
| [ H1: ?x = E, H2: ?y = E, H3: ?w ∪ ?q = E |- ?r = E]
|
||||||
|
=> rewrite H1, H2 in H3; rewrite nl in H3; rewrite nl in H3
|
||||||
|
end.
|
||||||
|
|
||||||
|
|
||||||
|
Lemma transport_dom_eq (D1 D2 C: Type) (P: D1 = D2) (f: D1 -> C) :
|
||||||
|
transport (fun T: Type => T -> C) P f = fun y => f (transport (fun X => X) P^ y).
|
||||||
|
Proof.
|
||||||
|
induction P.
|
||||||
|
hott_simpl.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma transport_dom_eq_gen (Ty: Type) (D1 D2: Ty) (C: Type) (P: D1 = D2)
|
||||||
|
(Q : Ty -> Type) (f: Q D1 -> C) :
|
||||||
|
transport (fun X: Ty => Q X -> C) P f = fun y => f (transport Q P^ y).
|
||||||
|
Proof.
|
||||||
|
induction P.
|
||||||
|
hott_simpl.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma min {HFun: Funext} (x: FSet A): x <> ∅ -> A.
|
||||||
|
Proof.
|
||||||
|
hrecursion x.
|
||||||
|
- intro H. destruct H. reflexivity.
|
||||||
|
- intros. exact a.
|
||||||
|
- intros x y rx ry H.
|
||||||
|
apply union_non_empty' in H.
|
||||||
|
destruct H.
|
||||||
|
+ destruct p. specialize (rx fst). exact rx.
|
||||||
|
+ destruct s.
|
||||||
|
* destruct p. specialize (ry snd). exact ry.
|
||||||
|
* destruct p. specialize (rx fst). specialize (ry snd).
|
||||||
|
destruct (TotalOrder_Total rx ry) as [Heq | [ Hx | Hy ]].
|
||||||
|
** exact rx.
|
||||||
|
** exact rx.
|
||||||
|
** exact ry.
|
||||||
|
- intros. rewrite transport_dom_eq_gen.
|
||||||
|
apply path_forall. intro y0.
|
||||||
|
destruct ( union_non_empty' x y ∪ z
|
||||||
|
(transport (fun X : FSet A => X <> ∅) (assoc x y z)^ y0))
|
||||||
|
as [[ G1 G2] | [[ G3 G4] | [G5 G6]]].
|
||||||
|
+ pose (G2' := G2). apply eset_union_lr in G2'; destruct G2'. cbn.
|
||||||
|
destruct (union_non_empty' x ∪ y z y0) as
|
||||||
|
[[H'x H'y] | [ [H'a H'b] | [H'c H'd]]]; try eq_neq_tac.
|
||||||
|
destruct (union_non_empty' x y H'x).
|
||||||
|
** destruct p. assert (G1 = fst0). apply path_forall. intro.
|
||||||
|
apply path_ishprop. rewrite X. reflexivity.
|
||||||
|
** destruct s; destruct p; eq_neq_tac.
|
||||||
|
+ destruct (union_non_empty' y z G4) as
|
||||||
|
[[H'x H'y] | [ [H'a H'b] | [H'c H'd]]]; try eq_neq_tac.
|
||||||
|
destruct (union_non_empty' x ∪ y z y0).
|
||||||
|
** destruct p. cbn. destruct (union_non_empty' x y fst).
|
||||||
|
*** destruct p; eq_neq_tac.
|
||||||
|
*** destruct s. destruct p.
|
||||||
|
**** assert (H'x = snd0). apply path_forall. intro.
|
||||||
|
apply path_ishprop. rewrite X. reflexivity.
|
||||||
|
**** destruct p. eq_neq_tac.
|
||||||
|
** destruct s; destruct p; try eq_neq_tac.
|
||||||
|
** destruct (union_non_empty' x ∪ y z y0).
|
||||||
|
*** destruct p. eq_neq_tac.
|
||||||
|
*** destruct s. destruct p.
|
||||||
|
**** assert (H'b = snd). apply path_forall. intro.
|
||||||
|
apply path_ishprop. rewrite X. reflexivity.
|
||||||
|
**** destruct p. assert (x ∪ y = E).
|
||||||
|
rewrite H'a, G3. apply union_idem. eq_neq_tac.
|
||||||
|
** cbn. destruct (TotalOrder_Total (py H'c) (pz H'd)).
|
||||||
|
*** destruct (union_non_empty' x ∪ y z y0).
|
||||||
|
**** destruct p0. eq_neq_tac.
|
||||||
|
**** destruct s.
|
||||||
|
***** destruct p0. rewrite G3, nl in fst. eq_neq_tac.
|
||||||
|
***** destruct p0. destruct (union_non_empty' x y fst).
|
||||||
|
****** destruct p0. eq_neq_tac.
|
||||||
|
****** destruct s.
|
||||||
|
******* destruct p0.
|
||||||
|
destruct (TotalOrder_Total (py snd0) (pz snd)).
|
||||||
|
f_ap. apply path_forall. intro.
|
||||||
|
apply path_ishprop.
|
||||||
|
destruct s. f_ap. apply path_forall. intro.
|
||||||
|
apply path_ishprop.
|
||||||
|
rewrite p. f_ap. apply path_forall. intro.
|
||||||
|
apply path_ishprop.
|
||||||
|
******* destruct p0. eq_neq_tac.
|
||||||
|
*** destruct (union_non_empty' x ∪ y z y0).
|
||||||
|
**** destruct p. eq_neq_tac.
|
||||||
|
**** destruct s0. destruct p. rewrite comm in fst.
|
||||||
|
apply eset_union_l in fst. eq_neq_tac.
|
||||||
|
destruct p.
|
||||||
|
destruct (union_non_empty' x y fst).
|
||||||
|
***** destruct p; eq_neq_tac.
|
||||||
|
***** destruct s0. destruct p.
|
||||||
|
destruct (TotalOrder_Total (py snd0) (pz snd));
|
||||||
|
destruct s; try (f_ap; apply path_forall; intro;
|
||||||
|
apply path_ishprop).
|
||||||
|
rewrite p. f_ap; apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
destruct s0. f_ap; apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
assert (snd0 = H'c). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
assert (snd = H'd). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
rewrite <- X0 in r. rewrite X in r0.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
destruct s0.
|
||||||
|
assert (snd0 = H'c). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
assert (snd = H'd). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
rewrite <- X in r. rewrite X0 in r0.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
f_ap; apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
destruct p; eq_neq_tac.
|
||||||
|
+ cbn. destruct (union_non_empty' y z G6).
|
||||||
|
** destruct p. destruct ( union_non_empty' x ∪ y z y0).
|
||||||
|
*** destruct p. destruct (union_non_empty' x y fst0).
|
||||||
|
**** destruct p; eq_neq_tac.
|
||||||
|
**** destruct s; destruct p. eq_neq_tac.
|
||||||
|
assert (fst1 = G5). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
assert (fst = snd1). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
rewrite X, X0.
|
||||||
|
destruct (TotalOrder_Total (px G5) (py snd1)).
|
||||||
|
reflexivity.
|
||||||
|
destruct s; reflexivity.
|
||||||
|
*** destruct s; destruct p; eq_neq_tac.
|
||||||
|
** destruct (union_non_empty' x ∪ y z y0).
|
||||||
|
*** destruct p. destruct s; destruct p; eq_neq_tac.
|
||||||
|
*** destruct s. destruct p. destruct s0. destruct p.
|
||||||
|
apply eset_union_l in fst0. eq_neq_tac.
|
||||||
|
**** destruct p.
|
||||||
|
assert (snd = snd0). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
|
||||||
|
destruct (union_non_empty' x y fst0).
|
||||||
|
destruct p.
|
||||||
|
assert (fst1 = G5). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
assert (fst = snd1). apply set_path2.
|
||||||
|
***** rewrite X0. rewrite <- X. reflexivity.
|
||||||
|
***** destruct s; destruct p; eq_neq_tac.
|
||||||
|
**** destruct s0. destruct p0. destruct p.
|
||||||
|
***** apply eset_union_l in fst. eq_neq_tac.
|
||||||
|
***** destruct p, p0.
|
||||||
|
assert (snd0 = snd). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
rewrite X.
|
||||||
|
destruct (union_non_empty' x y fst0).
|
||||||
|
destruct p; eq_neq_tac.
|
||||||
|
destruct s. destruct p; eq_neq_tac.
|
||||||
|
destruct p.
|
||||||
|
assert (fst = snd1). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
assert (fst1 = G5). apply path_forall; intro;
|
||||||
|
apply path_ishprop.
|
||||||
|
rewrite <- X0. rewrite X1.
|
||||||
|
destruct (TotalOrder_Total (py fst) (pz snd)).
|
||||||
|
****** rewrite <- p.
|
||||||
|
destruct (TotalOrder_Total (px G5) (py fst)).
|
||||||
|
rewrite <- p0.
|
||||||
|
destruct (TotalOrder_Total (px G5) (px G5)).
|
||||||
|
reflexivity.
|
||||||
|
destruct s; reflexivity.
|
||||||
|
destruct s. destruct (TotalOrder_Total (px G5) (py fst)).
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
reflexivity.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
destruct (TotalOrder_Total (py fst) (py fst)).
|
||||||
|
reflexivity.
|
||||||
|
destruct s;
|
||||||
|
reflexivity.
|
||||||
|
****** destruct s.
|
||||||
|
destruct (TotalOrder_Total (px G5) (py fst)).
|
||||||
|
destruct (TotalOrder_Total (px G5) (pz snd)).
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
reflexivity. rewrite <- p in r.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
destruct s.
|
||||||
|
destruct ( TotalOrder_Total (px G5) (pz snd)).
|
||||||
|
reflexivity.
|
||||||
|
destruct s. reflexivity.
|
||||||
|
apply (TotalOrder_Transitive (px G5)) in r.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
assumption.
|
||||||
|
destruct (TotalOrder_Total (py fst) (pz snd)). reflexivity.
|
||||||
|
destruct s. reflexivity.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
*******
|
||||||
|
destruct ( TotalOrder_Total (px G5) (py fst)).
|
||||||
|
reflexivity.
|
||||||
|
destruct s. destruct (TotalOrder_Total (px G5) (pz snd)).
|
||||||
|
reflexivity. destruct s; reflexivity.
|
||||||
|
destruct ( TotalOrder_Total (px G5) (pz snd)).
|
||||||
|
rewrite <- p.
|
||||||
|
destruct (TotalOrder_Total (py fst) (px G5)).
|
||||||
|
apply symmetry; assumption.
|
||||||
|
destruct s. rewrite <- p in r.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
reflexivity. destruct s.
|
||||||
|
assert ((py fst) = (pz snd)). apply TotalOrder_Antisymmetric.
|
||||||
|
apply (TotalOrder_Transitive (py fst) (px G5)); assumption.
|
||||||
|
assumption. rewrite X2. assert (px G5 = pz snd).
|
||||||
|
apply TotalOrder_Antisymmetric. assumption.
|
||||||
|
apply (TotalOrder_Transitive (pz snd) (py fst)); assumption.
|
||||||
|
rewrite X3.
|
||||||
|
destruct ( TotalOrder_Total (pz snd) (pz snd)).
|
||||||
|
reflexivity. destruct s; reflexivity.
|
||||||
|
destruct (TotalOrder_Total (py fst) (pz snd)).
|
||||||
|
apply TotalOrder_Antisymmetric. assumption. rewrite p.
|
||||||
|
apply (TotalOrder_Reflexive). destruct s.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption. reflexivity.
|
||||||
|
- intros. rewrite transport_dom_eq_gen.
|
||||||
|
apply path_forall. intro y0. cbn.
|
||||||
|
destruct
|
||||||
|
(union_non_empty' x y
|
||||||
|
(transport (fun X : FSet A => X <> ∅) (comm x y)^ y0)) as
|
||||||
|
[[Hx Hy] | [ [Ha Hb] | [Hc Hd]]];
|
||||||
|
destruct (union_non_empty' y x y0) as
|
||||||
|
[[H'x H'y] | [ [H'a H'b] | [H'c H'd]]];
|
||||||
|
try (eq_neq_tac).
|
||||||
|
assert (Hx = H'b). apply path_forall. intro.
|
||||||
|
apply path_ishprop. rewrite X. reflexivity.
|
||||||
|
assert (Hb = H'x). apply path_forall. intro.
|
||||||
|
apply path_ishprop. rewrite X. reflexivity.
|
||||||
|
assert (Hd = H'c). apply path_forall. intro.
|
||||||
|
apply path_ishprop. rewrite X.
|
||||||
|
assert (H'd = Hc). apply path_forall. intro.
|
||||||
|
apply path_ishprop.
|
||||||
|
rewrite X0. rewrite <- X.
|
||||||
|
destruct
|
||||||
|
(TotalOrder_Total (px Hc) (py Hd)) as [G1 | [G2 | G3]];
|
||||||
|
destruct
|
||||||
|
(TotalOrder_Total (py Hd) (px Hc)) as [T1 | [T2 | T3]];
|
||||||
|
try (assumption);
|
||||||
|
try (reflexivity);
|
||||||
|
try (apply symmetry; assumption);
|
||||||
|
try (apply TotalOrder_Antisymmetric; assumption).
|
||||||
|
|
||||||
|
- intros. rewrite transport_dom_eq_gen.
|
||||||
|
apply path_forall. intro y.
|
||||||
|
destruct (union_non_empty' ∅ x (transport (fun X : FSet A => X <> ∅) (nl x)^ y)).
|
||||||
|
destruct p. eq_neq_tac.
|
||||||
|
destruct s.
|
||||||
|
destruct p.
|
||||||
|
assert (y = snd).
|
||||||
|
apply path_forall. intro.
|
||||||
|
apply path_ishprop. rewrite X. reflexivity.
|
||||||
|
destruct p. destruct fst.
|
||||||
|
- intros. rewrite transport_dom_eq_gen.
|
||||||
|
apply path_forall. intro y.
|
||||||
|
destruct (union_non_empty' x ∅ (transport (fun X : FSet A => X <> ∅) (nr x)^ y)).
|
||||||
|
destruct p. assert (y = fst). apply path_forall. intro.
|
||||||
|
apply path_ishprop. rewrite X. reflexivity.
|
||||||
|
destruct s.
|
||||||
|
destruct p.
|
||||||
|
eq_neq_tac.
|
||||||
|
destruct p.
|
||||||
|
destruct snd.
|
||||||
|
- intros. rewrite transport_dom_eq_gen.
|
||||||
|
apply path_forall. intro y.
|
||||||
|
destruct ( union_non_empty' {|x|} {|x|} (transport (fun X : FSet A => X <> ∅) (idem x)^ y)).
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
reflexivity.
|
||||||
|
destruct p.
|
||||||
|
cbn. destruct (TotalOrder_Total x x). reflexivity.
|
||||||
|
destruct s; reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
Definition minfset {HFun: Funext} :
|
||||||
|
FSet A -> { Y: (FSet A) & (Y = E) + { a: A & Y = L a } }.
|
||||||
|
intro X.
|
||||||
|
hinduction X.
|
||||||
|
- exists E. left. reflexivity.
|
||||||
|
- intro a. exists (L a). right. exists a. reflexivity.
|
||||||
|
- intros IH1 IH2.
|
||||||
|
destruct IH1 as [R1 HR1].
|
||||||
|
destruct IH2 as [R2 HR2].
|
||||||
|
destruct HR1.
|
||||||
|
destruct HR2.
|
||||||
|
exists E; left. reflexivity.
|
||||||
|
destruct s as [a Ha]. exists (L a). right.
|
||||||
|
exists a. reflexivity.
|
||||||
|
destruct HR2.
|
||||||
|
destruct s as [a Ha].
|
||||||
|
exists (L a). right. exists a. reflexivity.
|
||||||
|
destruct s as [a1 Ha1].
|
||||||
|
destruct s0 as [a2 Ha2].
|
||||||
|
assert (a1 = a2 \/ R a1 a2 \/ R a2 a1).
|
||||||
|
apply TotalOrder_Total.
|
||||||
|
destruct X.
|
||||||
|
exists (L a1). right. exists a1. reflexivity.
|
||||||
|
destruct s.
|
||||||
|
exists (L a1). right. exists a1. reflexivity.
|
||||||
|
exists (L a2). right. exists a2. reflexivity.
|
||||||
|
- cbn. intros R1 R2 R3.
|
||||||
|
destruct R1 as [Res1 HR1].
|
||||||
|
destruct HR1 as [HR1E | HR1S].
|
||||||
|
destruct R2 as [Res2 HR2].
|
||||||
|
destruct HR2 as [HR2E | HR2S].
|
||||||
|
destruct R3 as [Res3 HR3].
|
||||||
|
destruct HR3 as [HR3E | HR3S].
|
||||||
|
+ cbn. reflexivity.
|
||||||
|
+ cbn. reflexivity.
|
||||||
|
+ cbn. destruct R3 as [Res3 HR3].
|
||||||
|
destruct HR3 as [HR3E | HR3S].
|
||||||
|
* cbn. reflexivity.
|
||||||
|
* destruct HR2S as [a2 Ha2].
|
||||||
|
destruct HR3S as [a3 Ha3].
|
||||||
|
destruct (TotalOrder_Total a2 a3).
|
||||||
|
** cbn. reflexivity.
|
||||||
|
** destruct s. cbn. reflexivity.
|
||||||
|
cbn. reflexivity.
|
||||||
|
+ destruct HR1S as [a1 Ha1].
|
||||||
|
destruct R2 as [Res2 HR2].
|
||||||
|
destruct HR2 as [HR2E | HR2S].
|
||||||
|
destruct R3 as [Res3 HR3].
|
||||||
|
destruct HR3 as [HR3E | HR3S].
|
||||||
|
* cbn. reflexivity.
|
||||||
|
* destruct HR3S as [a3 Ha3].
|
||||||
|
destruct (TotalOrder_Total a1 a3).
|
||||||
|
reflexivity.
|
||||||
|
destruct s; reflexivity.
|
||||||
|
* destruct HR2S as [a2 Ha2].
|
||||||
|
destruct R3 as [Res3 HR3].
|
||||||
|
destruct HR3 as [HR3E | HR3S].
|
||||||
|
cbn. destruct (TotalOrder_Total a1 a2).
|
||||||
|
cbn. reflexivity.
|
||||||
|
destruct s.
|
||||||
|
cbn. reflexivity.
|
||||||
|
cbn. reflexivity.
|
||||||
|
destruct HR3S as [a3 Ha3].
|
||||||
|
destruct (TotalOrder_Total a2 a3).
|
||||||
|
** rewrite p.
|
||||||
|
destruct (TotalOrder_Total a1 a3).
|
||||||
|
rewrite p0.
|
||||||
|
destruct ( TotalOrder_Total a3 a3).
|
||||||
|
reflexivity.
|
||||||
|
destruct s; reflexivity.
|
||||||
|
destruct s. cbn.
|
||||||
|
destruct (TotalOrder_Total a1 a3).
|
||||||
|
reflexivity.
|
||||||
|
destruct s. reflexivity.
|
||||||
|
assert (a1 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity.
|
||||||
|
cbn. destruct (TotalOrder_Total a3 a3).
|
||||||
|
reflexivity.
|
||||||
|
destruct s; reflexivity.
|
||||||
|
** destruct s.
|
||||||
|
*** cbn. destruct (TotalOrder_Total a1 a2).
|
||||||
|
cbn. destruct (TotalOrder_Total a1 a3).
|
||||||
|
reflexivity.
|
||||||
|
destruct s. reflexivity.
|
||||||
|
rewrite <- p in r.
|
||||||
|
assert (a1 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity.
|
||||||
|
destruct s. cbn.
|
||||||
|
destruct (TotalOrder_Total a1 a3).
|
||||||
|
reflexivity.
|
||||||
|
destruct s. reflexivity.
|
||||||
|
assert (R a1 a3).
|
||||||
|
apply (TotalOrder_Transitive a1 a2); assumption.
|
||||||
|
assert (a1 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X0. reflexivity.
|
||||||
|
cbn. destruct (TotalOrder_Total a2 a3).
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
reflexivity.
|
||||||
|
assert (a2 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity.
|
||||||
|
*** cbn. destruct (TotalOrder_Total a1 a3).
|
||||||
|
rewrite p. destruct (TotalOrder_Total a3 a2).
|
||||||
|
cbn. destruct (TotalOrder_Total a3 a3).
|
||||||
|
reflexivity. destruct s; reflexivity.
|
||||||
|
destruct s. cbn.
|
||||||
|
destruct (TotalOrder_Total a3 a3).
|
||||||
|
reflexivity. destruct s; reflexivity.
|
||||||
|
cbn. destruct (TotalOrder_Total a2 a3).
|
||||||
|
rewrite p0.
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
assert (a2 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity. reflexivity.
|
||||||
|
destruct s.
|
||||||
|
cbn.
|
||||||
|
destruct (TotalOrder_Total a1 a2).
|
||||||
|
cbn.
|
||||||
|
destruct (TotalOrder_Total a1 a3).
|
||||||
|
reflexivity.
|
||||||
|
assert (a1 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric. assumption.
|
||||||
|
rewrite <- p in r. assumption.
|
||||||
|
destruct s. reflexivity. rewrite X. reflexivity.
|
||||||
|
destruct s. cbn.
|
||||||
|
destruct (TotalOrder_Total a1 a3). reflexivity.
|
||||||
|
destruct s. reflexivity.
|
||||||
|
assert (a1 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity.
|
||||||
|
cbn. destruct (TotalOrder_Total a2 a3).
|
||||||
|
rewrite p in r1.
|
||||||
|
assert (a2 = a1).
|
||||||
|
transitivity a3.
|
||||||
|
assumption.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity.
|
||||||
|
destruct s.
|
||||||
|
assert (a1 = a2).
|
||||||
|
apply TotalOrder_Antisymmetric.
|
||||||
|
apply (TotalOrder_Transitive a1 a3); assumption.
|
||||||
|
assumption.
|
||||||
|
rewrite X. reflexivity.
|
||||||
|
assert (a1 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric.
|
||||||
|
assumption.
|
||||||
|
apply (TotalOrder_Transitive a3 a2); assumption.
|
||||||
|
rewrite X. reflexivity.
|
||||||
|
destruct ( TotalOrder_Total a1 a2).
|
||||||
|
cbn.
|
||||||
|
destruct (TotalOrder_Total a1 a3).
|
||||||
|
rewrite p0.
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
assert (a1 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity. reflexivity.
|
||||||
|
destruct s.
|
||||||
|
cbn.
|
||||||
|
destruct (TotalOrder_Total a1 a3 ).
|
||||||
|
rewrite p.
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
assert (a1 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity. reflexivity.
|
||||||
|
cbn.
|
||||||
|
destruct (TotalOrder_Total a1 a3 ).
|
||||||
|
assert (a2 = a3).
|
||||||
|
rewrite p in r1.
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. destruct (TotalOrder_Total a3 a3). reflexivity.
|
||||||
|
destruct s; reflexivity.
|
||||||
|
destruct s.
|
||||||
|
destruct (TotalOrder_Total a2 a3).
|
||||||
|
rewrite p.
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
assert (a2 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity.
|
||||||
|
reflexivity.
|
||||||
|
cbn. destruct (TotalOrder_Total a2 a3).
|
||||||
|
rewrite p.
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
assert (a2 = a3).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X. reflexivity. reflexivity.
|
||||||
|
- cbn. intros R1 R2.
|
||||||
|
destruct R1 as [La1 HR1].
|
||||||
|
destruct HR1 as [HR1E | HR1S].
|
||||||
|
destruct R2 as [La2 HR2].
|
||||||
|
destruct HR2 as [HR2E | HR2S].
|
||||||
|
reflexivity.
|
||||||
|
reflexivity.
|
||||||
|
destruct R2 as [La2 HR2].
|
||||||
|
destruct HR2 as [HR2E | HR2S].
|
||||||
|
reflexivity.
|
||||||
|
destruct HR1S as [a1 Ha1].
|
||||||
|
destruct HR2S as [a2 Ha2].
|
||||||
|
destruct (TotalOrder_Total a1 a2).
|
||||||
|
rewrite p.
|
||||||
|
destruct (TotalOrder_Total a2 a2).
|
||||||
|
reflexivity.
|
||||||
|
destruct s; reflexivity.
|
||||||
|
destruct s.
|
||||||
|
destruct (TotalOrder_Total a2 a1).
|
||||||
|
rewrite p.
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
assert (a1 = a2).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X.
|
||||||
|
reflexivity.
|
||||||
|
reflexivity.
|
||||||
|
destruct (TotalOrder_Total a2 a1).
|
||||||
|
rewrite p.
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
reflexivity.
|
||||||
|
assert (a1 = a2).
|
||||||
|
apply TotalOrder_Antisymmetric; assumption.
|
||||||
|
rewrite X.
|
||||||
|
reflexivity.
|
||||||
|
- cbn. intro R. destruct R as [La HR].
|
||||||
|
destruct HR. rewrite <- p. reflexivity.
|
||||||
|
destruct s as [a1 H].
|
||||||
|
apply (path_sigma' _ H^).
|
||||||
|
rewrite transport_sum.
|
||||||
|
f_ap.
|
||||||
|
rewrite transport_sigma.
|
||||||
|
simpl.
|
||||||
|
simple refine (path_sigma' _ _ _ ).
|
||||||
|
apply transport_const.
|
||||||
|
apply set_path2.
|
||||||
|
|
||||||
|
- intros R. cbn.
|
||||||
|
destruct R as [ R HR].
|
||||||
|
destruct HR as [HE | Ha ].
|
||||||
|
rewrite <- HE. reflexivity.
|
||||||
|
destruct Ha as [a Ha].
|
||||||
|
apply (path_sigma' _ Ha^).
|
||||||
|
rewrite transport_sum.
|
||||||
|
f_ap.
|
||||||
|
rewrite transport_sigma.
|
||||||
|
simpl.
|
||||||
|
simple refine (path_sigma' _ _ _ ).
|
||||||
|
apply transport_const.
|
||||||
|
apply set_path2.
|
||||||
|
- cbn. intro.
|
||||||
|
destruct (TotalOrder_Total x x).
|
||||||
|
reflexivity.
|
||||||
|
destruct s.
|
||||||
|
reflexivity.
|
||||||
|
reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
Require Import HoTT HitTactics.
|
Require Import HoTT HitTactics.
|
||||||
Require Import definition operations.
|
Require Export definition operations.
|
||||||
|
|
||||||
Section properties.
|
Section properties.
|
||||||
|
|
||||||
|
|
@ -9,7 +9,7 @@ Context {A_deceq : DecidablePaths A}.
|
||||||
(** union properties *)
|
(** union properties *)
|
||||||
Theorem union_idem : forall x: FSet A, U x x = x.
|
Theorem union_idem : forall x: FSet A, U x x = x.
|
||||||
Proof.
|
Proof.
|
||||||
hinduction;
|
hinduction;
|
||||||
try (intros ; apply set_path2) ; cbn.
|
try (intros ; apply set_path2) ; cbn.
|
||||||
- apply nl.
|
- apply nl.
|
||||||
- apply idem.
|
- apply idem.
|
||||||
|
|
@ -20,28 +20,27 @@ try (intros ; apply set_path2) ; cbn.
|
||||||
rewrite P.
|
rewrite P.
|
||||||
rewrite (comm y x).
|
rewrite (comm y x).
|
||||||
rewrite <- (assoc x y y).
|
rewrite <- (assoc x y y).
|
||||||
rewrite Q.
|
f_ap.
|
||||||
reflexivity.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
(** isIn properties *)
|
(** isIn properties *)
|
||||||
Lemma isIn_singleton_eq (a b: A) : isIn a (L b) = true -> a = b.
|
Lemma isIn_singleton_eq (a b: A) : isIn a (L b) = true -> a = b.
|
||||||
Proof. unfold isIn. simpl.
|
Proof. unfold isIn. simpl.
|
||||||
destruct (dec (a = b)). intro. apply p.
|
destruct (dec (a = b)). intro. apply p.
|
||||||
intro X.
|
intro X.
|
||||||
contradiction (false_ne_true X).
|
contradiction (false_ne_true X).
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma isIn_empty_false (a: A) : isIn a E = true -> Empty.
|
Lemma isIn_empty_false (a: A) : isIn a E = true -> Empty.
|
||||||
Proof.
|
Proof.
|
||||||
cbv. intro X.
|
cbv. intro X.
|
||||||
contradiction (false_ne_true X).
|
contradiction (false_ne_true X).
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Lemma isIn_union (a: A) (X Y: FSet A) :
|
Lemma isIn_union (a: A) (X Y: FSet A) :
|
||||||
isIn a (U X Y) = (isIn a X || isIn a Y)%Bool.
|
isIn a (U X Y) = (isIn a X || isIn a Y)%Bool.
|
||||||
Proof. reflexivity. Qed.
|
Proof. reflexivity. Qed.
|
||||||
|
|
||||||
(** comprehension properties *)
|
(** comprehension properties *)
|
||||||
Lemma comprehension_false Y : comprehension (fun a => isIn a E) Y = E.
|
Lemma comprehension_false Y : comprehension (fun a => isIn a E) Y = E.
|
||||||
|
|
@ -58,20 +57,20 @@ hrecursion Y; try (intros; apply set_path2).
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Theorem comprehension_or : forall ϕ ψ (x: FSet A),
|
Theorem comprehension_or : forall ϕ ψ (x: FSet A),
|
||||||
comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x)
|
comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x)
|
||||||
(comprehension ψ x).
|
(comprehension ψ x).
|
||||||
Proof.
|
Proof.
|
||||||
intros ϕ ψ.
|
intros ϕ ψ.
|
||||||
hinduction; try (intros; apply set_path2).
|
hinduction; try (intros; apply set_path2).
|
||||||
- cbn. symmetry ; apply nl.
|
- cbn. symmetry ; apply nl.
|
||||||
- cbn. intros.
|
- cbn. intros.
|
||||||
destruct (ϕ a) ; destruct (ψ a) ; symmetry.
|
destruct (ϕ a) ; destruct (ψ a) ; symmetry.
|
||||||
* apply idem.
|
* apply idem.
|
||||||
* apply nr.
|
* apply nr.
|
||||||
* apply nl.
|
* apply nl.
|
||||||
* apply nl.
|
* apply nl.
|
||||||
- simpl. intros x y P Q.
|
- simpl. intros x y P Q.
|
||||||
cbn.
|
cbn.
|
||||||
rewrite P.
|
rewrite P.
|
||||||
rewrite Q.
|
rewrite Q.
|
||||||
rewrite <- assoc.
|
rewrite <- assoc.
|
||||||
|
|
@ -105,8 +104,8 @@ Defined.
|
||||||
|
|
||||||
(** intersection properties *)
|
(** intersection properties *)
|
||||||
Lemma intersection_0l: forall X: FSet A, intersection E X = E.
|
Lemma intersection_0l: forall X: FSet A, intersection E X = E.
|
||||||
Proof.
|
Proof.
|
||||||
hinduction;
|
hinduction;
|
||||||
try (intros ; apply set_path2).
|
try (intros ; apply set_path2).
|
||||||
- reflexivity.
|
- reflexivity.
|
||||||
- intro a.
|
- intro a.
|
||||||
|
|
@ -144,7 +143,7 @@ hinduction; try (intros ; apply set_path2).
|
||||||
destruct (isIn a x) ; destruct (isIn a y).
|
destruct (isIn a x) ; destruct (isIn a y).
|
||||||
* apply idem.
|
* apply idem.
|
||||||
* apply nr.
|
* apply nr.
|
||||||
* apply nl.
|
* apply nl.
|
||||||
* apply nl.
|
* apply nl.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
|
|
@ -163,7 +162,7 @@ hrecursion X; try (intros; apply set_path2).
|
||||||
* destruct (dec (b = a)) as [pb|]; [|reflexivity].
|
* destruct (dec (b = a)) as [pb|]; [|reflexivity].
|
||||||
by contradiction npa.
|
by contradiction npa.
|
||||||
+ cbn -[isIn]. intros Y1 Y2 IH1 IH2.
|
+ cbn -[isIn]. intros Y1 Y2 IH1 IH2.
|
||||||
rewrite IH1.
|
rewrite IH1.
|
||||||
rewrite IH2.
|
rewrite IH2.
|
||||||
symmetry.
|
symmetry.
|
||||||
apply (comprehension_or (fun a => isIn a Y1) (fun a => isIn a Y2) (L a)).
|
apply (comprehension_or (fun a => isIn a Y1) (fun a => isIn a Y2) (L a)).
|
||||||
|
|
@ -171,32 +170,34 @@ hrecursion X; try (intros; apply set_path2).
|
||||||
cbn.
|
cbn.
|
||||||
unfold intersection in *.
|
unfold intersection in *.
|
||||||
rewrite <- IH1.
|
rewrite <- IH1.
|
||||||
rewrite <- IH2.
|
rewrite <- IH2.
|
||||||
apply comprehension_or.
|
apply comprehension_or.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Theorem intersection_idem : forall (X : FSet A), intersection X X = X.
|
Theorem intersection_idem : forall (X : FSet A), intersection X X = X.
|
||||||
Proof.
|
Proof.
|
||||||
hinduction; try (intros; apply set_path2).
|
hinduction; try (intros ; apply set_path2).
|
||||||
- reflexivity.
|
- reflexivity.
|
||||||
- intro a.
|
- intro a.
|
||||||
destruct (dec (a = a)).
|
destruct (dec (a = a)).
|
||||||
* reflexivity.
|
* reflexivity.
|
||||||
* contradiction (n idpath).
|
* contradiction (n idpath).
|
||||||
- intros X Y IHX IHY.
|
- intros X Y IHX IHY.
|
||||||
|
f_ap;
|
||||||
unfold intersection in *.
|
unfold intersection in *.
|
||||||
rewrite comprehension_or.
|
+ transitivity (U (comprehension (fun a => isIn a X) X) (comprehension (fun a => isIn a Y) X)).
|
||||||
rewrite comprehension_or.
|
apply comprehension_or.
|
||||||
rewrite IHX.
|
rewrite IHX.
|
||||||
rewrite IHY.
|
rewrite (comm X).
|
||||||
rewrite comprehension_subset.
|
apply comprehension_subset.
|
||||||
rewrite (comm X).
|
+ transitivity (U (comprehension (fun a => isIn a X) Y) (comprehension (fun a => isIn a Y) Y)).
|
||||||
rewrite comprehension_subset.
|
apply comprehension_or.
|
||||||
reflexivity.
|
rewrite IHY.
|
||||||
|
apply comprehension_subset.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
(** assorted lattice laws *)
|
(** assorted lattice laws *)
|
||||||
Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A,
|
Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A,
|
||||||
intersection (U (L a) z) Y = U (intersection (L a) Y) (intersection z Y).
|
intersection (U (L a) z) Y = U (intersection (L a) Y) (intersection z Y).
|
||||||
Proof.
|
Proof.
|
||||||
hinduction; try (intros ; apply set_path2) ; cbn.
|
hinduction; try (intros ; apply set_path2) ; cbn.
|
||||||
|
|
@ -266,12 +267,10 @@ hinduction x; try (intros ; apply set_path2) ; cbn.
|
||||||
cbn.
|
cbn.
|
||||||
rewrite P.
|
rewrite P.
|
||||||
rewrite Q.
|
rewrite Q.
|
||||||
destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ;
|
destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ;
|
||||||
reflexivity.
|
reflexivity.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Theorem intersection_assoc (X Y Z: FSet A) :
|
Theorem intersection_assoc (X Y Z: FSet A) :
|
||||||
intersection X (intersection Y Z) = intersection (intersection X Y) Z.
|
intersection X (intersection Y Z) = intersection (intersection X Y) Z.
|
||||||
Proof.
|
Proof.
|
||||||
|
|
@ -292,7 +291,7 @@ hinduction X; try (intros ; apply set_path2).
|
||||||
+ reflexivity.
|
+ reflexivity.
|
||||||
+ reflexivity.
|
+ reflexivity.
|
||||||
* rewrite intersection_0l.
|
* rewrite intersection_0l.
|
||||||
reflexivity.
|
reflexivity.
|
||||||
- unfold intersection. cbn.
|
- unfold intersection. cbn.
|
||||||
intros X1 X2 P Q.
|
intros X1 X2 P Q.
|
||||||
rewrite comprehension_or.
|
rewrite comprehension_or.
|
||||||
|
|
@ -314,17 +313,15 @@ hinduction; try (intros ; apply set_path2).
|
||||||
* reflexivity.
|
* reflexivity.
|
||||||
* contradiction (n idpath).
|
* contradiction (n idpath).
|
||||||
- intros X1 X2 P Q.
|
- intros X1 X2 P Q.
|
||||||
rewrite comprehension_or.
|
f_ap; (etransitivity; [ apply comprehension_or |]).
|
||||||
rewrite comprehension_or.
|
rewrite P. rewrite (comm X1).
|
||||||
rewrite P.
|
apply comprehension_subset.
|
||||||
|
|
||||||
rewrite Q.
|
rewrite Q.
|
||||||
rewrite comprehension_subset.
|
apply comprehension_subset.
|
||||||
rewrite (comm X1).
|
|
||||||
rewrite comprehension_subset.
|
|
||||||
reflexivity.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
Theorem distributive_U_int (X1 X2 Y : FSet A) :
|
Theorem distributive_U_int (X1 X2 Y : FSet A) :
|
||||||
U (intersection X1 X2) Y = intersection (U X1 Y) (U X2 Y).
|
U (intersection X1 X2) Y = intersection (U X1 Y) (U X2 Y).
|
||||||
Proof.
|
Proof.
|
||||||
|
|
@ -338,18 +335,21 @@ hinduction X1; try (intros ; apply set_path2) ; cbn.
|
||||||
rewrite p.
|
rewrite p.
|
||||||
rewrite comprehension_subset.
|
rewrite comprehension_subset.
|
||||||
reflexivity.
|
reflexivity.
|
||||||
- intros. unfold intersection. (* TODO isIn is simplified too much *)
|
- intros.
|
||||||
rewrite comprehension_or.
|
assert (Y = intersection (U (L a) Y) Y) as HY.
|
||||||
rewrite comprehension_or.
|
{ unfold intersection. symmetry.
|
||||||
(* rewrite intersection_La. *)
|
transitivity (U (comprehension (fun x => isIn x (L a)) Y) (comprehension (fun x => isIn x Y) Y)).
|
||||||
|
apply comprehension_or.
|
||||||
|
rewrite comprehension_all.
|
||||||
|
apply comprehension_subset. }
|
||||||
|
rewrite <- HY.
|
||||||
admit.
|
admit.
|
||||||
- unfold intersection.
|
- unfold intersection.
|
||||||
cbn.
|
|
||||||
intros Z1 Z2 P Q.
|
intros Z1 Z2 P Q.
|
||||||
rewrite comprehension_or.
|
rewrite comprehension_or.
|
||||||
assert (U (U (comprehension (fun a : A => isIn a Z1) X2)
|
assert (U (U (comprehension (fun a : A => isIn a Z1) X2)
|
||||||
(comprehension (fun a : A => isIn a Z2) X2))
|
(comprehension (fun a : A => isIn a Z2) X2))
|
||||||
Y = U (U (comprehension (fun a : A => isIn a Z1) X2)
|
Y = U (U (comprehension (fun a : A => isIn a Z1) X2)
|
||||||
(comprehension (fun a : A => isIn a Z2) X2))
|
(comprehension (fun a : A => isIn a Z2) X2))
|
||||||
(U Y Y)).
|
(U Y Y)).
|
||||||
rewrite (union_idem Y).
|
rewrite (union_idem Y).
|
||||||
|
|
@ -358,22 +358,23 @@ hinduction X1; try (intros ; apply set_path2) ; cbn.
|
||||||
rewrite <- assoc.
|
rewrite <- assoc.
|
||||||
rewrite (assoc (comprehension (fun a : A => isIn a Z2) X2)).
|
rewrite (assoc (comprehension (fun a : A => isIn a Z2) X2)).
|
||||||
rewrite Q.
|
rewrite Q.
|
||||||
rewrite
|
cbn.
|
||||||
|
rewrite
|
||||||
(comm (U (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)
|
(comm (U (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)
|
||||||
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) Y).
|
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) Y).
|
||||||
rewrite assoc.
|
rewrite assoc.
|
||||||
rewrite P.
|
rewrite P.
|
||||||
rewrite <- assoc.
|
rewrite <- assoc. cbn.
|
||||||
rewrite (assoc (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)).
|
rewrite (assoc (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)).
|
||||||
rewrite (comm (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)).
|
rewrite (comm (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)).
|
||||||
rewrite <- assoc.
|
rewrite <- assoc.
|
||||||
rewrite assoc.
|
rewrite assoc.
|
||||||
enough (C : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) X2)
|
enough (C : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) X2)
|
||||||
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2))
|
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2))
|
||||||
= (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) X2)).
|
= (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) X2)).
|
||||||
rewrite C.
|
rewrite C.
|
||||||
enough (D : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)
|
enough (D : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)
|
||||||
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y))
|
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y))
|
||||||
= (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) Y)).
|
= (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) Y)).
|
||||||
rewrite D.
|
rewrite D.
|
||||||
reflexivity.
|
reflexivity.
|
||||||
|
|
@ -436,49 +437,204 @@ hrecursion X; try (intros ; apply set_path2).
|
||||||
rewrite <- Q.
|
rewrite <- Q.
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
||||||
|
Theorem union_isIn (X Y : FSet A) (a : A) : isIn a (U X Y) = orb (isIn a X) (isIn a Y).
|
||||||
|
Proof.
|
||||||
|
reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
(* Properties about subset relation. *)
|
(* Properties about subset relation. *)
|
||||||
Lemma subsect_intersection `{Funext} (X Y : FSet A) :
|
Lemma subset_union `{Funext} (X Y : FSet A) :
|
||||||
X ⊆ Y = true -> U X Y = Y.
|
subset X Y = true -> U X Y = Y.
|
||||||
Proof.
|
Proof.
|
||||||
hinduction X; try (intros; apply path_forall; intro; apply set_path2).
|
hinduction X; try (intros; apply path_forall; intro; apply set_path2).
|
||||||
- intros. apply nl.
|
- intros. apply nl.
|
||||||
- intros a. hinduction Y;
|
- intros a. hinduction Y;
|
||||||
try (intros; apply path_forall; intro; apply set_path2).
|
try (intros; apply path_forall; intro; apply set_path2).
|
||||||
(*intros. apply equiv_hprop_allpath.*)
|
+ intro. contradiction (false_ne_true).
|
||||||
+ intro. cbn. contradiction (false_ne_true).
|
+ intros. destruct (dec (a = a0)).
|
||||||
+ intros. destruct (dec (a = a0)).
|
rewrite p; apply idem.
|
||||||
rewrite p; apply idem.
|
contradiction (false_ne_true).
|
||||||
contradiction (false_ne_true).
|
+ intros X1 X2 IH1 IH2.
|
||||||
+ intros X1 X2 IH1 IH2.
|
intro Ho.
|
||||||
intro Ho.
|
destruct (isIn a X1);
|
||||||
destruct (isIn a X1);
|
destruct (isIn a X2).
|
||||||
destruct (isIn a X2).
|
* specialize (IH1 idpath).
|
||||||
specialize (IH1 idpath).
|
rewrite assoc. f_ap.
|
||||||
specialize (IH2 idpath).
|
* specialize (IH1 idpath).
|
||||||
rewrite assoc. rewrite IH1. reflexivity.
|
rewrite assoc. f_ap.
|
||||||
specialize (IH1 idpath).
|
* specialize (IH2 idpath).
|
||||||
rewrite assoc. rewrite IH1. reflexivity.
|
rewrite (comm X1 X2).
|
||||||
specialize (IH2 idpath).
|
rewrite assoc. f_ap.
|
||||||
rewrite assoc. rewrite (comm (L a)). rewrite <- assoc. rewrite IH2.
|
* contradiction (false_ne_true).
|
||||||
reflexivity.
|
- intros X1 X2 IH1 IH2 G.
|
||||||
cbn in Ho. contradiction (false_ne_true).
|
destruct (subset X1 Y);
|
||||||
- intros X1 X2 IH1 IH2 G.
|
destruct (subset X2 Y).
|
||||||
destruct (subset X1 Y);
|
* specialize (IH1 idpath).
|
||||||
destruct (subset X2 Y).
|
specialize (IH2 idpath).
|
||||||
specialize (IH1 idpath).
|
rewrite <- assoc. rewrite IH2. apply IH1.
|
||||||
specialize (IH2 idpath).
|
* contradiction (false_ne_true).
|
||||||
rewrite <- assoc. rewrite IH2. rewrite IH1. reflexivity.
|
* contradiction (false_ne_true).
|
||||||
specialize (IH1 idpath).
|
* contradiction (false_ne_true).
|
||||||
apply IH2 in G.
|
|
||||||
rewrite <- assoc. rewrite G. rewrite IH1. reflexivity.
|
|
||||||
specialize (IH2 idpath).
|
|
||||||
apply IH1 in G.
|
|
||||||
rewrite <- assoc. rewrite IH2. rewrite G. reflexivity.
|
|
||||||
specialize (IH1 G). specialize (IH2 G).
|
|
||||||
rewrite <- assoc. rewrite IH2. rewrite IH1. reflexivity.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Theorem
|
Lemma eq1 (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
|
||||||
|
Proof.
|
||||||
|
unshelve eapply BuildEquiv.
|
||||||
|
{ intro H. rewrite H. split; apply union_idem. }
|
||||||
|
unshelve esplit.
|
||||||
|
{ intros [H1 H2]. etransitivity. apply H1^.
|
||||||
|
rewrite comm. apply H2. }
|
||||||
|
intro; apply path_prod; apply set_path2.
|
||||||
|
all: intro; apply set_path2.
|
||||||
|
Defined.
|
||||||
|
|
||||||
End properties.
|
|
||||||
|
Lemma subset_union_l `{Funext} X :
|
||||||
|
forall Y, subset X (U X Y) = true.
|
||||||
|
hinduction X;
|
||||||
|
try (intros; apply path_forall; intro; apply set_path2).
|
||||||
|
- reflexivity.
|
||||||
|
- intros a Y. destruct (dec (a = a)).
|
||||||
|
* reflexivity.
|
||||||
|
* by contradiction n.
|
||||||
|
- intros X1 X2 HX1 HX2 Y.
|
||||||
|
enough (subset X1 (U (U X1 X2) Y) = true).
|
||||||
|
enough (subset X2 (U (U X1 X2) Y) = true).
|
||||||
|
rewrite X. rewrite X0. reflexivity.
|
||||||
|
{ rewrite (comm X1 X2).
|
||||||
|
rewrite <- (assoc X2 X1 Y).
|
||||||
|
apply (HX2 (U X1 Y)). }
|
||||||
|
{ rewrite <- (assoc X1 X2 Y). apply (HX1 (U X2 Y)). }
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma subset_union_equiv `{Funext}
|
||||||
|
: forall X Y : FSet A, subset X Y = true <~> U X Y = Y.
|
||||||
|
Proof.
|
||||||
|
intros X Y.
|
||||||
|
unshelve eapply BuildEquiv.
|
||||||
|
apply subset_union.
|
||||||
|
unshelve esplit.
|
||||||
|
{ intros HXY. rewrite <- HXY. clear HXY.
|
||||||
|
apply subset_union_l. }
|
||||||
|
all: intro; apply set_path2.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma eq_subset `{Funext} (X Y : FSet A) :
|
||||||
|
X = Y <~> ((subset Y X = true) * (subset X Y = true)).
|
||||||
|
Proof.
|
||||||
|
transitivity ((U Y X = X) * (U X Y = Y)).
|
||||||
|
apply eq1.
|
||||||
|
symmetry.
|
||||||
|
eapply equiv_functor_prod'; apply subset_union_equiv.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma subset_isIn `{FE : Funext} (X Y : FSet A) :
|
||||||
|
(forall (a : A), isIn a X = true -> isIn a Y = true)
|
||||||
|
<-> (subset X Y = true).
|
||||||
|
Proof.
|
||||||
|
split.
|
||||||
|
- hinduction X ; try (intros ; apply path_forall ; intro ; apply set_path2).
|
||||||
|
* intros ; reflexivity.
|
||||||
|
* intros a H.
|
||||||
|
apply H.
|
||||||
|
destruct (dec (a = a)).
|
||||||
|
+ reflexivity.
|
||||||
|
+ contradiction (n idpath).
|
||||||
|
* intros X1 X2 H1 H2 H.
|
||||||
|
enough (subset X1 Y = true).
|
||||||
|
rewrite X.
|
||||||
|
enough (subset X2 Y = true).
|
||||||
|
rewrite X0.
|
||||||
|
reflexivity.
|
||||||
|
+ apply H2.
|
||||||
|
intros a Ha.
|
||||||
|
apply H.
|
||||||
|
rewrite Ha.
|
||||||
|
destruct (isIn a X1) ; reflexivity.
|
||||||
|
+ apply H1.
|
||||||
|
intros a Ha.
|
||||||
|
apply H.
|
||||||
|
rewrite Ha.
|
||||||
|
reflexivity.
|
||||||
|
- hinduction X .
|
||||||
|
* intros. contradiction (false_ne_true X0).
|
||||||
|
* intros b H a.
|
||||||
|
destruct (dec (a = b)).
|
||||||
|
+ intros ; rewrite p ; apply H.
|
||||||
|
+ intros X ; contradiction (false_ne_true X).
|
||||||
|
* intros X1 X2.
|
||||||
|
intros IH1 IH2 H1 a H2.
|
||||||
|
destruct (subset X1 Y) ; destruct (subset X2 Y);
|
||||||
|
cbv in H1; try by contradiction false_ne_true.
|
||||||
|
specialize (IH1 idpath a). specialize (IH2 idpath a).
|
||||||
|
destruct (isIn a X1); destruct (isIn a X2);
|
||||||
|
cbv in H2; try by contradiction false_ne_true.
|
||||||
|
by apply IH1.
|
||||||
|
by apply IH1.
|
||||||
|
by apply IH2.
|
||||||
|
* repeat (intro; intros; apply path_forall).
|
||||||
|
intros; intro; intros; apply set_path2.
|
||||||
|
* repeat (intro; intros; apply path_forall).
|
||||||
|
intros; intro; intros; apply set_path2.
|
||||||
|
* repeat (intro; intros; apply path_forall).
|
||||||
|
intros; intro; intros; apply set_path2.
|
||||||
|
* repeat (intro; intros; apply path_forall).
|
||||||
|
intros; intro; intros; apply set_path2.
|
||||||
|
* repeat (intro; intros; apply path_forall);
|
||||||
|
intros; intro; intros; apply set_path2.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Lemma HPropEquiv (X Y : Type) (P : IsHProp X) (Q : IsHProp Y) :
|
||||||
|
(X <-> Y) -> (X <~> Y).
|
||||||
|
Proof.
|
||||||
|
intros [f g].
|
||||||
|
simple refine (BuildEquiv _ _ _ _).
|
||||||
|
apply f.
|
||||||
|
simple refine (BuildIsEquiv _ _ _ _ _ _ _).
|
||||||
|
- apply g.
|
||||||
|
- unfold Sect.
|
||||||
|
intro x.
|
||||||
|
apply Q.
|
||||||
|
- unfold Sect.
|
||||||
|
intro x.
|
||||||
|
apply P.
|
||||||
|
- intros.
|
||||||
|
apply set_path2.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Theorem fset_ext `{Funext} (X Y : FSet A) :
|
||||||
|
X = Y <~> (forall (a : A), isIn a X = isIn a Y).
|
||||||
|
Proof.
|
||||||
|
etransitivity. apply eq_subset.
|
||||||
|
transitivity
|
||||||
|
((forall a, isIn a Y = true -> isIn a X = true)
|
||||||
|
*(forall a, isIn a X = true -> isIn a Y = true)).
|
||||||
|
- eapply equiv_functor_prod'.
|
||||||
|
apply HPropEquiv.
|
||||||
|
exact _.
|
||||||
|
exact _.
|
||||||
|
split ; apply subset_isIn.
|
||||||
|
apply HPropEquiv.
|
||||||
|
exact _.
|
||||||
|
exact _.
|
||||||
|
split ; apply subset_isIn.
|
||||||
|
- apply HPropEquiv.
|
||||||
|
exact _.
|
||||||
|
exact _.
|
||||||
|
split.
|
||||||
|
* intros [H1 H2 a].
|
||||||
|
specialize (H1 a) ; specialize (H2 a).
|
||||||
|
destruct (isIn a X).
|
||||||
|
+ symmetry ; apply (H2 idpath).
|
||||||
|
+ destruct (isIn a Y).
|
||||||
|
{ apply (H1 idpath). }
|
||||||
|
{ reflexivity. }
|
||||||
|
* intros H1.
|
||||||
|
split ; intro a ; intro H2.
|
||||||
|
+ rewrite (H1 a).
|
||||||
|
apply H2.
|
||||||
|
+ rewrite <- (H1 a).
|
||||||
|
apply H2.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
End properties.
|
||||||
Loading…
Reference in New Issue