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.