D'abord, création d'un ensemble inductif à partir de Z:
Require Export ZArith.
Inductive GaussInt : Set :=
c : Z ->Z-> GaussInt.
Definition g0 := c 0 0.
Definition g1 := c 1 0.
Definition gi := c 0 1.
Definition Gadd (x y : GaussInt):GaussInt := match x with c a b => match y with c a1 b1 => c (a+a1) (b+b1) end end. Definition Gmult (x y : GaussInt) : GaussInt := match x with c a b => match y with c a1 b1 => c (a*a1 - b*b1) (a*b1 + a1*b) end end. Definition Gopp ( x y : GaussInt): GaussInt := match x with c a b => match y with c a1 b1 => c (a-a1) (b-b1) end end.
Lemma l : forall x:GaussInt, Gadd g0 x = x. Proof. intros. induction x. simpl. reflexivity. Qed.
Lemma Gplus_comm : forall a b:GaussInt, Gadd a b = Gadd b a. Proof. intros. induction a. induction b. simpl. rewrite Zplus_comm. rewrite (Zplus_comm z0 z2). reflexivity. Qed. Lemma Gmult_comm : forall a b :GaussInt, Gmult a b = Gmult b a. Proof. intros. induction a. induction b. simpl. rewrite (Zmult_comm z z1). rewrite (Zmult_comm z0 z2). rewrite (Zplus_comm (z1 * z0) (z * z2)). reflexivity. Qed.
Lemma Gplus_assoc : forall a b c:GaussInt, Gadd (Gadd a b) c = Gadd a (Gadd b c). Proof. intros. destruct a;destruct b; destruct c0. simpl. rewrite Zplus_assoc. rewrite Zplus_assoc. reflexivity. Qed.
Tiens, pas fait pour multiplication…peut être pas vrai?
Lemma Gmult_distrib : forall a b c : GaussInt, Gmult a (Gadd b c) = Gadd (Gmult a b) (Gmult a c). Proof. intros. destruct a;destruct b; destruct c0. simpl. rewrite Zmult_plus_distr_r. rewrite Zmult_plus_distr_r. rewrite Zmult_plus_distr_r. rewrite Zmult_plus_distr_l. rewrite Zplus_assoc. rewrite Zplus_assoc. SearchAbout [ Zplus "distr" ]. unfold Zminus. rewrite Zopp_plus_distr. rewrite Zplus_assoc. rewrite Zplus_assoc. rewrite Zplus_comm. rewrite Zplus_comm. (* et maintenant? comment mettre les produits dans le bon ordre pour qu'il admette reflexivity? rewrite (Zplus_comm (z*z3) + - (z0*z2)). ...ne passe pas, unknown interpretation for notation"-_" *) rewrite (Zplus_comm (z*z3) + (- (z0*z2))). reflexivity. simpl. rewrite Zmult_plus_distr_r. rewrite Zmult_plus_distr_r.