From a61265585b2d30df288f8a94bb5125950348cb42 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 2 Aug 2017 21:58:26 +0200 Subject: [PATCH] Start proving that Mod2 is a semiring --- int/Mod2.v | 192 ++++++++++++++++++++++++++++++++++++++++++++++++ int/Mod2_ring.v | 13 ++++ int/_CoqProject | 5 ++ 3 files changed, 210 insertions(+) create mode 100644 int/Mod2.v create mode 100644 int/Mod2_ring.v create mode 100644 int/_CoqProject diff --git a/int/Mod2.v b/int/Mod2.v new file mode 100644 index 0000000..401637f --- /dev/null +++ b/int/Mod2.v @@ -0,0 +1,192 @@ +Require Export HoTT. +Require Import HitTactics. + +Module Export modulo. + +Private Inductive Mod2 : Type0 := + | Z : Mod2 + | succ : Mod2 -> Mod2. + +Axiom mod : Z = succ(succ Z). + +Fixpoint Mod2_ind + (P : Mod2 -> Type) + (a : P Z) + (s : forall (n : Mod2), P n -> P (succ n)) + (mod' : mod # a = s (succ Z) (s Z a)) + (x : Mod2) + {struct x} + : P x + := + (match x return _ -> P x with + | Z => fun _ => a + | succ n => fun _ => s n ((Mod2_ind P a s mod') n) + end) mod'. + +Axiom Mod2_ind_beta_mod : forall + (P : Mod2 -> Type) + (a : P Z) + (s : forall (n : Mod2), P n -> P (succ n)) + (mod' : mod # a = s (succ Z) (s Z a)) + , apD (Mod2_ind P a s mod') mod = mod'. + +Fixpoint Mod2_rec + (P : Type) + (a : P) + (s : P -> P) + (mod' : a = s (s a)) + (x : Mod2) + {struct x} + : P + := + (match x return _ -> P with + | Z => fun _ => a + | succ n => fun _ => s ((Mod2_rec P a s mod') n) + end) mod'. + +Axiom Mod2_rec_beta_mod : forall + (P : Type) + (a : P) + (s : P -> P) + (mod' : a = s (s a)) + , ap (Mod2_rec P a s mod') mod = mod'. + +Instance: HitRecursion Mod2 := { + indTy := _; recTy := _; + H_inductor := Mod2_ind; + H_recursor := Mod2_rec }. + +End modulo. + +Definition negate : Mod2 -> Mod2. +Proof. +hrecursion. +- apply Z. +- intros. apply (succ H). +- simpl. apply mod. +Defined. + + +Definition Bool_to_Mod2 : Bool -> Mod2. +Proof. +intro b. +destruct b. ++ apply (succ Z). ++ apply Z. +Defined. + +Definition Mod2_to_Bool : Mod2 -> Bool. +Proof. +intro x. +hrecursion x. +- exact false. +- exact negb. +- simpl. reflexivity. +Defined. + +Theorem eq1 : forall n : Bool, Mod2_to_Bool (Bool_to_Mod2 n) = n. +Proof. +intro b. +destruct b; compute; reflexivity. +Qed. + +Theorem Bool_to_Mod2_negb : forall x : Bool, + succ (Bool_to_Mod2 x) = Bool_to_Mod2 (negb x). +Proof. +intros. +destruct x; compute. ++ apply mod^. ++ apply reflexivity. +Defined. + +Theorem eq2 : forall n : Mod2, Bool_to_Mod2 (Mod2_to_Bool n) = n. +Proof. +intro n. +hinduction n. +- reflexivity. +- intros n IHn. + symmetry. etransitivity. apply (ap succ IHn^). + etransitivity. apply Bool_to_Mod2_negb. + hott_simpl. +- rewrite @HoTT.Types.Paths.transport_paths_FlFr. + hott_simpl. + rewrite ap_compose. + enough (ap Mod2_to_Bool mod = idpath). + + rewrite X. hott_simpl. + + apply (Mod2_rec_beta_mod Bool false negb 1). +Defined. + +Theorem adj : + forall x : Mod2, eq1 (Mod2_to_Bool x) = ap Mod2_to_Bool (eq2 x). +Proof. +intro x. +apply hset_bool. +Defined. + +Instance: IsEquiv Mod2_to_Bool. +Proof. +apply (BuildIsEquiv Mod2 Bool Mod2_to_Bool Bool_to_Mod2 eq1 eq2 adj). +Qed. + +Definition Mod2_value : Mod2 <~> Bool := BuildEquiv _ _ Mod2_to_Bool _. + +Instance mod2_hset : IsHSet Mod2. +Proof. +apply (trunc_equiv Bool Mod2_value^-1). +Defined. + +Theorem modulo2 : forall n : Mod2, n = succ(succ n). +Proof. +hinduction. +- apply mod. +- intros n p. + apply (ap succ p). +- apply set_path2. +Defined. + +Definition plus : Mod2 -> Mod2 -> Mod2. +Proof. +intros n. +hrecursion. +- exact n. +- apply succ. +- apply modulo2. +Defined. + +Lemma plus_x_Z_x : forall x, plus x Z = x. +Proof. +hinduction; cbn. +- reflexivity. +- intros n. refine (ap succ). +- apply set_path2. +Defined. + +Lemma plus_S_x_S : forall x y, + plus (succ x) y = succ (plus x y). +Proof. +intros x. +hinduction; cbn. +- reflexivity. +- intros n Hn. refine (ap succ Hn). +- apply set_path2. +Defined. + +Lemma plus_x_x_Z : forall x, plus x x = Z. +Proof. +hinduction. +- reflexivity. +- intros n Hn. cbn. + refine (ap succ (plus_S_x_S n n) @ _). + refine (ap (succ o succ) Hn @ _). + apply mod^. +- apply set_path2. +Defined. + +Definition mult : Mod2 -> Mod2 -> Mod2. +intros x. hrecursion. +- exact Z. +- intros y. exact (plus x y). +- simpl. + refine (_ @ ap (plus x) (plus_x_Z_x _)^). + apply (plus_x_x_Z x)^. +Defined. diff --git a/int/Mod2_ring.v b/int/Mod2_ring.v new file mode 100644 index 0000000..4900716 --- /dev/null +++ b/int/Mod2_ring.v @@ -0,0 +1,13 @@ +Require Import HoTT HitTactics. +Require Export Mod2. + +From HoTTClasses Require Import interfaces.abstract_algebra tactics.ring_tac. + +Section Mod2_ring. + +Instance Mod2_plus : Plus Mod2 := Mod2.plus. +Instance Mod2_mult : Mult Mod2 := Mod2.mult. +Instance Mod2_zero : Zero Mod2 := Z. +Instance Mod2_one : One Mod2 := succ Z. + +End Mod2_ring. diff --git a/int/_CoqProject b/int/_CoqProject new file mode 100644 index 0000000..6c766a7 --- /dev/null +++ b/int/_CoqProject @@ -0,0 +1,5 @@ +-R . "" COQC = hoqc COQDEP = hoqdep +-R ../prelude "" +-R ../../HoTTClasses/theories HoTTClasses +Mod2.v +Mod2_ring.v