# Library Coq.ring.Setoid_ring_normalize

Require Import Setoid_ring_theory.
Require Import Quote.
Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
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 as Asetoid.
Variable plus_morph :
forall a a0:A, Aequiv a a0 ->
forall a1 a2:A, Aequiv a1 a2 ->
Aequiv (Aplus a a1) (Aplus a0 a2).
Variable mult_morph :
forall a a0:A, Aequiv a a0 ->
forall a1 a2:A, Aequiv a1 a2 ->
Aequiv (Amult a a1) (Amult a0 a2).
Variable opp_morph : forall a a0:A, Aequiv a a0 -> Aequiv (Aopp a) (Aopp a0).
Add Morphism Aplus : Aplus_ext.
Qed.
Add Morphism Amult : Amult_ext.
Qed.
Add Morphism Aopp : Aopp_ext.
Qed.
Let equiv_refl := Seq_refl A Aequiv S.
Let equiv_sym := Seq_sym A Aequiv S.
Let equiv_trans := Seq_trans A Aequiv S.
Hint Resolve equiv_refl equiv_trans.
Hint Immediate equiv_sym.
Section semi_setoid_rings.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Inductive setspolynomial : Type :=
| SetSPvar : index -> setspolynomial
| SetSPconst : A -> setspolynomial
| SetSPplus : setspolynomial -> setspolynomial -> setspolynomial
| SetSPmult : setspolynomial -> setspolynomial -> setspolynomial.
Fixpoint setspolynomial_normalize (p:setspolynomial) : canonical_sum :=
match p with
| 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 :=
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 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 (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.
Definition interp_m (c:A) (l:varlist) :=
match l with
| Nil_var => c
| Cons_var x t => Amult c (ivl_aux x t)
end.
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).
Definition interp_setcs (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_setsp (p:setspolynomial) : A :=
match p with
| 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.
Variable T : Semi_Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aeq.
Hint Resolve (SSR_plus_comm T).
Hint Resolve (SSR_plus_assoc T).
Hint Resolve (SSR_plus_assoc2 S T).
Hint Resolve (SSR_mult_comm T).
Hint Resolve (SSR_mult_assoc T).
Hint Resolve (SSR_mult_assoc2 S T).
Hint Resolve (SSR_plus_zero_left T).
Hint Resolve (SSR_plus_zero_left2 S T).
Hint Resolve (SSR_mult_one_left T).
Hint Resolve (SSR_mult_one_left2 S T).
Hint Resolve (SSR_mult_zero_left T).
Hint Resolve (SSR_mult_zero_left2 S T).
Hint Resolve (SSR_distr_left T).
Hint Resolve (SSR_distr_left2 S T).
Hint Resolve (SSR_plus_reg_left T).
Hint Resolve (SSR_plus_permute S plus_morph T).
Hint Resolve (SSR_mult_permute S mult_morph T).
Hint Resolve (SSR_distr_right S plus_morph T).
Hint Resolve (SSR_distr_right2 S plus_morph T).
Hint Resolve (SSR_mult_zero_right S T).
Hint Resolve (SSR_mult_zero_right2 S T).
Hint Resolve (SSR_plus_zero_right S T).
Hint Resolve (SSR_plus_zero_right2 S T).
Hint Resolve (SSR_mult_one_right S T).
Hint Resolve (SSR_mult_one_right2 S T).
Hint Resolve (SSR_plus_reg_right S T).
Hint Resolve refl_equal sym_equal trans_equal.
Hint Immediate T.
Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y.
Remark ivl_aux_ok :
forall (v:varlist) (i:index),
Aequiv (ivl_aux i v) (Amult (interp_var i) (interp_vl v)).
Lemma varlist_merge_ok :
forall x y:varlist,
Aequiv (interp_vl (varlist_merge x y)) (Amult (interp_vl x) (interp_vl y)).
Remark ics_aux_ok :
forall (x:A) (s:canonical_sum),
Aequiv (ics_aux x s) (Aplus x (interp_setcs s)).
Remark interp_m_ok :
forall (x:A) (l:varlist), Aequiv (interp_m x l) (Amult x (interp_vl l)).
Hint Resolve ivl_aux_ok.
Hint Resolve ics_aux_ok.
Hint Resolve interp_m_ok.
Lemma canonical_sum_merge_ok :
forall x y:canonical_sum,
Aequiv (interp_setcs (canonical_sum_merge x y))
(Aplus (interp_setcs x) (interp_setcs y)).
Lemma monom_insert_ok :
forall (a:A) (l:varlist) (s:canonical_sum),
Aequiv (interp_setcs (monom_insert a l s))
(Aplus (Amult a (interp_vl l)) (interp_setcs s)).
Lemma varlist_insert_ok :
forall (l:varlist) (s:canonical_sum),
Aequiv (interp_setcs (varlist_insert l s))
(Aplus (interp_vl l) (interp_setcs s)).
Lemma canonical_sum_scalar_ok :
forall (a:A) (s:canonical_sum),
Aequiv (interp_setcs (canonical_sum_scalar a s))
(Amult a (interp_setcs s)).
Lemma canonical_sum_scalar2_ok :
forall (l:varlist) (s:canonical_sum),
Aequiv (interp_setcs (canonical_sum_scalar2 l s))
(Amult (interp_vl l) (interp_setcs s)).
Lemma canonical_sum_scalar3_ok :
forall (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))).
Lemma canonical_sum_prod_ok :
forall x y:canonical_sum,
Aequiv (interp_setcs (canonical_sum_prod x y))
(Amult (interp_setcs x) (interp_setcs y)).
Theorem setspolynomial_normalize_ok :
forall p:setspolynomial,
Aequiv (interp_setcs (setspolynomial_normalize p)) (interp_setsp p).
Lemma canonical_sum_simplify_ok :
forall s:canonical_sum,
Aequiv (interp_setcs (canonical_sum_simplify s)) (interp_setcs s).
Theorem setspolynomial_simplify_ok :
forall p:setspolynomial,
Aequiv (interp_setcs (setspolynomial_simplify p)) (interp_setsp p).
End semi_setoid_rings.
Implicit Arguments Cons_varlist.
Implicit Arguments Cons_monom.
Implicit Arguments SetSPconst.
Implicit Arguments SetSPplus.
Implicit Arguments SetSPmult.
Section setoid_rings.
Variable vm : varmap A.
Variable T : Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq.
Hint Resolve (STh_plus_comm T).
Hint Resolve (STh_plus_assoc T).
Hint Resolve (STh_plus_assoc2 S T).
Hint Resolve (STh_mult_comm T).
Hint Resolve (STh_mult_assoc T).
Hint Resolve (STh_mult_assoc2 S T).
Hint Resolve (STh_plus_zero_left T).
Hint Resolve (STh_plus_zero_left2 S T).
Hint Resolve (STh_mult_one_left T).
Hint Resolve (STh_mult_one_left2 S T).
Hint Resolve (STh_mult_zero_left S plus_morph mult_morph T).
Hint Resolve (STh_mult_zero_left2 S plus_morph mult_morph T).
Hint Resolve (STh_distr_left T).
Hint Resolve (STh_distr_left2 S T).
Hint Resolve (STh_plus_reg_left S plus_morph T).
Hint Resolve (STh_plus_permute S plus_morph T).
Hint Resolve (STh_mult_permute S mult_morph T).
Hint Resolve (STh_distr_right S plus_morph T).
Hint Resolve (STh_distr_right2 S plus_morph T).
Hint Resolve (STh_mult_zero_right S plus_morph mult_morph T).
Hint Resolve (STh_mult_zero_right2 S plus_morph mult_morph T).
Hint Resolve (STh_plus_zero_right S T).
Hint Resolve (STh_plus_zero_right2 S T).
Hint Resolve (STh_mult_one_right S T).
Hint Resolve (STh_mult_one_right2 S T).
Hint Resolve (STh_plus_reg_right S plus_morph T).
Hint Resolve refl_equal sym_equal trans_equal.
Hint Immediate T.
Inductive setpolynomial : Type :=
| SetPvar : index -> setpolynomial
| SetPconst : A -> setpolynomial
| SetPplus : setpolynomial -> setpolynomial -> setpolynomial
| SetPmult : setpolynomial -> setpolynomial -> setpolynomial
| SetPopp : setpolynomial -> setpolynomial.
Fixpoint setpolynomial_normalize (x:setpolynomial) : canonical_sum :=
match x with
| 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 :=
match x with
| 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.
Fixpoint interp_setp (p:setpolynomial) : A :=
match p with
| 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.
Lemma setspolynomial_of_ok :
forall p:setpolynomial,
Aequiv (interp_setp p) (interp_setsp vm (setspolynomial_of p)).
Theorem setpolynomial_normalize_ok :
forall p:setpolynomial,
setpolynomial_normalize p = setspolynomial_normalize (setspolynomial_of p).
Theorem setpolynomial_simplify_ok :
forall p:setpolynomial,
Aequiv (interp_setcs vm (setpolynomial_simplify p)) (interp_setp p).
End setoid_rings.
End setoid.