Library Coq.ring.Ring_abstract
Require Import LegacyRing_theory.
Require Import Quote.
Require Import Ring_normalize.
Section abstract_semi_rings.
Inductive aspolynomial : Type :=
| ASPvar : index -> aspolynomial
| ASP0 : aspolynomial
| ASP1 : aspolynomial
| ASPplus : aspolynomial -> aspolynomial -> aspolynomial
| ASPmult : aspolynomial -> aspolynomial -> aspolynomial.
Inductive abstract_sum : Type :=
| Nil_acs : abstract_sum
| Cons_acs : varlist -> abstract_sum -> abstract_sum.
Fixpoint abstract_sum_merge (s1:abstract_sum) :
abstract_sum -> abstract_sum :=
match s1 with
| Cons_acs l1 t1 =>
(fix asm_aux (s2:abstract_sum) : abstract_sum :=
match s2 with
| Cons_acs l2 t2 =>
if varlist_lt l1 l2
then Cons_acs l1 (abstract_sum_merge t1 s2)
else Cons_acs l2 (asm_aux t2)
| Nil_acs => s1
end)
| Nil_acs => fun s2 => s2
end.
Fixpoint abstract_varlist_insert (l1:varlist) (s2:abstract_sum) {struct s2} :
abstract_sum :=
match s2 with
| Cons_acs l2 t2 =>
if varlist_lt l1 l2
then Cons_acs l1 s2
else Cons_acs l2 (abstract_varlist_insert l1 t2)
| Nil_acs => Cons_acs l1 Nil_acs
end.
Fixpoint abstract_sum_scalar (l1:varlist) (s2:abstract_sum) {struct s2} :
abstract_sum :=
match s2 with
| Cons_acs l2 t2 =>
abstract_varlist_insert (varlist_merge l1 l2)
(abstract_sum_scalar l1 t2)
| Nil_acs => Nil_acs
end.
Fixpoint abstract_sum_prod (s1 s2:abstract_sum) {struct s1} : abstract_sum :=
match s1 with
| Cons_acs l1 t1 =>
abstract_sum_merge (abstract_sum_scalar l1 s2)
(abstract_sum_prod t1 s2)
| Nil_acs => Nil_acs
end.
Fixpoint aspolynomial_normalize (p:aspolynomial) : abstract_sum :=
match p with
| ASPvar i => Cons_acs (Cons_var i Nil_var) Nil_acs
| ASP1 => Cons_acs Nil_var Nil_acs
| ASP0 => Nil_acs
| ASPplus l r =>
abstract_sum_merge (aspolynomial_normalize l)
(aspolynomial_normalize r)
| ASPmult l r =>
abstract_sum_prod (aspolynomial_normalize l) (aspolynomial_normalize r)
end.
Variable A : Type.
Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
Variable Aeq : A -> A -> bool.
Variable vm : varmap A.
Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
Fixpoint interp_asp (p:aspolynomial) : A :=
match p with
| ASPvar i => interp_var Azero vm i
| ASP0 => Azero
| ASP1 => Aone
| ASPplus l r => Aplus (interp_asp l) (interp_asp r)
| ASPmult l r => Amult (interp_asp l) (interp_asp r)
end.
Definition iacs_aux :=
(fix iacs_aux (a:A) (s:abstract_sum) {struct s} : A :=
match s with
| Nil_acs => a
| Cons_acs l t =>
Aplus a (iacs_aux (interp_vl Amult Aone Azero vm l) t)
end).
Definition interp_acs (s:abstract_sum) : A :=
match s with
| Cons_acs l t => iacs_aux (interp_vl Amult Aone Azero vm l) t
| Nil_acs => Azero
end.
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_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 refl_equal sym_equal trans_equal.
Hint Immediate T.
Remark iacs_aux_ok :
forall (x:A) (s:abstract_sum), iacs_aux x s = Aplus x (interp_acs s).
Hint Extern 10 (_ = _ :>A) => rewrite iacs_aux_ok: core.
Lemma abstract_varlist_insert_ok :
forall (l:varlist) (s:abstract_sum),
interp_acs (abstract_varlist_insert l s) =
Aplus (interp_vl Amult Aone Azero vm l) (interp_acs s).
Lemma abstract_sum_merge_ok :
forall x y:abstract_sum,
interp_acs (abstract_sum_merge x y) = Aplus (interp_acs x) (interp_acs y).
Lemma abstract_sum_scalar_ok :
forall (l:varlist) (s:abstract_sum),
interp_acs (abstract_sum_scalar l s) =
Amult (interp_vl Amult Aone Azero vm l) (interp_acs s).
Lemma abstract_sum_prod_ok :
forall x y:abstract_sum,
interp_acs (abstract_sum_prod x y) = Amult (interp_acs x) (interp_acs y).
Theorem aspolynomial_normalize_ok :
forall x:aspolynomial, interp_asp x = interp_acs (aspolynomial_normalize x).
End abstract_semi_rings.
Section abstract_rings.
Inductive apolynomial : Type :=
| APvar : index -> apolynomial
| AP0 : apolynomial
| AP1 : apolynomial
| APplus : apolynomial -> apolynomial -> apolynomial
| APmult : apolynomial -> apolynomial -> apolynomial
| APopp : apolynomial -> apolynomial.
Inductive signed_sum : Type :=
| Nil_varlist : signed_sum
| Plus_varlist : varlist -> signed_sum -> signed_sum
| Minus_varlist : varlist -> signed_sum -> signed_sum.
Fixpoint signed_sum_merge (s1:signed_sum) : signed_sum -> signed_sum :=
match s1 with
| Plus_varlist l1 t1 =>
(fix ssm_aux (s2:signed_sum) : signed_sum :=
match s2 with
| Plus_varlist l2 t2 =>
if varlist_lt l1 l2
then Plus_varlist l1 (signed_sum_merge t1 s2)
else Plus_varlist l2 (ssm_aux t2)
| Minus_varlist l2 t2 =>
if varlist_eq l1 l2
then signed_sum_merge t1 t2
else
if varlist_lt l1 l2
then Plus_varlist l1 (signed_sum_merge t1 s2)
else Minus_varlist l2 (ssm_aux t2)
| Nil_varlist => s1
end)
| Minus_varlist l1 t1 =>
(fix ssm_aux2 (s2:signed_sum) : signed_sum :=
match s2 with
| Plus_varlist l2 t2 =>
if varlist_eq l1 l2
then signed_sum_merge t1 t2
else
if varlist_lt l1 l2
then Minus_varlist l1 (signed_sum_merge t1 s2)
else Plus_varlist l2 (ssm_aux2 t2)
| Minus_varlist l2 t2 =>
if varlist_lt l1 l2
then Minus_varlist l1 (signed_sum_merge t1 s2)
else Minus_varlist l2 (ssm_aux2 t2)
| Nil_varlist => s1
end)
| Nil_varlist => fun s2 => s2
end.
Fixpoint plus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} :
signed_sum :=
match s2 with
| Plus_varlist l2 t2 =>
if varlist_lt l1 l2
then Plus_varlist l1 s2
else Plus_varlist l2 (plus_varlist_insert l1 t2)
| Minus_varlist l2 t2 =>
if varlist_eq l1 l2
then t2
else
if varlist_lt l1 l2
then Plus_varlist l1 s2
else Minus_varlist l2 (plus_varlist_insert l1 t2)
| Nil_varlist => Plus_varlist l1 Nil_varlist
end.
Fixpoint minus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} :
signed_sum :=
match s2 with
| Plus_varlist l2 t2 =>
if varlist_eq l1 l2
then t2
else
if varlist_lt l1 l2
then Minus_varlist l1 s2
else Plus_varlist l2 (minus_varlist_insert l1 t2)
| Minus_varlist l2 t2 =>
if varlist_lt l1 l2
then Minus_varlist l1 s2
else Minus_varlist l2 (minus_varlist_insert l1 t2)
| Nil_varlist => Minus_varlist l1 Nil_varlist
end.
Fixpoint signed_sum_opp (s:signed_sum) : signed_sum :=
match s with
| Plus_varlist l2 t2 => Minus_varlist l2 (signed_sum_opp t2)
| Minus_varlist l2 t2 => Plus_varlist l2 (signed_sum_opp t2)
| Nil_varlist => Nil_varlist
end.
Fixpoint plus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} :
signed_sum :=
match s2 with
| Plus_varlist l2 t2 =>
plus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2)
| Minus_varlist l2 t2 =>
minus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2)
| Nil_varlist => Nil_varlist
end.
Fixpoint minus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} :
signed_sum :=
match s2 with
| Plus_varlist l2 t2 =>
minus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2)
| Minus_varlist l2 t2 =>
plus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2)
| Nil_varlist => Nil_varlist
end.
Fixpoint signed_sum_prod (s1 s2:signed_sum) {struct s1} : signed_sum :=
match s1 with
| Plus_varlist l1 t1 =>
signed_sum_merge (plus_sum_scalar l1 s2) (signed_sum_prod t1 s2)
| Minus_varlist l1 t1 =>
signed_sum_merge (minus_sum_scalar l1 s2) (signed_sum_prod t1 s2)
| Nil_varlist => Nil_varlist
end.
Fixpoint apolynomial_normalize (p:apolynomial) : signed_sum :=
match p with
| APvar i => Plus_varlist (Cons_var i Nil_var) Nil_varlist
| AP1 => Plus_varlist Nil_var Nil_varlist
| AP0 => Nil_varlist
| APplus l r =>
signed_sum_merge (apolynomial_normalize l) (apolynomial_normalize r)
| APmult l r =>
signed_sum_prod (apolynomial_normalize l) (apolynomial_normalize r)
| APopp q => signed_sum_opp (apolynomial_normalize q)
end.
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.
Definition isacs_aux :=
(fix isacs_aux (a:A) (s:signed_sum) {struct s} : A :=
match s with
| Nil_varlist => a
| Plus_varlist l t =>
Aplus a (isacs_aux (interp_vl Amult Aone Azero vm l) t)
| Minus_varlist l t =>
Aplus a
(isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t)
end).
Definition interp_sacs (s:signed_sum) : A :=
match s with
| Plus_varlist l t => isacs_aux (interp_vl Amult Aone Azero vm l) t
| Minus_varlist l t => isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t
| Nil_varlist => Azero
end.
Fixpoint interp_ap (p:apolynomial) : A :=
match p with
| APvar i => interp_var Azero vm i
| AP0 => Azero
| AP1 => Aone
| APplus l r => Aplus (interp_ap l) (interp_ap r)
| APmult l r => Amult (interp_ap l) (interp_ap r)
| APopp q => Aopp (interp_ap q)
end.
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_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_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 refl_equal sym_equal trans_equal.
Hint Immediate T.
Lemma isacs_aux_ok :
forall (x:A) (s:signed_sum), isacs_aux x s = Aplus x (interp_sacs s).
Hint Extern 10 (_ = _ :>A) => rewrite isacs_aux_ok: core.
Ltac solve1 v v0 H H0 :=
simpl in |- *; elim (varlist_lt v v0); simpl in |- *; rewrite isacs_aux_ok;
[ rewrite H; simpl in |- *; auto | simpl in H0; rewrite H0; auto ].
Lemma signed_sum_merge_ok :
forall x y:signed_sum,
interp_sacs (signed_sum_merge x y) = Aplus (interp_sacs x) (interp_sacs y).
Ltac solve2 l v H :=
elim (varlist_lt l v); simpl in |- *; rewrite isacs_aux_ok;
[ auto | rewrite H; auto ].
Lemma plus_varlist_insert_ok :
forall (l:varlist) (s:signed_sum),
interp_sacs (plus_varlist_insert l s) =
Aplus (interp_vl Amult Aone Azero vm l) (interp_sacs s).
Lemma minus_varlist_insert_ok :
forall (l:varlist) (s:signed_sum),
interp_sacs (minus_varlist_insert l s) =
Aplus (Aopp (interp_vl Amult Aone Azero vm l)) (interp_sacs s).
Lemma signed_sum_opp_ok :
forall s:signed_sum, interp_sacs (signed_sum_opp s) = Aopp (interp_sacs s).
Lemma plus_sum_scalar_ok :
forall (l:varlist) (s:signed_sum),
interp_sacs (plus_sum_scalar l s) =
Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s).
Lemma minus_sum_scalar_ok :
forall (l:varlist) (s:signed_sum),
interp_sacs (minus_sum_scalar l s) =
Aopp (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)).
Lemma signed_sum_prod_ok :
forall x y:signed_sum,
interp_sacs (signed_sum_prod x y) = Amult (interp_sacs x) (interp_sacs y).
Theorem apolynomial_normalize_ok :
forall p:apolynomial, interp_sacs (apolynomial_normalize p) = interp_ap p.
End abstract_rings.