TP 3: GaussInt

TP 3: GaussInt

GaussInt : Set

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.

Définition des Opérations

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.

Preuves des propriétés

Elément neutre

Lemma l : forall x:GaussInt, Gadd g0 x = x.
Proof.
intros.
induction x.
simpl.
reflexivity.
Qed.

Commutativité

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.

Associativité

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?

Distributativité de multiplication sur addition

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.