summaryrefslogtreecommitdiff
path: root/contrib7/ring/Setoid_ring_normalize.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib7/ring/Setoid_ring_normalize.v')
-rw-r--r--contrib7/ring/Setoid_ring_normalize.v1141
1 files changed, 1141 insertions, 0 deletions
diff --git a/contrib7/ring/Setoid_ring_normalize.v b/contrib7/ring/Setoid_ring_normalize.v
new file mode 100644
index 00000000..b6b79dae
--- /dev/null
+++ b/contrib7/ring/Setoid_ring_normalize.v
@@ -0,0 +1,1141 @@
+(************************************************************************)
+(* 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: Setoid_ring_normalize.v,v 1.1.2.1 2004/07/16 19:30:19 herbelin Exp $ *)
+
+Require Setoid_ring_theory.
+Require Quote.
+
+Set Implicit Arguments.
+
+Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m.
+Proof.
+ Induction n; Induction m; Simpl; Try (Reflexivity Orelse Contradiction).
+ Intros; Rewrite (H i0); Trivial.
+ Intros; Rewrite (H i0); Trivial.
+Save.
+
+Section setoid.
+
+Variable A : Type.
+Variable Aequiv : A -> A -> Prop.
+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 S : (Setoid_Theory A Aequiv).
+
+Add Setoid A Aequiv S.
+
+Variable plus_morph : (a,a0,a1,a2:A)
+ (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Aplus a a1) (Aplus a0 a2)).
+Variable mult_morph : (a,a0,a1,a2:A)
+ (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Amult a a1) (Amult a0 a2)).
+Variable opp_morph : (a,a0:A)
+ (Aequiv a a0)->(Aequiv (Aopp a) (Aopp a0)).
+
+Add Morphism Aplus : Aplus_ext.
+Exact plus_morph.
+Save.
+
+Add Morphism Amult : Amult_ext.
+Exact mult_morph.
+Save.
+
+Add Morphism Aopp : Aopp_ext.
+Exact opp_morph.
+Save.
+
+Local equiv_refl := (Seq_refl A Aequiv S).
+Local equiv_sym := (Seq_sym A Aequiv S).
+Local equiv_trans := (Seq_trans A Aequiv S).
+
+Hints Resolve equiv_refl equiv_trans.
+Hints Immediate equiv_sym.
+
+Section semi_setoid_rings.
+
+(* 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-setoid-ring polynomials *)
+
+Inductive Type setspolynomial :=
+ SetSPvar : index -> setspolynomial
+| SetSPconst : A -> setspolynomial
+| SetSPplus : setspolynomial -> setspolynomial -> setspolynomial
+| SetSPmult : setspolynomial -> setspolynomial -> setspolynomial.
+
+Fixpoint setspolynomial_normalize [p:setspolynomial] : canonical_sum :=
+ Cases p of
+ | (SetSPplus l r) => (canonical_sum_merge (setspolynomial_normalize l) (setspolynomial_normalize r))
+ | (SetSPmult l r) => (canonical_sum_prod (setspolynomial_normalize l) (setspolynomial_normalize r))
+ | (SetSPconst c) => (Cons_monom c Nil_var Nil_monom)
+ | (SetSPvar i) => (Cons_varlist (Cons_var i Nil_var) Nil_monom)
+ end.
+
+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 setspolynomial_simplify :=
+ [x:setspolynomial] (canonical_sum_simplify (setspolynomial_normalize x)).
+
+Variable vm : (varmap A).
+
+Definition interp_var [i:index] := (varmap_find Azero i vm).
+
+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.
+
+Definition interp_m := [c:A][l:varlist]
+ Cases l of
+ | Nil_var => c
+ | (Cons_var x t) =>
+ (Amult c (ivl_aux x t))
+ end.
+
+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}.
+
+Definition interp_setcs : 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_setsp [p:setspolynomial] : A :=
+ Cases p of
+ | (SetSPconst c) => c
+ | (SetSPvar i) => (interp_var i)
+ | (SetSPplus p1 p2) => (Aplus (interp_setsp p1) (interp_setsp p2))
+ | (SetSPmult p1 p2) => (Amult (interp_setsp p1) (interp_setsp p2))
+ end.
+
+(* End interpretation. *)
+
+Unset Implicit Arguments.
+
+(* Section properties. *)
+
+Variable T : (Semi_Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aeq).
+
+Hint SSR_plus_sym_T := Resolve (SSR_plus_sym T).
+Hint SSR_plus_assoc_T := Resolve (SSR_plus_assoc T).
+Hint SSR_plus_assoc2_T := Resolve (SSR_plus_assoc2 S T).
+Hint SSR_mult_sym_T := Resolve (SSR_mult_sym T).
+Hint SSR_mult_assoc_T := Resolve (SSR_mult_assoc T).
+Hint SSR_mult_assoc2_T := Resolve (SSR_mult_assoc2 S T).
+Hint SSR_plus_zero_left_T := Resolve (SSR_plus_zero_left T).
+Hint SSR_plus_zero_left2_T := Resolve (SSR_plus_zero_left2 S T).
+Hint SSR_mult_one_left_T := Resolve (SSR_mult_one_left T).
+Hint SSR_mult_one_left2_T := Resolve (SSR_mult_one_left2 S T).
+Hint SSR_mult_zero_left_T := Resolve (SSR_mult_zero_left T).
+Hint SSR_mult_zero_left2_T := Resolve (SSR_mult_zero_left2 S T).
+Hint SSR_distr_left_T := Resolve (SSR_distr_left T).
+Hint SSR_distr_left2_T := Resolve (SSR_distr_left2 S T).
+Hint SSR_plus_reg_left_T := Resolve (SSR_plus_reg_left T).
+Hint SSR_plus_permute_T := Resolve (SSR_plus_permute S plus_morph T).
+Hint SSR_mult_permute_T := Resolve (SSR_mult_permute S mult_morph T).
+Hint SSR_distr_right_T := Resolve (SSR_distr_right S plus_morph T).
+Hint SSR_distr_right2_T := Resolve (SSR_distr_right2 S plus_morph T).
+Hint SSR_mult_zero_right_T := Resolve (SSR_mult_zero_right S T).
+Hint SSR_mult_zero_right2_T := Resolve (SSR_mult_zero_right2 S T).
+Hint SSR_plus_zero_right_T := Resolve (SSR_plus_zero_right S T).
+Hint SSR_plus_zero_right2_T := Resolve (SSR_plus_zero_right2 S T).
+Hint SSR_mult_one_right_T := Resolve (SSR_mult_one_right S T).
+Hint SSR_mult_one_right2_T := Resolve (SSR_mult_one_right2 S T).
+Hint SSR_plus_reg_right_T := Resolve (SSR_plus_reg_right S 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)
+ (Aequiv (ivl_aux i v) (Amult (interp_var i) (interp_vl v))).
+Proof.
+ Induction v; Simpl; Intros.
+ Trivial.
+ Rewrite (H i); Trivial.
+Save.
+
+Lemma varlist_merge_ok : (x,y:varlist)
+ (Aequiv (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.
+
+ Rewrite (ivl_aux_ok v i).
+ Rewrite (ivl_aux_ok v0 i0).
+ Rewrite (ivl_aux_ok (varlist_merge v (Cons_var i0 v0)) i).
+ Rewrite (H (Cons_var i0 v0)).
+ Simpl.
+ Rewrite (ivl_aux_ok v0 i0).
+ EAuto.
+
+ Rewrite (ivl_aux_ok v i).
+ Rewrite (ivl_aux_ok v0 i0).
+ Rewrite (ivl_aux_ok
+ (Fix vm_aux
+ {vm_aux [l2:varlist] : varlist :=
+ Cases (l2) of
+ Nil_var => (Cons_var i v)
+ | (Cons_var v2 t2) =>
+ (if (index_lt i v2)
+ then (Cons_var i (varlist_merge v l2))
+ else (Cons_var v2 (vm_aux t2)))
+ end} v0) i0).
+ Rewrite H0.
+ Rewrite (ivl_aux_ok v i).
+ EAuto.
+Save.
+
+Remark ics_aux_ok : (x:A)(s:canonical_sum)
+ (Aequiv (ics_aux x s) (Aplus x (interp_setcs s))).
+Proof.
+ Induction s; Simpl; Intros;Trivial.
+Save.
+
+Remark interp_m_ok : (x:A)(l:varlist)
+ (Aequiv (interp_m x l) (Amult x (interp_vl l))).
+Proof.
+ NewDestruct l;Trivial.
+Save.
+
+Hint ivl_aux_ok_ := Resolve ivl_aux_ok.
+Hint ics_aux_ok_ := Resolve ics_aux_ok.
+Hint interp_m_ok_ := Resolve interp_m_ok.
+
+(* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *)
+
+Lemma canonical_sum_merge_ok : (x,y:canonical_sum)
+ (Aequiv (interp_setcs (canonical_sum_merge x y))
+ (Aplus (interp_setcs x) (interp_setcs y))).
+Proof.
+Induction x; Simpl.
+Trivial.
+
+Induction y; Simpl; Intros.
+EAuto.
+
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl.
+Rewrite (ics_aux_ok (interp_m a v0) c).
+Rewrite (ics_aux_ok (interp_m a0 v0) c0).
+Rewrite (ics_aux_ok (interp_m (Aplus a a0) v0)
+ (canonical_sum_merge c c0)).
+Rewrite (H c0).
+Rewrite (interp_m_ok (Aplus a a0) v0).
+Rewrite (interp_m_ok a v0).
+Rewrite (interp_m_ok a0 v0).
+Setoid_replace (Amult (Aplus a a0) (interp_vl v0))
+ with (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0))).
+Setoid_replace (Aplus
+ (Aplus (Amult a (interp_vl v0))
+ (Amult a0 (interp_vl v0)))
+ (Aplus (interp_setcs c) (interp_setcs c0)))
+ with (Aplus (Amult a (interp_vl v0))
+ (Aplus (Amult a0 (interp_vl v0))
+ (Aplus (interp_setcs c) (interp_setcs c0)))).
+Setoid_replace (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
+ (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0)))
+ with (Aplus (Amult a (interp_vl v0))
+ (Aplus (interp_setcs c)
+ (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0)))).
+Auto.
+
+Elim (varlist_lt v v0); Simpl.
+Intro.
+Rewrite (ics_aux_ok (interp_m a v)
+ (canonical_sum_merge c (Cons_monom a0 v0 c0))).
+Rewrite (ics_aux_ok (interp_m a v) c).
+Rewrite (ics_aux_ok (interp_m a0 v0) c0).
+Rewrite (H (Cons_monom a0 v0 c0)); Simpl.
+Rewrite (ics_aux_ok (interp_m a0 v0) c0); Auto.
+
+Intro.
+Rewrite (ics_aux_ok (interp_m a0 v0)
+ (Fix csm_aux
+ {csm_aux [s2:canonical_sum] : canonical_sum :=
+ Cases (s2) of
+ Nil_monom => (Cons_monom a v c)
+ | (Cons_monom c2 l2 t2) =>
+ (if (varlist_eq v l2)
+ then
+ (Cons_monom (Aplus a c2) v
+ (canonical_sum_merge c t2))
+ else
+ (if (varlist_lt v l2)
+ then
+ (Cons_monom a v
+ (canonical_sum_merge c s2))
+ else (Cons_monom c2 l2 (csm_aux t2))))
+ | (Cons_varlist l2 t2) =>
+ (if (varlist_eq v l2)
+ then
+ (Cons_monom (Aplus a Aone) v
+ (canonical_sum_merge c t2))
+ else
+ (if (varlist_lt v l2)
+ then
+ (Cons_monom a v
+ (canonical_sum_merge c s2))
+ else (Cons_varlist l2 (csm_aux t2))))
+ end} c0)).
+Rewrite H0.
+Rewrite (ics_aux_ok (interp_m a v) c);
+Rewrite (ics_aux_ok (interp_m a0 v0) c0); Simpl; Auto.
+
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl.
+Rewrite (ics_aux_ok (interp_m (Aplus a Aone) v0)
+ (canonical_sum_merge c c0));
+Rewrite (ics_aux_ok (interp_m a v0) c);
+Rewrite (ics_aux_ok (interp_vl v0) c0).
+Rewrite (H c0).
+Rewrite (interp_m_ok (Aplus a Aone) v0).
+Rewrite (interp_m_ok a v0).
+Setoid_replace (Amult (Aplus a Aone) (interp_vl v0))
+ with (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0))).
+Setoid_replace (Aplus
+ (Aplus (Amult a (interp_vl v0))
+ (Amult Aone (interp_vl v0)))
+ (Aplus (interp_setcs c) (interp_setcs c0)))
+ with (Aplus (Amult a (interp_vl v0))
+ (Aplus (Amult Aone (interp_vl v0))
+ (Aplus (interp_setcs c) (interp_setcs c0)))).
+Setoid_replace (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
+ (Aplus (interp_vl v0) (interp_setcs c0)))
+ with (Aplus (Amult a (interp_vl v0))
+ (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))).
+Setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0).
+Auto.
+
+Elim (varlist_lt v v0); Simpl.
+Intro.
+Rewrite (ics_aux_ok (interp_m a v)
+ (canonical_sum_merge c (Cons_varlist v0 c0)));
+Rewrite (ics_aux_ok (interp_m a v) c);
+Rewrite (ics_aux_ok (interp_vl v0) c0).
+Rewrite (H (Cons_varlist v0 c0)); Simpl.
+Rewrite (ics_aux_ok (interp_vl v0) c0).
+Auto.
+
+Intro.
+Rewrite (ics_aux_ok (interp_vl v0)
+ (Fix csm_aux
+ {csm_aux [s2:canonical_sum] : canonical_sum :=
+ Cases (s2) of
+ Nil_monom => (Cons_monom a v c)
+ | (Cons_monom c2 l2 t2) =>
+ (if (varlist_eq v l2)
+ then
+ (Cons_monom (Aplus a c2) v
+ (canonical_sum_merge c t2))
+ else
+ (if (varlist_lt v l2)
+ then
+ (Cons_monom a v
+ (canonical_sum_merge c s2))
+ else (Cons_monom c2 l2 (csm_aux t2))))
+ | (Cons_varlist l2 t2) =>
+ (if (varlist_eq v l2)
+ then
+ (Cons_monom (Aplus a Aone) v
+ (canonical_sum_merge c t2))
+ else
+ (if (varlist_lt v l2)
+ then
+ (Cons_monom a v
+ (canonical_sum_merge c s2))
+ else (Cons_varlist l2 (csm_aux t2))))
+ end} c0)); Rewrite H0.
+Rewrite (ics_aux_ok (interp_m a v) c);
+Rewrite (ics_aux_ok (interp_vl v0) c0); Simpl.
+Auto.
+
+Induction y; Simpl; Intros.
+Trivial.
+
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl.
+Rewrite (ics_aux_ok (interp_m (Aplus Aone a) v0)
+ (canonical_sum_merge c c0));
+Rewrite (ics_aux_ok (interp_vl v0) c);
+Rewrite (ics_aux_ok (interp_m a v0) c0); Rewrite (
+H c0).
+Rewrite (interp_m_ok (Aplus Aone a) v0);
+Rewrite (interp_m_ok a v0).
+Setoid_replace (Amult (Aplus Aone a) (interp_vl v0))
+ with (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)));
+Setoid_replace (Aplus
+ (Aplus (Amult Aone (interp_vl v0))
+ (Amult a (interp_vl v0)))
+ (Aplus (interp_setcs c) (interp_setcs c0)))
+ with (Aplus (Amult Aone (interp_vl v0))
+ (Aplus (Amult a (interp_vl v0))
+ (Aplus (interp_setcs c) (interp_setcs c0))));
+Setoid_replace (Aplus (Aplus (interp_vl v0) (interp_setcs c))
+ (Aplus (Amult a (interp_vl v0)) (interp_setcs c0)))
+ with (Aplus (interp_vl v0)
+ (Aplus (interp_setcs c)
+ (Aplus (Amult a (interp_vl v0)) (interp_setcs c0)))).
+Auto.
+
+Elim (varlist_lt v v0); Simpl; Intros.
+Rewrite (ics_aux_ok (interp_vl v)
+ (canonical_sum_merge c (Cons_monom a v0 c0)));
+Rewrite (ics_aux_ok (interp_vl v) c);
+Rewrite (ics_aux_ok (interp_m a v0) c0).
+Rewrite (H (Cons_monom a v0 c0)); Simpl.
+Rewrite (ics_aux_ok (interp_m a v0) c0); Auto.
+
+Rewrite (ics_aux_ok (interp_m a v0)
+ (Fix csm_aux2
+ {csm_aux2 [s2:canonical_sum] : canonical_sum :=
+ Cases (s2) of
+ Nil_monom => (Cons_varlist v c)
+ | (Cons_monom c2 l2 t2) =>
+ (if (varlist_eq v l2)
+ then
+ (Cons_monom (Aplus Aone c2) v
+ (canonical_sum_merge c t2))
+ else
+ (if (varlist_lt v l2)
+ then
+ (Cons_varlist v
+ (canonical_sum_merge c s2))
+ else (Cons_monom c2 l2 (csm_aux2 t2))))
+ | (Cons_varlist l2 t2) =>
+ (if (varlist_eq v l2)
+ then
+ (Cons_monom (Aplus Aone Aone) v
+ (canonical_sum_merge c t2))
+ else
+ (if (varlist_lt v l2)
+ then
+ (Cons_varlist v
+ (canonical_sum_merge c s2))
+ else (Cons_varlist l2 (csm_aux2 t2))))
+ end} c0)); Rewrite H0.
+Rewrite (ics_aux_ok (interp_vl v) c);
+Rewrite (ics_aux_ok (interp_m a v0) c0); Simpl; Auto.
+
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0); Intros.
+Rewrite (H1 I); Simpl.
+Rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v0)
+ (canonical_sum_merge c c0));
+Rewrite (ics_aux_ok (interp_vl v0) c);
+Rewrite (ics_aux_ok (interp_vl v0) c0); Rewrite (
+H c0).
+Rewrite (interp_m_ok (Aplus Aone Aone) v0).
+Setoid_replace (Amult (Aplus Aone Aone) (interp_vl v0))
+ with (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)));
+Setoid_replace (Aplus
+ (Aplus (Amult Aone (interp_vl v0))
+ (Amult Aone (interp_vl v0)))
+ (Aplus (interp_setcs c) (interp_setcs c0)))
+ with (Aplus (Amult Aone (interp_vl v0))
+ (Aplus (Amult Aone (interp_vl v0))
+ (Aplus (interp_setcs c) (interp_setcs c0))));
+Setoid_replace (Aplus (Aplus (interp_vl v0) (interp_setcs c))
+ (Aplus (interp_vl v0) (interp_setcs c0)))
+ with (Aplus (interp_vl v0)
+ (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0)))).
+Setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); Auto.
+
+Elim (varlist_lt v v0); Simpl.
+Rewrite (ics_aux_ok (interp_vl v)
+ (canonical_sum_merge c (Cons_varlist v0 c0)));
+Rewrite (ics_aux_ok (interp_vl v) c);
+Rewrite (ics_aux_ok (interp_vl v0) c0);
+Rewrite (H (Cons_varlist v0 c0)); Simpl.
+Rewrite (ics_aux_ok (interp_vl v0) c0); Auto.
+
+Rewrite (ics_aux_ok (interp_vl v0)
+ (Fix csm_aux2
+ {csm_aux2 [s2:canonical_sum] : canonical_sum :=
+ Cases (s2) of
+ Nil_monom => (Cons_varlist v c)
+ | (Cons_monom c2 l2 t2) =>
+ (if (varlist_eq v l2)
+ then
+ (Cons_monom (Aplus Aone c2) v
+ (canonical_sum_merge c t2))
+ else
+ (if (varlist_lt v l2)
+ then
+ (Cons_varlist v
+ (canonical_sum_merge c s2))
+ else (Cons_monom c2 l2 (csm_aux2 t2))))
+ | (Cons_varlist l2 t2) =>
+ (if (varlist_eq v l2)
+ then
+ (Cons_monom (Aplus Aone Aone) v
+ (canonical_sum_merge c t2))
+ else
+ (if (varlist_lt v l2)
+ then
+ (Cons_varlist v
+ (canonical_sum_merge c s2))
+ else (Cons_varlist l2 (csm_aux2 t2))))
+ end} c0)); Rewrite H0.
+Rewrite (ics_aux_ok (interp_vl v) c);
+Rewrite (ics_aux_ok (interp_vl v0) c0); Simpl; Auto.
+Save.
+
+Lemma monom_insert_ok: (a:A)(l:varlist)(s:canonical_sum)
+ (Aequiv (interp_setcs (monom_insert a l s))
+ (Aplus (Amult a (interp_vl l)) (interp_setcs s))).
+Proof.
+Induction s; Intros.
+Simpl; Rewrite (interp_m_ok a l); Trivial.
+
+Simpl; Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl.
+Rewrite (ics_aux_ok (interp_m (Aplus a a0) v) c);
+Rewrite (ics_aux_ok (interp_m a0 v) c).
+Rewrite (interp_m_ok (Aplus a a0) v);
+Rewrite (interp_m_ok a0 v).
+Setoid_replace (Amult (Aplus a a0) (interp_vl v))
+ with (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v))).
+Auto.
+
+Elim (varlist_lt l v); Simpl; Intros.
+Rewrite (ics_aux_ok (interp_m a0 v) c).
+Rewrite (interp_m_ok a0 v); Rewrite (interp_m_ok a l).
+Auto.
+
+Rewrite (ics_aux_ok (interp_m a0 v) (monom_insert a l c));
+Rewrite (ics_aux_ok (interp_m a0 v) c); Rewrite H.
+Auto.
+
+Simpl.
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl.
+Rewrite (ics_aux_ok (interp_m (Aplus a Aone) v) c);
+Rewrite (ics_aux_ok (interp_vl v) c).
+Rewrite (interp_m_ok (Aplus a Aone) v).
+Setoid_replace (Amult (Aplus a Aone) (interp_vl v))
+ with (Aplus (Amult a (interp_vl v)) (Amult Aone (interp_vl v))).
+Setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v).
+Auto.
+
+Elim (varlist_lt l v); Simpl; Intros; Auto.
+Rewrite (ics_aux_ok (interp_vl v) (monom_insert a l c));
+Rewrite H.
+Rewrite (ics_aux_ok (interp_vl v) c); Auto.
+Save.
+
+Lemma varlist_insert_ok :
+ (l:varlist)(s:canonical_sum)
+ (Aequiv (interp_setcs (varlist_insert l s))
+ (Aplus (interp_vl l) (interp_setcs s))).
+Proof.
+Induction s; Simpl; Intros.
+Trivial.
+
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl.
+Rewrite (ics_aux_ok (interp_m (Aplus Aone a) v) c);
+Rewrite (ics_aux_ok (interp_m a v) c).
+Rewrite (interp_m_ok (Aplus Aone a) v);
+Rewrite (interp_m_ok a v).
+Setoid_replace (Amult (Aplus Aone a) (interp_vl v))
+ with (Aplus (Amult Aone (interp_vl v)) (Amult a (interp_vl v))).
+Setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); Auto.
+
+Elim (varlist_lt l v); Simpl; Intros; Auto.
+Rewrite (ics_aux_ok (interp_m a v) (varlist_insert l c));
+Rewrite (ics_aux_ok (interp_m a v) c).
+Rewrite (interp_m_ok a v).
+Rewrite H; Auto.
+
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl.
+Rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v) c);
+Rewrite (ics_aux_ok (interp_vl v) c).
+Rewrite (interp_m_ok (Aplus Aone Aone) v).
+Setoid_replace (Amult (Aplus Aone Aone) (interp_vl v))
+ with (Aplus (Amult Aone (interp_vl v)) (Amult Aone (interp_vl v))).
+Setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); Auto.
+
+Elim (varlist_lt l v); Simpl; Intros; Auto.
+Rewrite (ics_aux_ok (interp_vl v) (varlist_insert l c)).
+Rewrite H.
+Rewrite (ics_aux_ok (interp_vl v) c); Auto.
+Save.
+
+Lemma canonical_sum_scalar_ok : (a:A)(s:canonical_sum)
+ (Aequiv (interp_setcs (canonical_sum_scalar a s)) (Amult a (interp_setcs s))).
+Proof.
+Induction s; Simpl; Intros.
+Trivial.
+
+Rewrite (ics_aux_ok (interp_m (Amult a a0) v)
+ (canonical_sum_scalar a c));
+Rewrite (ics_aux_ok (interp_m a0 v) c).
+Rewrite (interp_m_ok (Amult a a0) v);
+Rewrite (interp_m_ok a0 v).
+Rewrite H.
+Setoid_replace (Amult a (Aplus (Amult a0 (interp_vl v)) (interp_setcs c)))
+ with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_setcs c))).
+Auto.
+
+Rewrite (ics_aux_ok (interp_m a v) (canonical_sum_scalar a c));
+Rewrite (ics_aux_ok (interp_vl v) c); Rewrite H.
+Rewrite (interp_m_ok a v).
+Auto.
+Save.
+
+Lemma canonical_sum_scalar2_ok : (l:varlist; s:canonical_sum)
+ (Aequiv (interp_setcs (canonical_sum_scalar2 l s)) (Amult (interp_vl l) (interp_setcs s))).
+Proof.
+Induction s; Simpl; Intros; Auto.
+Rewrite (monom_insert_ok a (varlist_merge l v)
+ (canonical_sum_scalar2 l c)).
+Rewrite (ics_aux_ok (interp_m a v) c).
+Rewrite (interp_m_ok a v).
+Rewrite H.
+Rewrite (varlist_merge_ok l v).
+Setoid_replace (Amult (interp_vl l)
+ (Aplus (Amult a (interp_vl v)) (interp_setcs c)))
+ with (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
+ (Amult (interp_vl l) (interp_setcs c))).
+Auto.
+
+Rewrite (varlist_insert_ok (varlist_merge l v)
+ (canonical_sum_scalar2 l c)).
+Rewrite (ics_aux_ok (interp_vl v) c).
+Rewrite H.
+Rewrite (varlist_merge_ok l v).
+Auto.
+Save.
+
+Lemma canonical_sum_scalar3_ok : (c:A; l:varlist; s:canonical_sum)
+ (Aequiv (interp_setcs (canonical_sum_scalar3 c l s)) (Amult c (Amult (interp_vl l) (interp_setcs s)))).
+Proof.
+Induction s; Simpl; Intros.
+Rewrite (SSR_mult_zero_right S T (interp_vl l)).
+Auto.
+
+Rewrite (monom_insert_ok (Amult c a) (varlist_merge l v)
+ (canonical_sum_scalar3 c l c0)).
+Rewrite (ics_aux_ok (interp_m a v) c0).
+Rewrite (interp_m_ok a v).
+Rewrite H.
+Rewrite (varlist_merge_ok l v).
+Setoid_replace (Amult (interp_vl l)
+ (Aplus (Amult a (interp_vl v)) (interp_setcs c0)))
+ with (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
+ (Amult (interp_vl l) (interp_setcs c0))).
+Setoid_replace (Amult c
+ (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
+ (Amult (interp_vl l) (interp_setcs c0))))
+ with (Aplus (Amult c (Amult (interp_vl l) (Amult a (interp_vl v))))
+ (Amult c (Amult (interp_vl l) (interp_setcs c0)))).
+Setoid_replace (Amult (Amult c a) (Amult (interp_vl l) (interp_vl v)))
+ with (Amult c (Amult a (Amult (interp_vl l) (interp_vl v)))).
+Auto.
+
+Rewrite (monom_insert_ok c (varlist_merge l v)
+ (canonical_sum_scalar3 c l c0)).
+Rewrite (ics_aux_ok (interp_vl v) c0).
+Rewrite H.
+Rewrite (varlist_merge_ok l v).
+Setoid_replace (Aplus (Amult c (Amult (interp_vl l) (interp_vl v)))
+ (Amult c (Amult (interp_vl l) (interp_setcs c0))))
+ with (Amult c
+ (Aplus (Amult (interp_vl l) (interp_vl v))
+ (Amult (interp_vl l) (interp_setcs c0)))).
+Auto.
+Save.
+
+Lemma canonical_sum_prod_ok : (x,y:canonical_sum)
+ (Aequiv (interp_setcs (canonical_sum_prod x y)) (Amult (interp_setcs x) (interp_setcs y))).
+Proof.
+Induction x; Simpl; Intros.
+Trivial.
+
+Rewrite (canonical_sum_merge_ok (canonical_sum_scalar3 a v y)
+ (canonical_sum_prod c y)).
+Rewrite (canonical_sum_scalar3_ok a v y).
+Rewrite (ics_aux_ok (interp_m a v) c).
+Rewrite (interp_m_ok a v).
+Rewrite (H y).
+Setoid_replace (Amult a (Amult (interp_vl v) (interp_setcs y)))
+ with (Amult (Amult a (interp_vl v)) (interp_setcs y)).
+Setoid_replace (Amult (Aplus (Amult a (interp_vl v)) (interp_setcs c))
+ (interp_setcs y))
+ with (Aplus (Amult (Amult a (interp_vl v)) (interp_setcs y))
+ (Amult (interp_setcs c) (interp_setcs y))).
+Trivial.
+
+Rewrite (canonical_sum_merge_ok (canonical_sum_scalar2 v y)
+ (canonical_sum_prod c y)).
+Rewrite (canonical_sum_scalar2_ok v y).
+Rewrite (ics_aux_ok (interp_vl v) c).
+Rewrite (H y).
+Trivial.
+Save.
+
+Theorem setspolynomial_normalize_ok : (p:setspolynomial)
+ (Aequiv (interp_setcs (setspolynomial_normalize p)) (interp_setsp p)).
+Proof.
+Induction p; Simpl; Intros; Trivial.
+Rewrite (canonical_sum_merge_ok (setspolynomial_normalize s)
+ (setspolynomial_normalize s0)).
+Rewrite H; Rewrite H0; Trivial.
+
+Rewrite (canonical_sum_prod_ok (setspolynomial_normalize s)
+ (setspolynomial_normalize s0)).
+Rewrite H; Rewrite H0; Trivial.
+Save.
+
+Lemma canonical_sum_simplify_ok : (s:canonical_sum)
+ (Aequiv (interp_setcs (canonical_sum_simplify s)) (interp_setcs s)).
+Proof.
+Induction s; Simpl; Intros.
+Trivial.
+
+Generalize (SSR_eq_prop T 9!a 10!Azero).
+Elim (Aeq a Azero).
+Simpl.
+Intros.
+Rewrite (ics_aux_ok (interp_m a v) c).
+Rewrite (interp_m_ok a v).
+Rewrite (H0 I).
+Setoid_replace (Amult Azero (interp_vl v)) with Azero.
+Rewrite H.
+Trivial.
+
+Intros; Simpl.
+Generalize (SSR_eq_prop T 9!a 10!Aone).
+Elim (Aeq a Aone).
+Intros.
+Rewrite (ics_aux_ok (interp_m a v) c).
+Rewrite (interp_m_ok a v).
+Rewrite (H1 I).
+Simpl.
+Rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)).
+Rewrite H.
+Auto.
+
+Simpl.
+Intros.
+Rewrite (ics_aux_ok (interp_m a v) (canonical_sum_simplify c)).
+Rewrite (ics_aux_ok (interp_m a v) c).
+Rewrite H; Trivial.
+
+Rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)).
+Rewrite H.
+Auto.
+Save.
+
+Theorem setspolynomial_simplify_ok : (p:setspolynomial)
+ (Aequiv (interp_setcs (setspolynomial_simplify p)) (interp_setsp p)).
+Proof.
+Intro.
+Unfold setspolynomial_simplify.
+Rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)).
+Exact (setspolynomial_normalize_ok p).
+Save.
+
+End semi_setoid_rings.
+
+Implicits Cons_varlist.
+Implicits Cons_monom.
+Implicits SetSPconst.
+Implicits SetSPplus.
+Implicits SetSPmult.
+
+
+
+Section setoid_rings.
+
+Set Implicit Arguments.
+
+Variable vm : (varmap A).
+Variable T : (Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq).
+
+Hint STh_plus_sym_T := Resolve (STh_plus_sym T).
+Hint STh_plus_assoc_T := Resolve (STh_plus_assoc T).
+Hint STh_plus_assoc2_T := Resolve (STh_plus_assoc2 S T).
+Hint STh_mult_sym_T := Resolve (STh_mult_sym T).
+Hint STh_mult_assoc_T := Resolve (STh_mult_assoc T).
+Hint STh_mult_assoc2_T := Resolve (STh_mult_assoc2 S T).
+Hint STh_plus_zero_left_T := Resolve (STh_plus_zero_left T).
+Hint STh_plus_zero_left2_T := Resolve (STh_plus_zero_left2 S T).
+Hint STh_mult_one_left_T := Resolve (STh_mult_one_left T).
+Hint STh_mult_one_left2_T := Resolve (STh_mult_one_left2 S T).
+Hint STh_mult_zero_left_T := Resolve (STh_mult_zero_left S plus_morph mult_morph T).
+Hint STh_mult_zero_left2_T := Resolve (STh_mult_zero_left2 S plus_morph mult_morph T).
+Hint STh_distr_left_T := Resolve (STh_distr_left T).
+Hint STh_distr_left2_T := Resolve (STh_distr_left2 S T).
+Hint STh_plus_reg_left_T := Resolve (STh_plus_reg_left S plus_morph T).
+Hint STh_plus_permute_T := Resolve (STh_plus_permute S plus_morph T).
+Hint STh_mult_permute_T := Resolve (STh_mult_permute S mult_morph T).
+Hint STh_distr_right_T := Resolve (STh_distr_right S plus_morph T).
+Hint STh_distr_right2_T := Resolve (STh_distr_right2 S plus_morph T).
+Hint STh_mult_zero_right_T := Resolve (STh_mult_zero_right S plus_morph mult_morph T).
+Hint STh_mult_zero_right2_T := Resolve (STh_mult_zero_right2 S plus_morph mult_morph T).
+Hint STh_plus_zero_right_T := Resolve (STh_plus_zero_right S T).
+Hint STh_plus_zero_right2_T := Resolve (STh_plus_zero_right2 S T).
+Hint STh_mult_one_right_T := Resolve (STh_mult_one_right S T).
+Hint STh_mult_one_right2_T := Resolve (STh_mult_one_right2 S T).
+Hint STh_plus_reg_right_T := Resolve (STh_plus_reg_right S plus_morph T).
+Hints Resolve refl_equal sym_equal trans_equal.
+(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hints Immediate T.
+
+
+(*** Definitions *)
+
+Inductive Type setpolynomial :=
+ SetPvar : index -> setpolynomial
+| SetPconst : A -> setpolynomial
+| SetPplus : setpolynomial -> setpolynomial -> setpolynomial
+| SetPmult : setpolynomial -> setpolynomial -> setpolynomial
+| SetPopp : setpolynomial -> setpolynomial.
+
+Fixpoint setpolynomial_normalize [x:setpolynomial] : canonical_sum :=
+ Cases x of
+ | (SetPplus l r) => (canonical_sum_merge
+ (setpolynomial_normalize l)
+ (setpolynomial_normalize r))
+ | (SetPmult l r) => (canonical_sum_prod
+ (setpolynomial_normalize l)
+ (setpolynomial_normalize r))
+ | (SetPconst c) => (Cons_monom c Nil_var Nil_monom)
+ | (SetPvar i) => (Cons_varlist (Cons_var i Nil_var) Nil_monom)
+ | (SetPopp p) => (canonical_sum_scalar3
+ (Aopp Aone) Nil_var
+ (setpolynomial_normalize p))
+ end.
+
+Definition setpolynomial_simplify :=
+ [x:setpolynomial](canonical_sum_simplify (setpolynomial_normalize x)).
+
+Fixpoint setspolynomial_of [x:setpolynomial] : setspolynomial :=
+ Cases x of
+ | (SetPplus l r) => (SetSPplus (setspolynomial_of l) (setspolynomial_of r))
+ | (SetPmult l r) => (SetSPmult (setspolynomial_of l) (setspolynomial_of r))
+ | (SetPconst c) => (SetSPconst c)
+ | (SetPvar i) => (SetSPvar i)
+ | (SetPopp p) => (SetSPmult (SetSPconst (Aopp Aone)) (setspolynomial_of p))
+ end.
+
+(*** Interpretation *)
+
+Fixpoint interp_setp [p:setpolynomial] : A :=
+ Cases p of
+ | (SetPconst c) => c
+ | (SetPvar i) => (varmap_find Azero i vm)
+ | (SetPplus p1 p2) => (Aplus (interp_setp p1) (interp_setp p2))
+ | (SetPmult p1 p2) => (Amult (interp_setp p1) (interp_setp p2))
+ | (SetPopp p1) => (Aopp (interp_setp p1))
+ end.
+
+(*** Properties *)
+
+Unset Implicit Arguments.
+
+Lemma setspolynomial_of_ok : (p:setpolynomial)
+ (Aequiv (interp_setp p) (interp_setsp vm (setspolynomial_of p))).
+Induction p; Trivial; Simpl; Intros.
+Rewrite H; Rewrite H0; Trivial.
+Rewrite H; Rewrite H0; Trivial.
+Rewrite H.
+Rewrite (STh_opp_mult_left2 S plus_morph mult_morph T Aone
+ (interp_setsp vm (setspolynomial_of s))).
+Rewrite (STh_mult_one_left T
+ (interp_setsp vm (setspolynomial_of s))).
+Trivial.
+Save.
+
+Theorem setpolynomial_normalize_ok : (p:setpolynomial)
+ (setpolynomial_normalize p)
+ ==(setspolynomial_normalize (setspolynomial_of p)).
+Induction p; Trivial; Simpl; Intros.
+Rewrite H; Rewrite H0; Reflexivity.
+Rewrite H; Rewrite H0; Reflexivity.
+Rewrite H; Simpl.
+Elim (canonical_sum_scalar3 (Aopp Aone) Nil_var
+ (setspolynomial_normalize (setspolynomial_of s)));
+ [ Reflexivity
+ | Simpl; Intros; Rewrite H0; Reflexivity
+ | Simpl; Intros; Rewrite H0; Reflexivity ].
+Save.
+
+Theorem setpolynomial_simplify_ok : (p:setpolynomial)
+ (Aequiv (interp_setcs vm (setpolynomial_simplify p)) (interp_setp p)).
+Intro.
+Unfold setpolynomial_simplify.
+Rewrite (setspolynomial_of_ok p).
+Rewrite setpolynomial_normalize_ok.
+Rewrite (canonical_sum_simplify_ok vm
+ (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp
+ Aeq plus_morph mult_morph T)
+ (setspolynomial_normalize (setspolynomial_of p))).
+Rewrite (setspolynomial_normalize_ok vm
+ (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp
+ Aeq plus_morph mult_morph T) (setspolynomial_of p)).
+Trivial.
+Save.
+
+End setoid_rings.
+
+End setoid.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 01:43:53 +0000