diff options
Diffstat (limited to 'contrib7/ring')
| -rw-r--r-- | contrib7/ring/ArithRing.v | 81 | ||||
| -rw-r--r-- | contrib7/ring/NArithRing.v | 44 | ||||
| -rw-r--r-- | contrib7/ring/Quote.v | 85 | ||||
| -rw-r--r-- | contrib7/ring/Ring.v | 34 | ||||
| -rw-r--r-- | contrib7/ring/Ring_abstract.v | 699 | ||||
| -rw-r--r-- | contrib7/ring/Ring_normalize.v | 893 | ||||
| -rw-r--r-- | contrib7/ring/Ring_theory.v | 384 | ||||
| -rw-r--r-- | contrib7/ring/Setoid_ring.v | 13 | ||||
| -rw-r--r-- | contrib7/ring/Setoid_ring_normalize.v | 1141 | ||||
| -rw-r--r-- | contrib7/ring/Setoid_ring_theory.v | 429 | ||||
| -rw-r--r-- | contrib7/ring/ZArithRing.v | 35 |
11 files changed, 3838 insertions, 0 deletions
diff --git a/contrib7/ring/ArithRing.v b/contrib7/ring/ArithRing.v new file mode 100644 index 00000000..c2abc4d1 --- /dev/null +++ b/contrib7/ring/ArithRing.v @@ -0,0 +1,81 @@ +(************************************************************************) +(* 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: ArithRing.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *) + +(* Instantiation of the Ring tactic for the naturals of Arith $*) + +Require Export Ring. +Require Export Arith. +Require Eqdep_dec. + +V7only [Import nat_scope.]. +Open Local Scope nat_scope. + +Fixpoint nateq [n,m:nat] : bool := + Cases n m of + | O O => true + | (S n') (S m') => (nateq n' m') + | _ _ => false + end. + +Lemma nateq_prop : (n,m:nat)(Is_true (nateq n m))->n==m. +Proof. + Induction n; Induction m; Intros; Try Contradiction. + Trivial. + Unfold Is_true in H1. + Rewrite (H n1 H1). + Trivial. +Save. + +Hints Resolve nateq_prop eq2eqT : arithring. + +Definition NatTheory : (Semi_Ring_Theory plus mult (1) (0) nateq). + Split; Intros; Auto with arith arithring. + Apply eq2eqT; Apply simpl_plus_l with n:=n. + Apply eqT2eq; Trivial. +Defined. + + +Add Semi Ring nat plus mult (1) (0) nateq NatTheory [O S]. + +Goal (n:nat)(S n)=(plus (S O) n). +Intro; Reflexivity. +Save S_to_plus_one. + +(* Replace all occurrences of (S exp) by (plus (S O) exp), except when + exp is already O and only for those occurrences than can be reached by going + down plus and mult operations *) +Recursive Meta Definition S_to_plus t := + Match t With + | [(S O)] -> '(S O) + | [(S ?1)] -> Let t1 = (S_to_plus ?1) In + '(plus (S O) t1) + | [(plus ?1 ?2)] -> Let t1 = (S_to_plus ?1) + And t2 = (S_to_plus ?2) In + '(plus t1 t2) + | [(mult ?1 ?2)] -> Let t1 = (S_to_plus ?1) + And t2 = (S_to_plus ?2) In + '(mult t1 t2) + | [?] -> 't. + +(* Apply S_to_plus on both sides of an equality *) +Tactic Definition S_to_plus_eq := + Match Context With + | [ |- ?1 = ?2 ] -> + (**) Try (**) + Let t1 = (S_to_plus ?1) + And t2 = (S_to_plus ?2) In + Change t1=t2 + | [ |- ?1 == ?2 ] -> + (**) Try (**) + Let t1 = (S_to_plus ?1) + And t2 = (S_to_plus ?2) In + Change (t1==t2). + +Tactic Definition NatRing := S_to_plus_eq;Ring. diff --git a/contrib7/ring/NArithRing.v b/contrib7/ring/NArithRing.v new file mode 100644 index 00000000..f4548bbb --- /dev/null +++ b/contrib7/ring/NArithRing.v @@ -0,0 +1,44 @@ +(************************************************************************) +(* 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: NArithRing.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *) + +(* Instantiation of the Ring tactic for the binary natural numbers *) + +Require Export Ring. +Require Export ZArith_base. +Require NArith. +Require Eqdep_dec. + +Definition Neq := [n,m:entier] + Cases (Ncompare n m) of + EGAL => true + | _ => false + end. + +Lemma Neq_prop : (n,m:entier)(Is_true (Neq n m)) -> n=m. + Intros n m H; Unfold Neq in H. + Apply Ncompare_Eq_eq. + NewDestruct (Ncompare n m); [Reflexivity | Contradiction | Contradiction ]. +Save. + +Definition NTheory : (Semi_Ring_Theory Nplus Nmult (Pos xH) Nul Neq). + Split. + Apply Nplus_comm. + Apply Nplus_assoc. + Apply Nmult_comm. + Apply Nmult_assoc. + Apply Nplus_0_l. + Apply Nmult_1_l. + Apply Nmult_0_l. + Apply Nmult_plus_distr_r. + Apply Nplus_reg_l. + Apply Neq_prop. +Save. + +Add Semi Ring entier Nplus Nmult (Pos xH) Nul Neq NTheory [Pos Nul xO xI xH]. diff --git a/contrib7/ring/Quote.v b/contrib7/ring/Quote.v new file mode 100644 index 00000000..12a51c9f --- /dev/null +++ b/contrib7/ring/Quote.v @@ -0,0 +1,85 @@ +(************************************************************************) +(* 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: Quote.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *) + +(*********************************************************************** + The "abstract" type index is defined to represent variables. + + index : Set + index_eq : index -> bool + index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m + index_lt : index -> bool + varmap : Type -> Type. + varmap_find : (A:Type)A -> index -> (varmap A) -> A. + + The first arg. of varmap_find is the default value to take + if the object is not found in the varmap. + + index_lt defines a total well-founded order, but we don't prove that. + +***********************************************************************) + +Set Implicit Arguments. + +Section variables_map. + +Variable A : Type. + +Inductive varmap : Type := + Empty_vm : varmap +| Node_vm : A->varmap->varmap->varmap. + +Inductive index : Set := +| Left_idx : index -> index +| Right_idx : index -> index +| End_idx : index +. + +Fixpoint varmap_find [default_value:A; i:index; v:varmap] : A := + Cases i v of + End_idx (Node_vm x _ _) => x + | (Right_idx i1) (Node_vm x v1 v2) => (varmap_find default_value i1 v2) + | (Left_idx i1) (Node_vm x v1 v2) => (varmap_find default_value i1 v1) + | _ _ => default_value + end. + +Fixpoint index_eq [n,m:index] : bool := + Cases n m of + | End_idx End_idx => true + | (Left_idx n') (Left_idx m') => (index_eq n' m') + | (Right_idx n') (Right_idx m') => (index_eq n' m') + | _ _ => false + end. + +Fixpoint index_lt[n,m:index] : bool := + Cases n m of + | End_idx (Left_idx _) => true + | End_idx (Right_idx _) => true + | (Left_idx n') (Right_idx m') => true + | (Right_idx n') (Right_idx m') => (index_lt n' m') + | (Left_idx n') (Left_idx m') => (index_lt n' m') + | _ _ => false + end. + +Lemma index_eq_prop : (n,m:index)(index_eq n m)=true -> n=m. + Induction n; Induction m; Simpl; Intros. + Rewrite (H i0 H1); Reflexivity. + Discriminate. + Discriminate. + Discriminate. + Rewrite (H i0 H1); Reflexivity. + Discriminate. + Discriminate. + Discriminate. + Reflexivity. +Save. + +End variables_map. + +Unset Implicit Arguments. diff --git a/contrib7/ring/Ring.v b/contrib7/ring/Ring.v new file mode 100644 index 00000000..860dda13 --- /dev/null +++ b/contrib7/ring/Ring.v @@ -0,0 +1,34 @@ +(************************************************************************) +(* 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: Ring.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *) + +Require Export Bool. +Require Export Ring_theory. +Require Export Quote. +Require Export Ring_normalize. +Require Export Ring_abstract. + +(* As an example, we provide an instantation for bool. *) +(* Other instatiations are given in ArithRing and ZArithRing in the + same directory *) + +Definition BoolTheory : (Ring_Theory xorb andb true false [b:bool]b eqb). +Split; Simpl. +NewDestruct n; NewDestruct m; Reflexivity. +NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity. +NewDestruct n; NewDestruct m; Reflexivity. +NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity. +NewDestruct n; Reflexivity. +NewDestruct n; Reflexivity. +NewDestruct n; Reflexivity. +NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity. +NewDestruct x; NewDestruct y; Reflexivity Orelse Simpl; Tauto. +Defined. + +Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ]. diff --git a/contrib7/ring/Ring_abstract.v b/contrib7/ring/Ring_abstract.v new file mode 100644 index 00000000..55bb31da --- /dev/null +++ b/contrib7/ring/Ring_abstract.v @@ -0,0 +1,699 @@ +(************************************************************************) +(* 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: Ring_abstract.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *) + +Require Ring_theory. +Require Quote. +Require Ring_normalize. + +Section abstract_semi_rings. + +Inductive Type aspolynomial := + 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 := +Cases s1 of +| (Cons_acs l1 t1) => + Fix asm_aux{asm_aux[s2:abstract_sum] : abstract_sum := + Cases s2 of + | (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 => [s2]s2 +end. + +Fixpoint abstract_varlist_insert [l1:varlist; s2:abstract_sum] + : abstract_sum := + Cases s2 of + | (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] + : abstract_sum := + Cases s2 of + | (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:abstract_sum] + : abstract_sum -> abstract_sum := + [s2]Cases s1 of + | (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 := + Cases p of + | (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 := + Cases p of + | (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{iacs_aux [a:A; s:abstract_sum] : A := + Cases s of + | 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 := + Cases s of + | (Cons_acs l t) => (iacs_aux (interp_vl Amult Aone Azero vm l) t) + | Nil_acs => Azero + end. + +Hint SR_plus_sym_T := Resolve (SR_plus_sym T). +Hint SR_plus_assoc_T := Resolve (SR_plus_assoc T). +Hint SR_plus_assoc2_T := Resolve (SR_plus_assoc2 T). +Hint SR_mult_sym_T := Resolve (SR_mult_sym T). +Hint SR_mult_assoc_T := Resolve (SR_mult_assoc T). +Hint SR_mult_assoc2_T := Resolve (SR_mult_assoc2 T). +Hint SR_plus_zero_left_T := Resolve (SR_plus_zero_left T). +Hint SR_plus_zero_left2_T := Resolve (SR_plus_zero_left2 T). +Hint SR_mult_one_left_T := Resolve (SR_mult_one_left T). +Hint SR_mult_one_left2_T := Resolve (SR_mult_one_left2 T). +Hint SR_mult_zero_left_T := Resolve (SR_mult_zero_left T). +Hint SR_mult_zero_left2_T := Resolve (SR_mult_zero_left2 T). +Hint SR_distr_left_T := Resolve (SR_distr_left T). +Hint SR_distr_left2_T := Resolve (SR_distr_left2 T). +Hint SR_plus_reg_left_T := Resolve (SR_plus_reg_left T). +Hint SR_plus_permute_T := Resolve (SR_plus_permute T). +Hint SR_mult_permute_T := Resolve (SR_mult_permute T). +Hint SR_distr_right_T := Resolve (SR_distr_right T). +Hint SR_distr_right2_T := Resolve (SR_distr_right2 T). +Hint SR_mult_zero_right_T := Resolve (SR_mult_zero_right T). +Hint SR_mult_zero_right2_T := Resolve (SR_mult_zero_right2 T). +Hint SR_plus_zero_right_T := Resolve (SR_plus_zero_right T). +Hint SR_plus_zero_right2_T := Resolve (SR_plus_zero_right2 T). +Hint SR_mult_one_right_T := Resolve (SR_mult_one_right T). +Hint SR_mult_one_right2_T := Resolve (SR_mult_one_right2 T). +Hint SR_plus_reg_right_T := Resolve (SR_plus_reg_right T). +Hints Resolve refl_equal sym_equal trans_equal. +(*Hints Resolve refl_eqT sym_eqT trans_eqT.*) +Hints Immediate T. + +Remark iacs_aux_ok : (x:A)(s:abstract_sum) + (iacs_aux x s)==(Aplus x (interp_acs s)). +Proof. + Induction s; Simpl; Intros. + Trivial. + Reflexivity. +Save. + +Hint rew_iacs_aux : core := Extern 10 (eqT A ? ?) Rewrite iacs_aux_ok. + +Lemma abstract_varlist_insert_ok : (l:varlist)(s:abstract_sum) + (interp_acs (abstract_varlist_insert l s)) + ==(Aplus (interp_vl Amult Aone Azero vm l) (interp_acs s)). + + Induction s. + Trivial. + + Simpl; Intros. + Elim (varlist_lt l v); Simpl. + EAuto. + Rewrite iacs_aux_ok. + Rewrite H; Auto. + +Save. + +Lemma abstract_sum_merge_ok : (x,y:abstract_sum) + (interp_acs (abstract_sum_merge x y)) + ==(Aplus (interp_acs x) (interp_acs y)). + +Proof. + Induction x. + Trivial. + 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. +Save. + +Lemma abstract_sum_scalar_ok : (l:varlist)(s:abstract_sum) + (interp_acs (abstract_sum_scalar l s)) + == (Amult (interp_vl Amult Aone Azero vm l) (interp_acs s)). +Proof. + 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. +Save. + +Lemma abstract_sum_prod_ok : (x,y:abstract_sum) + (interp_acs (abstract_sum_prod x y)) + == (Amult (interp_acs x) (interp_acs y)). + +Proof. + Induction x. + Intros; Simpl; EAuto. + + NewDestruct y; 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. +Save. + +Theorem aspolynomial_normalize_ok : (x:aspolynomial) + (interp_asp x)==(interp_acs (aspolynomial_normalize x)). +Proof. + 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. +Save. + +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 Type apolynomial := + 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 := +Cases s1 of +| (Plus_varlist l1 t1) => + Fix ssm_aux{ssm_aux[s2:signed_sum] : signed_sum := + Cases s2 of + | (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{ssm_aux2[s2:signed_sum] : signed_sum := + Cases s2 of + | (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 => [s2]s2 +end. + +Fixpoint plus_varlist_insert [l1:varlist; s2:signed_sum] + : signed_sum := + Cases s2 of + | (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] + : signed_sum := + Cases s2 of + | (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 := + Cases s of + | (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] + : signed_sum := + Cases s2 of + | (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] + : signed_sum := + Cases s2 of + | (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:signed_sum] + : signed_sum -> signed_sum := + [s2]Cases s1 of + | (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 := + Cases p of + | (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{isacs_aux [a:A; s:signed_sum] : A := + Cases s of + | 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 := + Cases s of + | (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 := + Cases p of + | (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 Th_plus_sym_T := Resolve (Th_plus_sym T). +Hint Th_plus_assoc_T := Resolve (Th_plus_assoc T). +Hint Th_plus_assoc2_T := Resolve (Th_plus_assoc2 T). +Hint Th_mult_sym_T := Resolve (Th_mult_sym T). +Hint Th_mult_assoc_T := Resolve (Th_mult_assoc T). +Hint Th_mult_assoc2_T := Resolve (Th_mult_assoc2 T). +Hint Th_plus_zero_left_T := Resolve (Th_plus_zero_left T). +Hint Th_plus_zero_left2_T := Resolve (Th_plus_zero_left2 T). +Hint Th_mult_one_left_T := Resolve (Th_mult_one_left T). +Hint Th_mult_one_left2_T := Resolve (Th_mult_one_left2 T). +Hint Th_mult_zero_left_T := Resolve (Th_mult_zero_left T). +Hint Th_mult_zero_left2_T := Resolve (Th_mult_zero_left2 T). +Hint Th_distr_left_T := Resolve (Th_distr_left T). +Hint Th_distr_left2_T := Resolve (Th_distr_left2 T). +Hint Th_plus_reg_left_T := Resolve (Th_plus_reg_left T). +Hint Th_plus_permute_T := Resolve (Th_plus_permute T). +Hint Th_mult_permute_T := Resolve (Th_mult_permute T). +Hint Th_distr_right_T := Resolve (Th_distr_right T). +Hint Th_distr_right2_T := Resolve (Th_distr_right2 T). +Hint Th_mult_zero_right2_T := Resolve (Th_mult_zero_right2 T). +Hint Th_plus_zero_right_T := Resolve (Th_plus_zero_right T). +Hint Th_plus_zero_right2_T := Resolve (Th_plus_zero_right2 T). +Hint Th_mult_one_right_T := Resolve (Th_mult_one_right T). +Hint Th_mult_one_right2_T := Resolve (Th_mult_one_right2 T). +Hint Th_plus_reg_right_T := Resolve (Th_plus_reg_right T). +Hints Resolve refl_equal sym_equal trans_equal. +(*Hints Resolve refl_eqT sym_eqT trans_eqT.*) +Hints Immediate T. + +Lemma isacs_aux_ok : (x:A)(s:signed_sum) + (isacs_aux x s)==(Aplus x (interp_sacs s)). +Proof. + Induction s; Simpl; Intros. + Trivial. + Reflexivity. + Reflexivity. +Save. + +Hint rew_isacs_aux : core := Extern 10 (eqT A ? ?) Rewrite isacs_aux_ok. + +Tactic Definition 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 : (x,y:signed_sum) + (interp_sacs (signed_sum_merge x y)) + ==(Aplus (interp_sacs x) (interp_sacs y)). + + Induction x. + Intro; Simpl; Auto. + + 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_sym 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. + + 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. + +Save. + +Tactic Definition Solve2 l v H := + Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok; + [ Auto + | Rewrite H; Auto ]. + +Lemma plus_varlist_insert_ok : (l:varlist)(s:signed_sum) + (interp_sacs (plus_varlist_insert l s)) + == (Aplus (interp_vl Amult Aone Azero vm l) (interp_sacs s)). +Proof. + + 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. + +Save. + +Lemma minus_varlist_insert_ok : (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. + + 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_sym 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. + +Save. + +Lemma signed_sum_opp_ok : (s:signed_sum) + (interp_sacs (signed_sum_opp s)) + == (Aopp (interp_sacs s)). +Proof. + + 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. + +Save. + +Lemma plus_sum_scalar_ok : (l:varlist)(s:signed_sum) + (interp_sacs (plus_sum_scalar l s)) + == (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)). +Proof. + + 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. + +Save. + +Lemma minus_sum_scalar_ok : (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. + + 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. + +Save. + +Lemma signed_sum_prod_ok : (x,y:signed_sum) + (interp_sacs (signed_sum_prod x y)) == + (Amult (interp_sacs x) (interp_sacs y)). +Proof. + + 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. + +Save. + +Theorem apolynomial_normalize_ok : (p:apolynomial) + (interp_sacs (apolynomial_normalize p))==(interp_ap p). +Proof. + 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. +Save. + +End abstract_rings. diff --git a/contrib7/ring/Ring_normalize.v b/contrib7/ring/Ring_normalize.v new file mode 100644 index 00000000..1dbd9d56 --- /dev/null +++ b/contrib7/ring/Ring_normalize.v @@ -0,0 +1,893 @@ +(************************************************************************) +(* 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: Ring_normalize.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *) + +Require Ring_theory. +Require Quote. + +Set Implicit Arguments. + +Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m. +Proof. + Intros. + Apply Quote.index_eq_prop. + Generalize H. + Case (index_eq n m); Simpl; Trivial; Intros. + Contradiction. +Save. + +Section semi_rings. + +Variable A : Type. +Variable Aplus : A -> A -> A. +Variable Amult : A -> A -> A. +Variable Aone : A. +Variable Azero : A. +Variable Aeq : A -> A -> bool. + +(* 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-ring polynomials *) +Inductive Type spolynomial := + SPvar : index -> spolynomial +| SPconst : A -> spolynomial +| SPplus : spolynomial -> spolynomial -> spolynomial +| SPmult : spolynomial -> spolynomial -> spolynomial. + +Fixpoint spolynomial_normalize[p:spolynomial] : canonical_sum := + Cases p of + | (SPvar i) => (Cons_varlist (Cons_var i Nil_var) Nil_monom) + | (SPconst c) => (Cons_monom c Nil_var Nil_monom) + | (SPplus l r) => (canonical_sum_merge (spolynomial_normalize l) + (spolynomial_normalize r)) + | (SPmult l r) => (canonical_sum_prod (spolynomial_normalize l) + (spolynomial_normalize r)) + end. + +(* Deletion of useless 0 and 1 in canonical sums *) +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 spolynomial_simplify := + [x:spolynomial](canonical_sum_simplify (spolynomial_normalize x)). + +(* End definitions. *) + +(* Section interpretation. *) + +(*** Here a variable map is defined and the interpetation of a spolynom + acording to a certain variables map. Once again the choosen definition + is generic and could be changed ****) + +Variable vm : (varmap A). + +(* Interpretation of list of variables + * [x1; ... ; xn ] is interpreted as (find v x1)* ... *(find v xn) + * The unbound variables are mapped to 0. Normally this case sould + * never occur. Since we want only to prove correctness theorems, which form + * is : for any varmap and any spolynom ... this is a safe and pain-saving + * choice *) +Definition interp_var [i:index] := (varmap_find Azero i vm). + +(* Local *) 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. + +(* Local *) Definition interp_m := [c:A][l:varlist] + Cases l of + | Nil_var => c + | (Cons_var x t) => + (Amult c (ivl_aux x t)) + end. + +(* Local *) 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}. + +(* Interpretation of a canonical sum *) +Definition interp_cs : 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_sp [p:spolynomial] : A := + Cases p of + (SPconst c) => c + | (SPvar i) => (interp_var i) + | (SPplus p1 p2) => (Aplus (interp_sp p1) (interp_sp p2)) + | (SPmult p1 p2) => (Amult (interp_sp p1) (interp_sp p2)) + end. + + +(* End interpretation. *) + +Unset Implicit Arguments. + +(* Section properties. *) + +Variable T : (Semi_Ring_Theory Aplus Amult Aone Azero Aeq). + +Hint SR_plus_sym_T := Resolve (SR_plus_sym T). +Hint SR_plus_assoc_T := Resolve (SR_plus_assoc T). +Hint SR_plus_assoc2_T := Resolve (SR_plus_assoc2 T). +Hint SR_mult_sym_T := Resolve (SR_mult_sym T). +Hint SR_mult_assoc_T := Resolve (SR_mult_assoc T). +Hint SR_mult_assoc2_T := Resolve (SR_mult_assoc2 T). +Hint SR_plus_zero_left_T := Resolve (SR_plus_zero_left T). +Hint SR_plus_zero_left2_T := Resolve (SR_plus_zero_left2 T). +Hint SR_mult_one_left_T := Resolve (SR_mult_one_left T). +Hint SR_mult_one_left2_T := Resolve (SR_mult_one_left2 T). +Hint SR_mult_zero_left_T := Resolve (SR_mult_zero_left T). +Hint SR_mult_zero_left2_T := Resolve (SR_mult_zero_left2 T). +Hint SR_distr_left_T := Resolve (SR_distr_left T). +Hint SR_distr_left2_T := Resolve (SR_distr_left2 T). +Hint SR_plus_reg_left_T := Resolve (SR_plus_reg_left T). +Hint SR_plus_permute_T := Resolve (SR_plus_permute T). +Hint SR_mult_permute_T := Resolve (SR_mult_permute T). +Hint SR_distr_right_T := Resolve (SR_distr_right T). +Hint SR_distr_right2_T := Resolve (SR_distr_right2 T). +Hint SR_mult_zero_right_T := Resolve (SR_mult_zero_right T). +Hint SR_mult_zero_right2_T := Resolve (SR_mult_zero_right2 T). +Hint SR_plus_zero_right_T := Resolve (SR_plus_zero_right T). +Hint SR_plus_zero_right2_T := Resolve (SR_plus_zero_right2 T). +Hint SR_mult_one_right_T := Resolve (SR_mult_one_right T). +Hint SR_mult_one_right2_T := Resolve (SR_mult_one_right2 T). +Hint SR_plus_reg_right_T := Resolve (SR_plus_reg_right 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) + (ivl_aux i v)==(Amult (interp_var i) (interp_vl v)). +Proof. + Induction v; Simpl; Intros. + Trivial. + Rewrite H; Trivial. +Save. + +Lemma varlist_merge_ok : (x,y:varlist) + (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. + + Repeat Rewrite ivl_aux_ok. + Rewrite H. Simpl. + Rewrite ivl_aux_ok. + EAuto. + + Repeat Rewrite ivl_aux_ok. + Rewrite H0. + Rewrite ivl_aux_ok. + EAuto. +Save. + +Remark ics_aux_ok : (x:A)(s:canonical_sum) + (ics_aux x s)==(Aplus x (interp_cs s)). +Proof. + Induction s; Simpl; Intros. + Trivial. + Reflexivity. + Reflexivity. +Save. + +Remark interp_m_ok : (x:A)(l:varlist) + (interp_m x l)==(Amult x (interp_vl l)). +Proof. + NewDestruct l. + Simpl; Trivial. + Reflexivity. +Save. + +Lemma canonical_sum_merge_ok : (x,y:canonical_sum) + (interp_cs (canonical_sum_merge x y)) + ==(Aplus (interp_cs x) (interp_cs y)). + +Induction x; Simpl. +Trivial. + +Induction y; Simpl; Intros. +(* monom and nil *) +EAuto. + +(* monom and monom *) +Generalize (varlist_eq_prop v v0). +Elim (varlist_eq v v0). +Intros; Rewrite (H1 I). +Simpl; Repeat Rewrite ics_aux_ok; Rewrite H. +Repeat Rewrite interp_m_ok. +Rewrite (SR_distr_left T). +Repeat Rewrite <- (SR_plus_assoc T). +Apply congr_eqT with f:=(Aplus (Amult a (interp_vl v0))). +Trivial. + +Elim (varlist_lt v v0); Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto. + +Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto. + +(* monom and varlist *) +Generalize (varlist_eq_prop v v0). +Elim (varlist_eq v v0). +Intros; Rewrite (H1 I). +Simpl; Repeat Rewrite ics_aux_ok; Rewrite H. +Repeat Rewrite interp_m_ok. +Rewrite (SR_distr_left T). +Repeat Rewrite <- (SR_plus_assoc T). +Apply congr_eqT with f:=(Aplus (Amult a (interp_vl v0))). +Rewrite (SR_mult_one_left T). +Trivial. + +Elim (varlist_lt v v0); Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto. +Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto. + +Induction y; Simpl; Intros. +(* varlist and nil *) +Trivial. + +(* varlist and monom *) +Generalize (varlist_eq_prop v v0). +Elim (varlist_eq v v0). +Intros; Rewrite (H1 I). +Simpl; Repeat Rewrite ics_aux_ok; Rewrite H. +Repeat Rewrite interp_m_ok. +Rewrite (SR_distr_left T). +Repeat Rewrite <- (SR_plus_assoc T). +Rewrite (SR_mult_one_left T). +Apply congr_eqT with f:=(Aplus (interp_vl v0)). +Trivial. + +Elim (varlist_lt v v0); Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto. +Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto. + +(* varlist and varlist *) +Generalize (varlist_eq_prop v v0). +Elim (varlist_eq v v0). +Intros; Rewrite (H1 I). +Simpl; Repeat Rewrite ics_aux_ok; Rewrite H. +Repeat Rewrite interp_m_ok. +Rewrite (SR_distr_left T). +Repeat Rewrite <- (SR_plus_assoc T). +Rewrite (SR_mult_one_left T). +Apply congr_eqT with f:=(Aplus (interp_vl v0)). +Trivial. + +Elim (varlist_lt v v0); Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto. +Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto. +Save. + +Lemma monom_insert_ok: (a:A)(l:varlist)(s:canonical_sum) + (interp_cs (monom_insert a l s)) + == (Aplus (Amult a (interp_vl l)) (interp_cs s)). +Intros; Generalize s; Induction s0. + +Simpl; Rewrite interp_m_ok; Trivial. + +Simpl; Intros. +Generalize (varlist_eq_prop l v); Elim (varlist_eq l v). +Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok; + Repeat Rewrite ics_aux_ok; Rewrite interp_m_ok; + Rewrite (SR_distr_left T); EAuto. +Elim (varlist_lt l v); Simpl; +[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto +| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; + Rewrite H; Rewrite ics_aux_ok; EAuto]. + +Simpl; Intros. +Generalize (varlist_eq_prop l v); Elim (varlist_eq l v). +Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok; + Repeat Rewrite ics_aux_ok; + Rewrite (SR_distr_left T); Rewrite (SR_mult_one_left T); EAuto. +Elim (varlist_lt l v); Simpl; +[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto +| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; + Rewrite H; Rewrite ics_aux_ok; EAuto]. +Save. + +Lemma varlist_insert_ok : + (l:varlist)(s:canonical_sum) + (interp_cs (varlist_insert l s)) + == (Aplus (interp_vl l) (interp_cs s)). +Intros; Generalize s; Induction s0. + +Simpl; Trivial. + +Simpl; Intros. +Generalize (varlist_eq_prop l v); Elim (varlist_eq l v). +Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok; + Repeat Rewrite ics_aux_ok; Rewrite interp_m_ok; + Rewrite (SR_distr_left T); Rewrite (SR_mult_one_left T); EAuto. +Elim (varlist_lt l v); Simpl; +[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto +| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; + Rewrite H; Rewrite ics_aux_ok; EAuto]. + +Simpl; Intros. +Generalize (varlist_eq_prop l v); Elim (varlist_eq l v). +Intro Hr; Rewrite (Hr I); Simpl; Rewrite interp_m_ok; + Repeat Rewrite ics_aux_ok; + Rewrite (SR_distr_left T); Rewrite (SR_mult_one_left T); EAuto. +Elim (varlist_lt l v); Simpl; +[ Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; EAuto +| Repeat Rewrite interp_m_ok; Rewrite ics_aux_ok; + Rewrite H; Rewrite ics_aux_ok; EAuto]. +Save. + +Lemma canonical_sum_scalar_ok : (a:A)(s:canonical_sum) + (interp_cs (canonical_sum_scalar a s)) + ==(Amult a (interp_cs s)). +Induction s. +Simpl; EAuto. + +Simpl; Intros. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Reflexivity. + +Simpl; Intros. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Reflexivity. +Save. + +Lemma canonical_sum_scalar2_ok : (l:varlist; s:canonical_sum) + (interp_cs (canonical_sum_scalar2 l s)) + ==(Amult (interp_vl l) (interp_cs s)). +Induction s. +Simpl; Trivial. + +Simpl; Intros. +Rewrite monom_insert_ok. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite varlist_merge_ok. +Repeat Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Repeat Rewrite <- (SR_plus_assoc T). +Rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). +Reflexivity. + +Simpl; Intros. +Rewrite varlist_insert_ok. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite varlist_merge_ok. +Repeat Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Repeat Rewrite <- (SR_plus_assoc T). +Reflexivity. +Save. + +Lemma canonical_sum_scalar3_ok : (c:A; l:varlist; s:canonical_sum) + (interp_cs (canonical_sum_scalar3 c l s)) + ==(Amult c (Amult (interp_vl l) (interp_cs s))). +Induction s. +Simpl; Repeat Rewrite (SR_mult_zero_right T); Reflexivity. + +Simpl; Intros. +Rewrite monom_insert_ok. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite varlist_merge_ok. +Repeat Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Repeat Rewrite <- (SR_plus_assoc T). +Rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). +Reflexivity. + +Simpl; Intros. +Rewrite monom_insert_ok. +Repeat Rewrite ics_aux_ok. +Repeat Rewrite interp_m_ok. +Rewrite H. +Rewrite varlist_merge_ok. +Repeat Rewrite (SR_distr_right T). +Repeat Rewrite <- (SR_mult_assoc T). +Repeat Rewrite <- (SR_plus_assoc T). +Rewrite (SR_mult_permute T c (interp_vl l) (interp_vl v)). +Reflexivity. +Save. + +Lemma canonical_sum_prod_ok : (x,y:canonical_sum) + (interp_cs (canonical_sum_prod x y)) + ==(Amult (interp_cs x) (interp_cs y)). +Induction x; Simpl; Intros. +Trivial. + +Rewrite canonical_sum_merge_ok. +Rewrite canonical_sum_scalar3_ok. +Rewrite ics_aux_ok. +Rewrite interp_m_ok. +Rewrite H. +Rewrite (SR_mult_assoc T a (interp_vl v) (interp_cs y)). +Symmetry. +EAuto. + +Rewrite canonical_sum_merge_ok. +Rewrite canonical_sum_scalar2_ok. +Rewrite ics_aux_ok. +Rewrite H. +Trivial. +Save. + +Theorem spolynomial_normalize_ok : (p:spolynomial) + (interp_cs (spolynomial_normalize p)) == (interp_sp p). +Induction p; Simpl; Intros. + +Reflexivity. +Reflexivity. + +Rewrite canonical_sum_merge_ok. +Rewrite H; Rewrite H0. +Reflexivity. + +Rewrite canonical_sum_prod_ok. +Rewrite H; Rewrite H0. +Reflexivity. +Save. + +Lemma canonical_sum_simplify_ok : (s:canonical_sum) + (interp_cs (canonical_sum_simplify s)) == (interp_cs s). +Induction s. + +Reflexivity. + +(* cons_monom *) +Simpl; Intros. +Generalize (SR_eq_prop T 8!a 9!Azero). +Elim (Aeq a Azero). +Intro Heq; Rewrite (Heq I). +Rewrite H. +Rewrite ics_aux_ok. +Rewrite interp_m_ok. +Rewrite (SR_mult_zero_left T). +Trivial. + +Intros; Simpl. +Generalize (SR_eq_prop T 8!a 9!Aone). +Elim (Aeq a Aone). +Intro Heq; Rewrite (Heq I). +Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite interp_m_ok. +Rewrite H. +Rewrite (SR_mult_one_left T). +Reflexivity. + +Simpl. +Repeat Rewrite ics_aux_ok. +Rewrite interp_m_ok. +Rewrite H. +Reflexivity. + +(* cons_varlist *) +Simpl; Intros. +Repeat Rewrite ics_aux_ok. +Rewrite H. +Reflexivity. + +Save. + +Theorem spolynomial_simplify_ok : (p:spolynomial) + (interp_cs (spolynomial_simplify p)) == (interp_sp p). +Intro. +Unfold spolynomial_simplify. +Rewrite canonical_sum_simplify_ok. +Apply spolynomial_normalize_ok. +Save. + +(* End properties. *) +End semi_rings. + +Implicits Cons_varlist. +Implicits Cons_monom. +Implicits SPconst. +Implicits SPplus. +Implicits SPmult. + +Section rings. + +(* Here the coercion between Ring and Semi-Ring will be useful *) + +Set Implicit Arguments. + +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). + +Hint Th_plus_sym_T := Resolve (Th_plus_sym T). +Hint Th_plus_assoc_T := Resolve (Th_plus_assoc T). +Hint Th_plus_assoc2_T := Resolve (Th_plus_assoc2 T). +Hint Th_mult_sym_T := Resolve (Th_mult_sym T). +Hint Th_mult_assoc_T := Resolve (Th_mult_assoc T). +Hint Th_mult_assoc2_T := Resolve (Th_mult_assoc2 T). +Hint Th_plus_zero_left_T := Resolve (Th_plus_zero_left T). +Hint Th_plus_zero_left2_T := Resolve (Th_plus_zero_left2 T). +Hint Th_mult_one_left_T := Resolve (Th_mult_one_left T). +Hint Th_mult_one_left2_T := Resolve (Th_mult_one_left2 T). +Hint Th_mult_zero_left_T := Resolve (Th_mult_zero_left T). +Hint Th_mult_zero_left2_T := Resolve (Th_mult_zero_left2 T). +Hint Th_distr_left_T := Resolve (Th_distr_left T). +Hint Th_distr_left2_T := Resolve (Th_distr_left2 T). +Hint Th_plus_reg_left_T := Resolve (Th_plus_reg_left T). +Hint Th_plus_permute_T := Resolve (Th_plus_permute T). +Hint Th_mult_permute_T := Resolve (Th_mult_permute T). +Hint Th_distr_right_T := Resolve (Th_distr_right T). +Hint Th_distr_right2_T := Resolve (Th_distr_right2 T). +Hint Th_mult_zero_right_T := Resolve (Th_mult_zero_right T). +Hint Th_mult_zero_right2_T := Resolve (Th_mult_zero_right2 T). +Hint Th_plus_zero_right_T := Resolve (Th_plus_zero_right T). +Hint Th_plus_zero_right2_T := Resolve (Th_plus_zero_right2 T). +Hint Th_mult_one_right_T := Resolve (Th_mult_one_right T). +Hint Th_mult_one_right2_T := Resolve (Th_mult_one_right2 T). +Hint Th_plus_reg_right_T := Resolve (Th_plus_reg_right T). +Hints Resolve refl_equal sym_equal trans_equal. +(*Hints Resolve refl_eqT sym_eqT trans_eqT.*) +Hints Immediate T. + +(*** Definitions *) + +Inductive Type polynomial := + Pvar : index -> polynomial +| Pconst : A -> polynomial +| Pplus : polynomial -> polynomial -> polynomial +| Pmult : polynomial -> polynomial -> polynomial +| Popp : polynomial -> polynomial. + +Fixpoint polynomial_normalize [x:polynomial] : (canonical_sum A) := + Cases x of + (Pplus l r) => (canonical_sum_merge Aplus Aone + (polynomial_normalize l) + (polynomial_normalize r)) + | (Pmult l r) => (canonical_sum_prod Aplus Amult Aone + (polynomial_normalize l) + (polynomial_normalize r)) + | (Pconst c) => (Cons_monom c Nil_var (Nil_monom A)) + | (Pvar i) => (Cons_varlist (Cons_var i Nil_var) (Nil_monom A)) + | (Popp p) => (canonical_sum_scalar3 Aplus Amult Aone + (Aopp Aone) Nil_var + (polynomial_normalize p)) + end. + +Definition polynomial_simplify := + [x:polynomial](canonical_sum_simplify Aone Azero Aeq + (polynomial_normalize x)). + +Fixpoint spolynomial_of [x:polynomial] : (spolynomial A) := + Cases x of + (Pplus l r) => (SPplus (spolynomial_of l) (spolynomial_of r)) + | (Pmult l r) => (SPmult (spolynomial_of l) (spolynomial_of r)) + | (Pconst c) => (SPconst c) + | (Pvar i) => (SPvar A i) + | (Popp p) => (SPmult (SPconst (Aopp Aone)) (spolynomial_of p)) + end. + +(*** Interpretation *) + +Fixpoint interp_p [p:polynomial] : A := + Cases p of + (Pconst c) => c + | (Pvar i) => (varmap_find Azero i vm) + | (Pplus p1 p2) => (Aplus (interp_p p1) (interp_p p2)) + | (Pmult p1 p2) => (Amult (interp_p p1) (interp_p p2)) + | (Popp p1) => (Aopp (interp_p p1)) + end. + +(*** Properties *) + +Unset Implicit Arguments. + +Lemma spolynomial_of_ok : (p:polynomial) + (interp_p p)==(interp_sp Aplus Amult Azero vm (spolynomial_of p)). +Induction p; Reflexivity Orelse (Simpl; Intros). +Rewrite H; Rewrite H0; Reflexivity. +Rewrite H; Rewrite H0; Reflexivity. +Rewrite H. +Rewrite (Th_opp_mult_left2 T). +Rewrite (Th_mult_one_left T). +Reflexivity. +Save. + +Theorem polynomial_normalize_ok : (p:polynomial) + (polynomial_normalize p) + ==(spolynomial_normalize Aplus Amult Aone (spolynomial_of p)). +Induction p; Reflexivity Orelse (Simpl; Intros). +Rewrite H; Rewrite H0; Reflexivity. +Rewrite H; Rewrite H0; Reflexivity. +Rewrite H; Simpl. +Elim (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var + (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0))); +[ Reflexivity +| Simpl; Intros; Rewrite H0; Reflexivity +| Simpl; Intros; Rewrite H0; Reflexivity ]. +Save. + +Theorem polynomial_simplify_ok : (p:polynomial) + (interp_cs Aplus Amult Aone Azero vm (polynomial_simplify p)) + ==(interp_p p). +Intro. +Unfold polynomial_simplify. +Rewrite spolynomial_of_ok. +Rewrite polynomial_normalize_ok. +Rewrite (canonical_sum_simplify_ok A Aplus Amult Aone Azero Aeq vm T). +Rewrite (spolynomial_normalize_ok A Aplus Amult Aone Azero Aeq vm T). +Reflexivity. +Save. + +End rings. + +V8Infix "+" Pplus : ring_scope. +V8Infix "*" Pmult : ring_scope. +V8Notation "- x" := (Popp x) : ring_scope. +V8Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope. + +Delimits Scope ring_scope with ring. diff --git a/contrib7/ring/Ring_theory.v b/contrib7/ring/Ring_theory.v new file mode 100644 index 00000000..85fb7f6c --- /dev/null +++ b/contrib7/ring/Ring_theory.v @@ -0,0 +1,384 @@ +(************************************************************************) +(* 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: Ring_theory.v,v 1.1.2.1 2004/07/16 19:30:19 herbelin Exp $ *) + +Require Export Bool. + +Set Implicit Arguments. + +Section Theory_of_semi_rings. + +Variable A : Type. +Variable Aplus : A -> A -> A. +Variable Amult : A -> A -> A. +Variable Aone : A. +Variable Azero : A. +(* There is also a "weakly decidable" equality on A. That means + that if (A_eq x y)=true then x=y but x=y can arise when + (A_eq x y)=false. On an abstract ring the function [x,y:A]false + is a good choice. The proof of A_eq_prop is in this case easy. *) +Variable Aeq : A -> A -> bool. + +Infix 4 "+" Aplus V8only 50 (left associativity). +Infix 4 "*" Amult V8only 40 (left associativity). +Notation "0" := Azero. +Notation "1" := Aone. + +Record Semi_Ring_Theory : Prop := +{ SR_plus_sym : (n,m:A) n + m == m + n; + SR_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; + SR_mult_sym : (n,m:A) n*m == m*n; + SR_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; + SR_plus_zero_left :(n:A) 0 + n == n; + SR_mult_one_left : (n:A) 1*n == n; + SR_mult_zero_left : (n:A) 0*n == 0; + SR_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; + SR_plus_reg_left : (n,m,p:A) n + m == n + p -> m==p; + SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y +}. + +Variable T : Semi_Ring_Theory. + +Local plus_sym := (SR_plus_sym T). +Local plus_assoc := (SR_plus_assoc T). +Local mult_sym := ( SR_mult_sym T). +Local mult_assoc := (SR_mult_assoc T). +Local plus_zero_left := (SR_plus_zero_left T). +Local mult_one_left := (SR_mult_one_left T). +Local mult_zero_left := (SR_mult_zero_left T). +Local distr_left := (SR_distr_left T). +Local plus_reg_left := (SR_plus_reg_left T). + +Hints Resolve plus_sym plus_assoc mult_sym mult_assoc + plus_zero_left mult_one_left mult_zero_left distr_left + plus_reg_left. + +(* Lemmas whose form is x=y are also provided in form y=x because Auto does + not symmetry *) +Lemma SR_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). +Symmetry; EAuto. Qed. + +Lemma SR_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). +Symmetry; EAuto. Qed. + +Lemma SR_plus_zero_left2 : (n:A) n == 0 + n. +Symmetry; EAuto. Qed. + +Lemma SR_mult_one_left2 : (n:A) n == 1*n. +Symmetry; EAuto. Qed. + +Lemma SR_mult_zero_left2 : (n:A) 0 == 0*n. +Symmetry; EAuto. Qed. + +Lemma SR_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. +Symmetry; EAuto. Qed. + +Lemma SR_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p). +Intros. +Rewrite -> plus_assoc. +Elim (plus_sym m n). +Rewrite <- plus_assoc. +Reflexivity. +Qed. + +Lemma SR_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). +Intros. +Rewrite -> mult_assoc. +Elim (mult_sym m n). +Rewrite <- mult_assoc. +Reflexivity. +Qed. + +Hints Resolve SR_plus_permute SR_mult_permute. + +Lemma SR_distr_right : (n,m,p:A) n*(m + p) == (n*m) + (n*p). +Intros. +Repeat Rewrite -> (mult_sym n). +EAuto. +Qed. + +Lemma SR_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p). +Symmetry; Apply SR_distr_right. Qed. + +Lemma SR_mult_zero_right : (n:A) n*0 == 0. +Intro; Rewrite mult_sym; EAuto. +Qed. + +Lemma SR_mult_zero_right2 : (n:A) 0 == n*0. +Intro; Rewrite mult_sym; EAuto. +Qed. + +Lemma SR_plus_zero_right :(n:A) n + 0 == n. +Intro; Rewrite plus_sym; EAuto. +Qed. +Lemma SR_plus_zero_right2 :(n:A) n == n + 0. +Intro; Rewrite plus_sym; EAuto. +Qed. + +Lemma SR_mult_one_right : (n:A) n*1 == n. +Intro; Elim mult_sym; Auto. +Qed. + +Lemma SR_mult_one_right2 : (n:A) n == n*1. +Intro; Elim mult_sym; Auto. +Qed. + +Lemma SR_plus_reg_right : (n,m,p:A) m + n == p + n -> m==p. +Intros n m p; Rewrite (plus_sym m n); Rewrite (plus_sym p n); EAuto. +Qed. + +End Theory_of_semi_rings. + +Section Theory_of_rings. + +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. + +Infix 4 "+" Aplus V8only 50 (left associativity). +Infix 4 "*" Amult V8only 40 (left associativity). +Notation "0" := Azero. +Notation "1" := Aone. +Notation "- x" := (Aopp x) (at level 0) V8only. + +Record Ring_Theory : Prop := +{ Th_plus_sym : (n,m:A) n + m == m + n; + Th_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; + Th_mult_sym : (n,m:A) n*m == m*n; + Th_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; + Th_plus_zero_left :(n:A) 0 + n == n; + Th_mult_one_left : (n:A) 1*n == n; + Th_opp_def : (n:A) n + (-n) == 0; + Th_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; + Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y +}. + +Variable T : Ring_Theory. + +Local plus_sym := (Th_plus_sym T). +Local plus_assoc := (Th_plus_assoc T). +Local mult_sym := ( Th_mult_sym T). +Local mult_assoc := (Th_mult_assoc T). +Local plus_zero_left := (Th_plus_zero_left T). +Local mult_one_left := (Th_mult_one_left T). +Local opp_def := (Th_opp_def T). +Local distr_left := (Th_distr_left T). + +Hints Resolve plus_sym plus_assoc mult_sym mult_assoc + plus_zero_left mult_one_left opp_def distr_left. + +(* Lemmas whose form is x=y are also provided in form y=x because Auto does + not symmetry *) +Lemma Th_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). +Symmetry; EAuto. Qed. + +Lemma Th_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). +Symmetry; EAuto. Qed. + +Lemma Th_plus_zero_left2 : (n:A) n == 0 + n. +Symmetry; EAuto. Qed. + +Lemma Th_mult_one_left2 : (n:A) n == 1*n. +Symmetry; EAuto. Qed. + +Lemma Th_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. +Symmetry; EAuto. Qed. + +Lemma Th_opp_def2 : (n:A) 0 == n + (-n). +Symmetry; EAuto. Qed. + +Lemma Th_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p). +Intros. +Rewrite -> plus_assoc. +Elim (plus_sym m n). +Rewrite <- plus_assoc. +Reflexivity. +Qed. + +Lemma Th_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). +Intros. +Rewrite -> mult_assoc. +Elim (mult_sym m n). +Rewrite <- mult_assoc. +Reflexivity. +Qed. + +Hints Resolve Th_plus_permute Th_mult_permute. + +Lemma aux1 : (a:A) a + a == a -> a == 0. +Intros. +Generalize (opp_def a). +Pattern 1 a. +Rewrite <- H. +Rewrite <- plus_assoc. +Rewrite -> opp_def. +Elim plus_sym. +Rewrite plus_zero_left. +Trivial. +Qed. + +Lemma Th_mult_zero_left :(n:A) 0*n == 0. +Intros. +Apply aux1. +Rewrite <- distr_left. +Rewrite plus_zero_left. +Reflexivity. +Qed. +Hints Resolve Th_mult_zero_left. + +Lemma Th_mult_zero_left2 : (n:A) 0 == 0*n. +Symmetry; EAuto. Qed. + +Lemma aux2 : (x,y,z:A) x+y==0 -> x+z==0 -> y==z. +Intros. +Rewrite <- (plus_zero_left y). +Elim H0. +Elim plus_assoc. +Elim (plus_sym y z). +Rewrite -> plus_assoc. +Rewrite -> H. +Rewrite plus_zero_left. +Reflexivity. +Qed. + +Lemma Th_opp_mult_left : (x,y:A) -(x*y) == (-x)*y. +Intros. +Apply (aux2 1!x*y); +[ Apply opp_def +| Rewrite <- distr_left; + Rewrite -> opp_def; + Auto]. +Qed. +Hints Resolve Th_opp_mult_left. + +Lemma Th_opp_mult_left2 : (x,y:A) (-x)*y == -(x*y). +Symmetry; EAuto. Qed. + +Lemma Th_mult_zero_right : (n:A) n*0 == 0. +Intro; Elim mult_sym; EAuto. +Qed. + +Lemma Th_mult_zero_right2 : (n:A) 0 == n*0. +Intro; Elim mult_sym; EAuto. +Qed. + +Lemma Th_plus_zero_right :(n:A) n + 0 == n. +Intro; Rewrite plus_sym; EAuto. +Qed. + +Lemma Th_plus_zero_right2 :(n:A) n == n + 0. +Intro; Rewrite plus_sym; EAuto. +Qed. + +Lemma Th_mult_one_right : (n:A) n*1 == n. +Intro;Elim mult_sym; EAuto. +Qed. + +Lemma Th_mult_one_right2 : (n:A) n == n*1. +Intro;Elim mult_sym; EAuto. +Qed. + +Lemma Th_opp_mult_right : (x,y:A) -(x*y) == x*(-y). +Intros; Do 2 Rewrite -> (mult_sym x); Auto. +Qed. + +Lemma Th_opp_mult_right2 : (x,y:A) x*(-y) == -(x*y). +Intros; Do 2 Rewrite -> (mult_sym x); Auto. +Qed. + +Lemma Th_plus_opp_opp : (x,y:A) (-x) + (-y) == -(x+y). +Intros. +Apply (aux2 1! x + y); +[ Elim plus_assoc; + Rewrite -> (Th_plus_permute y (-x)); Rewrite -> plus_assoc; + Rewrite -> opp_def; Rewrite plus_zero_left; Auto +| Auto ]. +Qed. + +Lemma Th_plus_permute_opp: (n,m,p:A) (-m)+(n+p) == n+((-m)+p). +EAuto. Qed. + +Lemma Th_opp_opp : (n:A) -(-n) == n. +Intro; Apply (aux2 1! -n); + [ Auto | Elim plus_sym; Auto ]. +Qed. +Hints Resolve Th_opp_opp. + +Lemma Th_opp_opp2 : (n:A) n == -(-n). +Symmetry; EAuto. Qed. + +Lemma Th_mult_opp_opp : (x,y:A) (-x)*(-y) == x*y. +Intros; Rewrite <- Th_opp_mult_left; Rewrite <- Th_opp_mult_right; Auto. +Qed. + +Lemma Th_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y). +Symmetry; Apply Th_mult_opp_opp. Qed. + +Lemma Th_opp_zero : -0 == 0. +Rewrite <- (plus_zero_left (-0)). +Auto. Qed. + +Lemma Th_plus_reg_left : (n,m,p:A) n + m == n + p -> m==p. +Intros; Generalize (congr_eqT ? ? [z] (-n)+z ? ? H). +Repeat Rewrite plus_assoc. +Rewrite (plus_sym (-n) n). +Rewrite opp_def. +Repeat Rewrite Th_plus_zero_left; EAuto. +Qed. + +Lemma Th_plus_reg_right : (n,m,p:A) m + n == p + n -> m==p. +Intros. +EApply Th_plus_reg_left with n. +Rewrite (plus_sym n m). +Rewrite (plus_sym n p). +Auto. +Qed. + +Lemma Th_distr_right : (n,m,p:A) n*(m + p) == (n*m) + (n*p). +Intros. +Repeat Rewrite -> (mult_sym n). +EAuto. +Qed. + +Lemma Th_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p). +Symmetry; Apply Th_distr_right. +Qed. + +End Theory_of_rings. + +Hints Resolve Th_mult_zero_left Th_plus_reg_left : core. + +Unset Implicit Arguments. + +Definition Semi_Ring_Theory_of : + (A:Type)(Aplus : A -> A -> A)(Amult : A -> A -> A)(Aone : A) + (Azero : A)(Aopp : A -> A)(Aeq : A -> A -> bool) + (Ring_Theory Aplus Amult Aone Azero Aopp Aeq) + ->(Semi_Ring_Theory Aplus Amult Aone Azero Aeq). +Intros until 1; Case H. +Split; Intros; Simpl; EAuto. +Defined. + +(* Every ring can be viewed as a semi-ring : this property will be used + in Abstract_polynom. *) +Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory. + + +Section product_ring. + +End product_ring. + +Section power_ring. + +End power_ring. diff --git a/contrib7/ring/Setoid_ring.v b/contrib7/ring/Setoid_ring.v new file mode 100644 index 00000000..222104e5 --- /dev/null +++ b/contrib7/ring/Setoid_ring.v @@ -0,0 +1,13 @@ +(************************************************************************) +(* 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.v,v 1.1.2.1 2004/07/16 19:30:19 herbelin Exp $ *) + +Require Export Setoid_ring_theory. +Require Export Quote. +Require Export Setoid_ring_normalize. 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. diff --git a/contrib7/ring/Setoid_ring_theory.v b/contrib7/ring/Setoid_ring_theory.v new file mode 100644 index 00000000..13afc5ee --- /dev/null +++ b/contrib7/ring/Setoid_ring_theory.v @@ -0,0 +1,429 @@ +(************************************************************************) +(* 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_theory.v,v 1.1.2.1 2004/07/16 19:30:19 herbelin Exp $ *) + +Require Export Bool. +Require Export Setoid. + +Set Implicit Arguments. + +Section Setoid_rings. + +Variable A : Type. +Variable Aequiv : A -> A -> Prop. + +Infix Local "==" Aequiv (at level 5, no associativity). + +Variable S : (Setoid_Theory A Aequiv). + +Add Setoid A Aequiv S. + +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. + +Infix 4 "+" Aplus V8only 50 (left associativity). +Infix 4 "*" Amult V8only 40 (left associativity). +Notation "0" := Azero. +Notation "1" := Aone. +Notation "- x" := (Aopp x) (at level 0) V8only. + +Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2. +Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2. +Variable opp_morph : (a,a0:A) a == a0 -> -a == -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. + +Section Theory_of_semi_setoid_rings. + +Record Semi_Setoid_Ring_Theory : Prop := +{ SSR_plus_sym : (n,m:A) n + m == m + n; + SSR_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; + SSR_mult_sym : (n,m:A) n*m == m*n; + SSR_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; + SSR_plus_zero_left :(n:A) 0 + n == n; + SSR_mult_one_left : (n:A) 1*n == n; + SSR_mult_zero_left : (n:A) 0*n == 0; + SSR_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; + SSR_plus_reg_left : (n,m,p:A)n + m == n + p -> m == p; + SSR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y +}. + +Variable T : Semi_Setoid_Ring_Theory. + +Local plus_sym := (SSR_plus_sym T). +Local plus_assoc := (SSR_plus_assoc T). +Local mult_sym := ( SSR_mult_sym T). +Local mult_assoc := (SSR_mult_assoc T). +Local plus_zero_left := (SSR_plus_zero_left T). +Local mult_one_left := (SSR_mult_one_left T). +Local mult_zero_left := (SSR_mult_zero_left T). +Local distr_left := (SSR_distr_left T). +Local plus_reg_left := (SSR_plus_reg_left T). +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 plus_sym plus_assoc mult_sym mult_assoc + plus_zero_left mult_one_left mult_zero_left distr_left + plus_reg_left equiv_refl (*equiv_sym*). +Hints Immediate equiv_sym. + +(* Lemmas whose form is x=y are also provided in form y=x because + Auto does not symmetry *) +Lemma SSR_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). +Auto. Save. + +Lemma SSR_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). +Auto. Save. + +Lemma SSR_plus_zero_left2 : (n:A) n == 0 + n. +Auto. Save. + +Lemma SSR_mult_one_left2 : (n:A) n == 1*n. +Auto. Save. + +Lemma SSR_mult_zero_left2 : (n:A) 0 == 0*n. +Auto. Save. + +Lemma SSR_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. +Auto. Save. + +Lemma SSR_plus_permute : (n,m,p:A) n+(m+p) == m+(n+p). +Intros. +Rewrite (plus_assoc n m p). +Rewrite (plus_sym n m). +Rewrite <- (plus_assoc m n p). +Trivial. +Save. + +Lemma SSR_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). +Intros. +Rewrite (mult_assoc n m p). +Rewrite (mult_sym n m). +Rewrite <- (mult_assoc m n p). +Trivial. +Save. + +Hints Resolve SSR_plus_permute SSR_mult_permute. + +Lemma SSR_distr_right : (n,m,p:A) n*(m+p) == (n*m) + (n*p). +Intros. +Rewrite (mult_sym n (Aplus m p)). +Rewrite (mult_sym n m). +Rewrite (mult_sym n p). +Auto. +Save. + +Lemma SSR_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p). +Intros. +Apply equiv_sym. +Apply SSR_distr_right. +Save. + +Lemma SSR_mult_zero_right : (n:A) n*0 == 0. +Intro; Rewrite (mult_sym n Azero); Auto. +Save. + +Lemma SSR_mult_zero_right2 : (n:A) 0 == n*0. +Intro; Rewrite (mult_sym n Azero); Auto. +Save. + +Lemma SSR_plus_zero_right :(n:A) n + 0 == n. +Intro; Rewrite (plus_sym n Azero); Auto. +Save. + +Lemma SSR_plus_zero_right2 :(n:A) n == n + 0. +Intro; Rewrite (plus_sym n Azero); Auto. +Save. + +Lemma SSR_mult_one_right : (n:A) n*1 == n. +Intro; Rewrite (mult_sym n Aone); Auto. +Save. + +Lemma SSR_mult_one_right2 : (n:A) n == n*1. +Intro; Rewrite (mult_sym n Aone); Auto. +Save. + +Lemma SSR_plus_reg_right : (n,m,p:A) m+n == p+n -> m==p. +Intros n m p; Rewrite (plus_sym m n); Rewrite (plus_sym p n). +Intro; Apply plus_reg_left with n; Trivial. +Save. + +End Theory_of_semi_setoid_rings. + +Section Theory_of_setoid_rings. + +Record Setoid_Ring_Theory : Prop := +{ STh_plus_sym : (n,m:A) n + m == m + n; + STh_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; + STh_mult_sym : (n,m:A) n*m == m*n; + STh_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; + STh_plus_zero_left :(n:A) 0 + n == n; + STh_mult_one_left : (n:A) 1*n == n; + STh_opp_def : (n:A) n + (-n) == 0; + STh_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; + STh_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y +}. + +Variable T : Setoid_Ring_Theory. + +Local plus_sym := (STh_plus_sym T). +Local plus_assoc := (STh_plus_assoc T). +Local mult_sym := (STh_mult_sym T). +Local mult_assoc := (STh_mult_assoc T). +Local plus_zero_left := (STh_plus_zero_left T). +Local mult_one_left := (STh_mult_one_left T). +Local opp_def := (STh_opp_def T). +Local distr_left := (STh_distr_left T). +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 plus_sym plus_assoc mult_sym mult_assoc + plus_zero_left mult_one_left opp_def distr_left + equiv_refl equiv_sym. + +(* Lemmas whose form is x=y are also provided in form y=x because Auto does + not symmetry *) + +Lemma STh_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). +Auto. Save. + +Lemma STh_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). +Auto. Save. + +Lemma STh_plus_zero_left2 : (n:A) n == 0 + n. +Auto. Save. + +Lemma STh_mult_one_left2 : (n:A) n == 1*n. +Auto. Save. + +Lemma STh_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. +Auto. Save. + +Lemma STh_opp_def2 : (n:A) 0 == n + (-n). +Auto. Save. + +Lemma STh_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p). +Intros. +Rewrite (plus_assoc n m p). +Rewrite (plus_sym n m). +Rewrite <- (plus_assoc m n p). +Trivial. +Save. + +Lemma STh_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). +Intros. +Rewrite (mult_assoc n m p). +Rewrite (mult_sym n m). +Rewrite <- (mult_assoc m n p). +Trivial. +Save. + +Hints Resolve STh_plus_permute STh_mult_permute. + +Lemma Saux1 : (a:A) a + a == a -> a == 0. +Intros. +Rewrite <- (plus_zero_left a). +Rewrite (plus_sym Azero a). +Setoid_replace (Aplus a Azero) with (Aplus a (Aplus a (Aopp a))); Auto. +Rewrite (plus_assoc a a (Aopp a)). +Rewrite H. +Apply opp_def. +Save. + +Lemma STh_mult_zero_left :(n:A) 0*n == 0. +Intros. +Apply Saux1. +Rewrite <- (distr_left Azero Azero n). +Rewrite (plus_zero_left Azero). +Trivial. +Save. +Hints Resolve STh_mult_zero_left. + +Lemma STh_mult_zero_left2 : (n:A) 0 == 0*n. +Auto. +Save. + +Lemma Saux2 : (x,y,z:A) x+y==0 -> x+z==0 -> y == z. +Intros. +Rewrite <- (plus_zero_left y). +Rewrite <- H0. +Rewrite <- (plus_assoc x z y). +Rewrite (plus_sym z y). +Rewrite (plus_assoc x y z). +Rewrite H. +Auto. +Save. + +Lemma STh_opp_mult_left : (x,y:A) -(x*y) == (-x)*y. +Intros. +Apply Saux2 with (Amult x y); Auto. +Rewrite <- (distr_left x (Aopp x) y). +Rewrite (opp_def x). +Auto. +Save. +Hints Resolve STh_opp_mult_left. + +Lemma STh_opp_mult_left2 : (x,y:A) (-x)*y == -(x*y) . +Auto. +Save. + +Lemma STh_mult_zero_right : (n:A) n*0 == 0. +Intro; Rewrite (mult_sym n Azero); Auto. +Save. + +Lemma STh_mult_zero_right2 : (n:A) 0 == n*0. +Intro; Rewrite (mult_sym n Azero); Auto. +Save. + +Lemma STh_plus_zero_right :(n:A) n + 0 == n. +Intro; Rewrite (plus_sym n Azero); Auto. +Save. + +Lemma STh_plus_zero_right2 :(n:A) n == n + 0. +Intro; Rewrite (plus_sym n Azero); Auto. +Save. + +Lemma STh_mult_one_right : (n:A) n*1 == n. +Intro; Rewrite (mult_sym n Aone); Auto. +Save. + +Lemma STh_mult_one_right2 : (n:A) n == n*1. +Intro; Rewrite (mult_sym n Aone); Auto. +Save. + +Lemma STh_opp_mult_right : (x,y:A) -(x*y) == x*(-y). +Intros. +Rewrite (mult_sym x y). +Rewrite (mult_sym x (Aopp y)). +Auto. +Save. + +Lemma STh_opp_mult_right2 : (x,y:A) x*(-y) == -(x*y). +Intros. +Rewrite (mult_sym x y). +Rewrite (mult_sym x (Aopp y)). +Auto. +Save. + +Lemma STh_plus_opp_opp : (x,y:A) (-x) + (-y) == -(x+y). +Intros. +Apply Saux2 with (Aplus x y); Auto. +Rewrite (STh_plus_permute (Aplus x y) (Aopp x) (Aopp y)). +Rewrite <- (plus_assoc x y (Aopp y)). +Rewrite (opp_def y); Rewrite (STh_plus_zero_right x). +Rewrite (STh_opp_def2 x); Trivial. +Save. + +Lemma STh_plus_permute_opp: (n,m,p:A) (-m)+(n+p) == n+((-m)+p). +Auto. +Save. + +Lemma STh_opp_opp : (n:A) -(-n) == n. +Intro. +Apply Saux2 with (Aopp n); Auto. +Rewrite (plus_sym (Aopp n) n); Auto. +Save. +Hints Resolve STh_opp_opp. + +Lemma STh_opp_opp2 : (n:A) n == -(-n). +Auto. +Save. + +Lemma STh_mult_opp_opp : (x,y:A) (-x)*(-y) == x*y. +Intros. +Rewrite (STh_opp_mult_left2 x (Aopp y)). +Rewrite (STh_opp_mult_right2 x y). +Trivial. +Save. + +Lemma STh_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y). +Intros. +Apply equiv_sym. +Apply STh_mult_opp_opp. +Save. + +Lemma STh_opp_zero : -0 == 0. +Rewrite <- (plus_zero_left (Aopp Azero)). +Trivial. +Save. + +Lemma STh_plus_reg_left : (n,m,p:A) n+m == n+p -> m==p. +Intros. +Rewrite <- (plus_zero_left m). +Rewrite <- (plus_zero_left p). +Rewrite <- (opp_def n). +Rewrite (plus_sym n (Aopp n)). +Rewrite <- (plus_assoc (Aopp n) n m). +Rewrite <- (plus_assoc (Aopp n) n p). +Auto. +Save. + +Lemma STh_plus_reg_right : (n,m,p:A) m+n == p+n -> m==p. +Intros. +Apply STh_plus_reg_left with n. +Rewrite (plus_sym n m); Rewrite (plus_sym n p); +Assumption. +Save. + +Lemma STh_distr_right : (n,m,p:A) n*(m+p) == (n*m)+(n*p). +Intros. +Rewrite (mult_sym n (Aplus m p)). +Rewrite (mult_sym n m). +Rewrite (mult_sym n p). +Trivial. +Save. + +Lemma STh_distr_right2 : (n,m,p:A) (n*m)+(n*p) == n*(m+p). +Intros. +Apply equiv_sym. +Apply STh_distr_right. +Save. + +End Theory_of_setoid_rings. + +Hints Resolve STh_mult_zero_left STh_plus_reg_left : core. + +Unset Implicit Arguments. + +Definition Semi_Setoid_Ring_Theory_of : + Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory. +Intros until 1; Case H. +Split; Intros; Simpl; EAuto. +Defined. + +Coercion Semi_Setoid_Ring_Theory_of : + Setoid_Ring_Theory >-> Semi_Setoid_Ring_Theory. + + + +Section product_ring. + +End product_ring. + +Section power_ring. + +End power_ring. + +End Setoid_rings. diff --git a/contrib7/ring/ZArithRing.v b/contrib7/ring/ZArithRing.v new file mode 100644 index 00000000..fc7ef29f --- /dev/null +++ b/contrib7/ring/ZArithRing.v @@ -0,0 +1,35 @@ +(************************************************************************) +(* 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: ZArithRing.v,v 1.1.2.1 2004/07/16 19:30:19 herbelin Exp $ *) + +(* Instantiation of the Ring tactic for the binary integers of ZArith *) + +Require Export ArithRing. +Require Export ZArith_base. +Require Eqdep_dec. + +Definition Zeq := [x,y:Z] + Cases `x ?= y ` of + EGAL => true + | _ => false + end. + +Lemma Zeq_prop : (x,y:Z)(Is_true (Zeq x y)) -> x==y. + Intros x y H; Unfold Zeq in H. + Apply Zcompare_EGAL_eq. + NewDestruct (Zcompare x y); [Reflexivity | Contradiction | Contradiction ]. +Save. + +Definition ZTheory : (Ring_Theory Zplus Zmult `1` `0` Zopp Zeq). + Split; Intros; Apply eq2eqT; EAuto with zarith. + Apply eqT2eq; Apply Zeq_prop; Assumption. +Save. + +(* NatConstants and NatTheory are defined in Ring_theory.v *) +Add Ring Z Zplus Zmult `1` `0` Zopp Zeq ZTheory [POS NEG ZERO xO xI xH]. |