diff options
Diffstat (limited to 'plugins/ring/Ring_abstract.v')
| -rw-r--r-- | plugins/ring/Ring_abstract.v | 700 |
1 files changed, 0 insertions, 700 deletions
diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v deleted file mode 100644 index 4aec3893..00000000 --- a/plugins/ring/Ring_abstract.v +++ /dev/null @@ -1,700 +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. -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. - -(* Local *) 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_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. - -Remark iacs_aux_ok : - forall (x:A) (s:abstract_sum), iacs_aux x s = Aplus x (interp_acs s). -Proof. - simple induction s; simpl; intros. - trivial. - reflexivity. -Qed. - -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). - - simple induction s. - trivial. - - simpl; intros. - elim (varlist_lt l v); simpl. - eauto. - rewrite iacs_aux_ok. - rewrite H; auto. - -Qed. - -Lemma abstract_sum_merge_ok : - forall x y:abstract_sum, - interp_acs (abstract_sum_merge x y) = Aplus (interp_acs x) (interp_acs y). - -Proof. - simple induction x. - trivial. - simple induction y; intros. - - auto. - - simpl; elim (varlist_lt v v0); simpl. - repeat rewrite iacs_aux_ok. - rewrite H; simpl; auto. - - simpl in H0. - repeat rewrite iacs_aux_ok. - rewrite H0. simpl; auto. -Qed. - -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). -Proof. - simple induction s. - simpl; eauto. - - simpl; intros. - rewrite iacs_aux_ok. - rewrite abstract_varlist_insert_ok. - rewrite H. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - auto. -Qed. - -Lemma abstract_sum_prod_ok : - forall x y:abstract_sum, - interp_acs (abstract_sum_prod x y) = Amult (interp_acs x) (interp_acs y). - -Proof. - simple induction x. - intros; simpl; eauto. - - destruct y as [| v0 a0]; intros. - - simpl; rewrite H; eauto. - - unfold abstract_sum_prod; fold abstract_sum_prod. - rewrite abstract_sum_merge_ok. - rewrite abstract_sum_scalar_ok. - rewrite H; simpl; auto. -Qed. - -Theorem aspolynomial_normalize_ok : - forall x:aspolynomial, interp_asp x = interp_acs (aspolynomial_normalize x). -Proof. - simple induction x; simpl; intros; trivial. - rewrite abstract_sum_merge_ok. - rewrite H; rewrite H0; eauto. - rewrite abstract_sum_prod_ok. - rewrite H; rewrite H0; eauto. -Qed. - -End abstract_semi_rings. - -Section abstract_rings. - -(* In abstract polynomials there is no constants other - than 0 and 1. An abstract ring is a ring whose operations plus, - and mult are not functions but constructors. In other words, - when c1 and c2 are closed, (plus c1 c2) doesn't reduce to a closed - term. "closed" mean here "without plus and mult". *) - -(* this section is not parametrized by a (semi-)ring. - Nevertheless, they are two different types for semi-rings and rings - and there will be 2 correction theorems *) - -Inductive apolynomial : Type := - | APvar : index -> apolynomial - | AP0 : apolynomial - | AP1 : apolynomial - | APplus : apolynomial -> apolynomial -> apolynomial - | APmult : apolynomial -> apolynomial -> apolynomial - | APopp : apolynomial -> apolynomial. - -(* A canonical "abstract" sum is a list of varlist with the sign "+" or "-". - Invariant : the list is sorted and there is no varlist is present - with both signs. +x +x +x -x is forbidden => the canonical form is +x+x *) - -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. - -(* Local *) 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_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_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. - -Lemma isacs_aux_ok : - forall (x:A) (s:signed_sum), isacs_aux x s = Aplus x (interp_sacs s). -Proof. - simple induction s; simpl; intros. - trivial. - reflexivity. - reflexivity. -Qed. - -Hint Extern 10 (_ = _ :>A) => rewrite isacs_aux_ok: core. - -Ltac solve1 v v0 H H0 := - simpl; elim (varlist_lt v v0); simpl; rewrite isacs_aux_ok; - [ rewrite H; simpl; 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). - - simple induction x. - intro; simpl; auto. - - simple induction y; intros. - - auto. - - solve1 v v0 H H0. - - simpl; generalize (varlist_eq_prop v v0). - elim (varlist_eq v v0); simpl. - - intro Heq; rewrite (Heq I). - rewrite H. - repeat rewrite isacs_aux_ok. - rewrite (Th_plus_permute T). - repeat rewrite (Th_plus_assoc T). - rewrite - (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v0)) - (interp_vl Amult Aone Azero vm v0)). - rewrite (Th_opp_def T). - rewrite (Th_plus_zero_left T). - reflexivity. - - solve1 v v0 H H0. - - simple induction y; intros. - - auto. - - simpl; generalize (varlist_eq_prop v v0). - elim (varlist_eq v v0); simpl. - - intro Heq; rewrite (Heq I). - rewrite H. - repeat rewrite isacs_aux_ok. - rewrite (Th_plus_permute T). - repeat rewrite (Th_plus_assoc T). - rewrite (Th_opp_def T). - rewrite (Th_plus_zero_left T). - reflexivity. - - solve1 v v0 H H0. - - solve1 v v0 H H0. - -Qed. - -Ltac solve2 l v H := - elim (varlist_lt l v); simpl; 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). -Proof. - - simple induction s. - trivial. - - simpl; intros. - solve2 l v H. - - simpl; intros. - generalize (varlist_eq_prop l v). - elim (varlist_eq l v); simpl. - - intro Heq; rewrite (Heq I). - repeat rewrite isacs_aux_ok. - repeat rewrite (Th_plus_assoc T). - rewrite (Th_opp_def T). - rewrite (Th_plus_zero_left T). - reflexivity. - - solve2 l v H. - -Qed. - -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). -Proof. - - simple induction s. - trivial. - - simpl; intros. - generalize (varlist_eq_prop l v). - elim (varlist_eq l v); simpl. - - intro Heq; rewrite (Heq I). - repeat rewrite isacs_aux_ok. - repeat rewrite (Th_plus_assoc T). - rewrite - (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v)) - (interp_vl Amult Aone Azero vm v)). - rewrite (Th_opp_def T). - auto. - - simpl; intros. - solve2 l v H. - - simpl; intros; solve2 l v H. - -Qed. - -Lemma signed_sum_opp_ok : - forall s:signed_sum, interp_sacs (signed_sum_opp s) = Aopp (interp_sacs s). -Proof. - - simple induction s; simpl; intros. - - symmetry ; apply (Th_opp_zero T). - - repeat rewrite isacs_aux_ok. - rewrite H. - rewrite (Th_plus_opp_opp T). - reflexivity. - - repeat rewrite isacs_aux_ok. - rewrite H. - rewrite <- (Th_plus_opp_opp T). - rewrite (Th_opp_opp T). - reflexivity. - -Qed. - -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). -Proof. - - simple induction s. - trivial. - - simpl; intros. - rewrite plus_varlist_insert_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - repeat rewrite isacs_aux_ok. - rewrite H. - auto. - - simpl; intros. - rewrite minus_varlist_insert_ok. - repeat rewrite isacs_aux_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - rewrite H. - rewrite (Th_distr_right T). - rewrite <- (Th_opp_mult_right T). - reflexivity. - -Qed. - -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)). -Proof. - - simple induction s; simpl; intros. - - rewrite (Th_mult_zero_right T); symmetry ; apply (Th_opp_zero T). - - simpl; intros. - rewrite minus_varlist_insert_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - repeat rewrite isacs_aux_ok. - rewrite H. - rewrite (Th_distr_right T). - rewrite (Th_plus_opp_opp T). - reflexivity. - - simpl; intros. - rewrite plus_varlist_insert_ok. - repeat rewrite isacs_aux_ok. - rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). - rewrite H. - rewrite (Th_distr_right T). - rewrite <- (Th_opp_mult_right T). - rewrite <- (Th_plus_opp_opp T). - rewrite (Th_opp_opp T). - reflexivity. - -Qed. - -Lemma signed_sum_prod_ok : - forall x y:signed_sum, - interp_sacs (signed_sum_prod x y) = Amult (interp_sacs x) (interp_sacs y). -Proof. - - simple induction x. - - simpl; eauto 1. - - intros; simpl. - rewrite signed_sum_merge_ok. - rewrite plus_sum_scalar_ok. - repeat rewrite isacs_aux_ok. - rewrite H. - auto. - - intros; simpl. - repeat rewrite isacs_aux_ok. - rewrite signed_sum_merge_ok. - rewrite minus_sum_scalar_ok. - rewrite H. - rewrite (Th_distr_left T). - rewrite (Th_opp_mult_left T). - reflexivity. - -Qed. - -Theorem apolynomial_normalize_ok : - forall p:apolynomial, interp_sacs (apolynomial_normalize p) = interp_ap p. -Proof. - simple induction p; simpl; auto 1. - intros. - rewrite signed_sum_merge_ok. - rewrite H; rewrite H0; reflexivity. - intros. - rewrite signed_sum_prod_ok. - rewrite H; rewrite H0; reflexivity. - intros. - rewrite signed_sum_opp_ok. - rewrite H; reflexivity. -Qed. - -End abstract_rings. |