mirror of https://github.com/nmvdw/HITs-Examples
Add files via upload
This commit is contained in:
parent
3999bbdd18
commit
5608c93b39
23
Integers.v
23
Integers.v
|
@ -1,25 +1,6 @@
|
||||||
Require Import HoTT.
|
Require Import HoTT.
|
||||||
Require Export HoTT.
|
Require Export HoTT.
|
||||||
|
|
||||||
Theorem useful :
|
|
||||||
forall (A B : Type)
|
|
||||||
(f g : A -> B)
|
|
||||||
(a a' : A)
|
|
||||||
(p : a = a')
|
|
||||||
(q : f a = g a),
|
|
||||||
transport (fun x => f x = g x) p q = (ap f p)^ @ q @ (ap g p).
|
|
||||||
Proof.
|
|
||||||
intros.
|
|
||||||
induction p.
|
|
||||||
rewrite transport_1.
|
|
||||||
rewrite ap_1.
|
|
||||||
rewrite ap_1.
|
|
||||||
rewrite concat_p1.
|
|
||||||
simpl.
|
|
||||||
rewrite concat_1p.
|
|
||||||
reflexivity.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Module Export Ints.
|
Module Export Ints.
|
||||||
|
|
||||||
Private Inductive Z : Type0 :=
|
Private Inductive Z : Type0 :=
|
||||||
|
@ -175,7 +156,7 @@ refine (Z_rec _ _ _ _ _ _).
|
||||||
Focus 2.
|
Focus 2.
|
||||||
apply loop.
|
apply loop.
|
||||||
|
|
||||||
rewrite useful.
|
rewrite @HoTT.Types.Paths.transport_paths_FlFr.
|
||||||
rewrite ap_idmap.
|
rewrite ap_idmap.
|
||||||
rewrite concat_Vp.
|
rewrite concat_Vp.
|
||||||
rewrite concat_1p.
|
rewrite concat_1p.
|
||||||
|
@ -417,7 +398,7 @@ refine (Z'_ind _ _ _ _).
|
||||||
reflexivity.
|
reflexivity.
|
||||||
|
|
||||||
simpl.
|
simpl.
|
||||||
rewrite useful.
|
rewrite @HoTT.Types.Paths.transport_paths_FlFr.
|
||||||
rewrite concat_p1.
|
rewrite concat_p1.
|
||||||
rewrite ap_idmap.
|
rewrite ap_idmap.
|
||||||
|
|
||||||
|
|
182
Mod2.v
182
Mod2.v
|
@ -1,25 +1,6 @@
|
||||||
Require Import HoTT.
|
Require Import HoTT.
|
||||||
Require Export HoTT.
|
Require Export HoTT.
|
||||||
|
|
||||||
Theorem useful :
|
|
||||||
forall (A B : Type)
|
|
||||||
(f g : A -> B)
|
|
||||||
(a a' : A)
|
|
||||||
(p : a = a')
|
|
||||||
(q : f a = g a),
|
|
||||||
transport (fun x => f x = g x) p q = (ap f p)^ @ q @ (ap g p).
|
|
||||||
Proof.
|
|
||||||
intros.
|
|
||||||
induction p.
|
|
||||||
rewrite transport_1.
|
|
||||||
rewrite ap_1.
|
|
||||||
rewrite ap_1.
|
|
||||||
rewrite concat_p1.
|
|
||||||
simpl.
|
|
||||||
rewrite concat_1p.
|
|
||||||
reflexivity.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Module Export modulo.
|
Module Export modulo.
|
||||||
|
|
||||||
Private Inductive Mod2 : Type0 :=
|
Private Inductive Mod2 : Type0 :=
|
||||||
|
@ -72,65 +53,6 @@ Axiom Mod2_rec_beta_mod : forall
|
||||||
|
|
||||||
End modulo.
|
End modulo.
|
||||||
|
|
||||||
Module Export moduloAlt.
|
|
||||||
|
|
||||||
Private Inductive Mod2A : Type0 :=
|
|
||||||
| ZA : Mod2A
|
|
||||||
| succA : Mod2A -> Mod2A.
|
|
||||||
|
|
||||||
Axiom modA : forall n : Mod2A, n = succA(succA n).
|
|
||||||
|
|
||||||
Fixpoint Mod2A_ind
|
|
||||||
(P : Mod2A -> Type)
|
|
||||||
(z : P ZA)
|
|
||||||
(s : forall n : Mod2A, P n -> P (succA n))
|
|
||||||
(mod' : forall (n : Mod2A) (a : P n),
|
|
||||||
modA n # a = s (succA n) (s n a))
|
|
||||||
(x : Mod2A)
|
|
||||||
{struct x}
|
|
||||||
: P x
|
|
||||||
:=
|
|
||||||
(match x return _ -> P x with
|
|
||||||
| ZA => fun _ => z
|
|
||||||
| succA n => fun _ => s n ((Mod2A_ind P z s mod') n)
|
|
||||||
end) mod'.
|
|
||||||
|
|
||||||
|
|
||||||
Axiom Mod2A_ind_beta_mod : forall
|
|
||||||
(P : Mod2A -> Type)
|
|
||||||
(z : P ZA)
|
|
||||||
(s : forall n : Mod2A, P n -> P (succA n))
|
|
||||||
(mod' : forall (n : Mod2A) (a : P n),
|
|
||||||
modA n # a = s (succA n) (s n a))
|
|
||||||
(n : Mod2A)
|
|
||||||
, apD (Mod2A_ind P z s mod') (modA n) = mod' n (Mod2A_ind P z s mod' n).
|
|
||||||
|
|
||||||
Fixpoint Mod2A_rec
|
|
||||||
(P : Type)
|
|
||||||
(z : P)
|
|
||||||
(s : P -> P)
|
|
||||||
(mod' : forall (a : P),
|
|
||||||
a = s (s a))
|
|
||||||
(x : Mod2A)
|
|
||||||
{struct x}
|
|
||||||
: P
|
|
||||||
:=
|
|
||||||
(match x return _ -> P with
|
|
||||||
| ZA => fun _ => z
|
|
||||||
| succA n => fun _ => s ((Mod2A_rec P z s mod') n)
|
|
||||||
end) mod'.
|
|
||||||
|
|
||||||
Axiom Mod2A_rec_beta_mod : forall
|
|
||||||
(P : Type)
|
|
||||||
(z : P)
|
|
||||||
(s : P -> P)
|
|
||||||
(mod' : forall (a : P),
|
|
||||||
a = s (s a))
|
|
||||||
(n : Mod2A)
|
|
||||||
, ap (Mod2A_rec P z s mod') (modA n) = mod' (Mod2A_rec P z s mod' n).
|
|
||||||
|
|
||||||
End moduloAlt.
|
|
||||||
|
|
||||||
Definition negate : Mod2 -> Mod2.
|
Definition negate : Mod2 -> Mod2.
|
||||||
Proof.
|
Proof.
|
||||||
refine (Mod2_ind _ _ _ _).
|
refine (Mod2_ind _ _ _ _).
|
||||||
|
@ -161,7 +83,7 @@ refine (Mod2_ind _ _ _ _).
|
||||||
apply (ap succ p).
|
apply (ap succ p).
|
||||||
|
|
||||||
simpl.
|
simpl.
|
||||||
rewrite useful.
|
rewrite @HoTT.Types.Paths.transport_paths_FlFr.
|
||||||
rewrite ap_idmap.
|
rewrite ap_idmap.
|
||||||
rewrite concat_Vp.
|
rewrite concat_Vp.
|
||||||
rewrite concat_1p.
|
rewrite concat_1p.
|
||||||
|
@ -265,7 +187,7 @@ refine (Mod2_ind _ _ _ _).
|
||||||
simpl.
|
simpl.
|
||||||
rewrite concat_p1.
|
rewrite concat_p1.
|
||||||
rewrite concat_1p.
|
rewrite concat_1p.
|
||||||
rewrite useful.
|
rewrite @HoTT.Types.Paths.transport_paths_FlFr.
|
||||||
rewrite concat_p1.
|
rewrite concat_p1.
|
||||||
rewrite ap_idmap.
|
rewrite ap_idmap.
|
||||||
rewrite ap_compose.
|
rewrite ap_compose.
|
||||||
|
@ -295,102 +217,4 @@ Defined.
|
||||||
Definition isomorphism : IsEquiv Mod2_to_Bool.
|
Definition isomorphism : IsEquiv Mod2_to_Bool.
|
||||||
Proof.
|
Proof.
|
||||||
apply (BuildIsEquiv Mod2 Bool Mod2_to_Bool Bool_to_Mod2 eq1 eq2 adj).
|
apply (BuildIsEquiv Mod2 Bool Mod2_to_Bool Bool_to_Mod2 eq1 eq2 adj).
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Definition Mod2ToMod2A : Mod2 -> Mod2A.
|
|
||||||
Proof.
|
|
||||||
refine (Mod2_rec _ _ _ _).
|
|
||||||
Unshelve.
|
|
||||||
Focus 2.
|
|
||||||
apply ZA.
|
|
||||||
|
|
||||||
Focus 2.
|
|
||||||
apply succA.
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
simpl.
|
|
||||||
apply modA.
|
|
||||||
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Definition Mod2AToMod2 : Mod2A -> Mod2.
|
|
||||||
Proof.
|
|
||||||
refine (Mod2A_rec _ _ _ _).
|
|
||||||
Unshelve.
|
|
||||||
Focus 1.
|
|
||||||
apply Z.
|
|
||||||
|
|
||||||
Focus 2.
|
|
||||||
apply succ.
|
|
||||||
|
|
||||||
Focus 1.
|
|
||||||
intro a.
|
|
||||||
apply (modulo2 a).
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma Mod2AToMod2succA :
|
|
||||||
forall (n : Mod2A), Mod2AToMod2(succA n) = succ (Mod2AToMod2 n).
|
|
||||||
Proof.
|
|
||||||
reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Lemma Mod2ToMod2Asucc :
|
|
||||||
forall (n : Mod2), Mod2ToMod2A(succ n) = succA (Mod2ToMod2A n).
|
|
||||||
Proof.
|
|
||||||
reflexivity.
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
|
|
||||||
Theorem eqI1 : forall (n : Mod2), n = Mod2AToMod2(Mod2ToMod2A n).
|
|
||||||
Proof.
|
|
||||||
refine (Mod2_ind _ _ _ _).
|
|
||||||
Unshelve.
|
|
||||||
Focus 2.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
Focus 2.
|
|
||||||
intro n.
|
|
||||||
intro H.
|
|
||||||
rewrite Mod2ToMod2Asucc.
|
|
||||||
rewrite Mod2AToMod2succA.
|
|
||||||
rewrite <- H.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
simpl.
|
|
||||||
rewrite useful.
|
|
||||||
rewrite ap_idmap.
|
|
||||||
rewrite concat_p1.
|
|
||||||
rewrite ap_compose.
|
|
||||||
rewrite Mod2_rec_beta_mod.
|
|
||||||
rewrite Mod2A_rec_beta_mod.
|
|
||||||
simpl.
|
|
||||||
simpl.
|
|
||||||
enough (modulo2 Z = mod).
|
|
||||||
rewrite X.
|
|
||||||
apply concat_Vp.
|
|
||||||
|
|
||||||
compute.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
Defined.
|
|
||||||
|
|
||||||
Theorem eqI2 : forall (n : Mod2A), n = Mod2ToMod2A(Mod2AToMod2 n).
|
|
||||||
Proof.
|
|
||||||
refine (Mod2A_ind _ _ _ _).
|
|
||||||
Focus 1.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
Unshelve.
|
|
||||||
Focus 2.
|
|
||||||
intros.
|
|
||||||
rewrite Mod2AToMod2succA.
|
|
||||||
rewrite Mod2ToMod2Asucc.
|
|
||||||
rewrite <- X.
|
|
||||||
reflexivity.
|
|
||||||
|
|
||||||
intros.
|
|
||||||
simpl.
|
|
||||||
rewrite useful.
|
|
||||||
rewrite ap_idmap.
|
|
||||||
rewrite ap_compose.
|
|
||||||
rewrite Mod2A_rec_beta_mod.
|
|
Loading…
Reference in New Issue