diff options
Diffstat (limited to 'contrib7/ring/Ring_normalize.v')
| -rw-r--r-- | contrib7/ring/Ring_normalize.v | 893 |
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. |