(* Setoids for Beginners / Setoides pour les Nuls *) (**************************************************) (* For coq CVS (>= February 2005) *) (* Pierre Castéran *) Require Import Setoid. Require Import Arith. Require Import Relations. Require Import Compare_dec. Require Import ArithRing. Require Import Omega. Set Implicit Arguments. (* We represent integers as pairs of Peano numbers *) Delimit Scope Z'_scope with Z'. Open Scope Z'_scope. Inductive Z' : Set := mkZ' : nat -> nat -> Z'. (* The equivalence relation on Z' *) Definition Z'eq (z z':Z') : Prop := let (a, b) := z in let (c, d) := z' in a + d = b + c. Notation "a =Z= b" := (Z'eq a b) (at level 70): Z'_scope. (* a characteristic property of =Z= *) Lemma Z'eq_inv : forall a b c d, mkZ' a b =Z= mkZ' c d -> {q:nat | (a = q + b /\ c = q + d) \/ (b = q + a /\ d = q + c)}. Proof. intros a b c d H ; simpl in H. case (le_lt_dec a b). exists (b-a); right; omega. exists (a-b); left; omega. Qed. (* Z'eq is an equivalence relation *) Lemma Z'eq_refl : reflexive Z' Z'eq. Proof. unfold reflexive. intro z; case z. unfold Z'eq. auto with arith. Qed. Lemma Z'eq_sym : symmetric _ Z'eq. Proof. unfold symmetric. intros z z'; case z; case z'. intros a b c d H. unfold Z'eq. symmetry. simpl in H. rewrite (plus_comm b c). rewrite (plus_comm a d). trivial. Qed. Lemma Z'eq_trans : transitive _ Z'eq. Proof. unfold transitive. intros x y z; case x;case y;case z. unfold Z'eq;intros;omega. Qed. (* We can now build a setoid *) Theorem Z'oid : Setoid_Theory _ Z'eq. split. exact Z'eq_refl. exact Z'eq_sym. exact Z'eq_trans. Qed. Add Setoid Z' Z'eq Z'oid as Z'_register. (* definition of operations in Z' *) Definition Z'_plus (z z':Z') := let (a, b) := z in let (c, d) := z' in mkZ'( a + c)(b + d). Notation "z + z'" := (Z'_plus z z'): Z'_scope. Add Morphism Z'_plus : Z'_plus_morph. intros z z0; case z;case z0. intros a b c d E. intros z1 z2; case z1 ; case z2; intros a' b' c' d' E'. simpl. simpl in E; simpl in E'. omega. Qed. Definition Z'_mult (z z':Z') := let (a, b) := z in let (c, d) := z' in mkZ'( a*c + b*d)(a*d + b*c). Notation "z * z'" := (Z'_mult z z'): Z'_scope. Add Morphism Z'_mult : Z'_mult_morph. intros z1 z2; case z1; case z2; intros a b c d E. intros z3 z4; case z3;case z4; intros a' b' c' d' E'. simpl in E; simpl in E'. case (Z'eq_inv E). case (Z'eq_inv E'). destruct 1; destruct 1. case H;case H0; intros; subst c; subst a;subst c'; subst a'. clear H0 E H E';simpl. ring_nat. case H;case H0; intros; subst d;subst b; subst c';subst a'. clear H0 E H E';simpl. ring_nat. case H;case H0; intros; subst c;subst a; subst d';subst b'. clear H E H0 E';simpl. ring_nat. case H;case H0; intros; subst d;subst b; subst d';subst b'. clear H0 E H E';simpl. ring_nat. Qed. Definition Z'_opp (z:Z') := let (a,b) := z in (mkZ' b a). Add Morphism Z'_opp : Z'_opp_morph. Proof. intros z z'; case z;case z'. intros a b a' b' e; case (Z'eq_inv e). intros x [(Ha',Ha)|(Hb',Hb)]. subst a;subst a'; simpl; auto with arith. subst b; subst b';simpl;auto with arith. Qed. Definition Z'_zero := mkZ' 0 0. Definition Z'_one := mkZ' 1 0. Theorem Z'_zero_l : forall z, Z'_zero + z =Z= z. Proof. intro z; case z; simpl. auto with arith. Qed. Theorem Z'_zero_r : forall z, z + Z'_zero =Z= z. Proof. intro z; case z; simpl. intros; omega. Qed. Theorem Z'_plus_assoc : forall z z' z'', z + (z' + z'') =Z= (z + z') + z''. Proof. destruct z; destruct z'; destruct z''. simpl. ring_nat. Qed. Theorem Z'_mult_assoc : forall z z' z'', z * (z' * z'') =Z= (z * z') * z''. Proof. destruct z; destruct z'; destruct z''. simpl. ring_nat. Qed. Theorem Z'_1_l : forall z, Z'_one * z =Z= z. Proof. destruct z;simpl. ring_nat. Qed. Theorem Z'_1_r : forall z, z =Z= Z'_one * z. Proof. destruct z;simpl. ring_nat. Qed. Theorem Z'_plus_comm : forall z z', z + z' =Z= z' + z. Proof. destruct z; destruct z';simpl. ring_nat. Qed. Theorem Z'_mult_comm : forall z z', z * z' =Z= z' * z. Proof. destruct z; destruct z';simpl. ring_nat. Qed. Theorem Z'_mult_dist : forall z z' z'', (z + z') * z'' =Z= z * z'' + z' * z''. Proof. destruct z;destruct z';destruct z''. simpl. ring_nat. Qed. (* technical lemma for proving integrity *) Lemma diff : forall a b:nat , {d:nat | (a = b + d \/ b = a + d)%nat}. Proof. intros a b; case (le_lt_dec a b). exists (b-a); right ; omega. exists (a-b);left;omega. Qed. Lemma nat_mult_is_zero : forall x y:nat, mult x y = 0 -> x = 0 \/ y = 0. Proof. destruct x; destruct y;auto. simpl; discriminate 1. Qed. Theorem Z'_integrity : forall z z', z * z' =Z= Z'_zero -> z =Z= Z'_zero \/ z' =Z= Z'_zero. Proof. intros z z' ; case z ; case z'; simpl; intros a b c d H. case (diff a b); case (diff c d). intros x [Hx|Hx] y [Hy|Hy]; [ (subst a; subst c) | (subst c; subst b) | (subst d; subst a) | (subst d;subst b)]; (do 2 rewrite plus_0_r in H; repeat rewrite mult_plus_distr_l in H; repeat rewrite mult_plus_distr_r in H; repeat rewrite plus_assoc in H; assert (x*y=0)%nat;[ omega | idtac]; case (nat_mult_is_zero _ _ H0);[ intro;subst x;left;auto with arith | intro;subst y;right;auto with arith]). Qed. Lemma plenty_of_zeros : forall n, Z'eq (mkZ' n n) (mkZ' 0 0). Proof. simpl. auto with arith. Qed. Lemma plenty_of_neutral : forall n z, Z'eq (Z'_plus (mkZ' n n) z) z. Proof. intros. setoid_rewrite plenty_of_zeros. setoid_rewrite Z'_zero_l. apply Z'eq_refl. Qed. Definition Z'_sub (z z':Z') := z + (Z'_opp z'). Notation "z - z'" := (Z'_sub z z'): Z'_scope. Add Morphism Z'_sub : Z'_sub_morph. unfold Z'_sub. intros z z0 e z1 z2 e'. setoid_rewrite e. setoid_rewrite e'. apply Z'eq_refl. Qed. (* Building Z modulo p *) (***********************) (* multiplication : nat -> Z' -> Z' *) Definition external_mult (n:nat)(z:Z') : Z' := let (a,b) := z in mkZ' (mult n a) ( mult n b). Add Morphism external_mult : external_morph. intros n z z0;case z; case z0. simpl. intros. transitivity (n*(n2+n1))%nat. ring_nat. transitivity (n*(n3+n0))%nat. rewrite H;trivial. ring_nat. Qed. Lemma external_zero : forall p, external_mult p (Z'_zero) =Z= Z'_zero. Proof. induction p. simpl. auto. unfold Z'_zero. simpl; auto. Qed. (* equivalence modulo p *) Inductive Z'_mod (p:nat)(z z':Z'):Prop := Z'_mod_i: forall q, z - z' =Z= external_mult p q -> Z'_mod p z z'. Lemma mod_refl : forall p z, Z'_mod p z z. Proof. destruct z;simpl. exists (Z'_zero). simpl. auto with arith. Qed. Lemma mod_sym : forall p z z', Z'_mod p z z' -> Z'_mod p z' z. Proof. destruct z;destruct z'. inversion 1. exists (Z'_opp q). simpl. simpl in H0. generalize q H0. clear H0. destruct q0. simpl. intro. omega. Qed. Lemma mod_trans : forall p z z' z'', Z'_mod p z z' -> Z'_mod p z' z'' -> Z'_mod p z z'' . Proof. destruct z;destruct z'; destruct z''. inversion 1. inversion 1. exists (q+q0). generalize q H0 q0 H2. destruct q1. destruct q1. simpl. simpl in H3. intro. repeat rewrite mult_plus_distr_l. omega. Qed. Lemma mod_plus_compat_l : forall p z z0 z1, Z'_mod p z0 z1 -> Z'_mod p (z+z0) (z+z1). Proof. destruct z. destruct z0. destruct z1. inversion 1. exists q. generalize H0;case q. simpl. intros. omega. Qed. Lemma mod_plus_compat_r : forall p z z0 z1, Z'_mod p z0 z1 -> Z'_mod p (z0+z) (z1+z). Proof. destruct z. destruct z0. destruct z1. inversion 1. exists q. generalize H0;case q. simpl. intros. omega. Qed. Lemma mod_plus_compat : forall p z z0 z1 z2, Z'_mod p z z0 -> Z'_mod p z1 z2 -> Z'_mod p (z+z1) (z0+z2). Proof. intros. apply mod_trans with (z0+z1). apply mod_plus_compat_r; trivial. apply mod_plus_compat_l;trivial. Qed. (* let's build a new type upon Z' *) Inductive Zmod : Set := zmod : Z' -> Zmod. Definition modeq (p:nat)(m m':Zmod) := let (z) := m in let (z') := m' in Z'_mod p z z'. Definition zmodplus (p:nat)(m m':Zmod) := let (z) := m in let (z') := m' in zmod (z + z'). Lemma ZMT : forall p, Setoid_Theory Zmod (modeq p). Proof. split. destruct x;simpl. apply mod_refl. destruct x;destruct y;simpl;apply mod_sym. intros x y z; case x;case y;case z; simpl; intros. eapply mod_trans;eauto. Qed. (* Since setoid rewrite requires non dependent products, we have to fix now the value of p *) Definition eq16 := modeq 16. Add Setoid Zmod eq16 (ZMT 16) as Zmod_register. Definition plus16 := zmodplus 16. Notation "a =16= b" := (eq16 a b) (at level 70): mod16_scope. Notation "a + b" := (plus16 a b) :mod16_scope. Notation "'cl' a" := (zmod (mkZ' a 0)) (at level 29) :mod16_scope. Open Scope mod16_scope. Add Morphism plus16 : plus16_morph. Proof. intros z z0 ;case z;case z0. intros a b e; intros z1 z2; case z1 ;case z2;intros c d e'. simpl;apply mod_plus_compat;auto. Qed. Lemma cl_morph : forall n p:nat ,cl (n+p) =16= cl n + cl p. Proof. simpl. intros; apply mod_refl. Qed. Goal (cl 13) + (cl 13) =16= (cl 10). setoid_rewrite <- cl_morph. simpl. exists (mkZ' 1 0). simpl;auto. Qed.