mirror of https://github.com/nmvdw/HITs-Examples
Integers form a ring
This commit is contained in:
Niels
parent
6f016d1b7f
commit
376efbf2e9
401
Integers.v
401
Integers.v
|
|
@ -3,132 +3,334 @@ Require Export HoTT.
|
|||
|
||||
Module Export Ints.
|
||||
|
||||
Private Inductive Z : Type0 :=
|
||||
| nul : Z
|
||||
Private Inductive Z : Type :=
|
||||
| zero_Z : Z
|
||||
| succ : Z -> Z
|
||||
| pred : Z -> Z.
|
||||
|
||||
Axiom inv1 : forall n : Z, n = pred(succ n).
|
||||
Axiom inv2 : forall n : Z, n = succ(pred n).
|
||||
Axiom ZisSet : IsHSet Z.
|
||||
|
||||
Fixpoint Z_rec
|
||||
(P : Type)
|
||||
(a : P)
|
||||
(s : P -> P)
|
||||
(p : P -> P)
|
||||
(i1 : forall (m : P), m = p(s m))
|
||||
(i2 : forall (m : P), m = s(p m))
|
||||
(x : Z)
|
||||
{struct x}
|
||||
: P
|
||||
:=
|
||||
(match x return _ -> _ -> P with
|
||||
| nul => fun _ => fun _ => a
|
||||
| succ n => fun _ => fun _ => s ((Z_rec P a s p i1 i2) n)
|
||||
| pred n => fun _ => fun _ => p ((Z_rec P a s p i1 i2) n)
|
||||
end) i1 i2.
|
||||
|
||||
Axiom Z_rec_beta_inv1 : forall
|
||||
(P : Type)
|
||||
(a : P)
|
||||
(s : P -> P)
|
||||
(p : P -> P)
|
||||
(i1 : forall (m : P), m = p(s m))
|
||||
(i2 : forall (m : P), m = s(p m))
|
||||
(n : Z)
|
||||
, ap (Z_rec P a s p i1 i2) (inv1 n) = i1 (Z_rec P a s p i1 i2 n).
|
||||
|
||||
Axiom Z_rec_beta_inv2 : forall
|
||||
(P : Type)
|
||||
(a : P)
|
||||
(s : P -> P)
|
||||
(p : P -> P)
|
||||
(i1 : forall (m : P), m = p(s m))
|
||||
(i2 : forall (m : P), m = s(p m))
|
||||
(n : Z)
|
||||
, ap (Z_rec P a s p i1 i2) (inv2 n) = i2 (Z_rec P a s p i1 i2 n).
|
||||
|
||||
Fixpoint Z_ind
|
||||
(P : Z -> Type)
|
||||
(a : P nul)
|
||||
Section Z_induction.
|
||||
Variable (P : Z -> Type)
|
||||
(H : forall n, IsHSet (P n))
|
||||
(a : P zero_Z)
|
||||
(s : forall (n : Z), P n -> P (succ n))
|
||||
(p : forall (n : Z), P n -> P (pred n))
|
||||
(i1 : forall (n : Z) (m : P n), (inv1 n) # m = p (succ n) (s (n) m))
|
||||
(i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m))
|
||||
(i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m)).
|
||||
|
||||
Fixpoint Z_ind
|
||||
(x : Z)
|
||||
{struct x}
|
||||
: P x
|
||||
:=
|
||||
(match x return _ -> _ -> P x with
|
||||
| nul => fun _ => fun _ => a
|
||||
| succ n => fun _ => fun _ => s n ((Z_ind P a s p i1 i2) n)
|
||||
| pred n => fun _ => fun _ => p n ((Z_ind P a s p i1 i2) n)
|
||||
| zero_Z => fun _ => fun _ => a
|
||||
| succ n => fun _ => fun _ => s n (Z_ind n)
|
||||
| pred n => fun _ => fun _ => p n (Z_ind n)
|
||||
end) i1 i2.
|
||||
|
||||
Axiom Z_ind_beta_inv1 : forall
|
||||
(P : Z -> Type)
|
||||
(a : P nul)
|
||||
(s : forall (n : Z), P n -> P (succ n))
|
||||
(p : forall (n : Z), P n -> P (pred n))
|
||||
(i1 : forall (n : Z) (m : P n), (inv1 n) # m = p (succ n) (s (n) m))
|
||||
(i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m))
|
||||
(n : Z)
|
||||
, apD (Z_ind P a s p i1 i2) (inv1 n) = i1 n (Z_ind P a s p i1 i2 n).
|
||||
Axiom Z_ind_beta_inv1 : forall (n : Z), apD Z_ind (inv1 n) = i1 n (Z_ind n).
|
||||
|
||||
Axiom Z_ind_beta_inv2 : forall
|
||||
(P : Z -> Type)
|
||||
(a : P nul)
|
||||
(s : forall (n : Z), P n -> P (succ n))
|
||||
(p : forall (n : Z), P n -> P (pred n))
|
||||
(i1 : forall (n : Z) (m : P n), (inv1 n) # m = p (succ n) (s (n) m))
|
||||
(i2 : forall (n : Z) (m : P n), (inv2 n) # m = s (pred n) (p (n) m))
|
||||
(n : Z)
|
||||
, apD (Z_ind P a s p i1 i2) (inv2 n) = i2 n (Z_ind P a s p i1 i2 n).
|
||||
Axiom Z_ind_beta_inv2 : forall (n : Z), apD Z_ind (inv2 n) = i2 n (Z_ind n).
|
||||
End Z_induction.
|
||||
|
||||
Section Z_recursion.
|
||||
Variable (P : Type)
|
||||
(H : IsHSet P)
|
||||
(a : P)
|
||||
(s : P -> P)
|
||||
(p : P -> P)
|
||||
(i1 : forall (m : P), m = p(s m))
|
||||
(i2 : forall (m : P), m = s(p m)).
|
||||
|
||||
Definition Z_rec : Z -> P.
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; simpl.
|
||||
- apply a.
|
||||
- intro ; apply s.
|
||||
- intro ; apply p.
|
||||
- intros.
|
||||
refine (transport_const _ _ @ (i1 _)).
|
||||
- intros.
|
||||
refine (transport_const _ _ @ (i2 _)).
|
||||
Defined.
|
||||
|
||||
Definition Z_rec_beta_inv1 (n : Z) : ap Z_rec (inv1 n) = i1 (Z_rec n).
|
||||
Proof.
|
||||
unfold Z_rec.
|
||||
eapply (cancelL (transport_const (inv1 n) _)).
|
||||
simple refine ((apD_const _ _)^ @ _).
|
||||
apply Z_ind_beta_inv1.
|
||||
Defined.
|
||||
|
||||
Definition Z_rec_beta_inv2 (n : Z) : ap Z_rec (inv2 n) = i2 (Z_rec n).
|
||||
Proof.
|
||||
unfold Z_rec.
|
||||
eapply (cancelL (transport_const (inv2 n) _)).
|
||||
simple refine ((apD_const _ _)^ @ _).
|
||||
apply Z_ind_beta_inv2.
|
||||
Defined.
|
||||
|
||||
End Z_recursion.
|
||||
|
||||
End Ints.
|
||||
|
||||
Definition negate : Z -> Z.
|
||||
Section ring_Z.
|
||||
Fixpoint nat_to_Z (n : nat) : Z :=
|
||||
match n with
|
||||
| 0 => zero_Z
|
||||
| S m => succ (nat_to_Z m)
|
||||
end.
|
||||
|
||||
Definition plus : Z -> Z -> Z := fun x => Z_rec Z x succ pred inv1 inv2.
|
||||
|
||||
Lemma plus_0n : forall x, plus zero_Z x = x.
|
||||
Proof.
|
||||
intro x.
|
||||
refine (Z_rec _ _ _ _ _ _ x).
|
||||
Unshelve.
|
||||
Focus 1.
|
||||
apply nul.
|
||||
|
||||
Focus 3.
|
||||
apply pred.
|
||||
|
||||
Focus 3.
|
||||
apply succ.
|
||||
|
||||
Focus 2.
|
||||
apply inv1.
|
||||
|
||||
apply inv2.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros y Hy.
|
||||
apply (ap succ Hy).
|
||||
- intros y Hy.
|
||||
apply (ap pred Hy).
|
||||
Defined.
|
||||
|
||||
Definition plus : Z -> Z -> Z.
|
||||
Definition plus_n0 x : plus x zero_Z = x := idpath x.
|
||||
|
||||
Lemma plus_Sn x : forall y, plus (succ x) y = succ(plus x y).
|
||||
Proof.
|
||||
intro x.
|
||||
refine (Z_rec _ _ _ _ _ _).
|
||||
Unshelve.
|
||||
Focus 1.
|
||||
apply x.
|
||||
|
||||
Focus 3.
|
||||
apply succ.
|
||||
|
||||
Focus 3.
|
||||
apply pred.
|
||||
|
||||
Focus 1.
|
||||
apply inv1.
|
||||
|
||||
apply inv2.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros y Hy.
|
||||
apply (ap succ Hy).
|
||||
- intros y Hy.
|
||||
apply (ap pred Hy @ (inv1 (plus x y))^ @ inv2 (plus x y)).
|
||||
Defined.
|
||||
|
||||
Definition minus (x : Z) (y : Z) := plus x (negate y).
|
||||
Definition plus_nS x y : plus x (succ y) = succ(plus x y) := idpath.
|
||||
|
||||
Lemma plus_Pn x : forall y, plus (pred x) y = pred (plus x y).
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros y Hy.
|
||||
apply (ap succ Hy @ (inv2 (plus x y))^ @ inv1 (plus x y)).
|
||||
- intros y Hy.
|
||||
apply (ap pred Hy).
|
||||
Defined.
|
||||
|
||||
Definition plus_nP x y : plus x (pred y) = pred(plus x y) := idpath.
|
||||
|
||||
Lemma plus_comm x : forall y : Z, plus x y = plus y x.
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _)
|
||||
; simpl ; try (intros ; apply set_path2).
|
||||
- apply (plus_0n x)^.
|
||||
- intros n H1.
|
||||
apply (ap succ H1 @ (plus_Sn _ _)^).
|
||||
- intros n H1.
|
||||
apply (ap pred H1 @ (plus_Pn _ _)^).
|
||||
Defined.
|
||||
|
||||
Lemma plus_assoc x y : forall z : Z, plus (plus x y) z = plus x (plus y z).
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _)
|
||||
; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros Sz HSz.
|
||||
refine (ap succ HSz).
|
||||
- intros Pz HPz.
|
||||
apply (ap pred HPz).
|
||||
Defined.
|
||||
|
||||
Definition negate : Z -> Z := Z_rec Z zero_Z pred succ inv2 inv1.
|
||||
|
||||
Lemma negate_negate : forall x, negate(negate x) = x.
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros Sy HSy.
|
||||
apply (ap succ HSy).
|
||||
- intros Py HPy.
|
||||
apply (ap pred HPy).
|
||||
Defined.
|
||||
|
||||
Definition minus x y : Z := plus x (negate y).
|
||||
|
||||
Lemma plus_negatex : forall x, plus x (negate x) = zero_Z.
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros Sx HSx.
|
||||
refine (ap pred (plus_Sn _ _) @ _).
|
||||
refine ((inv1 _)^ @ HSx).
|
||||
- intros Px HPx.
|
||||
refine (ap succ (plus_Pn _ _) @ _).
|
||||
refine ((inv2 _)^ @ HPx).
|
||||
Defined.
|
||||
|
||||
Definition plus_xnegate x : plus (negate x) x = zero_Z :=
|
||||
plus_comm (negate x) x @ plus_negatex x.
|
||||
|
||||
Lemma plus_negate x : forall y, plus (negate x) (negate y) = negate (plus x y).
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros Sy HSy.
|
||||
apply (ap pred HSy).
|
||||
- intros Py HPy.
|
||||
apply (ap succ HPy).
|
||||
Defined.
|
||||
|
||||
Definition times (x : Z) : Z -> Z.
|
||||
Proof.
|
||||
simple refine (Z_rec _ _ _ _ _ _).
|
||||
- apply zero_Z.
|
||||
- apply (plus x).
|
||||
- apply (fun z => minus z x).
|
||||
- intros ; unfold minus.
|
||||
symmetry.
|
||||
refine (ap (fun z => plus z (negate x)) (plus_comm x m) @ _).
|
||||
refine (plus_assoc _ _ _ @ _).
|
||||
refine (ap (fun z => plus m z) (plus_negatex _) @ _).
|
||||
apply plus_n0.
|
||||
- intros ; unfold minus.
|
||||
symmetry.
|
||||
refine (ap (fun z => plus x z) (plus_comm _ _) @ _).
|
||||
refine ((plus_assoc _ _ _)^ @ _).
|
||||
refine (ap (fun z => plus z m) (plus_negatex _) @ _).
|
||||
apply plus_0n.
|
||||
Defined.
|
||||
|
||||
Lemma times_0n : forall x, times zero_Z x = zero_Z.
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; try (intros ; apply set_path2) ; simpl.
|
||||
- reflexivity.
|
||||
- intros Sx HSx.
|
||||
apply (plus_0n _ @ HSx).
|
||||
- intros Px HPx.
|
||||
unfold minus ; simpl ; apply HPx.
|
||||
Defined.
|
||||
|
||||
Definition times_n0 n : times n zero_Z = zero_Z := idpath.
|
||||
|
||||
Lemma times_Sn x : forall y, times (succ x) y = plus y (times x y).
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; try (intros ; apply set_path2) ; simpl.
|
||||
- reflexivity.
|
||||
- intros Sy HSy.
|
||||
refine (ap (fun z => plus (succ x) z) HSy @ _).
|
||||
refine (plus_Sn _ _ @ _).
|
||||
refine (_ @ (plus_Sn _ _)^).
|
||||
refine (ap succ _).
|
||||
refine ((plus_assoc _ _ _)^ @ _).
|
||||
refine (_ @ plus_assoc _ _ _).
|
||||
refine (ap (fun z => plus z (times x Sy)) (plus_comm _ _)).
|
||||
- intros Py HPy ; unfold minus.
|
||||
refine (ap (fun z => plus z (negate (succ x))) HPy @ _) ; simpl.
|
||||
refine (_ @ (plus_Pn _ _)^).
|
||||
refine (ap pred _).
|
||||
apply plus_assoc.
|
||||
Defined.
|
||||
|
||||
Definition times_nS x y : times x (succ y) = plus x (times x y) := idpath.
|
||||
|
||||
Lemma times_Pn x : forall y, times (pred x) y = minus (times x y) y.
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _) ; try (intros ; apply set_path2) ; simpl.
|
||||
- reflexivity.
|
||||
- intros Sy HSy.
|
||||
refine (ap (fun z => plus (pred x) z) HSy @ _) ; unfold minus.
|
||||
refine (plus_Pn _ _ @ _) ; simpl.
|
||||
refine (ap pred _).
|
||||
apply (plus_assoc _ _ _)^.
|
||||
- intros Py HPy.
|
||||
refine (ap (fun z => minus z (pred x)) HPy @ _) ; unfold minus ; simpl.
|
||||
refine (ap succ _).
|
||||
refine (plus_assoc _ _ _ @ _).
|
||||
refine (_ @ (plus_assoc _ _ _)^).
|
||||
refine (ap (fun z => plus (times x Py) z) (plus_comm _ _)).
|
||||
Defined.
|
||||
|
||||
Definition times_nP x y : times x (pred y) = minus (times x y) x := idpath.
|
||||
|
||||
Lemma times_comm x : forall y, times x y = times y x.
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _)
|
||||
; simpl ; try (intros ; apply set_path2).
|
||||
- apply (times_0n x)^.
|
||||
- intros Sx HSx.
|
||||
apply (ap (fun z => plus x z) HSx @ (times_Sn _ _)^).
|
||||
- intros Py HPy.
|
||||
apply (ap (fun z => minus z x) HPy @ (times_Pn _ _)^).
|
||||
Defined.
|
||||
|
||||
Lemma times_negatex x : forall y, times x (negate y) = negate (times x y).
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _)
|
||||
; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros Sy HSy.
|
||||
unfold minus.
|
||||
refine (ap (fun z => plus z (negate x)) HSy @ _).
|
||||
refine (plus_negate _ _ @ _).
|
||||
apply (ap negate (plus_comm _ _)).
|
||||
- intros Py HPy.
|
||||
refine (ap (plus x) HPy @ _).
|
||||
unfold minus.
|
||||
refine (ap (fun z => plus z (negate (times x Py))) (negate_negate _)^ @ _).
|
||||
refine (plus_negate _ _ @ _).
|
||||
refine (ap negate (plus_comm _ _)).
|
||||
Defined.
|
||||
|
||||
Definition times_xnegate x y : times (negate x) y = negate (times x y) :=
|
||||
times_comm (negate x) y @ times_negatex y x @ ap negate (times_comm y x).
|
||||
|
||||
Lemma dist_times_plus x y : forall z, times x (plus y z) = plus (times x y) (times x z).
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _)
|
||||
; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros Sz HSz.
|
||||
refine (ap (plus x) HSz @ _).
|
||||
refine ((plus_assoc _ _ _)^ @ _).
|
||||
refine (_ @ plus_assoc _ _ _).
|
||||
refine (ap (fun z => plus z (times x Sz)) (plus_comm _ _)).
|
||||
- intros Pz HPz.
|
||||
refine (ap (fun z => minus z x) HPz @ _).
|
||||
unfold minus ; simpl.
|
||||
apply plus_assoc.
|
||||
Defined.
|
||||
|
||||
Lemma dist_plus_times x y z : times (plus x y) z = plus (times x z) (times y z).
|
||||
Proof.
|
||||
refine (times_comm _ _ @ _).
|
||||
refine (dist_times_plus _ _ _ @ _).
|
||||
refine (ap (plus (times z x)) (times_comm _ _) @ _).
|
||||
apply (ap (fun a => plus a (times y z)) (times_comm _ _)).
|
||||
Defined.
|
||||
|
||||
Lemma times_assoc x y : forall z, times (times x y) z = times x (times y z).
|
||||
Proof.
|
||||
simple refine (Z_ind _ _ _ _ _ _)
|
||||
; simpl ; try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intros Sz HSz.
|
||||
refine (ap (plus (times x y)) HSz @ _).
|
||||
symmetry ; apply dist_times_plus.
|
||||
- intros Pz HPz.
|
||||
refine (ap (fun z => minus z (times x y)) HPz @ _).
|
||||
unfold minus.
|
||||
refine (_ @ (dist_times_plus _ _ _)^).
|
||||
refine (ap (plus (times x (times y Pz))) _).
|
||||
apply (times_negatex _ _)^.
|
||||
Defined.
|
||||
|
||||
End ring_Z.
|
||||
|
||||
(*
|
||||
Definition Z_to_S : Z -> S1.
|
||||
Proof.
|
||||
refine (Z_rec _ _ _ _ _ _).
|
||||
|
|
@ -630,3 +832,4 @@ Definition isomorphism2 : IsEquiv Z'_to_Z.
|
|||
Proof.
|
||||
apply (BuildIsEquiv Z' Z Z'_to_Z Z_to_Z' isoZEq2 isoZEq1 adj2).
|
||||
Qed.
|
||||
*)
|
||||
Loading…
Reference in New Issue