summaryrefslogtreecommitdiff
path: root/contrib7/ring/Ring_normalize.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib7/ring/Ring_normalize.v')
-rw-r--r--contrib7/ring/Ring_normalize.v893
1 files changed, 893 insertions, 0 deletions
diff --git a/contrib7/ring/Ring_normalize.v b/contrib7/ring/Ring_normalize.v
new file mode 100644
index 00000000..1dbd9d56
--- /dev/null
+++ b/contrib7/ring/Ring_normalize.v
@@ -0,0 +1,893 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: Ring_normalize.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *)
+
+Require Ring_theory.
+Require Quote.
+
+Set Implicit Arguments.
+
+Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m.
+Proof.
+ Intros.
+ Apply Quote.index_eq_prop.
+ Generalize H.
+ Case (index_eq n m); Simpl; Trivial; Intros.
+ Contradiction.
+Save.
+
+Section semi_rings.
+
+Variable A : Type.
+Variable Aplus : A -> A -> A.
+Variable Amult : A -> A -> A.
+Variable Aone : A.
+Variable Azero : A.
+Variable Aeq : A -> A -> bool.
+
+(* Section definitions. *)
+
+
+(******************************************)
+(* Normal abtract Polynomials *)
+(******************************************)
+(* DEFINITIONS :
+- A varlist is a sorted product of one or more variables : x, x*y*z
+- A monom is a constant, a varlist or the product of a constant by a varlist
+ variables. 2*x*y, x*y*z, 3 are monoms : 2*3, x*3*y, 4*x*3 are NOT.
+- A canonical sum is either a monom or an ordered sum of monoms
+ (the order on monoms is defined later)
+- A normal polynomial it either a constant or a canonical sum or a constant
+ plus a canonical sum
+*)
+
+(* varlist is isomorphic to (list var), but we built a special inductive
+ for efficiency *)
+Inductive varlist : Type :=
+| Nil_var : varlist
+| Cons_var : index -> varlist -> varlist
+.
+
+Inductive canonical_sum : Type :=
+| Nil_monom : canonical_sum
+| Cons_monom : A -> varlist -> canonical_sum -> canonical_sum
+| Cons_varlist : varlist -> canonical_sum -> canonical_sum
+.
+
+(* Order on monoms *)
+
+(* That's the lexicographic order on varlist, extended by :
+ - A constant is less than every monom
+ - The relation between two varlist is preserved by multiplication by a
+ constant.
+
+ Examples :
+ 3 < x < y
+ x*y < x*y*y*z
+ 2*x*y < x*y*y*z
+ x*y < 54*x*y*y*z
+ 4*x*y < 59*x*y*y*z
+*)
+
+Fixpoint varlist_eq [x,y:varlist] : bool :=
+ Cases x y of
+ | Nil_var Nil_var => true
+ | (Cons_var i xrest) (Cons_var j yrest) =>
+ (andb (index_eq i j) (varlist_eq xrest yrest))
+ | _ _ => false
+ end.
+
+Fixpoint varlist_lt [x,y:varlist] : bool :=
+ Cases x y of
+ | Nil_var (Cons_var _ _) => true
+ | (Cons_var i xrest) (Cons_var j yrest) =>
+ if (index_lt i j) then true
+ else (andb (index_eq i j) (varlist_lt xrest yrest))
+ | _ _ => false
+ end.
+
+(* merges two variables lists *)
+Fixpoint varlist_merge [l1:varlist] : varlist -> varlist :=
+ Cases l1 of
+ | (Cons_var v1 t1) =>
+ Fix vm_aux {vm_aux [l2:varlist] : varlist :=
+ Cases l2 of
+ | (Cons_var v2 t2) =>
+ if (index_lt v1 v2)
+ then (Cons_var v1 (varlist_merge t1 l2))
+ else (Cons_var v2 (vm_aux t2))
+ | Nil_var => l1
+ end}
+ | Nil_var => [l2]l2
+ end.
+
+(* returns the sum of two canonical sums *)
+Fixpoint canonical_sum_merge [s1:canonical_sum]
+ : canonical_sum -> canonical_sum :=
+Cases s1 of
+| (Cons_monom c1 l1 t1) =>
+ Fix csm_aux{csm_aux[s2:canonical_sum] : canonical_sum :=
+ Cases s2 of
+ | (Cons_monom c2 l2 t2) =>
+ if (varlist_eq l1 l2)
+ then (Cons_monom (Aplus c1 c2) l1
+ (canonical_sum_merge t1 t2))
+ else if (varlist_lt l1 l2)
+ then (Cons_monom c1 l1 (canonical_sum_merge t1 s2))
+ else (Cons_monom c2 l2 (csm_aux t2))
+ | (Cons_varlist l2 t2) =>
+ if (varlist_eq l1 l2)
+ then (Cons_monom (Aplus c1 Aone) l1
+ (canonical_sum_merge t1 t2))
+ else if (varlist_lt l1 l2)
+ then (Cons_monom c1 l1 (canonical_sum_merge t1 s2))
+ else (Cons_varlist l2 (csm_aux t2))
+ | Nil_monom => s1
+ end}
+| (Cons_varlist l1 t1) =>
+ Fix csm_aux2{csm_aux2[s2:canonical_sum] : canonical_sum :=
+ Cases s2 of
+ | (Cons_monom c2 l2 t2) =>
+ if (varlist_eq l1 l2)
+ then (Cons_monom (Aplus Aone c2) l1
+ (canonical_sum_merge t1 t2))
+ else if (varlist_lt l1 l2)
+ then (Cons_varlist l1 (canonical_sum_merge t1 s2))
+ else (Cons_monom c2 l2 (csm_aux2 t2))
+ | (Cons_varlist l2 t2) =>
+ if (varlist_eq l1 l2)
+ then (Cons_monom (Aplus Aone Aone) l1
+ (canonical_sum_merge t1 t2))
+ else if (varlist_lt l1 l2)
+ then (Cons_varlist l1 (canonical_sum_merge t1 s2))
+ else (Cons_varlist l2 (csm_aux2 t2))
+ | Nil_monom => s1
+ end}
+| Nil_monom => [s2]s2
+end.
+
+(* Insertion of a monom in a canonical sum *)
+Fixpoint monom_insert [c1:A; l1:varlist; s2 : canonical_sum]
+ : canonical_sum :=
+ Cases s2 of
+ | (Cons_monom c2 l2 t2) =>
+ if (varlist_eq l1 l2)
+ then (Cons_monom (Aplus c1 c2) l1 t2)
+ else if (varlist_lt l1 l2)
+ then (Cons_monom c1 l1 s2)
+ else (Cons_monom c2 l2 (monom_insert c1 l1 t2))
+ | (Cons_varlist l2 t2) =>
+ if (varlist_eq l1 l2)
+ then (Cons_monom (Aplus c1 Aone) l1 t2)
+ else if (varlist_lt l1 l2)
+ then (Cons_monom c1 l1 s2)
+ else (Cons_varlist l2 (monom_insert c1 l1 t2))
+ | Nil_monom => (Cons_monom c1 l1 Nil_monom)
+ end.
+
+Fixpoint varlist_insert [l1:varlist; s2:canonical_sum]
+ : canonical_sum :=
+ Cases s2 of
+ | (Cons_monom c2 l2 t2) =>
+ if (varlist_eq l1 l2)
+ then (Cons_monom (Aplus Aone c2) l1 t2)
+ else if (varlist_lt l1 l2)
+ then (Cons_varlist l1 s2)
+ else (Cons_monom c2 l2 (varlist_insert l1 t2))
+ | (Cons_varlist l2 t2) =>
+ if (varlist_eq l1 l2)
+ then (Cons_monom (Aplus Aone Aone) l1 t2)
+ else if (varlist_lt l1 l2)
+ then (Cons_varlist l1 s2)
+ else (Cons_varlist l2 (varlist_insert l1 t2))
+ | Nil_monom => (Cons_varlist l1 Nil_monom)
+ end.
+
+(* Computes c0*s *)
+Fixpoint canonical_sum_scalar [c0:A; s:canonical_sum] : canonical_sum :=
+ Cases s of
+ | (Cons_monom c l t) =>
+ (Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t))
+ | (Cons_varlist l t) =>
+ (Cons_monom c0 l (canonical_sum_scalar c0 t))
+ | Nil_monom => Nil_monom
+ end.
+
+(* Computes l0*s *)
+Fixpoint canonical_sum_scalar2 [l0:varlist; s:canonical_sum]
+ : canonical_sum :=
+ Cases s of
+ | (Cons_monom c l t) =>
+ (monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t))
+ | (Cons_varlist l t) =>
+ (varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t))
+ | Nil_monom => Nil_monom
+ end.
+
+(* Computes c0*l0*s *)
+Fixpoint canonical_sum_scalar3 [c0:A;l0:varlist; s:canonical_sum]
+ : canonical_sum :=
+ Cases s of
+ | (Cons_monom c l t) =>
+ (monom_insert (Amult c0 c) (varlist_merge l0 l)
+ (canonical_sum_scalar3 c0 l0 t))
+ | (Cons_varlist l t) =>
+ (monom_insert c0 (varlist_merge l0 l)
+ (canonical_sum_scalar3 c0 l0 t))
+ | Nil_monom => Nil_monom
+ end.
+
+(* returns the product of two canonical sums *)
+Fixpoint canonical_sum_prod [s1:canonical_sum]
+ : canonical_sum -> canonical_sum :=
+ [s2]Cases s1 of
+ | (Cons_monom c1 l1 t1) =>
+ (canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2)
+ (canonical_sum_prod t1 s2))
+ | (Cons_varlist l1 t1) =>
+ (canonical_sum_merge (canonical_sum_scalar2 l1 s2)
+ (canonical_sum_prod t1 s2))
+ | Nil_monom => Nil_monom
+ end.
+
+(* The type to represent concrete semi-ring polynomials *)
+Inductive Type spolynomial :=
+ SPvar : index -> spolynomial
+| SPconst : A -> spolynomial
+| SPplus : spolynomial -> spolynomial -> spolynomial
+| SPmult : spolynomial -> spolynomial -> spolynomial.
+
+Fixpoint spolynomial_normalize[p:spolynomial] : canonical_sum :=
+ Cases p of
+ | (SPvar i) => (Cons_varlist (Cons_var i Nil_var) Nil_monom)
+ | (SPconst c) => (Cons_monom c Nil_var Nil_monom)
+ | (SPplus l r) => (canonical_sum_merge (spolynomial_normalize l)
+ (spolynomial_normalize r))
+ | (SPmult l r) => (canonical_sum_prod (spolynomial_normalize l)
+ (spolynomial_normalize r))
+ end.
+
+(* Deletion of useless 0 and 1 in canonical sums *)
+Fixpoint canonical_sum_simplify [ s:canonical_sum] : canonical_sum :=
+ Cases s of
+ | (Cons_monom c l t) =>
+ if (Aeq c Azero)
+ then (canonical_sum_simplify t)
+ else if (Aeq c Aone)
+ then (Cons_varlist l (canonical_sum_simplify t))
+ else (Cons_monom c l (canonical_sum_simplify t))
+ | (Cons_varlist l t) => (Cons_varlist l (canonical_sum_simplify t))
+ | Nil_monom => Nil_monom
+ end.
+
+Definition spolynomial_simplify :=
+ [x:spolynomial](canonical_sum_simplify (spolynomial_normalize x)).
+
+(* End definitions. *)
+
+(* Section interpretation. *)
+
+(*** Here a variable map is defined and the interpetation of a spolynom
+ acording to a certain variables map. Once again the choosen definition
+ is generic and could be changed ****)
+
+Variable vm : (varmap A).
+
+(* Interpretation of list of variables
+ * [x1; ... ; xn ] is interpreted as (find v x1)* ... *(find v xn)
+ * The unbound variables are mapped to 0. Normally this case sould
+ * never occur. Since we want only to prove correctness theorems, which form
+ * is : for any varmap and any spolynom ... this is a safe and pain-saving
+ * choice *)
+Definition interp_var [i:index] := (varmap_find Azero i vm).
+
+(* Local *) Definition ivl_aux := Fix ivl_aux {ivl_aux[x:index; t:varlist] : A :=
+ Cases t of
+ | Nil_var => (interp_var x)
+ | (Cons_var x' t') => (Amult (interp_var x) (ivl_aux x' t'))
+ end}.
+
+Definition interp_vl := [l:varlist]
+ Cases l of
+ | Nil_var => Aone
+ | (Cons_var x t) => (ivl_aux x t)
+ end.
+
+(* Local *) Definition interp_m := [c:A][l:varlist]
+ Cases l of
+ | Nil_var => c
+ | (Cons_var x t) =>
+ (Amult c (ivl_aux x t))
+ end.
+
+(* Local *) Definition ics_aux := Fix ics_aux{ics_aux[a:A; s:canonical_sum] : A :=
+ Cases s of
+ | Nil_monom => a
+ | (Cons_varlist l t) => (Aplus a (ics_aux (interp_vl l) t))
+ | (Cons_monom c l t) => (Aplus a (ics_aux (interp_m c l) t))
+ end}.
+
+(* Interpretation of a canonical sum *)
+Definition interp_cs : canonical_sum -> A :=
+ [s]Cases s of
+ | Nil_monom => Azero
+ | (Cons_varlist l t) =>
+ (ics_aux (interp_vl l) t)
+ | (Cons_monom c l t) =>
+ (ics_aux (interp_m c l) t)
+ end.
+
+Fixpoint interp_sp [p:spolynomial] : A :=
+ Cases p of
+ (SPconst c) => c
+ | (SPvar i) => (interp_var i)
+ | (SPplus p1 p2) => (Aplus (interp_sp p1) (interp_sp p2))
+ | (SPmult p1 p2) => (Amult (interp_sp p1) (interp_sp p2))
+ end.
+
+
+(* End interpretation. *)
+
+Unset Implicit Arguments.
+
+(* Section properties. *)
+
+Variable T : (Semi_Ring_Theory Aplus Amult Aone Azero Aeq).
+
+Hint SR_plus_sym_T := Resolve (SR_plus_sym T).
+Hint SR_plus_assoc_T := Resolve (SR_plus_assoc T).
+Hint SR_plus_assoc2_T := Resolve (SR_plus_assoc2 T).
+Hint SR_mult_sym_T := Resolve (SR_mult_sym T).
+Hint SR_mult_assoc_T := Resolve (SR_mult_assoc T).
+Hint SR_mult_assoc2_T := Resolve (SR_mult_assoc2 T).
+Hint SR_plus_zero_left_T := Resolve (SR_plus_zero_left T).
+Hint SR_plus_zero_left2_T := Resolve (SR_plus_zero_left2 T).
+Hint SR_mult_one_left_T := Resolve (SR_mult_one_left T).
+Hint SR_mult_one_left2_T := Resolve (SR_mult_one_left2 T).
+Hint SR_mult_zero_left_T := Resolve (SR_mult_zero_left T).
+Hint SR_mult_zero_left2_T := Resolve (SR_mult_zero_left2 T).
+Hint SR_distr_left_T := Resolve (SR_distr_left T).
+Hint SR_distr_left2_T := Resolve (SR_distr_left2 T).
+Hint SR_plus_reg_left_T := Resolve (SR_plus_reg_left T).
+Hint SR_plus_permute_T := Resolve (SR_plus_permute T).
+Hint SR_mult_permute_T := Resolve (SR_mult_permute T).
+Hint SR_distr_right_T := Resolve (SR_distr_right T).
+Hint SR_distr_right2_T := Resolve (SR_distr_right2 T).
+Hint SR_mult_zero_right_T := Resolve (SR_mult_zero_right T).
+Hint SR_mult_zero_right2_T := Resolve (SR_mult_zero_right2 T).
+Hint SR_plus_zero_right_T := Resolve (SR_plus_zero_right T).
+Hint SR_plus_zero_right2_T := Resolve (SR_plus_zero_right2 T).
+Hint SR_mult_one_right_T := Resolve (SR_mult_one_right T).
+Hint SR_mult_one_right2_T := Resolve (SR_mult_one_right2 T).
+Hint SR_plus_reg_right_T := Resolve (SR_plus_reg_right T).
+Hints Resolve refl_equal sym_equal trans_equal.
+(* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
+Hints Immediate T.
+
+Lemma varlist_eq_prop : (x,y:varlist)
+ (Is_true (varlist_eq x y))->x==y.
+Proof.
+ Induction x; Induction y; Contradiction Orelse Try Reflexivity.
+ Simpl; Intros.
+ Generalize (andb_prop2 ? ? H1); Intros; Elim H2; Intros.
+ Rewrite (index_eq_prop H3); Rewrite (H v0 H4); Reflexivity.
+Save.
+
+Remark ivl_aux_ok : (v:varlist)(i:index)
+ (ivl_aux i v)==(Amult (interp_var i) (interp_vl v)).
+Proof.
+ Induction v; Simpl; Intros.
+ Trivial.
+ Rewrite H; Trivial.
+Save.
+
+Lemma varlist_merge_ok : (x,y:varlist)
+ (interp_vl (varlist_merge x y))
+ ==(Amult (interp_vl x) (interp_vl y)).
+Proof.
+ Induction x.
+ Simpl; Trivial.
+ Induction y.
+ Simpl; Trivial.
+ Simpl; Intros.
+ Elim (index_lt i i0); Simpl; Intros.
+
+ Repeat Rewrite ivl_aux_ok.
+ Rewrite H. Simpl.
+ Rewrite ivl_aux_ok.
+ EAuto.
+
+ Repeat Rewrite ivl_aux_ok.
+ Rewrite H0.
+ Rewrite ivl_aux_ok.
+ EAuto.
+Save.
+
+Remark ics_aux_ok : (x:A)(s:canonical_sum)
+ (ics_aux x s)==(Aplus x (interp_cs s)).
+Proof.
+ Induction s; Simpl; Intros.
+ Trivial.
+ Reflexivity.
+ Reflexivity.
+Save.
+
+Remark interp_m_ok : (x:A)(l:varlist)
+ (interp_m x l)==(Amult x (interp_vl l)).
+Proof.
+ NewDestruct l.
+ Simpl; Trivial.
+ Reflexivity.
+Save.
+
+Lemma canonical_sum_merge_ok : (x,y:canonical_sum)
+ (interp_cs (canonical_sum_merge x y))
+ ==(Aplus (interp_cs x) (interp_cs y)).
+
+Induction x; Simpl.
+Trivial.
+
+Induction y; Simpl; Intros.
+(* monom and nil *)
+EAuto.
+
+(* monom and monom *)
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl; Repeat Rewrite ics_aux_ok; Rewrite H.
+Repeat Rewrite interp_m_ok.
+Rewrite (SR_distr_left T).
+Repeat Rewrite <- (SR_plus_assoc T).
+Apply congr_eqT with f:=(Aplus (Amult a (interp_vl v0))).
+Trivial.
+
+Elim (varlist_lt v v0); Simpl.
+Repeat Rewrite ics_aux_ok.
+Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto.
+
+Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto.
+
+(* monom and varlist *)
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl; Repeat Rewrite ics_aux_ok; Rewrite H.
+Repeat Rewrite interp_m_ok.
+Rewrite (SR_distr_left T).
+Repeat Rewrite <- (SR_plus_assoc T).
+Apply congr_eqT with f:=(Aplus (Amult a (interp_vl v0))).
+Rewrite (SR_mult_one_left T).
+Trivial.
+
+Elim (varlist_lt v v0); Simpl.
+Repeat Rewrite ics_aux_ok.
+Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto.
+Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto.
+
+Induction y; Simpl; Intros.
+(* varlist and nil *)
+Trivial.
+
+(* varlist and monom *)
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl; Repeat Rewrite ics_aux_ok; Rewrite H.
+Repeat Rewrite interp_m_ok.
+Rewrite (SR_distr_left T).
+Repeat Rewrite <- (SR_plus_assoc T).
+Rewrite (SR_mult_one_left T).
+Apply congr_eqT with f:=(Aplus (interp_vl v0)).
+Trivial.
+
+Elim (varlist_lt v v0); Simpl.
+Repeat Rewrite ics_aux_ok.
+Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto.
+Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto.
+
+(* varlist and varlist *)
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl; Repeat Rewrite ics_aux_ok; Rewrite H.
+Repeat Rewrite interp_m_ok.
+Rewrite (SR_distr_left T).
+Repeat Rewrite <- (SR_plus_assoc T).
+Rewrite (SR_mult_one_left T).
+Apply congr_eqT with f:=(Aplus (interp_vl v0)).
+Trivial.
+
+Elim (varlist_lt v v0); Simpl.
+Repeat Rewrite ics_aux_ok.
+Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto.
+Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto.
+Save.
+
+Lemma monom_insert_ok: (a:A)(l:varlist)(s:canonical_sum)
+ (interp_cs (monom_insert a l s))
+ == (Aplus (Amult a (interp_vl l)) (interp_cs s)).
+Intros; Generalize s; Induction s0.
+
+Simpl; Rewrite interp_m_ok; Trivial.
+
+Simpl; Intros.
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok;
+ Repeat Rewrite ics_aux_ok; Rewrite interp_m_ok;
+ Rewrite (SR_distr_left T); EAuto.
+Elim (varlist_lt l v); Simpl;
+[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto
+| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok;
+ Rewrite H; Rewrite ics_aux_ok; EAuto].
+
+Simpl; Intros.
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok;
+ Repeat Rewrite ics_aux_ok;
+ Rewrite (SR_distr_left T); Rewrite (SR_mult_one_left T); EAuto.
+Elim (varlist_lt l v); Simpl;
+[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto
+| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok;
+ Rewrite H; Rewrite ics_aux_ok; EAuto].
+Save.
+
+Lemma varlist_insert_ok :
+ (l:varlist)(s:canonical_sum)
+ (interp_cs (varlist_insert l s))
+ == (Aplus (interp_vl l) (interp_cs s)).
+Intros; Generalize s; Induction s0.
+
+Simpl; Trivial.
+
+Simpl; Intros.
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok;
+ Repeat Rewrite ics_aux_ok; Rewrite interp_m_ok;
+ Rewrite (SR_distr_left T); Rewrite (SR_mult_one_left T); EAuto.
+Elim (varlist_lt l v); Simpl;
+[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto
+| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok;
+ Rewrite H; Rewrite ics_aux_ok; EAuto].
+
+Simpl; Intros.
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok;
+ Repeat Rewrite ics_aux_ok;
+ Rewrite (SR_distr_left T); Rewrite (SR_mult_one_left T); EAuto.
+Elim (varlist_lt l v); Simpl;
+[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto
+| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok;
+ Rewrite H; Rewrite ics_aux_ok; EAuto].
+Save.
+
+Lemma canonical_sum_scalar_ok : (a:A)(s:canonical_sum)
+ (interp_cs (canonical_sum_scalar a s))
+ ==(Amult a (interp_cs s)).
+Induction s.
+Simpl; EAuto.
+
+Simpl; Intros.
+Repeat Rewrite ics_aux_ok.
+Repeat Rewrite interp_m_ok.
+Rewrite H.
+Rewrite (SR_distr_right T).
+Repeat Rewrite <- (SR_mult_assoc T).
+Reflexivity.
+
+Simpl; Intros.
+Repeat Rewrite ics_aux_ok.
+Repeat Rewrite interp_m_ok.
+Rewrite H.
+Rewrite (SR_distr_right T).
+Repeat Rewrite <- (SR_mult_assoc T).
+Reflexivity.
+Save.
+
+Lemma canonical_sum_scalar2_ok : (l:varlist; s:canonical_sum)
+ (interp_cs (canonical_sum_scalar2 l s))
+ ==(Amult (interp_vl l) (interp_cs s)).
+Induction s.
+Simpl; Trivial.
+
+Simpl; Intros.
+Rewrite monom_insert_ok.
+Repeat Rewrite ics_aux_ok.
+Repeat Rewrite interp_m_ok.
+Rewrite H.
+Rewrite varlist_merge_ok.
+Repeat Rewrite (SR_distr_right T).
+Repeat Rewrite <- (SR_mult_assoc T).
+Repeat Rewrite <- (SR_plus_assoc T).
+Rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)).
+Reflexivity.
+
+Simpl; Intros.
+Rewrite varlist_insert_ok.
+Repeat Rewrite ics_aux_ok.
+Repeat Rewrite interp_m_ok.
+Rewrite H.
+Rewrite varlist_merge_ok.
+Repeat Rewrite (SR_distr_right T).
+Repeat Rewrite <- (SR_mult_assoc T).
+Repeat Rewrite <- (SR_plus_assoc T).
+Reflexivity.
+Save.
+
+Lemma canonical_sum_scalar3_ok : (c:A; l:varlist; s:canonical_sum)
+ (interp_cs (canonical_sum_scalar3 c l s))
+ ==(Amult c (Amult (interp_vl l) (interp_cs s))).
+Induction s.
+Simpl; Repeat Rewrite (SR_mult_zero_right T); Reflexivity.
+
+Simpl; Intros.
+Rewrite monom_insert_ok.
+Repeat Rewrite ics_aux_ok.
+Repeat Rewrite interp_m_ok.
+Rewrite H.
+Rewrite varlist_merge_ok.
+Repeat Rewrite (SR_distr_right T).
+Repeat Rewrite <- (SR_mult_assoc T).
+Repeat Rewrite <- (SR_plus_assoc T).
+Rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)).
+Reflexivity.
+
+Simpl; Intros.
+Rewrite monom_insert_ok.
+Repeat Rewrite ics_aux_ok.
+Repeat Rewrite interp_m_ok.
+Rewrite H.
+Rewrite varlist_merge_ok.
+Repeat Rewrite (SR_distr_right T).
+Repeat Rewrite <- (SR_mult_assoc T).
+Repeat Rewrite <- (SR_plus_assoc T).
+Rewrite (SR_mult_permute T c (interp_vl l) (interp_vl v)).
+Reflexivity.
+Save.
+
+Lemma canonical_sum_prod_ok : (x,y:canonical_sum)
+ (interp_cs (canonical_sum_prod x y))
+ ==(Amult (interp_cs x) (interp_cs y)).
+Induction x; Simpl; Intros.
+Trivial.
+
+Rewrite canonical_sum_merge_ok.
+Rewrite canonical_sum_scalar3_ok.
+Rewrite ics_aux_ok.
+Rewrite interp_m_ok.
+Rewrite H.
+Rewrite (SR_mult_assoc T a (interp_vl v) (interp_cs y)).
+Symmetry.
+EAuto.
+
+Rewrite canonical_sum_merge_ok.
+Rewrite canonical_sum_scalar2_ok.
+Rewrite ics_aux_ok.
+Rewrite H.
+Trivial.
+Save.
+
+Theorem spolynomial_normalize_ok : (p:spolynomial)
+ (interp_cs (spolynomial_normalize p)) == (interp_sp p).
+Induction p; Simpl; Intros.
+
+Reflexivity.
+Reflexivity.
+
+Rewrite canonical_sum_merge_ok.
+Rewrite H; Rewrite H0.
+Reflexivity.
+
+Rewrite canonical_sum_prod_ok.
+Rewrite H; Rewrite H0.
+Reflexivity.
+Save.
+
+Lemma canonical_sum_simplify_ok : (s:canonical_sum)
+ (interp_cs (canonical_sum_simplify s)) == (interp_cs s).
+Induction s.
+
+Reflexivity.
+
+(* cons_monom *)
+Simpl; Intros.
+Generalize (SR_eq_prop T 8!a 9!Azero).
+Elim (Aeq a Azero).
+Intro Heq; Rewrite (Heq I).
+Rewrite H.
+Rewrite ics_aux_ok.
+Rewrite interp_m_ok.
+Rewrite (SR_mult_zero_left T).
+Trivial.
+
+Intros; Simpl.
+Generalize (SR_eq_prop T 8!a 9!Aone).
+Elim (Aeq a Aone).
+Intro Heq; Rewrite (Heq I).
+Simpl.
+Repeat Rewrite ics_aux_ok.
+Rewrite interp_m_ok.
+Rewrite H.
+Rewrite (SR_mult_one_left T).
+Reflexivity.
+
+Simpl.
+Repeat Rewrite ics_aux_ok.
+Rewrite interp_m_ok.
+Rewrite H.
+Reflexivity.
+
+(* cons_varlist *)
+Simpl; Intros.
+Repeat Rewrite ics_aux_ok.
+Rewrite H.
+Reflexivity.
+
+Save.
+
+Theorem spolynomial_simplify_ok : (p:spolynomial)
+ (interp_cs (spolynomial_simplify p)) == (interp_sp p).
+Intro.
+Unfold spolynomial_simplify.
+Rewrite canonical_sum_simplify_ok.
+Apply spolynomial_normalize_ok.
+Save.
+
+(* End properties. *)
+End semi_rings.
+
+Implicits Cons_varlist.
+Implicits Cons_monom.
+Implicits SPconst.
+Implicits SPplus.
+Implicits SPmult.
+
+Section rings.
+
+(* Here the coercion between Ring and Semi-Ring will be useful *)
+
+Set Implicit Arguments.
+
+Variable A : Type.
+Variable Aplus : A -> A -> A.
+Variable Amult : A -> A -> A.
+Variable Aone : A.
+Variable Azero : A.
+Variable Aopp : A -> A.
+Variable Aeq : A -> A -> bool.
+Variable vm : (varmap A).
+Variable T : (Ring_Theory Aplus Amult Aone Azero Aopp Aeq).
+
+Hint Th_plus_sym_T := Resolve (Th_plus_sym T).
+Hint Th_plus_assoc_T := Resolve (Th_plus_assoc T).
+Hint Th_plus_assoc2_T := Resolve (Th_plus_assoc2 T).
+Hint Th_mult_sym_T := Resolve (Th_mult_sym T).
+Hint Th_mult_assoc_T := Resolve (Th_mult_assoc T).
+Hint Th_mult_assoc2_T := Resolve (Th_mult_assoc2 T).
+Hint Th_plus_zero_left_T := Resolve (Th_plus_zero_left T).
+Hint Th_plus_zero_left2_T := Resolve (Th_plus_zero_left2 T).
+Hint Th_mult_one_left_T := Resolve (Th_mult_one_left T).
+Hint Th_mult_one_left2_T := Resolve (Th_mult_one_left2 T).
+Hint Th_mult_zero_left_T := Resolve (Th_mult_zero_left T).
+Hint Th_mult_zero_left2_T := Resolve (Th_mult_zero_left2 T).
+Hint Th_distr_left_T := Resolve (Th_distr_left T).
+Hint Th_distr_left2_T := Resolve (Th_distr_left2 T).
+Hint Th_plus_reg_left_T := Resolve (Th_plus_reg_left T).
+Hint Th_plus_permute_T := Resolve (Th_plus_permute T).
+Hint Th_mult_permute_T := Resolve (Th_mult_permute T).
+Hint Th_distr_right_T := Resolve (Th_distr_right T).
+Hint Th_distr_right2_T := Resolve (Th_distr_right2 T).
+Hint Th_mult_zero_right_T := Resolve (Th_mult_zero_right T).
+Hint Th_mult_zero_right2_T := Resolve (Th_mult_zero_right2 T).
+Hint Th_plus_zero_right_T := Resolve (Th_plus_zero_right T).
+Hint Th_plus_zero_right2_T := Resolve (Th_plus_zero_right2 T).
+Hint Th_mult_one_right_T := Resolve (Th_mult_one_right T).
+Hint Th_mult_one_right2_T := Resolve (Th_mult_one_right2 T).
+Hint Th_plus_reg_right_T := Resolve (Th_plus_reg_right T).
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hints Immediate T.
+
+(*** Definitions *)
+
+Inductive Type polynomial :=
+ Pvar : index -> polynomial
+| Pconst : A -> polynomial
+| Pplus : polynomial -> polynomial -> polynomial
+| Pmult : polynomial -> polynomial -> polynomial
+| Popp : polynomial -> polynomial.
+
+Fixpoint polynomial_normalize [x:polynomial] : (canonical_sum A) :=
+ Cases x of
+ (Pplus l r) => (canonical_sum_merge Aplus Aone
+ (polynomial_normalize l)
+ (polynomial_normalize r))
+ | (Pmult l r) => (canonical_sum_prod Aplus Amult Aone
+ (polynomial_normalize l)
+ (polynomial_normalize r))
+ | (Pconst c) => (Cons_monom c Nil_var (Nil_monom A))
+ | (Pvar i) => (Cons_varlist (Cons_var i Nil_var) (Nil_monom A))
+ | (Popp p) => (canonical_sum_scalar3 Aplus Amult Aone
+ (Aopp Aone) Nil_var
+ (polynomial_normalize p))
+ end.
+
+Definition polynomial_simplify :=
+ [x:polynomial](canonical_sum_simplify Aone Azero Aeq
+ (polynomial_normalize x)).
+
+Fixpoint spolynomial_of [x:polynomial] : (spolynomial A) :=
+ Cases x of
+ (Pplus l r) => (SPplus (spolynomial_of l) (spolynomial_of r))
+ | (Pmult l r) => (SPmult (spolynomial_of l) (spolynomial_of r))
+ | (Pconst c) => (SPconst c)
+ | (Pvar i) => (SPvar A i)
+ | (Popp p) => (SPmult (SPconst (Aopp Aone)) (spolynomial_of p))
+ end.
+
+(*** Interpretation *)
+
+Fixpoint interp_p [p:polynomial] : A :=
+ Cases p of
+ (Pconst c) => c
+ | (Pvar i) => (varmap_find Azero i vm)
+ | (Pplus p1 p2) => (Aplus (interp_p p1) (interp_p p2))
+ | (Pmult p1 p2) => (Amult (interp_p p1) (interp_p p2))
+ | (Popp p1) => (Aopp (interp_p p1))
+ end.
+
+(*** Properties *)
+
+Unset Implicit Arguments.
+
+Lemma spolynomial_of_ok : (p:polynomial)
+ (interp_p p)==(interp_sp Aplus Amult Azero vm (spolynomial_of p)).
+Induction p; Reflexivity Orelse (Simpl; Intros).
+Rewrite H; Rewrite H0; Reflexivity.
+Rewrite H; Rewrite H0; Reflexivity.
+Rewrite H.
+Rewrite (Th_opp_mult_left2 T).
+Rewrite (Th_mult_one_left T).
+Reflexivity.
+Save.
+
+Theorem polynomial_normalize_ok : (p:polynomial)
+ (polynomial_normalize p)
+ ==(spolynomial_normalize Aplus Amult Aone (spolynomial_of p)).
+Induction p; Reflexivity Orelse (Simpl; Intros).
+Rewrite H; Rewrite H0; Reflexivity.
+Rewrite H; Rewrite H0; Reflexivity.
+Rewrite H; Simpl.
+Elim (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var
+ (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0)));
+[ Reflexivity
+| Simpl; Intros; Rewrite H0; Reflexivity
+| Simpl; Intros; Rewrite H0; Reflexivity ].
+Save.
+
+Theorem polynomial_simplify_ok : (p:polynomial)
+ (interp_cs Aplus Amult Aone Azero vm (polynomial_simplify p))
+ ==(interp_p p).
+Intro.
+Unfold polynomial_simplify.
+Rewrite spolynomial_of_ok.
+Rewrite polynomial_normalize_ok.
+Rewrite (canonical_sum_simplify_ok A Aplus Amult Aone Azero Aeq vm T).
+Rewrite (spolynomial_normalize_ok A Aplus Amult Aone Azero Aeq vm T).
+Reflexivity.
+Save.
+
+End rings.
+
+V8Infix "+" Pplus : ring_scope.
+V8Infix "*" Pmult : ring_scope.
+V8Notation "- x" := (Popp x) : ring_scope.
+V8Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope.
+
+Delimits Scope ring_scope with ring.
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-15 10:22:25 +0000