Correction sur commit errone de la version 1.3

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@815 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 206 insertions, 0 deletions

diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 60fa01ff1..6bb1f5aa9 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -448,4 +448,210 @@ Tactic Definition Solve1 :=
     [Rewrite H; Simpl; Auto
     |Simpl in H0; Rewrite H0; Auto ].
 
+Lemma signed_sum_merge_ok : (x,y:signed_sum)
+  (interp_sacs (signed_sum_merge x y))
+  ==(Aplus (interp_sacs x) (interp_sacs y)).
+
+  Induction x.
+  Intro; Simpl; Auto.
+
+  Induction y; Intros.
+
+  Auto.
+
+  Solve1.
+
+  Simpl; Generalize (varlist_eq_prop v v0).
+  Elim (varlist_eq v v0); Simpl.
+
+  Intro Heq; Rewrite (Heq I).
+  Rewrite H.
+  Repeat Rewrite isacs_aux_ok.
+  Rewrite (Th_plus_permute T). 
+  Repeat Rewrite (Th_plus_assoc T).
+  Rewrite (Th_plus_sym T (Aopp (interp_vl Amult Aone Azero vm v0))
+                         (interp_vl Amult Aone Azero vm v0)).
+  Rewrite (Th_opp_def T).
+  Rewrite (Th_plus_zero_left T).
+  Reflexivity.
+
+  Solve1.
+
+  Induction y; Intros.
+
+  Auto.
+
+  Simpl; Generalize (varlist_eq_prop v v0).
+  Elim (varlist_eq v v0); Simpl.
+
+  Intro Heq; Rewrite (Heq I).
+  Rewrite H.
+  Repeat Rewrite isacs_aux_ok.
+  Rewrite (Th_plus_permute T). 
+  Repeat Rewrite (Th_plus_assoc T).
+  Rewrite (Th_opp_def T).
+  Rewrite (Th_plus_zero_left T).
+  Reflexivity.
+
+  Solve1.
+
+  Solve1.
+
+Save.
+
+Tactic Definition Solve2 :=
+ 	Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok;
+  	[ Auto
+  	| Rewrite H; Auto ].
+
+Lemma plus_varlist_insert_ok : (l:varlist)(s:signed_sum)
+	(interp_sacs (plus_varlist_insert l s)) 
+	== (Aplus (interp_vl  Amult Aone Azero vm l) (interp_sacs s)).
+Proof.
+
+  Induction s.
+  Trivial.
+
+  Simpl; Intros.
+  Solve2.
+
+  Simpl; Intros.
+  Generalize (varlist_eq_prop l v).
+  Elim (varlist_eq l v); Simpl.
+
+  Intro Heq; Rewrite (Heq I).
+  Repeat Rewrite isacs_aux_ok.
+  Repeat Rewrite (Th_plus_assoc T).
+  Rewrite (Th_opp_def T).
+  Rewrite (Th_plus_zero_left T).
+  Reflexivity.
+
+  Solve2.
+
+Save.
+
+Lemma minus_varlist_insert_ok : (l:varlist)(s:signed_sum)
+	(interp_sacs (minus_varlist_insert l s)) 
+	== (Aplus (Aopp (interp_vl  Amult Aone Azero vm l)) (interp_sacs s)).
+Proof.
+
+  Induction s.
+  Trivial.
+
+  Simpl; Intros.
+  Generalize (varlist_eq_prop l v).
+  Elim (varlist_eq l v); Simpl.
+
+  Intro Heq; Rewrite (Heq I).
+  Repeat Rewrite isacs_aux_ok.
+  Repeat Rewrite (Th_plus_assoc T).
+  Rewrite (Th_plus_sym T (Aopp (interp_vl Amult Aone Azero vm v))
+         (interp_vl Amult Aone Azero vm v)).
+  Rewrite (Th_opp_def T).
+  Auto.
+
+  Simpl; Intros.
+  Solve2.
+
+  Simpl; Intros; Solve2.
+
+Save.
+
+Lemma plus_sum_scalar_ok : (l:varlist)(s:signed_sum)
+	(interp_sacs (plus_sum_scalar l s)) 
+	== (Amult (interp_vl  Amult Aone Azero vm l) (interp_sacs s)).
+Proof.
+
+  Induction s.
+  Trivial.
+
+  Simpl; Intros.
+  Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
+  Repeat Rewrite isacs_aux_ok.
+  Rewrite H.
+  Auto.
+
+  Simpl; Intros.
+  Repeat Rewrite isacs_aux_ok.
+  Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
+  Rewrite H.
+  Rewrite (Th_distr_right T).
+  Rewrite <- (Th_opp_mult_right T).
+  Reflexivity.
+
+Save.
+
+Lemma minus_sum_scalar_ok : (l:varlist)(s:signed_sum)
+	(interp_sacs (minus_sum_scalar l s)) 
+	== (Aopp (Amult (interp_vl  Amult Aone Azero vm l) (interp_sacs s))).
+Proof.
+
+  Induction s; Simpl; Intros.
+
+  Rewrite (Th_mult_zero_right T); Symmetry; Apply (Th_opp_zero T).
+
+  Simpl; Intros.
+  Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
+  Repeat Rewrite isacs_aux_ok.
+  Rewrite H.
+  Rewrite (Th_distr_right T).
+  Rewrite (Th_plus_opp_opp T).
+  Reflexivity.
+
+  Simpl; Intros.
+  Repeat Rewrite isacs_aux_ok.
+  Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
+  Rewrite H.
+  Rewrite (Th_distr_right T).
+  Rewrite <- (Th_opp_mult_right T).
+  Rewrite <- (Th_plus_opp_opp T).
+  Rewrite (Th_opp_opp T).
+  Reflexivity.
+
+Save.
+
+Lemma signed_sum_prod_ok : (x,y:signed_sum)
+	(interp_sacs (signed_sum_prod x y)) ==
+		(Amult (interp_sacs x) (interp_sacs y)).
+Proof.
+
+  Induction x.
+
+  Simpl; EAuto 1.
+
+  Intros; Simpl.
+  Rewrite signed_sum_merge_ok.
+  Rewrite plus_sum_scalar_ok.
+  Repeat Rewrite isacs_aux_ok.
+  Rewrite H.
+  Auto.
+
+  Intros; Simpl.
+  Repeat Rewrite isacs_aux_ok.
+  Rewrite signed_sum_merge_ok.
+  Rewrite minus_sum_scalar_ok.
+  Rewrite H.
+  Rewrite (Th_distr_left T).
+  Rewrite (Th_opp_mult_left T).
+  Reflexivity.
+
+Save.
+
+Theorem apolynomial_normalize_ok : (p:apolynomial)
+	(interp_sacs (apolynomial_normalize p))==(interp_ap p).
+Proof.
+  Induction p; Simpl; Auto 1.
+  Intros.
+    Rewrite signed_sum_merge_ok.
+    Rewrite H; Rewrite H0; Reflexivity.
+  Intros.
+    Rewrite signed_sum_prod_ok.
+    Rewrite H; Rewrite H0; Reflexivity.
+  Intros.
+    Rewrite minus_sum_scalar_ok.
+    Simpl. 
+    Rewrite (Th_mult_one_left T).
+    Rewrite H; Reflexivity.
+Save.  
+
 End abstract_rings.