mirror of https://github.com/nmvdw/HITs-Examples
Merge hrecursion into master
This commit is contained in:
Dan Frumin
commit
25d1e1c969
645
FinSets.v
645
FinSets.v
|
|
@ -1,31 +1,39 @@
|
||||||
Require Import HoTT.
|
|
||||||
Require Export HoTT.
|
Require Export HoTT.
|
||||||
|
Require Import HitTactics.
|
||||||
|
|
||||||
Module Export FinSet.
|
Module Export FinSet.
|
||||||
|
Section FSet.
|
||||||
|
Variable A : Type.
|
||||||
|
|
||||||
Private Inductive FinSets (A : Type) : Type :=
|
Private Inductive FSet : Type :=
|
||||||
| empty : FinSets A
|
| E : FSet
|
||||||
| L : A -> FinSets A
|
| L : A -> FSet
|
||||||
| U : FinSets A -> FinSets A -> FinSets A.
|
| U : FSet -> FSet -> FSet.
|
||||||
|
|
||||||
Axiom assoc : forall (A : Type) (x y z : FinSets A),
|
Notation "{| x |}" := (L x).
|
||||||
U A x (U A y z) = U A (U A x y) z.
|
Infix "∪" := U (at level 8, right associativity).
|
||||||
|
Notation "∅" := E.
|
||||||
|
|
||||||
Axiom comm : forall (A : Type) (x y : FinSets A),
|
Axiom assoc : forall (x y z : FSet ),
|
||||||
U A x y = U A y x.
|
x ∪ (y ∪ z) = (x ∪ y) ∪ z.
|
||||||
|
|
||||||
Axiom nl : forall (A : Type) (x : FinSets A),
|
Axiom comm : forall (x y : FSet),
|
||||||
U A (empty A) x = x.
|
x ∪ y = y ∪ x.
|
||||||
|
|
||||||
Axiom nr : forall (A : Type) (x : FinSets A),
|
Axiom nl : forall (x : FSet),
|
||||||
U A x (empty A) = x.
|
∅ ∪ x = x.
|
||||||
|
|
||||||
Axiom idem : forall (A : Type) (x : A),
|
Axiom nr : forall (x : FSet),
|
||||||
U A (L A x) (L A x) = L A x.
|
x ∪ ∅ = x.
|
||||||
|
|
||||||
Fixpoint FinSets_rec
|
Axiom idem : forall (x : A),
|
||||||
(A : Type)
|
{| x |} ∪ {|x|} = {|x|}.
|
||||||
|
|
||||||
|
Axiom trunc : IsHSet FSet.
|
||||||
|
|
||||||
|
Fixpoint FSet_rec
|
||||||
(P : Type)
|
(P : Type)
|
||||||
|
(H: IsHSet P)
|
||||||
(e : P)
|
(e : P)
|
||||||
(l : A -> P)
|
(l : A -> P)
|
||||||
(u : P -> P -> P)
|
(u : P -> P -> P)
|
||||||
|
|
@ -34,20 +42,20 @@ Fixpoint FinSets_rec
|
||||||
(nlP : forall (x : P), u e x = x)
|
(nlP : forall (x : P), u e x = x)
|
||||||
(nrP : forall (x : P), u x e = x)
|
(nrP : forall (x : P), u x e = x)
|
||||||
(idemP : forall (x : A), u (l x) (l x) = l x)
|
(idemP : forall (x : A), u (l x) (l x) = l x)
|
||||||
(x : FinSets A)
|
(x : FSet)
|
||||||
{struct x}
|
{struct x}
|
||||||
: P
|
: P
|
||||||
:= (match x return _ -> _ -> _ -> _ -> _ -> P with
|
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P with
|
||||||
| empty => fun _ => fun _ => fun _ => fun _ => fun _ => e
|
| E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => e
|
||||||
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => l a
|
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => l a
|
||||||
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => u
|
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => u
|
||||||
(FinSets_rec A P e l u assocP commP nlP nrP idemP y)
|
(FSet_rec P H e l u assocP commP nlP nrP idemP y)
|
||||||
(FinSets_rec A P e l u assocP commP nlP nrP idemP z)
|
(FSet_rec P H e l u assocP commP nlP nrP idemP z)
|
||||||
end) assocP commP nlP nrP idemP.
|
end) assocP commP nlP nrP idemP H.
|
||||||
|
|
||||||
Axiom FinSets_beta_assoc : forall
|
Axiom FSet_rec_beta_assoc : forall
|
||||||
(A : Type)
|
|
||||||
(P : Type)
|
(P : Type)
|
||||||
|
(H: IsHSet P)
|
||||||
(e : P)
|
(e : P)
|
||||||
(l : A -> P)
|
(l : A -> P)
|
||||||
(u : P -> P -> P)
|
(u : P -> P -> P)
|
||||||
|
|
@ -56,17 +64,17 @@ Axiom FinSets_beta_assoc : forall
|
||||||
(nlP : forall (x : P), u e x = x)
|
(nlP : forall (x : P), u e x = x)
|
||||||
(nrP : forall (x : P), u x e = x)
|
(nrP : forall (x : P), u x e = x)
|
||||||
(idemP : forall (x : A), u (l x) (l x) = l x)
|
(idemP : forall (x : A), u (l x) (l x) = l x)
|
||||||
(x y z : FinSets A),
|
(x y z : FSet),
|
||||||
ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (assoc A x y z)
|
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (assoc x y z)
|
||||||
=
|
=
|
||||||
(assocP (FinSets_rec A P e l u assocP commP nlP nrP idemP x)
|
(assocP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
|
||||||
(FinSets_rec A P e l u assocP commP nlP nrP idemP y)
|
(FSet_rec P H e l u assocP commP nlP nrP idemP y)
|
||||||
(FinSets_rec A P e l u assocP commP nlP nrP idemP z)
|
(FSet_rec P H e l u assocP commP nlP nrP idemP z)
|
||||||
).
|
).
|
||||||
|
|
||||||
Axiom FinSets_beta_comm : forall
|
Axiom FSet_rec_beta_comm : forall
|
||||||
(A : Type)
|
|
||||||
(P : Type)
|
(P : Type)
|
||||||
|
(H: IsHSet P)
|
||||||
(e : P)
|
(e : P)
|
||||||
(l : A -> P)
|
(l : A -> P)
|
||||||
(u : P -> P -> P)
|
(u : P -> P -> P)
|
||||||
|
|
@ -75,16 +83,16 @@ Axiom FinSets_beta_comm : forall
|
||||||
(nlP : forall (x : P), u e x = x)
|
(nlP : forall (x : P), u e x = x)
|
||||||
(nrP : forall (x : P), u x e = x)
|
(nrP : forall (x : P), u x e = x)
|
||||||
(idemP : forall (x : A), u (l x) (l x) = l x)
|
(idemP : forall (x : A), u (l x) (l x) = l x)
|
||||||
(x y : FinSets A),
|
(x y : FSet),
|
||||||
ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (comm A x y)
|
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (comm x y)
|
||||||
=
|
=
|
||||||
(commP (FinSets_rec A P e l u assocP commP nlP nrP idemP x)
|
(commP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
|
||||||
(FinSets_rec A P e l u assocP commP nlP nrP idemP y)
|
(FSet_rec P H e l u assocP commP nlP nrP idemP y)
|
||||||
).
|
).
|
||||||
|
|
||||||
Axiom FinSets_beta_nl : forall
|
Axiom FSet_rec_beta_nl : forall
|
||||||
(A : Type)
|
|
||||||
(P : Type)
|
(P : Type)
|
||||||
|
(H: IsHSet P)
|
||||||
(e : P)
|
(e : P)
|
||||||
(l : A -> P)
|
(l : A -> P)
|
||||||
(u : P -> P -> P)
|
(u : P -> P -> P)
|
||||||
|
|
@ -93,15 +101,15 @@ Axiom FinSets_beta_nl : forall
|
||||||
(nlP : forall (x : P), u e x = x)
|
(nlP : forall (x : P), u e x = x)
|
||||||
(nrP : forall (x : P), u x e = x)
|
(nrP : forall (x : P), u x e = x)
|
||||||
(idemP : forall (x : A), u (l x) (l x) = l x)
|
(idemP : forall (x : A), u (l x) (l x) = l x)
|
||||||
(x : FinSets A),
|
(x : FSet),
|
||||||
ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (nl A x)
|
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nl x)
|
||||||
=
|
=
|
||||||
(nlP (FinSets_rec A P e l u assocP commP nlP nrP idemP x)
|
(nlP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
|
||||||
).
|
).
|
||||||
|
|
||||||
Axiom FinSets_beta_nr : forall
|
Axiom FSet_rec_beta_nr : forall
|
||||||
(A : Type)
|
|
||||||
(P : Type)
|
(P : Type)
|
||||||
|
(H: IsHSet P)
|
||||||
(e : P)
|
(e : P)
|
||||||
(l : A -> P)
|
(l : A -> P)
|
||||||
(u : P -> P -> P)
|
(u : P -> P -> P)
|
||||||
|
|
@ -110,15 +118,15 @@ Axiom FinSets_beta_nr : forall
|
||||||
(nlP : forall (x : P), u e x = x)
|
(nlP : forall (x : P), u e x = x)
|
||||||
(nrP : forall (x : P), u x e = x)
|
(nrP : forall (x : P), u x e = x)
|
||||||
(idemP : forall (x : A), u (l x) (l x) = l x)
|
(idemP : forall (x : A), u (l x) (l x) = l x)
|
||||||
(x : FinSets A),
|
(x : FSet),
|
||||||
ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (nr A x)
|
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nr x)
|
||||||
=
|
=
|
||||||
(nrP (FinSets_rec A P e l u assocP commP nlP nrP idemP x)
|
(nrP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
|
||||||
).
|
).
|
||||||
|
|
||||||
Axiom FinSets_beta_idem : forall
|
Axiom FSet_rec_beta_idem : forall
|
||||||
(A : Type)
|
|
||||||
(P : Type)
|
(P : Type)
|
||||||
|
(H: IsHSet P)
|
||||||
(e : P)
|
(e : P)
|
||||||
(l : A -> P)
|
(l : A -> P)
|
||||||
(u : P -> P -> P)
|
(u : P -> P -> P)
|
||||||
|
|
@ -128,200 +136,397 @@ Axiom FinSets_beta_idem : forall
|
||||||
(nrP : forall (x : P), u x e = x)
|
(nrP : forall (x : P), u x e = x)
|
||||||
(idemP : forall (x : A), u (l x) (l x) = l x)
|
(idemP : forall (x : A), u (l x) (l x) = l x)
|
||||||
(x : A),
|
(x : A),
|
||||||
ap (FinSets_rec A P e l u assocP commP nlP nrP idemP) (idem A x)
|
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (idem x)
|
||||||
=
|
=
|
||||||
idemP x.
|
idemP x.
|
||||||
|
|
||||||
|
|
||||||
|
(* Induction principle *)
|
||||||
|
Fixpoint FSet_ind
|
||||||
|
(P : FSet -> Type)
|
||||||
|
(H : forall a : FSet, IsHSet (P a))
|
||||||
|
(eP : P E)
|
||||||
|
(lP : forall a: A, P (L a))
|
||||||
|
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
|
||||||
|
(assocP : forall (x y z : FSet)
|
||||||
|
(px: P x) (py: P y) (pz: P z),
|
||||||
|
assoc x y z #
|
||||||
|
(uP x (U y z) px (uP y z py pz))
|
||||||
|
=
|
||||||
|
(uP (U x y) z (uP x y px py) pz))
|
||||||
|
(commP : forall (x y: FSet) (px: P x) (py: P y),
|
||||||
|
comm x y #
|
||||||
|
uP x y px py = uP y x py px)
|
||||||
|
(nlP : forall (x : FSet) (px: P x),
|
||||||
|
nl x # uP E x eP px = px)
|
||||||
|
(nrP : forall (x : FSet) (px: P x),
|
||||||
|
nr x # uP x E px eP = px)
|
||||||
|
(idemP : forall (x : A),
|
||||||
|
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
|
||||||
|
(x : FSet)
|
||||||
|
{struct x}
|
||||||
|
: P x
|
||||||
|
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
|
||||||
|
| E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP
|
||||||
|
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
|
||||||
|
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
|
||||||
|
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
|
||||||
|
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
|
||||||
|
end) H assocP commP nlP nrP idemP.
|
||||||
|
|
||||||
|
|
||||||
|
Axiom FSet_ind_beta_assoc : forall
|
||||||
|
(P : FSet -> Type)
|
||||||
|
(H : forall a : FSet, IsHSet (P a))
|
||||||
|
(eP : P E)
|
||||||
|
(lP : forall a: A, P (L a))
|
||||||
|
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
|
||||||
|
(assocP : forall (x y z : FSet)
|
||||||
|
(px: P x) (py: P y) (pz: P z),
|
||||||
|
assoc x y z #
|
||||||
|
(uP x (U y z) px (uP y z py pz))
|
||||||
|
=
|
||||||
|
(uP (U x y) z (uP x y px py) pz))
|
||||||
|
(commP : forall (x y: FSet) (px: P x) (py: P y),
|
||||||
|
comm x y #
|
||||||
|
uP x y px py = uP y x py px)
|
||||||
|
(nlP : forall (x : FSet) (px: P x),
|
||||||
|
nl x # uP E x eP px = px)
|
||||||
|
(nrP : forall (x : FSet) (px: P x),
|
||||||
|
nr x # uP x E px eP = px)
|
||||||
|
(idemP : forall (x : A),
|
||||||
|
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
|
||||||
|
(x y z : FSet),
|
||||||
|
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP)
|
||||||
|
(assoc x y z)
|
||||||
|
=
|
||||||
|
(assocP x y z
|
||||||
|
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
|
||||||
|
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
|
||||||
|
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
|
||||||
|
).
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Axiom FSet_ind_beta_comm : forall
|
||||||
|
(P : FSet -> Type)
|
||||||
|
(H : forall a : FSet, IsHSet (P a))
|
||||||
|
(eP : P E)
|
||||||
|
(lP : forall a: A, P (L a))
|
||||||
|
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
|
||||||
|
(assocP : forall (x y z : FSet)
|
||||||
|
(px: P x) (py: P y) (pz: P z),
|
||||||
|
assoc x y z #
|
||||||
|
(uP x (U y z) px (uP y z py pz))
|
||||||
|
=
|
||||||
|
(uP (U x y) z (uP x y px py) pz))
|
||||||
|
(commP : forall (x y : FSet) (px: P x) (py: P y),
|
||||||
|
comm x y #
|
||||||
|
uP x y px py = uP y x py px)
|
||||||
|
(nlP : forall (x : FSet) (px: P x),
|
||||||
|
nl x # uP E x eP px = px)
|
||||||
|
(nrP : forall (x : FSet) (px: P x),
|
||||||
|
nr x # uP x E px eP = px)
|
||||||
|
(idemP : forall (x : A),
|
||||||
|
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
|
||||||
|
(x y : FSet),
|
||||||
|
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (comm x y)
|
||||||
|
=
|
||||||
|
(commP x y
|
||||||
|
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
|
||||||
|
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
|
||||||
|
).
|
||||||
|
|
||||||
|
Axiom FSet_ind_beta_nl : forall
|
||||||
|
(P : FSet -> Type)
|
||||||
|
(H : forall a : FSet, IsHSet (P a))
|
||||||
|
(eP : P E)
|
||||||
|
(lP : forall a: A, P (L a))
|
||||||
|
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
|
||||||
|
(assocP : forall (x y z : FSet)
|
||||||
|
(px: P x) (py: P y) (pz: P z),
|
||||||
|
assoc x y z #
|
||||||
|
(uP x (U y z) px (uP y z py pz))
|
||||||
|
=
|
||||||
|
(uP (U x y) z (uP x y px py) pz))
|
||||||
|
(commP : forall (x y : FSet) (px: P x) (py: P y),
|
||||||
|
comm x y #
|
||||||
|
uP x y px py = uP y x py px)
|
||||||
|
(nlP : forall (x : FSet) (px: P x),
|
||||||
|
nl x # uP E x eP px = px)
|
||||||
|
(nrP : forall (x : FSet) (px: P x),
|
||||||
|
nr x # uP x E px eP = px)
|
||||||
|
(idemP : forall (x : A),
|
||||||
|
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
|
||||||
|
(x : FSet),
|
||||||
|
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nl x)
|
||||||
|
=
|
||||||
|
(nlP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
|
||||||
|
).
|
||||||
|
|
||||||
|
Axiom FSet_ind_beta_nr : forall
|
||||||
|
(P : FSet -> Type)
|
||||||
|
(H : forall a : FSet, IsHSet (P a))
|
||||||
|
(eP : P E)
|
||||||
|
(lP : forall a: A, P (L a))
|
||||||
|
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
|
||||||
|
(assocP : forall (x y z : FSet)
|
||||||
|
(px: P x) (py: P y) (pz: P z),
|
||||||
|
assoc x y z #
|
||||||
|
(uP x (U y z) px (uP y z py pz))
|
||||||
|
=
|
||||||
|
(uP (U x y) z (uP x y px py) pz))
|
||||||
|
(commP : forall (x y : FSet) (px: P x) (py: P y),
|
||||||
|
comm x y #
|
||||||
|
uP x y px py = uP y x py px)
|
||||||
|
(nlP : forall (x : FSet) (px: P x),
|
||||||
|
nl x # uP E x eP px = px)
|
||||||
|
(nrP : forall (x : FSet) (px: P x),
|
||||||
|
nr x # uP x E px eP = px)
|
||||||
|
(idemP : forall (x : A),
|
||||||
|
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
|
||||||
|
(x : FSet),
|
||||||
|
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nr x)
|
||||||
|
=
|
||||||
|
(nrP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
|
||||||
|
).
|
||||||
|
|
||||||
|
Axiom FSet_ind_beta_idem : forall
|
||||||
|
(P : FSet -> Type)
|
||||||
|
(H : forall a : FSet, IsHSet (P a))
|
||||||
|
(eP : P E)
|
||||||
|
(lP : forall a: A, P (L a))
|
||||||
|
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
|
||||||
|
(assocP : forall (x y z : FSet)
|
||||||
|
(px: P x) (py: P y) (pz: P z),
|
||||||
|
assoc x y z #
|
||||||
|
(uP x (U y z) px (uP y z py pz))
|
||||||
|
=
|
||||||
|
(uP (U x y) z (uP x y px py) pz))
|
||||||
|
(commP : forall (x y : FSet) (px: P x) (py: P y),
|
||||||
|
comm x y #
|
||||||
|
uP x y px py = uP y x py px)
|
||||||
|
(nlP : forall (x : FSet) (px: P x),
|
||||||
|
nl x # uP E x eP px = px)
|
||||||
|
(nrP : forall (x : FSet) (px: P x),
|
||||||
|
nr x # uP x E px eP = px)
|
||||||
|
(idemP : forall (x : A),
|
||||||
|
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
|
||||||
|
(x : A),
|
||||||
|
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (idem x)
|
||||||
|
=
|
||||||
|
idemP x.
|
||||||
|
|
||||||
|
End FSet.
|
||||||
|
|
||||||
|
Instance FSet_recursion A : HitRecursion (FSet A) := {
|
||||||
|
indTy := _; recTy := _;
|
||||||
|
H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
|
||||||
|
|
||||||
|
Arguments E {_}.
|
||||||
|
Arguments U {_} _ _.
|
||||||
|
Arguments L {_} _.
|
||||||
|
|
||||||
End FinSet.
|
End FinSet.
|
||||||
|
|
||||||
Definition isIn : forall
|
Section functions.
|
||||||
(A : Type)
|
Parameter A : Type.
|
||||||
(eq : A -> A -> Bool),
|
Context {A_eqdec: DecidablePaths A}.
|
||||||
A -> FinSets A -> Bool.
|
|
||||||
|
Notation "{| x |}" := (L x).
|
||||||
|
Infix "∪" := U (at level 8, right associativity).
|
||||||
|
Notation "∅" := E.
|
||||||
|
|
||||||
|
(** Properties of union *)
|
||||||
|
Lemma union_idem : forall (X : FSet A), U X X = X.
|
||||||
Proof.
|
Proof.
|
||||||
intro A.
|
hinduction; try (intros; apply set_path2).
|
||||||
intro eq.
|
- apply nr.
|
||||||
intro a.
|
- intros. apply idem.
|
||||||
refine (FinSets_rec A _ _ _ _ _ _ _ _ _).
|
- intros X Y HX HY. etransitivity.
|
||||||
Unshelve.
|
rewrite assoc. rewrite (comm _ X Y). rewrite <- (assoc _ Y X X).
|
||||||
|
rewrite comm.
|
||||||
|
rewrite assoc. rewrite HX. rewrite HY. reflexivity.
|
||||||
|
rewrite comm. reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
Focus 6.
|
(** Membership predicate *)
|
||||||
apply false.
|
Definition isIn : A -> FSet A -> Bool.
|
||||||
|
Proof.
|
||||||
|
intros a.
|
||||||
|
hrecursion.
|
||||||
|
- exact false.
|
||||||
|
- intro a'. destruct (dec (a = a')); [exact true | exact false].
|
||||||
|
- apply orb.
|
||||||
|
- intros x y z. compute. destruct x; reflexivity.
|
||||||
|
- intros x y. compute. destruct x, y; reflexivity.
|
||||||
|
- intros x. compute. reflexivity.
|
||||||
|
- intros x. compute. destruct x; reflexivity.
|
||||||
|
- intros a'. compute. destruct (A_eqdec a a'); reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
Focus 6.
|
Infix "∈" := isIn (at level 9, right associativity).
|
||||||
intro a'.
|
|
||||||
apply (eq a a').
|
|
||||||
|
|
||||||
Focus 6.
|
Lemma isIn_singleton_eq a b : a ∈ {| b |} = true -> a = b.
|
||||||
intro b.
|
Proof. cbv.
|
||||||
intro b'.
|
destruct (A_eqdec a b). intro. apply p.
|
||||||
apply (orb b b').
|
intro X.
|
||||||
|
contradiction (false_ne_true X).
|
||||||
|
Defined.
|
||||||
|
|
||||||
Focus 3.
|
Lemma isIn_empty_false a : a ∈ ∅ = true -> Empty.
|
||||||
intros.
|
Proof.
|
||||||
compute.
|
cbv. intro X.
|
||||||
reflexivity.
|
contradiction (false_ne_true X).
|
||||||
|
Defined.
|
||||||
|
|
||||||
Focus 1.
|
Lemma isIn_union a X Y : a ∈ (X ∪ Y) = (a ∈ X || a ∈ Y)%Bool.
|
||||||
intros.
|
Proof. reflexivity. Qed.
|
||||||
compute.
|
|
||||||
destruct x.
|
|
||||||
reflexivity.
|
|
||||||
destruct y.
|
|
||||||
reflexivity.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
Focus 1.
|
(** Set comprehension *)
|
||||||
intros.
|
Definition comprehension :
|
||||||
compute.
|
(A -> Bool) -> FSet A -> FSet A.
|
||||||
destruct x.
|
Proof.
|
||||||
destruct y.
|
intros P.
|
||||||
reflexivity.
|
hrecursion.
|
||||||
reflexivity.
|
- apply E.
|
||||||
destruct y.
|
- intro a.
|
||||||
reflexivity.
|
refine (if (P a) then L a else E).
|
||||||
reflexivity.
|
- apply U.
|
||||||
|
- intros. cbv. apply assoc.
|
||||||
|
- intros. cbv. apply comm.
|
||||||
|
- intros. cbv. apply nl.
|
||||||
|
- intros. cbv. apply nr.
|
||||||
|
- intros. cbv.
|
||||||
|
destruct (P x); simpl.
|
||||||
|
+ apply idem.
|
||||||
|
+ apply nl.
|
||||||
|
Defined.
|
||||||
|
|
||||||
Focus 1.
|
Lemma comprehension_false Y : comprehension (fun a => a ∈ ∅) Y = E.
|
||||||
intros.
|
Proof.
|
||||||
compute.
|
hrecursion Y; try (intros; apply set_path2).
|
||||||
destruct x.
|
- cbn. reflexivity.
|
||||||
reflexivity.
|
- cbn. reflexivity.
|
||||||
reflexivity.
|
- intros x y IHa IHb.
|
||||||
|
cbn.
|
||||||
intros.
|
rewrite IHa.
|
||||||
compute.
|
rewrite IHb.
|
||||||
destruct (eq a x).
|
rewrite nl.
|
||||||
reflexivity.
|
|
||||||
reflexivity.
|
reflexivity.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition comprehension : forall
|
Lemma comprehension_union X Y Z :
|
||||||
(A : Type)
|
U (comprehension (fun a => isIn a Y) X)
|
||||||
(eq : A -> A -> Bool),
|
(comprehension (fun a => isIn a Z) X) =
|
||||||
(A -> Bool) -> FinSets A -> FinSets A.
|
comprehension (fun a => isIn a (U Y Z)) X.
|
||||||
Proof.
|
Proof.
|
||||||
intro A.
|
hrecursion X; try (intros; apply set_path2).
|
||||||
intro eq.
|
- cbn. apply nl.
|
||||||
intro phi.
|
- cbn. intro a.
|
||||||
refine (FinSets_rec A _ _ _ _ _ _ _ _ _).
|
destruct (isIn a Y); simpl;
|
||||||
Unshelve.
|
destruct (isIn a Z); simpl.
|
||||||
|
|
||||||
Focus 6.
|
|
||||||
apply empty.
|
|
||||||
|
|
||||||
Focus 6.
|
|
||||||
intro a.
|
|
||||||
apply (if (phi a) then L A a else (empty A)).
|
|
||||||
|
|
||||||
Focus 6.
|
|
||||||
intro x.
|
|
||||||
intro y.
|
|
||||||
apply (U A x y).
|
|
||||||
|
|
||||||
Focus 3.
|
|
||||||
intros.
|
|
||||||
compute.
|
|
||||||
apply nl.
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
intros.
|
|
||||||
compute.
|
|
||||||
apply assoc.
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
intros.
|
|
||||||
compute.
|
|
||||||
apply comm.
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
intros.
|
|
||||||
compute.
|
|
||||||
apply nr.
|
|
||||||
|
|
||||||
intros.
|
|
||||||
compute.
|
|
||||||
destruct (phi x).
|
|
||||||
apply idem.
|
apply idem.
|
||||||
|
apply nr.
|
||||||
apply nl.
|
apply nl.
|
||||||
|
apply nl.
|
||||||
|
- cbn. intros X1 X2 IH1 IH2.
|
||||||
|
rewrite assoc.
|
||||||
|
rewrite (comm _ (comprehension (fun a : A => isIn a Y) X1)
|
||||||
|
(comprehension (fun a : A => isIn a Y) X2)).
|
||||||
|
rewrite <- (assoc _
|
||||||
|
(comprehension (fun a : A => isIn a Y) X2)
|
||||||
|
(comprehension (fun a : A => isIn a Y) X1)
|
||||||
|
(comprehension (fun a : A => isIn a Z) X1)
|
||||||
|
).
|
||||||
|
rewrite IH1.
|
||||||
|
rewrite comm.
|
||||||
|
rewrite assoc.
|
||||||
|
rewrite (comm _ (comprehension (fun a : A => isIn a Z) X2) _).
|
||||||
|
rewrite IH2.
|
||||||
|
apply comm.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition intersection : forall (A : Type) (eq : A -> A -> Bool),
|
|
||||||
FinSets A -> FinSets A -> FinSets A.
|
Lemma comprehension_idem' `{Funext}:
|
||||||
|
forall (X:FSet A), forall Y, comprehension (fun x => x ∈ (U X Y)) X = X.
|
||||||
Proof.
|
Proof.
|
||||||
intro A.
|
hinduction.
|
||||||
intro eq.
|
all: try (intros; apply path_forall; intro; apply set_path2).
|
||||||
intro x.
|
- intro Y. cbv. reflexivity.
|
||||||
intro y.
|
- intros a Y. cbn.
|
||||||
apply (comprehension A eq (fun (a : A) => isIn A eq a x) y).
|
destruct (dec (a = a)); simpl.
|
||||||
|
+ reflexivity.
|
||||||
|
+ contradiction n. reflexivity.
|
||||||
|
- intros X1 X2 IH1 IH2 Y.
|
||||||
|
cbn -[isIn].
|
||||||
|
f_ap.
|
||||||
|
+ rewrite <- assoc. apply (IH1 (U X2 Y)).
|
||||||
|
+ rewrite (comm _ X1 X2).
|
||||||
|
rewrite <- (assoc _ X2 X1 Y).
|
||||||
|
apply (IH2 (U X1 Y)).
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition subset (A : Type) (eq : A -> A -> Bool) (x : FinSets A) (y : FinSets A) : Bool.
|
Lemma comprehension_idem `{Funext}:
|
||||||
|
forall (X:FSet A), comprehension (fun x => x ∈ X) X = X.
|
||||||
Proof.
|
Proof.
|
||||||
refine (FinSets_rec A _ _ _ _ _ _ _ _ _ _).
|
intros X.
|
||||||
Unshelve.
|
enough (comprehension (fun x : A => isIn x (U X X)) X = X).
|
||||||
|
rewrite (union_idem) in X0. assumption.
|
||||||
Focus 6.
|
apply comprehension_idem'.
|
||||||
apply x.
|
|
||||||
|
|
||||||
Focus 6.
|
|
||||||
apply true.
|
|
||||||
|
|
||||||
Focus 6.
|
|
||||||
intro a.
|
|
||||||
apply (isIn A eq a y).
|
|
||||||
|
|
||||||
Focus 6.
|
|
||||||
intro b.
|
|
||||||
intro b'.
|
|
||||||
apply (andb b b').
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
intros.
|
|
||||||
compute.
|
|
||||||
destruct x0.
|
|
||||||
destruct y0.
|
|
||||||
reflexivity.
|
|
||||||
reflexivity.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
intros.
|
|
||||||
compute.
|
|
||||||
destruct x0.
|
|
||||||
destruct y0.
|
|
||||||
reflexivity.
|
|
||||||
reflexivity.
|
|
||||||
destruct y0.
|
|
||||||
reflexivity.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
intros.
|
|
||||||
compute.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
intros.
|
|
||||||
compute.
|
|
||||||
destruct x0.
|
|
||||||
reflexivity.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
intros.
|
|
||||||
destruct (isIn A eq x0 y).
|
|
||||||
compute.
|
|
||||||
reflexivity.
|
|
||||||
compute.
|
|
||||||
reflexivity.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition equal_set (A : Type) (eq : A -> A -> Bool) (x : FinSets A) (y : FinSets A) : Bool
|
(** Set intersection *)
|
||||||
:= andb (subset A eq x y) (subset A eq y x).
|
Definition intersection :
|
||||||
|
FSet A -> FSet A -> FSet A.
|
||||||
|
Proof.
|
||||||
|
intros X Y.
|
||||||
|
apply (comprehension (fun (a : A) => isIn a X) Y).
|
||||||
|
Defined.
|
||||||
|
|
||||||
Fixpoint eq_nat n m : Bool :=
|
Lemma intersection_comm X Y: intersection X Y = intersection Y X.
|
||||||
match n, m with
|
Proof.
|
||||||
| O, O => true
|
hrecursion X; try (intros; apply set_path2).
|
||||||
| O, S _ => false
|
- cbn. unfold intersection. apply comprehension_false.
|
||||||
| S _, O => false
|
- cbn. unfold intersection. intros a.
|
||||||
| S n1, S m1 => eq_nat n1 m1
|
hrecursion Y; try (intros; apply set_path2).
|
||||||
end.
|
+ cbn. reflexivity.
|
||||||
|
+ cbn. intros.
|
||||||
|
destruct (dec (a0 = a)).
|
||||||
|
rewrite p. destruct (dec (a=a)).
|
||||||
|
reflexivity.
|
||||||
|
contradiction n.
|
||||||
|
reflexivity.
|
||||||
|
destruct (dec (a = a0)).
|
||||||
|
contradiction n. apply p^. reflexivity.
|
||||||
|
+ cbn -[isIn]. intros Y1 Y2 IH1 IH2.
|
||||||
|
rewrite IH1.
|
||||||
|
rewrite IH2.
|
||||||
|
apply (comprehension_union (L a)).
|
||||||
|
- intros X1 X2 IH1 IH2.
|
||||||
|
cbn.
|
||||||
|
unfold intersection in *.
|
||||||
|
rewrite <- IH1.
|
||||||
|
rewrite <- IH2. symmetry.
|
||||||
|
apply comprehension_union.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
|
||||||
|
(** Subset ordering *)
|
||||||
|
Definition subset (x : FSet A) (y : FSet A) : Bool.
|
||||||
|
Proof.
|
||||||
|
hrecursion x.
|
||||||
|
- apply true.
|
||||||
|
- intro a. apply (isIn a y).
|
||||||
|
- intros a b. apply (andb a b).
|
||||||
|
- intros a b c. compute. destruct a; reflexivity.
|
||||||
|
- intros a b. compute. destruct a, b; reflexivity.
|
||||||
|
- intros x. compute. reflexivity.
|
||||||
|
- intros x. compute. destruct x;reflexivity.
|
||||||
|
- intros a. simpl.
|
||||||
|
destruct (isIn a y); reflexivity.
|
||||||
|
Defined.
|
||||||
|
|
||||||
|
Infix "⊆" := subset (at level 8, right associativity).
|
||||||
|
|
||||||
|
End functions.
|
||||||
|
|
@ -0,0 +1,85 @@
|
||||||
|
Class HitRecursion (H : Type) := {
|
||||||
|
indTy : Type;
|
||||||
|
recTy : Type;
|
||||||
|
H_inductor : indTy;
|
||||||
|
H_recursor : recTy
|
||||||
|
}.
|
||||||
|
|
||||||
|
Definition hrecursion (H : Type) {HR : HitRecursion H} : @recTy H HR :=
|
||||||
|
@H_recursor H HR.
|
||||||
|
|
||||||
|
Definition hinduction (H : Type) {HR : HitRecursion H} : @indTy H HR :=
|
||||||
|
@H_inductor H HR.
|
||||||
|
|
||||||
|
Ltac hrecursion_ :=
|
||||||
|
lazymatch goal with
|
||||||
|
| [ |- ?T -> ?P ] =>
|
||||||
|
let hrec1 := eval cbv[hrecursion H_recursor] in (hrecursion T) in
|
||||||
|
let hrec := eval simpl in hrec1 in
|
||||||
|
match type of hrec with
|
||||||
|
| ?Q =>
|
||||||
|
match (eval simpl in Q) with
|
||||||
|
| forall Y, T -> Y =>
|
||||||
|
simple refine (hrec P)
|
||||||
|
| forall Y _, T -> Y =>
|
||||||
|
simple refine (hrec P _)
|
||||||
|
| forall Y _ _, T -> Y =>
|
||||||
|
simple refine (hrec P _ _)
|
||||||
|
| forall Y _ _ _, T -> Y =>
|
||||||
|
simple refine (hrec P _ _ _)
|
||||||
|
| forall Y _ _ _ _, T -> Y =>
|
||||||
|
simple refine (hrec P _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _, T -> Y =>
|
||||||
|
simple refine (hrec P _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _, T -> Y =>
|
||||||
|
simple refine (hrec P _ _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _ _, T -> Y =>
|
||||||
|
simple refine (hrec P _ _ _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _ _ _, T -> Y =>
|
||||||
|
simple refine (hrec P _ _ _ _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _ _ _ _, T -> Y =>
|
||||||
|
simple refine (hrec P _ _ _ _ _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _ _ _ _ _, T -> Y =>
|
||||||
|
simple refine (hrec P _ _ _ _ _ _ _ _ _ _)
|
||||||
|
| _ => fail "Cannot handle the recursion principle (too many parameters?) :("
|
||||||
|
end
|
||||||
|
end
|
||||||
|
| [ |- forall (target:?T), ?P] =>
|
||||||
|
let hind1 := eval cbv[hinduction H_inductor] in (hinduction T) in
|
||||||
|
let hind := eval simpl in hind1 in
|
||||||
|
match type of hind with
|
||||||
|
| ?Q =>
|
||||||
|
match (eval simpl in Q) with
|
||||||
|
| forall Y , (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _)
|
||||||
|
| forall Y _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _)
|
||||||
|
| forall Y _ _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _ _)
|
||||||
|
| forall Y _ _ _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _ _ _)
|
||||||
|
| forall Y _ _ _ _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _ _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _ _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _ _ _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _ _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _ _ _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _ _ _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _ _ _ _ _ _ _ _)
|
||||||
|
| forall Y _ _ _ _ _ _ _ _ _, (forall x, Y x) =>
|
||||||
|
simple refine (hind (fun target => P) _ _ _ _ _ _ _ _ _)
|
||||||
|
| _ => fail "Cannot handle the induction principle (too many parameters?) :("
|
||||||
|
end
|
||||||
|
end
|
||||||
|
(*| _ => fail "I am sorry, but something went wrong!"*)
|
||||||
|
end.
|
||||||
|
|
||||||
|
Tactic Notation "hrecursion" := hrecursion_; simpl.
|
||||||
|
Tactic Notation "hrecursion" ident(x) := revert x; hrecursion.
|
||||||
|
Tactic Notation "hinduction" := hrecursion_; simpl.
|
||||||
|
Tactic Notation "hinduction" ident(x) := revert x; hrecursion.
|
||||||
|
|
||||||
164
Mod2.v
164
Mod2.v
|
|
@ -1,5 +1,5 @@
|
||||||
Require Import HoTT.
|
|
||||||
Require Export HoTT.
|
Require Export HoTT.
|
||||||
|
Require Import HitTactics.
|
||||||
|
|
||||||
Module Export modulo.
|
Module Export modulo.
|
||||||
|
|
||||||
|
|
@ -51,166 +51,98 @@ Axiom Mod2_rec_beta_mod : forall
|
||||||
(mod' : a = s (s a))
|
(mod' : a = s (s a))
|
||||||
, ap (Mod2_rec P a s mod') mod = mod'.
|
, ap (Mod2_rec P a s mod') mod = mod'.
|
||||||
|
|
||||||
|
Instance: HitRecursion Mod2 := {
|
||||||
|
indTy := _; recTy := _;
|
||||||
|
H_inductor := Mod2_ind;
|
||||||
|
H_recursor := Mod2_rec }.
|
||||||
|
|
||||||
End modulo.
|
End modulo.
|
||||||
|
|
||||||
Definition negate : Mod2 -> Mod2.
|
|
||||||
Proof.
|
|
||||||
refine (Mod2_ind _ _ _ _).
|
|
||||||
Unshelve.
|
|
||||||
Focus 2.
|
|
||||||
apply (succ Z).
|
|
||||||
|
|
||||||
Focus 2.
|
|
||||||
intros.
|
|
||||||
apply (succ H).
|
|
||||||
|
|
||||||
simpl.
|
|
||||||
rewrite transport_const.
|
|
||||||
rewrite <- mod.
|
|
||||||
reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Theorem modulo2 : forall n : Mod2, n = succ(succ n).
|
Theorem modulo2 : forall n : Mod2, n = succ(succ n).
|
||||||
Proof.
|
Proof.
|
||||||
refine (Mod2_ind _ _ _ _).
|
|
||||||
Unshelve.
|
|
||||||
Focus 2.
|
|
||||||
apply mod.
|
|
||||||
|
|
||||||
Focus 2.
|
|
||||||
intro n.
|
intro n.
|
||||||
intro p.
|
hinduction n.
|
||||||
|
- apply mod.
|
||||||
|
- intros n p.
|
||||||
apply (ap succ p).
|
apply (ap succ p).
|
||||||
|
- simpl.
|
||||||
|
etransitivity.
|
||||||
|
eapply (@transport_paths_FlFr _ _ idmap (fun n => succ (succ n))).
|
||||||
|
hott_simpl.
|
||||||
|
apply ap_compose.
|
||||||
|
Defined.
|
||||||
|
|
||||||
simpl.
|
Definition negate : Mod2 -> Mod2.
|
||||||
rewrite @HoTT.Types.Paths.transport_paths_FlFr.
|
Proof.
|
||||||
rewrite ap_idmap.
|
hrecursion.
|
||||||
rewrite concat_Vp.
|
- apply Z.
|
||||||
rewrite concat_1p.
|
- intros. apply (succ H).
|
||||||
rewrite ap_compose.
|
- simpl. apply mod.
|
||||||
reflexivity.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition plus : Mod2 -> Mod2 -> Mod2.
|
Definition plus : Mod2 -> Mod2 -> Mod2.
|
||||||
Proof.
|
Proof.
|
||||||
intro n.
|
intros n m.
|
||||||
refine (Mod2_ind _ _ _ _).
|
hrecursion m.
|
||||||
Unshelve.
|
- exact n.
|
||||||
|
- apply succ.
|
||||||
Focus 2.
|
- apply modulo2.
|
||||||
apply n.
|
|
||||||
|
|
||||||
Focus 2.
|
|
||||||
intro m.
|
|
||||||
intro k.
|
|
||||||
apply (succ k).
|
|
||||||
|
|
||||||
simpl.
|
|
||||||
rewrite transport_const.
|
|
||||||
apply modulo2.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition Bool_to_Mod2 : Bool -> Mod2.
|
Definition Bool_to_Mod2 : Bool -> Mod2.
|
||||||
Proof.
|
Proof.
|
||||||
intro b.
|
intro b.
|
||||||
destruct b.
|
destruct b.
|
||||||
apply (succ Z).
|
+ apply (succ Z).
|
||||||
|
+ apply Z.
|
||||||
apply Z.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Definition Mod2_to_Bool : Mod2 -> Bool.
|
Definition Mod2_to_Bool : Mod2 -> Bool.
|
||||||
Proof.
|
Proof.
|
||||||
refine (Mod2_ind _ _ _ _).
|
intro x.
|
||||||
Unshelve.
|
hrecursion x.
|
||||||
Focus 2.
|
- exact false.
|
||||||
apply false.
|
- exact negb.
|
||||||
|
- simpl. reflexivity.
|
||||||
Focus 2.
|
|
||||||
intro n.
|
|
||||||
apply negb.
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
simpl.
|
|
||||||
apply transport_const.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Theorem eq1 : forall n : Bool, Mod2_to_Bool (Bool_to_Mod2 n) = n.
|
Theorem eq1 : forall n : Bool, Mod2_to_Bool (Bool_to_Mod2 n) = n.
|
||||||
Proof.
|
Proof.
|
||||||
intro b.
|
intro b.
|
||||||
destruct b.
|
destruct b; compute; reflexivity.
|
||||||
Focus 1.
|
|
||||||
compute.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
compute.
|
|
||||||
reflexivity.
|
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Theorem Bool_to_Mod2_negb : forall x : Bool,
|
Theorem Bool_to_Mod2_negb : forall x : Bool,
|
||||||
succ (Bool_to_Mod2 x) = Bool_to_Mod2 (negb x).
|
succ (Bool_to_Mod2 x) = Bool_to_Mod2 (negb x).
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
destruct x.
|
destruct x; compute.
|
||||||
compute.
|
+ apply mod^.
|
||||||
apply mod^.
|
+ apply reflexivity.
|
||||||
|
|
||||||
compute.
|
|
||||||
apply reflexivity.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Theorem eq2 : forall n : Mod2, Bool_to_Mod2 (Mod2_to_Bool n) = n.
|
Theorem eq2 : forall n : Mod2, Bool_to_Mod2 (Mod2_to_Bool n) = n.
|
||||||
Proof.
|
Proof.
|
||||||
refine (Mod2_ind _ _ _ _).
|
|
||||||
Unshelve.
|
|
||||||
Focus 2.
|
|
||||||
compute.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
Focus 2.
|
|
||||||
intro n.
|
intro n.
|
||||||
intro IHn.
|
hinduction n.
|
||||||
symmetry.
|
- reflexivity.
|
||||||
transitivity (succ (Bool_to_Mod2 (Mod2_to_Bool n))).
|
- intros n IHn.
|
||||||
|
symmetry. etransitivity. apply (ap succ IHn^).
|
||||||
Focus 1.
|
etransitivity. apply Bool_to_Mod2_negb.
|
||||||
symmetry.
|
hott_simpl.
|
||||||
apply (ap succ IHn).
|
- rewrite @HoTT.Types.Paths.transport_paths_FlFr.
|
||||||
|
hott_simpl.
|
||||||
transitivity (Bool_to_Mod2 (negb (Mod2_to_Bool n))).
|
|
||||||
apply Bool_to_Mod2_negb.
|
|
||||||
enough (negb (Mod2_to_Bool n) = Mod2_to_Bool (succ n)).
|
|
||||||
apply (ap Bool_to_Mod2 X).
|
|
||||||
|
|
||||||
compute.
|
|
||||||
reflexivity.
|
|
||||||
simpl.
|
|
||||||
rewrite concat_p1.
|
|
||||||
rewrite concat_1p.
|
|
||||||
rewrite @HoTT.Types.Paths.transport_paths_FlFr.
|
|
||||||
rewrite concat_p1.
|
|
||||||
rewrite ap_idmap.
|
|
||||||
rewrite ap_compose.
|
rewrite ap_compose.
|
||||||
|
enough (ap Mod2_to_Bool mod = idpath).
|
||||||
enough (ap Mod2_to_Bool mod = reflexivity false).
|
+ rewrite X. hott_simpl.
|
||||||
rewrite X.
|
+ apply (Mod2_rec_beta_mod Bool false negb 1).
|
||||||
simpl.
|
|
||||||
rewrite concat_1p.
|
|
||||||
rewrite inv_V.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
enough (IsHSet Bool).
|
|
||||||
apply axiomK_hset.
|
|
||||||
apply X.
|
|
||||||
apply hset_bool.
|
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
Theorem adj :
|
Theorem adj :
|
||||||
forall x : Mod2, eq1 (Mod2_to_Bool x) = ap Mod2_to_Bool (eq2 x).
|
forall x : Mod2, eq1 (Mod2_to_Bool x) = ap Mod2_to_Bool (eq2 x).
|
||||||
Proof.
|
Proof.
|
||||||
intro x.
|
intro x.
|
||||||
enough (IsHSet Bool).
|
|
||||||
apply set_path2.
|
|
||||||
apply hset_bool.
|
apply hset_bool.
|
||||||
Defined.
|
Defined.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,6 @@
|
||||||
-R . "" COQC = hoqc COQDEP = hoqdep
|
-R . "" COQC = hoqc COQDEP = hoqdep
|
||||||
|
|
||||||
|
HitTactics.v
|
||||||
Mod2.v
|
Mod2.v
|
||||||
FinSets.v
|
FinSets.v
|
||||||
Expressions.v
|
Expressions.v
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue