diff options
Diffstat (limited to 'plugins/ring/Ring_normalize.v')
| -rw-r--r-- | plugins/ring/Ring_normalize.v | 897 |
1 files changed, 0 insertions, 897 deletions
diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v deleted file mode 100644 index 6306c4a7..00000000 --- a/plugins/ring/Ring_normalize.v +++ /dev/null @@ -1,897 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import LegacyRing_theory. -Require Import Quote. - -Set Implicit Arguments. - -Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. -Proof. - intros. - apply index_eq_prop. - generalize H. - case (index_eq n m); simpl; trivial; intros. - contradiction. -Qed. - -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) {struct y} : bool := - match x, y with - | 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) {struct y} : bool := - match x, y with - | 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 := - match l1 with - | Cons_var v1 t1 => - (fix vm_aux (l2:varlist) : varlist := - match l2 with - | 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 => fun l2 => l2 - end. - -(* returns the sum of two canonical sums *) -Fixpoint canonical_sum_merge (s1:canonical_sum) : - canonical_sum -> canonical_sum := - match s1 with - | Cons_monom c1 l1 t1 => - (fix csm_aux (s2:canonical_sum) : canonical_sum := - match s2 with - | 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 (s2:canonical_sum) : canonical_sum := - match s2 with - | 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 => fun s2 => s2 - end. - -(* Insertion of a monom in a canonical sum *) -Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} : - canonical_sum := - match s2 with - | 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) {struct s2} : - canonical_sum := - match s2 with - | 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) {struct s} : - canonical_sum := - match s with - | 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) {struct s} : - canonical_sum := - match s with - | 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) {struct s} : canonical_sum := - match s with - | 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 s2:canonical_sum) {struct s1} : - canonical_sum := - match s1 with - | 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 spolynomial : Type := - | SPvar : index -> spolynomial - | SPconst : A -> spolynomial - | SPplus : spolynomial -> spolynomial -> spolynomial - | SPmult : spolynomial -> spolynomial -> spolynomial. - -Fixpoint spolynomial_normalize (p:spolynomial) : canonical_sum := - match p with - | 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 := - match s with - | 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 (x:index) (t:varlist) {struct t} : A := - match t with - | Nil_var => interp_var x - | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t') - end). - -Definition interp_vl (l:varlist) := - match l with - | Nil_var => Aone - | Cons_var x t => ivl_aux x t - end. - -(* Local *) Definition interp_m (c:A) (l:varlist) := - match l with - | Nil_var => c - | Cons_var x t => Amult c (ivl_aux x t) - end. - -(* Local *) Definition ics_aux := - (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A := - match s with - | 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 (s:canonical_sum) : A := - match s with - | 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 := - match p with - | 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 Resolve (SR_plus_comm T). -Hint Resolve (SR_plus_assoc T). -Hint Resolve (SR_plus_assoc2 T). -Hint Resolve (SR_mult_comm T). -Hint Resolve (SR_mult_assoc T). -Hint Resolve (SR_mult_assoc2 T). -Hint Resolve (SR_plus_zero_left T). -Hint Resolve (SR_plus_zero_left2 T). -Hint Resolve (SR_mult_one_left T). -Hint Resolve (SR_mult_one_left2 T). -Hint Resolve (SR_mult_zero_left T). -Hint Resolve (SR_mult_zero_left2 T). -Hint Resolve (SR_distr_left T). -Hint Resolve (SR_distr_left2 T). -(*Hint Resolve (SR_plus_reg_left T).*) -Hint Resolve (SR_plus_permute T). -Hint Resolve (SR_mult_permute T). -Hint Resolve (SR_distr_right T). -Hint Resolve (SR_distr_right2 T). -Hint Resolve (SR_mult_zero_right T). -Hint Resolve (SR_mult_zero_right2 T). -Hint Resolve (SR_plus_zero_right T). -Hint Resolve (SR_plus_zero_right2 T). -Hint Resolve (SR_mult_one_right T). -Hint Resolve (SR_mult_one_right2 T). -(*Hint Resolve (SR_plus_reg_right T).*) -Hint Resolve eq_refl eq_sym eq_trans. -Hint Immediate T. - -Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y. -Proof. - simple induction x; simple induction y; contradiction || (try reflexivity). - simpl; intros. - generalize (andb_prop2 _ _ H1); intros; elim H2; intros. - rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity. -Qed. - -Remark ivl_aux_ok : - forall (v:varlist) (i:index), - ivl_aux i v = Amult (interp_var i) (interp_vl v). -Proof. - simple induction v; simpl; intros. - trivial. - rewrite H; trivial. -Qed. - -Lemma varlist_merge_ok : - forall x y:varlist, - interp_vl (varlist_merge x y) = Amult (interp_vl x) (interp_vl y). -Proof. - simple induction x. - simpl; trivial. - simple 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. -Qed. - -Remark ics_aux_ok : - forall (x:A) (s:canonical_sum), ics_aux x s = Aplus x (interp_cs s). -Proof. - simple induction s; simpl; intros. - trivial. - reflexivity. - reflexivity. -Qed. - -Remark interp_m_ok : - forall (x:A) (l:varlist), interp_m x l = Amult x (interp_vl l). -Proof. - destruct l as [| i v]. - simpl; trivial. - reflexivity. -Qed. - -Lemma canonical_sum_merge_ok : - forall x y:canonical_sum, - interp_cs (canonical_sum_merge x y) = Aplus (interp_cs x) (interp_cs y). - -simple induction x; simpl. -trivial. - -simple 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 f_equal 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 f_equal 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. - -simple 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 f_equal 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 f_equal 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. -Qed. - -Lemma monom_insert_ok : - forall (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; simple 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 ]. -Qed. - -Lemma varlist_insert_ok : - forall (l:varlist) (s:canonical_sum), - interp_cs (varlist_insert l s) = Aplus (interp_vl l) (interp_cs s). -intros; generalize s; simple 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 ]. -Qed. - -Lemma canonical_sum_scalar_ok : - forall (a:A) (s:canonical_sum), - interp_cs (canonical_sum_scalar a s) = Amult a (interp_cs s). -simple 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. -Qed. - -Lemma canonical_sum_scalar2_ok : - forall (l:varlist) (s:canonical_sum), - interp_cs (canonical_sum_scalar2 l s) = Amult (interp_vl l) (interp_cs s). -simple 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. -Qed. - -Lemma canonical_sum_scalar3_ok : - forall (c:A) (l:varlist) (s:canonical_sum), - interp_cs (canonical_sum_scalar3 c l s) = - Amult c (Amult (interp_vl l) (interp_cs s)). -simple 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. -Qed. - -Lemma canonical_sum_prod_ok : - forall x y:canonical_sum, - interp_cs (canonical_sum_prod x y) = Amult (interp_cs x) (interp_cs y). -simple 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. -Qed. - -Theorem spolynomial_normalize_ok : - forall p:spolynomial, interp_cs (spolynomial_normalize p) = interp_sp p. -simple 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. -Qed. - -Lemma canonical_sum_simplify_ok : - forall s:canonical_sum, interp_cs (canonical_sum_simplify s) = interp_cs s. -simple induction s. - -reflexivity. - -(* cons_monom *) -simpl; intros. -generalize (SR_eq_prop T a 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 a 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. - -Qed. - -Theorem spolynomial_simplify_ok : - forall p:spolynomial, interp_cs (spolynomial_simplify p) = interp_sp p. -intro. -unfold spolynomial_simplify. -rewrite canonical_sum_simplify_ok. -apply spolynomial_normalize_ok. -Qed. - -(* End properties. *) -End semi_rings. - -Arguments Cons_varlist : default implicits. -Arguments Cons_monom : default implicits. -Arguments SPconst : default implicits. -Arguments SPplus : default implicits. -Arguments SPmult : default implicits. - -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 Resolve (Th_plus_comm T). -Hint Resolve (Th_plus_assoc T). -Hint Resolve (Th_plus_assoc2 T). -Hint Resolve (Th_mult_comm T). -Hint Resolve (Th_mult_assoc T). -Hint Resolve (Th_mult_assoc2 T). -Hint Resolve (Th_plus_zero_left T). -Hint Resolve (Th_plus_zero_left2 T). -Hint Resolve (Th_mult_one_left T). -Hint Resolve (Th_mult_one_left2 T). -Hint Resolve (Th_mult_zero_left T). -Hint Resolve (Th_mult_zero_left2 T). -Hint Resolve (Th_distr_left T). -Hint Resolve (Th_distr_left2 T). -(*Hint Resolve (Th_plus_reg_left T).*) -Hint Resolve (Th_plus_permute T). -Hint Resolve (Th_mult_permute T). -Hint Resolve (Th_distr_right T). -Hint Resolve (Th_distr_right2 T). -Hint Resolve (Th_mult_zero_right T). -Hint Resolve (Th_mult_zero_right2 T). -Hint Resolve (Th_plus_zero_right T). -Hint Resolve (Th_plus_zero_right2 T). -Hint Resolve (Th_mult_one_right T). -Hint Resolve (Th_mult_one_right2 T). -(*Hint Resolve (Th_plus_reg_right T).*) -Hint Resolve eq_refl eq_sym eq_trans. -Hint Immediate T. - -(*** Definitions *) - -Inductive polynomial : Type := - | 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 := - match x with - | 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 := - match x with - | 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 := - match p with - | 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 : - forall p:polynomial, - interp_p p = interp_sp Aplus Amult Azero vm (spolynomial_of p). -simple induction p; reflexivity || (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. -Qed. - -Theorem polynomial_normalize_ok : - forall p:polynomial, - polynomial_normalize p = - spolynomial_normalize Aplus Amult Aone (spolynomial_of p). -simple induction p; reflexivity || (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 ]. -Qed. - -Theorem polynomial_simplify_ok : - forall 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. -Qed. - -End rings. - -Infix "+" := Pplus : ring_scope. -Infix "*" := Pmult : ring_scope. -Notation "- x" := (Popp x) : ring_scope. -Notation "[ x ]" := (Pvar x) (at level 0) : ring_scope. - -Delimit Scope ring_scope with ring. |