diff options
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/ArithRing.v | 102 | ||||
| -rw-r--r-- | contrib/ring/NArithRing.v | 48 | ||||
| -rw-r--r-- | contrib/ring/Quote.v | 83 | ||||
| -rw-r--r-- | contrib/ring/Ring.v | 26 | ||||
| -rw-r--r-- | contrib/ring/Ring_abstract.v | 1063 | ||||
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 1414 | ||||
| -rw-r--r-- | contrib/ring/Ring_theory.v | 446 | ||||
| -rw-r--r-- | contrib/ring/Setoid_ring.v | 2 | ||||
| -rw-r--r-- | contrib/ring/Setoid_ring_normalize.v | 1930 | ||||
| -rw-r--r-- | contrib/ring/Setoid_ring_theory.v | 692 | ||||
| -rw-r--r-- | contrib/ring/ZArithRing.v | 29 |
11 files changed, 2922 insertions, 2913 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v index 0a49ecb476..6c600e7976 100644 --- a/contrib/ring/ArithRing.v +++ b/contrib/ring/ArithRing.v @@ -12,70 +12,78 @@ Require Export Ring. Require Export Arith. -Require Eqdep_dec. +Require Import 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 +Fixpoint nateq (n m:nat) {struct m} : bool := + match n, m with + | 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. +Lemma nateq_prop : forall 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. + simple induction n; simple induction m; intros; try contradiction. + trivial. + unfold Is_true in H1. + rewrite (H n1 H1). + trivial. +Qed. -Hints Resolve nateq_prop eq2eqT : arithring. +Hint 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. +Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq. + split; intros; auto with arith arithring. + apply eq2eqT; apply (fun n m p:nat => plus_reg_l m p n) with (n := n). + apply eqT2eq; trivial. Defined. -Add Semi Ring nat plus mult (1) (0) nateq NatTheory [O S]. +Add Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ]. -Goal (n:nat)(S n)=(plus (S O) n). -Intro; Reflexivity. +Goal forall n:nat, S n = 1 + 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. +Ltac rewrite_S_to_plus_term t := + match constr:t with + | 1 => constr:1 + | (S ?X1) => + let t1 := rewrite_S_to_plus_term X1 in + constr:(1 + t1) + | (?X1 + ?X2) => + let t1 := rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + constr:(t1 + t2) + | (?X1 * ?X2) => + let t1 := rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + constr:(t1 * t2) + | _ => constr:t + end. (* 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). +Ltac rewrite_S_to_plus := + match goal with + | |- (?X1 = ?X2) => + try + let t1 := + (**) (**) + rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + change (t1 = t2) in |- * + | |- (?X1 = ?X2) => + try + let t1 := + (**) (**) + rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + change (t1 = t2) in |- * + end. -Tactic Definition NatRing := S_to_plus_eq;Ring. +Ltac ring_nat := rewrite_S_to_plus; ring.
\ No newline at end of file diff --git a/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v index 65814a1400..b0a1f19511 100644 --- a/contrib/ring/NArithRing.v +++ b/contrib/ring/NArithRing.v @@ -12,33 +12,33 @@ Require Export Ring. Require Export ZArith_base. -Require NArith. -Require Eqdep_dec. +Require Import NArith. +Require Import Eqdep_dec. -Definition Neq := [n,m:entier] - Cases (Ncompare n m) of - EGAL => true +Definition Neq (n m:N) := + match (n ?= m)%N with + | Datatypes.Eq => 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. +Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m. + intros n m H; unfold Neq in H. + apply Ncompare_Eq_eq. + destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ]. +Qed. -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. +Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N 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. +Qed. -Add Semi Ring entier Nplus Nmult (Pos xH) Nul Neq NTheory [Pos Nul xO xI xH]. +Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
\ No newline at end of file diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v index e2bd0c5378..d50df9776f 100644 --- a/contrib/ring/Quote.v +++ b/contrib/ring/Quote.v @@ -32,54 +32,53 @@ 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 + | 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) {struct v} : A := + match i, v with + | 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 +Fixpoint index_eq (n m:index) {struct m} : bool := + match n, m with + | 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 +Fixpoint index_lt (n m:index) {struct m} : bool := + match n, m with + | 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. +Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m. + simple induction n; simple induction m; simpl in |- *; intros. + rewrite (H i0 H1); reflexivity. + discriminate. + discriminate. + discriminate. + rewrite (H i0 H1); reflexivity. + discriminate. + discriminate. + discriminate. + reflexivity. +Qed. End variables_map. -Unset Implicit Arguments. +Unset Implicit Arguments.
\ No newline at end of file diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v index fa2ba1ca0c..942c41d650 100644 --- a/contrib/ring/Ring.v +++ b/contrib/ring/Ring.v @@ -18,17 +18,19 @@ Require Export Ring_abstract. (* 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. +Definition BoolTheory : + Ring_Theory xorb andb true false (fun b:bool => b) eqb. +split; simpl in |- *. +destruct n; destruct m; reflexivity. +destruct n; destruct m; destruct p; reflexivity. +destruct n; destruct m; reflexivity. +destruct n; destruct m; destruct p; reflexivity. +destruct n; reflexivity. +destruct n; reflexivity. +destruct n; reflexivity. +destruct n; destruct m; destruct p; reflexivity. +destruct x; destruct y; reflexivity || simpl in |- *; tauto. Defined. -Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ]. +Add Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory + [ true false ].
\ No newline at end of file diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index 98b4cb858d..376cfb41f8 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -8,76 +8,75 @@ (* $Id$ *) -Require Ring_theory. -Require Quote. -Require Ring_normalize. +Require Import Ring_theory. +Require Import Quote. +Require Import 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) +Inductive aspolynomial : Type := + | ASPvar : index -> aspolynomial + | ASP0 : aspolynomial + | ASP1 : aspolynomial + | ASPplus : aspolynomial -> aspolynomial -> aspolynomial + | ASPmult : aspolynomial -> aspolynomial -> aspolynomial. + +Inductive abstract_sum : Type := + | Nil_acs : abstract_sum + | Cons_acs : varlist -> abstract_sum -> abstract_sum. + +Fixpoint abstract_sum_merge (s1:abstract_sum) : + abstract_sum -> abstract_sum := + match s1 with + | Cons_acs l1 t1 => + (fix asm_aux (s2:abstract_sum) : abstract_sum := + match s2 with + | Cons_acs l2 t2 => + if varlist_lt l1 l2 + then Cons_acs l1 (abstract_sum_merge t1 s2) + else Cons_acs l2 (asm_aux t2) + | Nil_acs => s1 + end) + | Nil_acs => fun s2 => s2 end. -Fixpoint abstract_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)) +Fixpoint abstract_varlist_insert (l1:varlist) (s2:abstract_sum) {struct s2} : + abstract_sum := + match s2 with + | Cons_acs l2 t2 => + if varlist_lt l1 l2 + then Cons_acs l1 s2 + else Cons_acs l2 (abstract_varlist_insert l1 t2) + | Nil_acs => Cons_acs l1 Nil_acs + end. + +Fixpoint abstract_sum_scalar (l1:varlist) (s2:abstract_sum) {struct s2} : + abstract_sum := + match s2 with + | Cons_acs l2 t2 => + abstract_varlist_insert (varlist_merge l1 l2) + (abstract_sum_scalar l1 t2) + | Nil_acs => Nil_acs + end. + +Fixpoint abstract_sum_prod (s1 s2:abstract_sum) {struct s1} : abstract_sum := + match s1 with + | Cons_acs l1 t1 => + abstract_sum_merge (abstract_sum_scalar l1 s2) + (abstract_sum_prod t1 s2) | Nil_acs => Nil_acs end. -Fixpoint 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) +Fixpoint aspolynomial_normalize (p:aspolynomial) : abstract_sum := + match p with + | ASPvar i => Cons_acs (Cons_var i Nil_var) Nil_acs + | ASP1 => Cons_acs Nil_var Nil_acs | ASP0 => Nil_acs - | (ASPplus l r) => (abstract_sum_merge (aspolynomial_normalize l) - (aspolynomial_normalize r)) - | (ASPmult l r) => (abstract_sum_prod (aspolynomial_normalize l) - (aspolynomial_normalize r)) + | 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. @@ -88,147 +87,151 @@ 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). +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) +Fixpoint interp_asp (p:aspolynomial) : A := + match p with + | ASPvar i => interp_var Azero vm i | ASP0 => Azero | ASP1 => Aone - | (ASPplus l r) => (Aplus (interp_asp l) (interp_asp r)) - | (ASPmult l r) => (Amult (interp_asp l) (interp_asp r)) + | 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) +(* Local *) Definition iacs_aux := + (fix iacs_aux (a:A) (s:abstract_sum) {struct s} : A := + match s with + | Nil_acs => a + | Cons_acs l t => + Aplus a (iacs_aux (interp_vl Amult Aone Azero vm l) t) + end). + +Definition interp_acs (s:abstract_sum) : A := + match s with + | Cons_acs l t => iacs_aux (interp_vl Amult Aone Azero vm l) t | Nil_acs => Azero end. -Hint 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. +Hint Resolve (SR_plus_comm T). +Hint Resolve (SR_plus_assoc T). +Hint Resolve (SR_plus_assoc2 T). +Hint Resolve (SR_mult_comm T). +Hint Resolve (SR_mult_assoc T). +Hint Resolve (SR_mult_assoc2 T). +Hint Resolve (SR_plus_zero_left T). +Hint Resolve (SR_plus_zero_left2 T). +Hint Resolve (SR_mult_one_left T). +Hint Resolve (SR_mult_one_left2 T). +Hint Resolve (SR_mult_zero_left T). +Hint Resolve (SR_mult_zero_left2 T). +Hint Resolve (SR_distr_left T). +Hint Resolve (SR_distr_left2 T). +Hint Resolve (SR_plus_reg_left T). +Hint Resolve (SR_plus_permute T). +Hint Resolve (SR_mult_permute T). +Hint Resolve (SR_distr_right T). +Hint Resolve (SR_distr_right2 T). +Hint Resolve (SR_mult_zero_right T). +Hint Resolve (SR_mult_zero_right2 T). +Hint Resolve (SR_plus_zero_right T). +Hint Resolve (SR_plus_zero_right2 T). +Hint Resolve (SR_mult_one_right T). +Hint Resolve (SR_mult_one_right2 T). +Hint Resolve (SR_plus_reg_right T). +Hint Resolve refl_equal sym_equal trans_equal. (*Hints Resolve refl_eqT sym_eqT trans_eqT.*) -Hints Immediate T. +Hint Immediate T. -Remark iacs_aux_ok : (x:A)(s:abstract_sum) - (iacs_aux x s)==(Aplus x (interp_acs s)). +Remark iacs_aux_ok : + forall (x:A) (s:abstract_sum), iacs_aux x s = Aplus x (interp_acs s). Proof. - Induction s; Simpl; Intros. - Trivial. - Reflexivity. -Save. + simple induction s; simpl in |- *; intros. + trivial. + reflexivity. +Qed. -Hint rew_iacs_aux : core := Extern 10 (eqT A ? ?) Rewrite iacs_aux_ok. +Hint Extern 10 (_ = _ :>A) => rewrite iacs_aux_ok: core. -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)). +Lemma abstract_varlist_insert_ok : + forall (l:varlist) (s:abstract_sum), + interp_acs (abstract_varlist_insert l s) = + Aplus (interp_vl Amult Aone Azero vm l) (interp_acs s). - Induction s. - Trivial. + simple induction s. + trivial. - Simpl; Intros. - Elim (varlist_lt l v); Simpl. - EAuto. - Rewrite iacs_aux_ok. - Rewrite H; Auto. + simpl in |- *; intros. + elim (varlist_lt l v); simpl in |- *. + eauto. + rewrite iacs_aux_ok. + rewrite H; auto. -Save. +Qed. -Lemma abstract_sum_merge_ok : (x,y:abstract_sum) - (interp_acs (abstract_sum_merge x y)) - ==(Aplus (interp_acs x) (interp_acs y)). +Lemma abstract_sum_merge_ok : + forall x y:abstract_sum, + interp_acs (abstract_sum_merge x y) = Aplus (interp_acs x) (interp_acs y). Proof. - Induction x. - Trivial. - Induction y; Intros. + simple induction x. + trivial. + simple induction y; intros. - Auto. + auto. - Simpl; Elim (varlist_lt v v0); Simpl. - Repeat Rewrite iacs_aux_ok. - Rewrite H; Simpl; Auto. + simpl in |- *; elim (varlist_lt v v0); simpl in |- *. + repeat rewrite iacs_aux_ok. + rewrite H; simpl in |- *; auto. - Simpl in H0. - Repeat Rewrite iacs_aux_ok. - Rewrite H0. Simpl; Auto. -Save. + simpl in H0. + repeat rewrite iacs_aux_ok. + rewrite H0. simpl in |- *; auto. +Qed. -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)). +Lemma abstract_sum_scalar_ok : + forall (l:varlist) (s:abstract_sum), + interp_acs (abstract_sum_scalar l s) = + Amult (interp_vl Amult Aone Azero vm l) (interp_acs s). Proof. - Induction s. - Simpl; EAuto. + simple induction s. + simpl in |- *; 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. + simpl in |- *; intros. + rewrite iacs_aux_ok. + rewrite abstract_varlist_insert_ok. + rewrite H. + rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). + auto. +Qed. -Lemma abstract_sum_prod_ok : (x,y:abstract_sum) - (interp_acs (abstract_sum_prod x y)) - == (Amult (interp_acs x) (interp_acs y)). +Lemma abstract_sum_prod_ok : + forall x y:abstract_sum, + interp_acs (abstract_sum_prod x y) = Amult (interp_acs x) (interp_acs y). Proof. - Induction x. - Intros; Simpl; EAuto. + simple induction x. + intros; simpl in |- *; eauto. - NewDestruct y; Intros. + destruct y as [| v0 a0]; intros. - Simpl; Rewrite H; EAuto. + simpl in |- *; 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. + unfold abstract_sum_prod in |- *; fold abstract_sum_prod in |- *. + rewrite abstract_sum_merge_ok. + rewrite abstract_sum_scalar_ok. + rewrite H; simpl in |- *; auto. +Qed. -Theorem aspolynomial_normalize_ok : (x:aspolynomial) - (interp_asp x)==(interp_acs (aspolynomial_normalize x)). +Theorem aspolynomial_normalize_ok : + forall 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. + simple induction x; simpl in |- *; intros; trivial. + rewrite abstract_sum_merge_ok. + rewrite H; rewrite H0; eauto. + rewrite abstract_sum_prod_ok. + rewrite H; rewrite H0; eauto. +Qed. End abstract_semi_rings. @@ -244,143 +247,141 @@ Section abstract_rings. 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 -. +Inductive apolynomial : Type := + | APvar : index -> apolynomial + | AP0 : apolynomial + | AP1 : apolynomial + | APplus : apolynomial -> apolynomial -> apolynomial + | APmult : apolynomial -> apolynomial -> apolynomial + | APopp : apolynomial -> apolynomial. (* A canonical "abstract" sum is a list of varlist with the sign "+" or "-". Invariant : the list is sorted and there is no varlist is present with both signs. +x +x +x -x is forbidden => the canonical form is +x+x *) -Inductive signed_sum : Type := -| Nil_varlist : signed_sum -| Plus_varlist : varlist -> signed_sum -> signed_sum -| Minus_varlist : varlist -> signed_sum -> signed_sum -. - -Fixpoint signed_sum_merge [s1:signed_sum] - : signed_sum -> signed_sum := -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) +Inductive signed_sum : Type := + | Nil_varlist : signed_sum + | Plus_varlist : varlist -> signed_sum -> signed_sum + | Minus_varlist : varlist -> signed_sum -> signed_sum. + +Fixpoint signed_sum_merge (s1:signed_sum) : signed_sum -> signed_sum := + match s1 with + | Plus_varlist l1 t1 => + (fix ssm_aux (s2:signed_sum) : signed_sum := + match s2 with + | Plus_varlist l2 t2 => + if varlist_lt l1 l2 + then Plus_varlist l1 (signed_sum_merge t1 s2) + else Plus_varlist l2 (ssm_aux t2) + | Minus_varlist l2 t2 => + if varlist_eq l1 l2 + then signed_sum_merge t1 t2 + else + if varlist_lt l1 l2 + then Plus_varlist l1 (signed_sum_merge t1 s2) + else Minus_varlist l2 (ssm_aux t2) + | Nil_varlist => s1 + end) + | Minus_varlist l1 t1 => + (fix ssm_aux2 (s2:signed_sum) : signed_sum := + match s2 with + | Plus_varlist l2 t2 => + if varlist_eq l1 l2 + then signed_sum_merge t1 t2 + else + if varlist_lt l1 l2 + then Minus_varlist l1 (signed_sum_merge t1 s2) + else Plus_varlist l2 (ssm_aux2 t2) + | Minus_varlist l2 t2 => + if varlist_lt l1 l2 + then Minus_varlist l1 (signed_sum_merge t1 s2) + else Minus_varlist l2 (ssm_aux2 t2) + | Nil_varlist => s1 + end) + | Nil_varlist => fun s2 => s2 end. -Fixpoint 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) +Fixpoint plus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} : + signed_sum := + match s2 with + | Plus_varlist l2 t2 => + if varlist_lt l1 l2 + then Plus_varlist l1 s2 + else Plus_varlist l2 (plus_varlist_insert l1 t2) + | Minus_varlist l2 t2 => + if varlist_eq l1 l2 + then t2 + else + if varlist_lt l1 l2 + then Plus_varlist l1 s2 + else Minus_varlist l2 (plus_varlist_insert l1 t2) + | Nil_varlist => Plus_varlist l1 Nil_varlist end. -Fixpoint 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)) +Fixpoint minus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} : + signed_sum := + match s2 with + | Plus_varlist l2 t2 => + if varlist_eq l1 l2 + then t2 + else + if varlist_lt l1 l2 + then Minus_varlist l1 s2 + else Plus_varlist l2 (minus_varlist_insert l1 t2) + | Minus_varlist l2 t2 => + if varlist_lt l1 l2 + then Minus_varlist l1 s2 + else Minus_varlist l2 (minus_varlist_insert l1 t2) + | Nil_varlist => Minus_varlist l1 Nil_varlist + end. + +Fixpoint signed_sum_opp (s:signed_sum) : signed_sum := + match s with + | Plus_varlist l2 t2 => Minus_varlist l2 (signed_sum_opp t2) + | Minus_varlist l2 t2 => Plus_varlist l2 (signed_sum_opp t2) | Nil_varlist => Nil_varlist end. -Fixpoint plus_sum_scalar [l1:varlist; s2:signed_sum] - : 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)) +Fixpoint plus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} : + signed_sum := + match s2 with + | Plus_varlist l2 t2 => + plus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2) + | Minus_varlist l2 t2 => + minus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2) + | Nil_varlist => Nil_varlist + end. + +Fixpoint minus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} : + signed_sum := + match s2 with + | Plus_varlist l2 t2 => + minus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2) + | Minus_varlist l2 t2 => + plus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2) | Nil_varlist => Nil_varlist end. -Fixpoint 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)) +Fixpoint signed_sum_prod (s1 s2:signed_sum) {struct s1} : signed_sum := + match s1 with + | Plus_varlist l1 t1 => + signed_sum_merge (plus_sum_scalar l1 s2) (signed_sum_prod t1 s2) + | Minus_varlist l1 t1 => + signed_sum_merge (minus_sum_scalar l1 s2) (signed_sum_prod t1 s2) | Nil_varlist => Nil_varlist end. -Fixpoint 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) +Fixpoint apolynomial_normalize (p:apolynomial) : signed_sum := + match p with + | APvar i => Plus_varlist (Cons_var i Nil_var) Nil_varlist + | AP1 => Plus_varlist Nil_var Nil_varlist | AP0 => Nil_varlist - | (APplus l r) => (signed_sum_merge (apolynomial_normalize l) - (apolynomial_normalize r)) - | (APmult l r) => (signed_sum_prod (apolynomial_normalize l) - (apolynomial_normalize r)) - | (APopp q) => (signed_sum_opp (apolynomial_normalize q)) + | 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. @@ -389,311 +390,315 @@ Variable Aplus : A -> A -> A. Variable Amult : A -> A -> A. Variable Aone : A. Variable Azero : A. -Variable Aopp :A -> 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) +Variable vm : varmap A. +Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq. + +(* Local *) Definition isacs_aux := + (fix isacs_aux (a:A) (s:signed_sum) {struct s} : A := + match s with + | Nil_varlist => a + | Plus_varlist l t => + Aplus a (isacs_aux (interp_vl Amult Aone Azero vm l) t) + | Minus_varlist l t => + Aplus a + (isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t) + end). + +Definition interp_sacs (s:signed_sum) : A := + match s with + | Plus_varlist l t => isacs_aux (interp_vl Amult Aone Azero vm l) t + | Minus_varlist l t => isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t | Nil_varlist => Azero end. -Fixpoint interp_ap [p:apolynomial] : A := - Cases p of - | (APvar i) => (interp_var Azero vm i) +Fixpoint interp_ap (p:apolynomial) : A := + match p with + | APvar i => interp_var Azero vm i | AP0 => Azero | AP1 => Aone - | (APplus l r) => (Aplus (interp_ap l) (interp_ap r)) - | (APmult l r) => (Amult (interp_ap l) (interp_ap r)) - | (APopp q) => (Aopp (interp_ap q)) + | 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. +Hint Resolve (Th_plus_comm T). +Hint Resolve (Th_plus_assoc T). +Hint Resolve (Th_plus_assoc2 T). +Hint Resolve (Th_mult_sym T). +Hint Resolve (Th_mult_assoc T). +Hint Resolve (Th_mult_assoc2 T). +Hint Resolve (Th_plus_zero_left T). +Hint Resolve (Th_plus_zero_left2 T). +Hint Resolve (Th_mult_one_left T). +Hint Resolve (Th_mult_one_left2 T). +Hint Resolve (Th_mult_zero_left T). +Hint Resolve (Th_mult_zero_left2 T). +Hint Resolve (Th_distr_left T). +Hint Resolve (Th_distr_left2 T). +Hint Resolve (Th_plus_reg_left T). +Hint Resolve (Th_plus_permute T). +Hint Resolve (Th_mult_permute T). +Hint Resolve (Th_distr_right T). +Hint Resolve (Th_distr_right2 T). +Hint Resolve (Th_mult_zero_right2 T). +Hint Resolve (Th_plus_zero_right T). +Hint Resolve (Th_plus_zero_right2 T). +Hint Resolve (Th_mult_one_right T). +Hint Resolve (Th_mult_one_right2 T). +Hint Resolve (Th_plus_reg_right T). +Hint Resolve refl_equal sym_equal trans_equal. (*Hints Resolve refl_eqT sym_eqT trans_eqT.*) -Hints Immediate T. +Hint Immediate T. -Lemma isacs_aux_ok : (x:A)(s:signed_sum) - (isacs_aux x s)==(Aplus x (interp_sacs s)). +Lemma isacs_aux_ok : + forall (x:A) (s:signed_sum), isacs_aux x s = Aplus x (interp_sacs s). Proof. - Induction s; Simpl; Intros. - Trivial. - Reflexivity. - Reflexivity. -Save. + simple induction s; simpl in |- *; intros. + trivial. + reflexivity. + reflexivity. +Qed. -Hint rew_isacs_aux : core := Extern 10 (eqT A ? ?) Rewrite isacs_aux_ok. +Hint Extern 10 (_ = _ :>A) => rewrite isacs_aux_ok: core. -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 ]. +Ltac solve1 v v0 H H0 := + simpl in |- *; elim (varlist_lt v v0); simpl in |- *; rewrite isacs_aux_ok; + [ rewrite H; simpl in |- *; auto | simpl in H0; rewrite H0; auto ]. -Lemma signed_sum_merge_ok : (x,y:signed_sum) - (interp_sacs (signed_sum_merge x y)) - ==(Aplus (interp_sacs x) (interp_sacs y)). +Lemma signed_sum_merge_ok : + forall x y:signed_sum, + interp_sacs (signed_sum_merge x y) = Aplus (interp_sacs x) (interp_sacs y). - Induction x. - Intro; Simpl; Auto. + simple induction x. + intro; simpl in |- *; auto. - Induction y; Intros. + simple induction y; intros. - Auto. + auto. - Solve1 v v0 H H0. + solve1 v v0 H H0. - Simpl; Generalize (varlist_eq_prop v v0). - Elim (varlist_eq v v0); Simpl. + simpl in |- *; generalize (varlist_eq_prop v v0). + elim (varlist_eq v v0); simpl in |- *. - 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. + intro Heq; rewrite (Heq I). + rewrite H. + repeat rewrite isacs_aux_ok. + rewrite (Th_plus_permute T). + repeat rewrite (Th_plus_assoc T). + rewrite + (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v0)) + (interp_vl Amult Aone Azero vm v0)). + rewrite (Th_opp_def T). + rewrite (Th_plus_zero_left T). + reflexivity. - Solve1 v v0 H H0. + solve1 v v0 H H0. - Induction y; Intros. + simple induction y; intros. - Auto. + auto. - Simpl; Generalize (varlist_eq_prop v v0). - Elim (varlist_eq v v0); Simpl. + simpl in |- *; generalize (varlist_eq_prop v v0). + elim (varlist_eq v v0); simpl in |- *. - 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. + 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. - Solve1 v v0 H H0. + solve1 v v0 H H0. -Save. +Qed. -Tactic Definition Solve2 l v H := - Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok; - [ Auto - | Rewrite H; Auto ]. +Ltac solve2 l v H := + elim (varlist_lt l v); simpl in |- *; rewrite isacs_aux_ok; + [ auto | rewrite H; auto ]. -Lemma plus_varlist_insert_ok : (l:varlist)(s:signed_sum) - (interp_sacs (plus_varlist_insert l s)) - == (Aplus (interp_vl Amult Aone Azero vm l) (interp_sacs s)). +Lemma plus_varlist_insert_ok : + forall (l:varlist) (s:signed_sum), + interp_sacs (plus_varlist_insert l s) = + Aplus (interp_vl Amult Aone Azero vm l) (interp_sacs s). Proof. - Induction s. - Trivial. + simple induction s. + trivial. - Simpl; Intros. - Solve2 l v H. + simpl in |- *; intros. + solve2 l v H. - Simpl; Intros. - Generalize (varlist_eq_prop l v). - Elim (varlist_eq l v); Simpl. + simpl in |- *; intros. + generalize (varlist_eq_prop l v). + elim (varlist_eq l v); simpl in |- *. - 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. + 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. + solve2 l v H. -Save. +Qed. -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)). +Lemma minus_varlist_insert_ok : + forall (l:varlist) (s:signed_sum), + interp_sacs (minus_varlist_insert l s) = + Aplus (Aopp (interp_vl Amult Aone Azero vm l)) (interp_sacs s). Proof. - Induction s. - Trivial. + simple induction s. + trivial. - Simpl; Intros. - Generalize (varlist_eq_prop l v). - Elim (varlist_eq l v); Simpl. + simpl in |- *; intros. + generalize (varlist_eq_prop l v). + elim (varlist_eq l v); simpl in |- *. - 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. + intro Heq; rewrite (Heq I). + repeat rewrite isacs_aux_ok. + repeat rewrite (Th_plus_assoc T). + rewrite + (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v)) + (interp_vl Amult Aone Azero vm v)). + rewrite (Th_opp_def T). + auto. - Simpl; Intros. - Solve2 l v H. + simpl in |- *; intros. + solve2 l v H. - Simpl; Intros; Solve2 l v H. + simpl in |- *; intros; solve2 l v H. -Save. +Qed. -Lemma signed_sum_opp_ok : (s:signed_sum) - (interp_sacs (signed_sum_opp s)) - == (Aopp (interp_sacs s)). +Lemma signed_sum_opp_ok : + forall s:signed_sum, interp_sacs (signed_sum_opp s) = Aopp (interp_sacs s). Proof. - Induction s; Simpl; Intros. + simple induction s; simpl in |- *; intros. - Symmetry; Apply (Th_opp_zero T). + symmetry in |- *; 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). + reflexivity. - Repeat Rewrite isacs_aux_ok. - Rewrite H. - Rewrite <- (Th_plus_opp_opp T). - Rewrite (Th_opp_opp T). - Reflexivity. + repeat rewrite isacs_aux_ok. + rewrite H. + rewrite <- (Th_plus_opp_opp T). + rewrite (Th_opp_opp T). + reflexivity. -Save. +Qed. -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)). +Lemma plus_sum_scalar_ok : + forall (l:varlist) (s:signed_sum), + interp_sacs (plus_sum_scalar l s) = + Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s). Proof. - 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))). + simple induction s. + trivial. + + simpl in |- *; 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 in |- *; intros. + rewrite minus_varlist_insert_ok. + repeat rewrite isacs_aux_ok. + rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). + rewrite H. + rewrite (Th_distr_right T). + rewrite <- (Th_opp_mult_right T). + reflexivity. + +Qed. + +Lemma minus_sum_scalar_ok : + forall (l:varlist) (s:signed_sum), + interp_sacs (minus_sum_scalar l s) = + Aopp (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)). Proof. - 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)). + simple induction s; simpl in |- *; intros. + + rewrite (Th_mult_zero_right T); symmetry in |- *; apply (Th_opp_zero T). + + simpl in |- *; 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 in |- *; intros. + rewrite plus_varlist_insert_ok. + repeat rewrite isacs_aux_ok. + rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T). + rewrite H. + rewrite (Th_distr_right T). + rewrite <- (Th_opp_mult_right T). + rewrite <- (Th_plus_opp_opp T). + rewrite (Th_opp_opp T). + reflexivity. + +Qed. + +Lemma signed_sum_prod_ok : + forall x y:signed_sum, + interp_sacs (signed_sum_prod x y) = Amult (interp_sacs x) (interp_sacs y). Proof. - Induction x. + simple induction x. - Simpl; EAuto 1. + simpl in |- *; eauto 1. - Intros; Simpl. - Rewrite signed_sum_merge_ok. - Rewrite plus_sum_scalar_ok. - Repeat Rewrite isacs_aux_ok. - Rewrite H. - Auto. + intros; simpl in |- *. + 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. + intros; simpl in |- *. + 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. +Qed. -Theorem apolynomial_normalize_ok : (p:apolynomial) - (interp_sacs (apolynomial_normalize p))==(interp_ap p). +Theorem apolynomial_normalize_ok : + forall 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. + simple induction p; simpl in |- *; auto 1. + intros. + rewrite signed_sum_merge_ok. + rewrite H; rewrite H0; reflexivity. + intros. + rewrite signed_sum_prod_ok. + rewrite H; rewrite H0; reflexivity. + intros. + rewrite signed_sum_opp_ok. + rewrite H; reflexivity. +Qed. + +End abstract_rings.
\ No newline at end of file diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 94ad71ffc8..faa892ce59 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -8,19 +8,19 @@ (* $Id$ *) -Require Ring_theory. -Require Quote. +Require Import Ring_theory. +Require Import Quote. Set Implicit Arguments. -Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m. +Lemma index_eq_prop : forall 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. + intros. + apply index_eq_prop. + generalize H. + case (index_eq n m); simpl in |- *; trivial; intros. + contradiction. +Qed. Section semi_rings. @@ -49,16 +49,14 @@ Variable Aeq : A -> A -> bool. (* 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 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 -. +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 *) @@ -75,199 +73,203 @@ Inductive canonical_sum : Type := 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 +Fixpoint varlist_eq (x y:varlist) {struct y} : bool := + match x, y with + | Nil_var, Nil_var => true + | Cons_var i xrest, Cons_var j yrest => + andb (index_eq i j) (varlist_eq xrest yrest) + | _, _ => false end. -Fixpoint varlist_lt [x,y:varlist] : 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 +Fixpoint varlist_lt (x y:varlist) {struct y} : bool := + match x, y with + | Nil_var, Cons_var _ _ => true + | Cons_var i xrest, Cons_var j yrest => + if index_lt i j + then true + else andb (index_eq i j) (varlist_lt xrest yrest) + | _, _ => false end. (* 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 +Fixpoint varlist_merge (l1:varlist) : varlist -> varlist := + match l1 with + | Cons_var v1 t1 => + (fix vm_aux (l2:varlist) : varlist := + match l2 with + | Cons_var v2 t2 => + if index_lt v1 v2 + then Cons_var v1 (varlist_merge t1 l2) + else Cons_var v2 (vm_aux t2) + | Nil_var => l1 + end) + | Nil_var => fun l2 => l2 end. (* 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. +Fixpoint canonical_sum_merge (s1:canonical_sum) : + canonical_sum -> canonical_sum := + match s1 with + | Cons_monom c1 l1 t1 => + (fix csm_aux (s2:canonical_sum) : canonical_sum := + match s2 with + | Cons_monom c2 l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2) + else + if varlist_lt l1 l2 + then Cons_monom c1 l1 (canonical_sum_merge t1 s2) + else Cons_monom c2 l2 (csm_aux t2) + | Cons_varlist l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2) + else + if varlist_lt l1 l2 + then Cons_monom c1 l1 (canonical_sum_merge t1 s2) + else Cons_varlist l2 (csm_aux t2) + | Nil_monom => s1 + end) + | Cons_varlist l1 t1 => + (fix csm_aux2 (s2:canonical_sum) : canonical_sum := + match s2 with + | Cons_monom c2 l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2) + else + if varlist_lt l1 l2 + then Cons_varlist l1 (canonical_sum_merge t1 s2) + else Cons_monom c2 l2 (csm_aux2 t2) + | Cons_varlist l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2) + else + if varlist_lt l1 l2 + then Cons_varlist l1 (canonical_sum_merge t1 s2) + else Cons_varlist l2 (csm_aux2 t2) + | Nil_monom => s1 + end) + | Nil_monom => fun s2 => s2 + end. (* 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) +Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} : + canonical_sum := + match s2 with + | Cons_monom c2 l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus c1 c2) l1 t2 + else + if varlist_lt l1 l2 + then Cons_monom c1 l1 s2 + else Cons_monom c2 l2 (monom_insert c1 l1 t2) + | Cons_varlist l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus c1 Aone) l1 t2 + else + if varlist_lt l1 l2 + then Cons_monom c1 l1 s2 + else Cons_varlist l2 (monom_insert c1 l1 t2) + | Nil_monom => Cons_monom c1 l1 Nil_monom end. -Fixpoint varlist_insert [l1:varlist; s2:canonical_sum] - : 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) +Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} : + canonical_sum := + match s2 with + | Cons_monom c2 l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus Aone c2) l1 t2 + else + if varlist_lt l1 l2 + then Cons_varlist l1 s2 + else Cons_monom c2 l2 (varlist_insert l1 t2) + | Cons_varlist l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus Aone Aone) l1 t2 + else + if varlist_lt l1 l2 + then Cons_varlist l1 s2 + else Cons_varlist l2 (varlist_insert l1 t2) + | Nil_monom => Cons_varlist l1 Nil_monom end. (* 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. +Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} : + canonical_sum := + match s with + | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t) + | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t) + | Nil_monom => Nil_monom + end. (* 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. +Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} : + canonical_sum := + match s with + | Cons_monom c l t => + monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) + | Cons_varlist l t => + varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) + | Nil_monom => Nil_monom + end. (* 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. +Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) + (s:canonical_sum) {struct s} : canonical_sum := + match s with + | Cons_monom c l t => + monom_insert (Amult c0 c) (varlist_merge l0 l) + (canonical_sum_scalar3 c0 l0 t) + | Cons_varlist l t => + monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t) + | Nil_monom => Nil_monom + end. (* 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. +Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} : + canonical_sum := + match s1 with + | Cons_monom c1 l1 t1 => + canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2) + (canonical_sum_prod t1 s2) + | Cons_varlist l1 t1 => + canonical_sum_merge (canonical_sum_scalar2 l1 s2) + (canonical_sum_prod t1 s2) + | Nil_monom => Nil_monom + end. (* 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)) +Inductive spolynomial : Type := + | SPvar : index -> spolynomial + | SPconst : A -> spolynomial + | SPplus : spolynomial -> spolynomial -> spolynomial + | SPmult : spolynomial -> spolynomial -> spolynomial. + +Fixpoint spolynomial_normalize (p:spolynomial) : canonical_sum := + match p with + | 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)) +Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum := + match s with + | Cons_monom c l t => + if Aeq c Azero + then canonical_sum_simplify t + else + if Aeq c Aone + then Cons_varlist l (canonical_sum_simplify t) + else Cons_monom c l (canonical_sum_simplify t) + | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t) | Nil_monom => Nil_monom end. -Definition spolynomial_simplify := - [x:spolynomial](canonical_sum_simplify (spolynomial_normalize x)). +Definition spolynomial_simplify (x:spolynomial) := + canonical_sum_simplify (spolynomial_normalize x). (* End definitions. *) @@ -277,7 +279,7 @@ Definition spolynomial_simplify := acording to a certain variables map. Once again the choosen definition is generic and could be changed ****) -Variable vm : (varmap A). +Variable vm : varmap A. (* Interpretation of list of variables * [x1; ... ; xn ] is interpreted as (find v x1)* ... *(find v xn) @@ -285,50 +287,49 @@ Variable vm : (varmap A). * 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). +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}. +(* Local *) Definition ivl_aux := + (fix ivl_aux (x:index) (t:varlist) {struct t} : A := + match t with + | Nil_var => interp_var x + | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t') + end). -Definition interp_vl := [l:varlist] - Cases l of +Definition interp_vl (l:varlist) := + match l with | Nil_var => Aone - | (Cons_var x t) => (ivl_aux x t) + | 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 interp_m (c:A) (l:varlist) := + match l with + | 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}. +(* Local *) Definition ics_aux := + (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A := + match s with + | Nil_monom => a + | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t) + | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t) + end). (* Interpretation of a canonical sum *) -Definition interp_cs : canonical_sum -> A := - [s]Cases s of +Definition interp_cs (s:canonical_sum) : A := + match s with | Nil_monom => Azero - | (Cons_varlist l t) => - (ics_aux (interp_vl l) t) - | (Cons_monom c l t) => - (ics_aux (interp_m c l) t) + | 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)) +Fixpoint interp_sp (p:spolynomial) : A := + match p with + | 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. @@ -338,415 +339,420 @@ 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. +Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq. + +Hint Resolve (SR_plus_comm T). +Hint Resolve (SR_plus_assoc T). +Hint Resolve (SR_plus_assoc2 T). +Hint Resolve (SR_mult_comm T). +Hint Resolve (SR_mult_assoc T). +Hint Resolve (SR_mult_assoc2 T). +Hint Resolve (SR_plus_zero_left T). +Hint Resolve (SR_plus_zero_left2 T). +Hint Resolve (SR_mult_one_left T). +Hint Resolve (SR_mult_one_left2 T). +Hint Resolve (SR_mult_zero_left T). +Hint Resolve (SR_mult_zero_left2 T). +Hint Resolve (SR_distr_left T). +Hint Resolve (SR_distr_left2 T). +Hint Resolve (SR_plus_reg_left T). +Hint Resolve (SR_plus_permute T). +Hint Resolve (SR_mult_permute T). +Hint Resolve (SR_distr_right T). +Hint Resolve (SR_distr_right2 T). +Hint Resolve (SR_mult_zero_right T). +Hint Resolve (SR_mult_zero_right2 T). +Hint Resolve (SR_plus_zero_right T). +Hint Resolve (SR_plus_zero_right2 T). +Hint Resolve (SR_mult_one_right T). +Hint Resolve (SR_mult_one_right2 T). +Hint Resolve (SR_plus_reg_right T). +Hint Resolve refl_equal sym_equal trans_equal. (* Hints Resolve refl_eqT sym_eqT trans_eqT. *) -Hints Immediate T. +Hint Immediate T. -Lemma varlist_eq_prop : (x,y:varlist) - (Is_true (varlist_eq x y))->x==y. +Lemma varlist_eq_prop : forall 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)). + simple induction x; simple induction y; contradiction || (try reflexivity). + simpl in |- *; intros. + generalize (andb_prop2 _ _ H1); intros; elim H2; intros. + rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity. +Qed. + +Remark ivl_aux_ok : + forall (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)). + simple induction v; simpl in |- *; intros. + trivial. + rewrite H; trivial. +Qed. + +Lemma varlist_merge_ok : + forall 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)). + simple induction x. + simpl in |- *; trivial. + simple induction y. + simpl in |- *; trivial. + simpl in |- *; intros. + elim (index_lt i i0); simpl in |- *; intros. + + repeat rewrite ivl_aux_ok. + rewrite H. simpl in |- *. + rewrite ivl_aux_ok. + eauto. + + repeat rewrite ivl_aux_ok. + rewrite H0. + rewrite ivl_aux_ok. + eauto. +Qed. + +Remark ics_aux_ok : + forall (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)). + simple induction s; simpl in |- *; intros. + trivial. + reflexivity. + reflexivity. +Qed. + +Remark interp_m_ok : + forall (x:A) (l:varlist), interp_m x l = Amult x (interp_vl l). Proof. - NewDestruct l. - Simpl; Trivial. - Reflexivity. -Save. + destruct l as [| i v]. + simpl in |- *; trivial. + reflexivity. +Qed. -Lemma canonical_sum_merge_ok : (x,y:canonical_sum) - (interp_cs (canonical_sum_merge x y)) - ==(Aplus (interp_cs x) (interp_cs y)). +Lemma canonical_sum_merge_ok : + forall x y:canonical_sum, + interp_cs (canonical_sum_merge x y) = Aplus (interp_cs x) (interp_cs y). -Induction x; Simpl. -Trivial. +simple induction x; simpl in |- *. +trivial. -Induction y; Simpl; Intros. +simple induction y; simpl in |- *; intros. (* monom and nil *) -EAuto. +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. +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *; repeat rewrite ics_aux_ok; rewrite H. +repeat rewrite interp_m_ok. +rewrite (SR_distr_left T). +repeat rewrite <- (SR_plus_assoc T). +apply f_equal with (f := Aplus (Amult a (interp_vl v0))). +trivial. + +elim (varlist_lt v v0); simpl in |- *. +repeat rewrite ics_aux_ok. +rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. + +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; + 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. +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *; repeat rewrite ics_aux_ok; rewrite H. +repeat rewrite interp_m_ok. +rewrite (SR_distr_left T). +repeat rewrite <- (SR_plus_assoc T). +apply f_equal with (f := Aplus (Amult a (interp_vl v0))). +rewrite (SR_mult_one_left T). +trivial. + +elim (varlist_lt v v0); simpl in |- *. +repeat rewrite ics_aux_ok. +rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; + eauto. + +simple induction y; simpl in |- *; intros. (* varlist and nil *) -Trivial. +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. +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *; 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 f_equal with (f := Aplus (interp_vl v0)). +trivial. + +elim (varlist_lt v v0); simpl in |- *. +repeat rewrite ics_aux_ok. +rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; + 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. +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *; 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 f_equal with (f := Aplus (interp_vl v0)). +trivial. + +elim (varlist_lt v v0); simpl in |- *. +repeat rewrite ics_aux_ok. +rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto. +rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *; + eauto. +Qed. + +Lemma monom_insert_ok : + forall (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; simple induction s0. + +simpl in |- *; rewrite interp_m_ok; trivial. + +simpl in |- *; intros. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *; 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 in |- *; + [ 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 in |- *; intros. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *; 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 in |- *; + [ 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 ]. +Qed. 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. + forall (l:varlist) (s:canonical_sum), + interp_cs (varlist_insert l s) = Aplus (interp_vl l) (interp_cs s). +intros; generalize s; simple induction s0. + +simpl in |- *; trivial. + +simpl in |- *; intros. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *; 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 in |- *; + [ 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 in |- *; intros. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *; 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 in |- *; + [ 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 ]. +Qed. + +Lemma canonical_sum_scalar_ok : + forall (a:A) (s:canonical_sum), + interp_cs (canonical_sum_scalar a s) = Amult a (interp_cs s). +simple induction s. +simpl in |- *; eauto. + +simpl in |- *; 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 in |- *; 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. +Qed. + +Lemma canonical_sum_scalar2_ok : + forall (l:varlist) (s:canonical_sum), + interp_cs (canonical_sum_scalar2 l s) = Amult (interp_vl l) (interp_cs s). +simple induction s. +simpl in |- *; trivial. + +simpl in |- *; 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 in |- *; 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. +Qed. + +Lemma canonical_sum_scalar3_ok : + forall (c:A) (l:varlist) (s:canonical_sum), + interp_cs (canonical_sum_scalar3 c l s) = + Amult c (Amult (interp_vl l) (interp_cs s)). +simple induction s. +simpl in |- *; repeat rewrite (SR_mult_zero_right T); reflexivity. + +simpl in |- *; 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 in |- *; 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. +Qed. + +Lemma canonical_sum_prod_ok : + forall x y:canonical_sum, + interp_cs (canonical_sum_prod x y) = Amult (interp_cs x) (interp_cs y). +simple induction x; simpl in |- *; 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 in |- *. +eauto. + +rewrite canonical_sum_merge_ok. +rewrite canonical_sum_scalar2_ok. +rewrite ics_aux_ok. +rewrite H. +trivial. +Qed. + +Theorem spolynomial_normalize_ok : + forall p:spolynomial, interp_cs (spolynomial_normalize p) = interp_sp p. +simple induction p; simpl in |- *; intros. + +reflexivity. +reflexivity. + +rewrite canonical_sum_merge_ok. +rewrite H; rewrite H0. +reflexivity. + +rewrite canonical_sum_prod_ok. +rewrite H; rewrite H0. +reflexivity. +Qed. + +Lemma canonical_sum_simplify_ok : + forall s:canonical_sum, interp_cs (canonical_sum_simplify s) = interp_cs s. +simple 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. +simpl in |- *; intros. +generalize (SR_eq_prop T a 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 in |- *. +generalize (SR_eq_prop T a Aone). +elim (Aeq a Aone). +intro Heq; rewrite (Heq I). +simpl in |- *. +repeat rewrite ics_aux_ok. +rewrite interp_m_ok. +rewrite H. +rewrite (SR_mult_one_left T). +reflexivity. + +simpl in |- *. +repeat rewrite ics_aux_ok. +rewrite interp_m_ok. +rewrite H. +reflexivity. (* cons_varlist *) -Simpl; Intros. -Repeat Rewrite ics_aux_ok. -Rewrite H. -Reflexivity. +simpl in |- *; intros. +repeat rewrite ics_aux_ok. +rewrite H. +reflexivity. -Save. +Qed. -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. +Theorem spolynomial_simplify_ok : + forall p:spolynomial, interp_cs (spolynomial_simplify p) = interp_sp p. +intro. +unfold spolynomial_simplify in |- *. +rewrite canonical_sum_simplify_ok. +apply spolynomial_normalize_ok. +Qed. (* End properties. *) End semi_rings. -Implicits Cons_varlist. -Implicits Cons_monom. -Implicits SPconst. -Implicits SPplus. -Implicits SPmult. +Implicit Arguments Cons_varlist. +Implicit Arguments Cons_monom. +Implicit Arguments SPconst. +Implicit Arguments SPplus. +Implicit Arguments SPmult. Section rings. @@ -761,133 +767,135 @@ 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. +Variable vm : varmap A. +Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq. + +Hint Resolve (Th_plus_comm T). +Hint Resolve (Th_plus_assoc T). +Hint Resolve (Th_plus_assoc2 T). +Hint Resolve (Th_mult_sym T). +Hint Resolve (Th_mult_assoc T). +Hint Resolve (Th_mult_assoc2 T). +Hint Resolve (Th_plus_zero_left T). +Hint Resolve (Th_plus_zero_left2 T). +Hint Resolve (Th_mult_one_left T). +Hint Resolve (Th_mult_one_left2 T). +Hint Resolve (Th_mult_zero_left T). +Hint Resolve (Th_mult_zero_left2 T). +Hint Resolve (Th_distr_left T). +Hint Resolve (Th_distr_left2 T). +Hint Resolve (Th_plus_reg_left T). +Hint Resolve (Th_plus_permute T). +Hint Resolve (Th_mult_permute T). +Hint Resolve (Th_distr_right T). +Hint Resolve (Th_distr_right2 T). +Hint Resolve (Th_mult_zero_right T). +Hint Resolve (Th_mult_zero_right2 T). +Hint Resolve (Th_plus_zero_right T). +Hint Resolve (Th_plus_zero_right2 T). +Hint Resolve (Th_mult_one_right T). +Hint Resolve (Th_mult_one_right2 T). +Hint Resolve (Th_plus_reg_right T). +Hint Resolve refl_equal sym_equal trans_equal. (*Hints Resolve refl_eqT sym_eqT trans_eqT.*) -Hints Immediate T. +Hint 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)) +Inductive polynomial : Type := + | 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 := + match x with + | 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)) +Definition polynomial_simplify (x:polynomial) := + canonical_sum_simplify Aone Azero Aeq (polynomial_normalize x). + +Fixpoint spolynomial_of (x:polynomial) : spolynomial A := + match x with + | 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)) +Fixpoint interp_p (p:polynomial) : A := + match p with + | 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. +Lemma spolynomial_of_ok : + forall p:polynomial, + interp_p p = interp_sp Aplus Amult Azero vm (spolynomial_of p). +simple induction p; reflexivity || (simpl in |- *; 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. +Qed. + +Theorem polynomial_normalize_ok : + forall p:polynomial, + polynomial_normalize p = + spolynomial_normalize Aplus Amult Aone (spolynomial_of p). +simple induction p; reflexivity || (simpl in |- *; intros). +rewrite H; rewrite H0; reflexivity. +rewrite H; rewrite H0; reflexivity. +rewrite H; simpl in |- *. +elim + (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var + (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0))); + [ reflexivity + | simpl in |- *; intros; rewrite H0; reflexivity + | simpl in |- *; intros; rewrite H0; reflexivity ]. +Qed. + +Theorem polynomial_simplify_ok : + forall p:polynomial, + interp_cs Aplus Amult Aone Azero vm (polynomial_simplify p) = interp_p p. +intro. +unfold polynomial_simplify in |- *. +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. +Qed. 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. +Infix "+" := Pplus : ring_scope. +Infix "*" := Pmult : ring_scope. +Notation "- x" := (Popp x) : ring_scope. +Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope. -Delimits Scope ring_scope with ring. +Delimit Scope ring_scope with ring.
\ No newline at end of file diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index ddc52f8127..c99cf3c4ab 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/Ring_theory.v @@ -25,112 +25,110 @@ Variable Azero : A. 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). +Infix "+" := Aplus (at level 50, left associativity). +Infix "*" := Amult (at level 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 -}. +Record Semi_Ring_Theory : Prop := + {SR_plus_comm : forall n m:A, n + m = m + n; + SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; + SR_mult_comm : forall n m:A, n * m = m * n; + SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; + SR_plus_zero_left : forall n:A, 0 + n = n; + SR_mult_one_left : forall n:A, 1 * n = n; + SR_mult_zero_left : forall n:A, 0 * n = 0; + SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; + SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p; + SR_eq_prop : forall 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). +Let plus_comm := SR_plus_comm T. +Let plus_assoc := SR_plus_assoc T. +Let mult_comm := SR_mult_comm T. +Let mult_assoc := SR_mult_assoc T. +Let plus_zero_left := SR_plus_zero_left T. +Let mult_one_left := SR_mult_one_left T. +Let mult_zero_left := SR_mult_zero_left T. +Let distr_left := SR_distr_left T. +Let 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. +Hint Resolve plus_comm plus_assoc mult_comm 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_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). +symmetry in |- *; eauto. Qed. -Lemma SR_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). -Symmetry; EAuto. Qed. +Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). +symmetry in |- *; eauto. Qed. -Lemma SR_plus_zero_left2 : (n:A) n == 0 + n. -Symmetry; EAuto. Qed. +Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n. +symmetry in |- *; eauto. Qed. -Lemma SR_mult_one_left2 : (n:A) n == 1*n. -Symmetry; EAuto. Qed. +Lemma SR_mult_one_left2 : forall n:A, n = 1 * n. +symmetry in |- *; eauto. Qed. -Lemma SR_mult_zero_left2 : (n:A) 0 == 0*n. -Symmetry; EAuto. Qed. +Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n. +symmetry in |- *; eauto. Qed. -Lemma SR_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. -Symmetry; EAuto. Qed. +Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. +symmetry in |- *; 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. +Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). +intros. +rewrite plus_assoc. +elim (plus_comm 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. +Lemma SR_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). +intros. +rewrite mult_assoc. +elim (mult_comm m n). +rewrite <- mult_assoc. +reflexivity. Qed. -Hints Resolve SR_plus_permute SR_mult_permute. +Hint 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. +Lemma SR_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. +intros. +repeat rewrite (mult_comm 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_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). +symmetry in |- *; apply SR_distr_right. Qed. -Lemma SR_mult_zero_right : (n:A) n*0 == 0. -Intro; Rewrite mult_sym; EAuto. +Lemma SR_mult_zero_right : forall n:A, n * 0 = 0. +intro; rewrite mult_comm; eauto. Qed. -Lemma SR_mult_zero_right2 : (n:A) 0 == n*0. -Intro; Rewrite mult_sym; EAuto. +Lemma SR_mult_zero_right2 : forall n:A, 0 = n * 0. +intro; rewrite mult_comm; eauto. Qed. -Lemma SR_plus_zero_right :(n:A) n + 0 == n. -Intro; Rewrite plus_sym; EAuto. +Lemma SR_plus_zero_right : forall n:A, n + 0 = n. +intro; rewrite plus_comm; eauto. Qed. -Lemma SR_plus_zero_right2 :(n:A) n == n + 0. -Intro; Rewrite plus_sym; EAuto. +Lemma SR_plus_zero_right2 : forall n:A, n = n + 0. +intro; rewrite plus_comm; eauto. Qed. -Lemma SR_mult_one_right : (n:A) n*1 == n. -Intro; Elim mult_sym; Auto. +Lemma SR_mult_one_right : forall n:A, n * 1 = n. +intro; elim mult_comm; auto. Qed. -Lemma SR_mult_one_right2 : (n:A) n == n*1. -Intro; Elim mult_sym; Auto. +Lemma SR_mult_one_right2 : forall n:A, n = n * 1. +intro; elim mult_comm; 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. +Lemma SR_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. +intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n); eauto. Qed. End Theory_of_semi_rings. @@ -146,228 +144,222 @@ 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). +Infix "+" := Aplus (at level 50, left associativity). +Infix "*" := Amult (at level 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 -}. +Notation "- x" := (Aopp x). + +Record Ring_Theory : Prop := + {Th_plus_comm : forall n m:A, n + m = m + n; + Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; + Th_mult_sym : forall n m:A, n * m = m * n; + Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; + Th_plus_zero_left : forall n:A, 0 + n = n; + Th_mult_one_left : forall n:A, 1 * n = n; + Th_opp_def : forall n:A, n + - n = 0; + Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; + Th_eq_prop : forall 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). +Let plus_comm := Th_plus_comm T. +Let plus_assoc := Th_plus_assoc T. +Let mult_comm := Th_mult_sym T. +Let mult_assoc := Th_mult_assoc T. +Let plus_zero_left := Th_plus_zero_left T. +Let mult_one_left := Th_mult_one_left T. +Let opp_def := Th_opp_def T. +Let 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. +Hint Resolve plus_comm plus_assoc mult_comm 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_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). +symmetry in |- *; eauto. Qed. -Lemma Th_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). -Symmetry; EAuto. Qed. +Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). +symmetry in |- *; eauto. Qed. -Lemma Th_plus_zero_left2 : (n:A) n == 0 + n. -Symmetry; EAuto. Qed. +Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n. +symmetry in |- *; eauto. Qed. -Lemma Th_mult_one_left2 : (n:A) n == 1*n. -Symmetry; EAuto. Qed. +Lemma Th_mult_one_left2 : forall n:A, n = 1 * n. +symmetry in |- *; eauto. Qed. -Lemma Th_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. -Symmetry; EAuto. Qed. +Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. +symmetry in |- *; eauto. Qed. -Lemma Th_opp_def2 : (n:A) 0 == n + (-n). -Symmetry; EAuto. Qed. +Lemma Th_opp_def2 : forall n:A, 0 = n + - n. +symmetry in |- *; 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. +Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). +intros. +rewrite plus_assoc. +elim (plus_comm 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. +Lemma Th_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). +intros. +rewrite mult_assoc. +elim (mult_comm 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. +Hint Resolve Th_plus_permute Th_mult_permute. + +Lemma aux1 : forall a:A, a + a = a -> a = 0. +intros. +generalize (opp_def a). +pattern a at 1 in |- *. +rewrite <- H. +rewrite <- plus_assoc. +rewrite opp_def. +elim plus_comm. +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. +Lemma Th_mult_zero_left : forall 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. +Hint Resolve Th_mult_zero_left. + +Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n. +symmetry in |- *; eauto. Qed. + +Lemma aux2 : forall 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_comm 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]. +Lemma Th_opp_mult_left : forall x y:A, - (x * y) = - x * y. +intros. +apply (aux2 (x:=(x * y))); + [ apply opp_def | rewrite <- distr_left; rewrite opp_def; auto ]. Qed. -Hints Resolve Th_opp_mult_left. +Hint Resolve Th_opp_mult_left. -Lemma Th_opp_mult_left2 : (x,y:A) (-x)*y == -(x*y). -Symmetry; EAuto. Qed. +Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y). +symmetry in |- *; eauto. Qed. -Lemma Th_mult_zero_right : (n:A) n*0 == 0. -Intro; Elim mult_sym; EAuto. +Lemma Th_mult_zero_right : forall n:A, n * 0 = 0. +intro; elim mult_comm; eauto. Qed. -Lemma Th_mult_zero_right2 : (n:A) 0 == n*0. -Intro; Elim mult_sym; EAuto. +Lemma Th_mult_zero_right2 : forall n:A, 0 = n * 0. +intro; elim mult_comm; eauto. Qed. -Lemma Th_plus_zero_right :(n:A) n + 0 == n. -Intro; Rewrite plus_sym; EAuto. +Lemma Th_plus_zero_right : forall n:A, n + 0 = n. +intro; rewrite plus_comm; eauto. Qed. -Lemma Th_plus_zero_right2 :(n:A) n == n + 0. -Intro; Rewrite plus_sym; EAuto. +Lemma Th_plus_zero_right2 : forall n:A, n = n + 0. +intro; rewrite plus_comm; eauto. Qed. -Lemma Th_mult_one_right : (n:A) n*1 == n. -Intro;Elim mult_sym; EAuto. +Lemma Th_mult_one_right : forall n:A, n * 1 = n. +intro; elim mult_comm; eauto. Qed. -Lemma Th_mult_one_right2 : (n:A) n == n*1. -Intro;Elim mult_sym; EAuto. +Lemma Th_mult_one_right2 : forall n:A, n = n * 1. +intro; elim mult_comm; eauto. Qed. -Lemma Th_opp_mult_right : (x,y:A) -(x*y) == x*(-y). -Intros; Do 2 Rewrite -> (mult_sym x); Auto. +Lemma Th_opp_mult_right : forall x y:A, - (x * y) = x * - y. +intros; do 2 rewrite (mult_comm x); auto. Qed. -Lemma Th_opp_mult_right2 : (x,y:A) x*(-y) == -(x*y). -Intros; Do 2 Rewrite -> (mult_sym x); Auto. +Lemma Th_opp_mult_right2 : forall x y:A, x * - y = - (x * y). +intros; do 2 rewrite (mult_comm 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 ]. +Lemma Th_plus_opp_opp : forall x y:A, - x + - y = - (x + y). +intros. +apply (aux2 (x:=(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_plus_permute_opp : forall 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 ]. +Lemma Th_opp_opp : forall n:A, - - n = n. +intro; apply (aux2 (x:=(- n))); [ auto | elim plus_comm; auto ]. Qed. -Hints Resolve Th_opp_opp. +Hint Resolve Th_opp_opp. -Lemma Th_opp_opp2 : (n:A) n == -(-n). -Symmetry; EAuto. Qed. +Lemma Th_opp_opp2 : forall n:A, n = - - n. +symmetry in |- *; 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. +Lemma Th_mult_opp_opp : forall 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_mult_opp_opp2 : forall x y:A, x * y = - x * - y. +symmetry in |- *; apply Th_mult_opp_opp. Qed. -Lemma Th_opp_zero : -0 == 0. -Rewrite <- (plus_zero_left (-0)). -Auto. 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. +Lemma Th_plus_reg_left : forall n m p:A, n + m = n + p -> m = p. +intros; generalize (f_equal (fun z => - n + z) H). +repeat rewrite plus_assoc. +rewrite (plus_comm (- 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. +Lemma Th_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. +intros. +eapply Th_plus_reg_left with n. +rewrite (plus_comm n m). +rewrite (plus_comm 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. +Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. +intros. +repeat rewrite (mult_comm n). +eauto. Qed. -Lemma Th_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p). -Symmetry; Apply Th_distr_right. +Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). +symmetry in |- *; apply Th_distr_right. Qed. End Theory_of_rings. -Hints Resolve Th_mult_zero_left Th_plus_reg_left : core. +Hint 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. + forall (A:Type) (Aplus Amult:A -> A -> A) (Aone 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 in |- *; eauto. Defined. (* Every ring can be viewed as a semi-ring : this property will be used @@ -381,4 +373,4 @@ End product_ring. Section power_ring. -End power_ring. +End power_ring.
\ No newline at end of file diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v index 567517e984..6c33032a27 100644 --- a/contrib/ring/Setoid_ring.v +++ b/contrib/ring/Setoid_ring.v @@ -10,4 +10,4 @@ Require Export Setoid_ring_theory. Require Export Quote. -Require Export Setoid_ring_normalize. +Require Export Setoid_ring_normalize.
\ No newline at end of file diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v index bbebde4223..c619f32654 100644 --- a/contrib/ring/Setoid_ring_normalize.v +++ b/contrib/ring/Setoid_ring_normalize.v @@ -8,17 +8,18 @@ (* $Id$ *) -Require Setoid_ring_theory. -Require Quote. +Require Import Setoid_ring_theory. +Require Import Quote. Set Implicit Arguments. -Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m. +Lemma index_eq_prop : forall 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. + simple induction n; simple induction m; simpl in |- *; + try reflexivity || contradiction. + intros; rewrite (H i0); trivial. + intros; rewrite (H i0); trivial. +Qed. Section setoid. @@ -31,35 +32,38 @@ Variable Azero : A. Variable Aopp : A -> A. Variable Aeq : A -> A -> bool. -Variable S : (Setoid_Theory A Aequiv). +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)). +Variable + plus_morph : + forall a a0 a1 a2:A, + Aequiv a a0 -> Aequiv a1 a2 -> Aequiv (Aplus a a1) (Aplus a0 a2). +Variable + mult_morph : + forall a a0 a1 a2:A, + Aequiv a a0 -> Aequiv a1 a2 -> Aequiv (Amult a a1) (Amult a0 a2). +Variable opp_morph : forall a a0:A, Aequiv a a0 -> Aequiv (Aopp a) (Aopp a0). Add Morphism Aplus : Aplus_ext. -Exact plus_morph. -Save. +exact plus_morph. +Qed. Add Morphism Amult : Amult_ext. -Exact mult_morph. -Save. +exact mult_morph. +Qed. Add Morphism Aopp : Aopp_ext. -Exact opp_morph. -Save. +exact opp_morph. +Qed. -Local equiv_refl := (Seq_refl A Aequiv S). -Local equiv_sym := (Seq_sym A Aequiv S). -Local equiv_trans := (Seq_trans A Aequiv S). +Let equiv_refl := Seq_refl A Aequiv S. +Let equiv_sym := Seq_sym A Aequiv S. +Let equiv_trans := Seq_trans A Aequiv S. -Hints Resolve equiv_refl equiv_trans. -Hints Immediate equiv_sym. +Hint Resolve equiv_refl equiv_trans. +Hint Immediate equiv_sym. Section semi_setoid_rings. @@ -81,16 +85,14 @@ Section semi_setoid_rings. (* 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 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 -. +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 *) @@ -107,244 +109,251 @@ Inductive canonical_sum : Type := 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 +Fixpoint varlist_eq (x y:varlist) {struct y} : bool := + match x, y with + | Nil_var, Nil_var => true + | Cons_var i xrest, Cons_var j yrest => + andb (index_eq i j) (varlist_eq xrest yrest) + | _, _ => false end. -Fixpoint varlist_lt [x,y:varlist] : 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 +Fixpoint varlist_lt (x y:varlist) {struct y} : bool := + match x, y with + | Nil_var, Cons_var _ _ => true + | Cons_var i xrest, Cons_var j yrest => + if index_lt i j + then true + else andb (index_eq i j) (varlist_lt xrest yrest) + | _, _ => false end. (* 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 +Fixpoint varlist_merge (l1:varlist) : varlist -> varlist := + match l1 with + | Cons_var v1 t1 => + (fix vm_aux (l2:varlist) : varlist := + match l2 with + | Cons_var v2 t2 => + if index_lt v1 v2 + then Cons_var v1 (varlist_merge t1 l2) + else Cons_var v2 (vm_aux t2) + | Nil_var => l1 + end) + | Nil_var => fun l2 => l2 end. (* 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. +Fixpoint canonical_sum_merge (s1:canonical_sum) : + canonical_sum -> canonical_sum := + match s1 with + | Cons_monom c1 l1 t1 => + (fix csm_aux (s2:canonical_sum) : canonical_sum := + match s2 with + | Cons_monom c2 l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2) + else + if varlist_lt l1 l2 + then Cons_monom c1 l1 (canonical_sum_merge t1 s2) + else Cons_monom c2 l2 (csm_aux t2) + | Cons_varlist l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2) + else + if varlist_lt l1 l2 + then Cons_monom c1 l1 (canonical_sum_merge t1 s2) + else Cons_varlist l2 (csm_aux t2) + | Nil_monom => s1 + end) + | Cons_varlist l1 t1 => + (fix csm_aux2 (s2:canonical_sum) : canonical_sum := + match s2 with + | Cons_monom c2 l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2) + else + if varlist_lt l1 l2 + then Cons_varlist l1 (canonical_sum_merge t1 s2) + else Cons_monom c2 l2 (csm_aux2 t2) + | Cons_varlist l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2) + else + if varlist_lt l1 l2 + then Cons_varlist l1 (canonical_sum_merge t1 s2) + else Cons_varlist l2 (csm_aux2 t2) + | Nil_monom => s1 + end) + | Nil_monom => fun s2 => s2 + end. (* 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) +Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} : + canonical_sum := + match s2 with + | Cons_monom c2 l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus c1 c2) l1 t2 + else + if varlist_lt l1 l2 + then Cons_monom c1 l1 s2 + else Cons_monom c2 l2 (monom_insert c1 l1 t2) + | Cons_varlist l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus c1 Aone) l1 t2 + else + if varlist_lt l1 l2 + then Cons_monom c1 l1 s2 + else Cons_varlist l2 (monom_insert c1 l1 t2) + | Nil_monom => Cons_monom c1 l1 Nil_monom end. -Fixpoint varlist_insert [l1:varlist; s2:canonical_sum] - : 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) +Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} : + canonical_sum := + match s2 with + | Cons_monom c2 l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus Aone c2) l1 t2 + else + if varlist_lt l1 l2 + then Cons_varlist l1 s2 + else Cons_monom c2 l2 (varlist_insert l1 t2) + | Cons_varlist l2 t2 => + if varlist_eq l1 l2 + then Cons_monom (Aplus Aone Aone) l1 t2 + else + if varlist_lt l1 l2 + then Cons_varlist l1 s2 + else Cons_varlist l2 (varlist_insert l1 t2) + | Nil_monom => Cons_varlist l1 Nil_monom end. (* 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. +Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} : + canonical_sum := + match s with + | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t) + | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t) + | Nil_monom => Nil_monom + end. (* 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. +Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} : + canonical_sum := + match s with + | Cons_monom c l t => + monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) + | Cons_varlist l t => + varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t) + | Nil_monom => Nil_monom + end. (* 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. +Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) + (s:canonical_sum) {struct s} : canonical_sum := + match s with + | Cons_monom c l t => + monom_insert (Amult c0 c) (varlist_merge l0 l) + (canonical_sum_scalar3 c0 l0 t) + | Cons_varlist l t => + monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t) + | Nil_monom => Nil_monom + end. (* 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. +Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} : + canonical_sum := + match s1 with + | Cons_monom c1 l1 t1 => + canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2) + (canonical_sum_prod t1 s2) + | Cons_varlist l1 t1 => + canonical_sum_merge (canonical_sum_scalar2 l1 s2) + (canonical_sum_prod t1 s2) + | Nil_monom => Nil_monom + end. (* 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)) +Inductive setspolynomial : Type := + | SetSPvar : index -> setspolynomial + | SetSPconst : A -> setspolynomial + | SetSPplus : setspolynomial -> setspolynomial -> setspolynomial + | SetSPmult : setspolynomial -> setspolynomial -> setspolynomial. + +Fixpoint setspolynomial_normalize (p:setspolynomial) : canonical_sum := + match p with + | SetSPplus l r => + canonical_sum_merge (setspolynomial_normalize l) + (setspolynomial_normalize r) + | SetSPmult l r => + canonical_sum_prod (setspolynomial_normalize l) + (setspolynomial_normalize r) + | SetSPconst c => Cons_monom c Nil_var Nil_monom + | SetSPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom + end. + +Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum := + match s with + | Cons_monom c l t => + if Aeq c Azero + then canonical_sum_simplify t + else + if Aeq c Aone + then Cons_varlist l (canonical_sum_simplify t) + else Cons_monom c l (canonical_sum_simplify t) + | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t) | Nil_monom => Nil_monom end. -Definition setspolynomial_simplify := - [x:setspolynomial] (canonical_sum_simplify (setspolynomial_normalize x)). +Definition setspolynomial_simplify (x:setspolynomial) := + canonical_sum_simplify (setspolynomial_normalize x). -Variable vm : (varmap A). +Variable vm : varmap A. -Definition interp_var [i:index] := (varmap_find Azero i vm). +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 ivl_aux := + (fix ivl_aux (x:index) (t:varlist) {struct t} : A := + match t with + | Nil_var => interp_var x + | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t') + end). -Definition interp_vl := [l:varlist] - Cases l of +Definition interp_vl (l:varlist) := + match l with | Nil_var => Aone - | (Cons_var x t) => (ivl_aux x t) + | Cons_var x t => ivl_aux x t end. -Definition interp_m := [c:A][l:varlist] - Cases l of +Definition interp_m (c:A) (l:varlist) := + match l with | Nil_var => c - | (Cons_var x t) => - (Amult c (ivl_aux x t)) + | 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 ics_aux := + (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A := + match s with + | Nil_monom => a + | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t) + | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t) + end). -Definition interp_setcs : canonical_sum -> A := - [s]Cases s of +Definition interp_setcs (s:canonical_sum) : A := + match s with | Nil_monom => Azero - | (Cons_varlist l t) => - (ics_aux (interp_vl l) t) - | (Cons_monom c l t) => - (ics_aux (interp_m c l) t) + | 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. +Fixpoint interp_setsp (p:setspolynomial) : A := + match p with + | SetSPconst c => c + | SetSPvar i => interp_var i + | SetSPplus p1 p2 => Aplus (interp_setsp p1) (interp_setsp p2) + | SetSPmult p1 p2 => Amult (interp_setsp p1) (interp_setsp p2) + end. (* End interpretation. *) @@ -352,655 +361,636 @@ 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. +Variable T : Semi_Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aeq. + +Hint Resolve (SSR_plus_comm T). +Hint Resolve (SSR_plus_assoc T). +Hint Resolve (SSR_plus_assoc2 S T). +Hint Resolve (SSR_mult_comm T). +Hint Resolve (SSR_mult_assoc T). +Hint Resolve (SSR_mult_assoc2 S T). +Hint Resolve (SSR_plus_zero_left T). +Hint Resolve (SSR_plus_zero_left2 S T). +Hint Resolve (SSR_mult_one_left T). +Hint Resolve (SSR_mult_one_left2 S T). +Hint Resolve (SSR_mult_zero_left T). +Hint Resolve (SSR_mult_zero_left2 S T). +Hint Resolve (SSR_distr_left T). +Hint Resolve (SSR_distr_left2 S T). +Hint Resolve (SSR_plus_reg_left T). +Hint Resolve (SSR_plus_permute S plus_morph T). +Hint Resolve (SSR_mult_permute S mult_morph T). +Hint Resolve (SSR_distr_right S plus_morph T). +Hint Resolve (SSR_distr_right2 S plus_morph T). +Hint Resolve (SSR_mult_zero_right S T). +Hint Resolve (SSR_mult_zero_right2 S T). +Hint Resolve (SSR_plus_zero_right S T). +Hint Resolve (SSR_plus_zero_right2 S T). +Hint Resolve (SSR_mult_one_right S T). +Hint Resolve (SSR_mult_one_right2 S T). +Hint Resolve (SSR_plus_reg_right S T). +Hint Resolve refl_equal sym_equal trans_equal. (*Hints Resolve refl_eqT sym_eqT trans_eqT.*) -Hints Immediate T. +Hint Immediate T. -Lemma varlist_eq_prop : (x,y:varlist) - (Is_true (varlist_eq x y))->x==y. +Lemma varlist_eq_prop : forall 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))). + simple induction x; simple induction y; contradiction || (try reflexivity). + simpl in |- *; intros. + generalize (andb_prop2 _ _ H1); intros; elim H2; intros. + rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity. +Qed. + +Remark ivl_aux_ok : + forall (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))). + simple induction v; simpl in |- *; intros. + trivial. + rewrite (H i); trivial. +Qed. + +Lemma varlist_merge_ok : + forall 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))). + simple induction x. + simpl in |- *; trivial. + simple induction y. + simpl in |- *; trivial. + simpl in |- *; intros. + elim (index_lt i i0); simpl in |- *; 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 in |- *. + 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 (l2:varlist) : varlist := + match l2 with + | 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. +Qed. + +Remark ics_aux_ok : + forall (x:A) (s:canonical_sum), + Aequiv (ics_aux x s) (Aplus x (interp_setcs s)). Proof. - Induction s; Simpl; Intros;Trivial. -Save. + simple induction s; simpl in |- *; intros; trivial. +Qed. -Remark interp_m_ok : (x:A)(l:varlist) - (Aequiv (interp_m x l) (Amult x (interp_vl l))). +Remark interp_m_ok : + forall (x:A) (l:varlist), Aequiv (interp_m x l) (Amult x (interp_vl l)). Proof. - NewDestruct l;Trivial. -Save. + destruct l as [| i v]; trivial. +Qed. -Hint ivl_aux_ok_ := Resolve ivl_aux_ok. -Hint ics_aux_ok_ := Resolve ics_aux_ok. -Hint interp_m_ok_ := Resolve interp_m_ok. +Hint Resolve ivl_aux_ok. +Hint Resolve ics_aux_ok. +Hint 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))). +Lemma canonical_sum_merge_ok : + forall x y:canonical_sum, + Aequiv (interp_setcs (canonical_sum_merge x y)) + (Aplus (interp_setcs x) (interp_setcs y)). 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))). +simple induction x; simpl in |- *. +trivial. + +simple induction y; simpl in |- *; intros. +eauto. + +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *. +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 in |- *. +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 in |- *. +rewrite (ics_aux_ok (interp_m a0 v0) c0); auto. + +intro. +rewrite + (ics_aux_ok (interp_m a0 v0) + ((fix csm_aux (s2:canonical_sum) : canonical_sum := + match s2 with + | 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 in |- *; + auto. + +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *. +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 in |- *. +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 in |- *. +rewrite (ics_aux_ok (interp_vl v0) c0). +auto. + +intro. +rewrite + (ics_aux_ok (interp_vl v0) + ((fix csm_aux (s2:canonical_sum) : canonical_sum := + match s2 with + | 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 in |- *. +auto. + +simple induction y; simpl in |- *; intros. +trivial. + +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0). +intros; rewrite (H1 I). +simpl in |- *. +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 in |- *; 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 in |- *. +rewrite (ics_aux_ok (interp_m a v0) c0); auto. + +rewrite + (ics_aux_ok (interp_m a v0) + ((fix csm_aux2 (s2:canonical_sum) : canonical_sum := + match s2 with + | 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 in |- *; auto. + +generalize (varlist_eq_prop v v0). +elim (varlist_eq v v0); intros. +rewrite (H1 I); simpl in |- *. +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 in |- *. +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 in |- *. +rewrite (ics_aux_ok (interp_vl v0) c0); auto. + +rewrite + (ics_aux_ok (interp_vl v0) + ((fix csm_aux2 (s2:canonical_sum) : canonical_sum := + match s2 with + | 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 in |- *; auto. +Qed. + +Lemma monom_insert_ok : + forall (a:A) (l:varlist) (s:canonical_sum), + Aequiv (interp_setcs (monom_insert a l s)) + (Aplus (Amult a (interp_vl l)) (interp_setcs s)). 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. +simple induction s; intros. +simpl in |- *; rewrite (interp_m_ok a l); trivial. + +simpl in |- *; generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *. +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 in |- *; 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 in |- *. +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *. +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 in |- *; 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. +Qed. Lemma varlist_insert_ok : - (l:varlist)(s:canonical_sum) - (Aequiv (interp_setcs (varlist_insert l s)) - (Aplus (interp_vl l) (interp_setcs s))). + forall (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))). +simple induction s; simpl in |- *; intros. +trivial. + +generalize (varlist_eq_prop l v); elim (varlist_eq l v). +intro Hr; rewrite (Hr I); simpl in |- *. +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 in |- *; 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 in |- *. +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 in |- *; intros; auto. +rewrite (ics_aux_ok (interp_vl v) (varlist_insert l c)). +rewrite H. +rewrite (ics_aux_ok (interp_vl v) c); auto. +Qed. + +Lemma canonical_sum_scalar_ok : + forall (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))) +simple induction s; simpl in |- *; 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))). +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. +Qed. + +Lemma canonical_sum_scalar2_ok : + forall (l:varlist) (s:canonical_sum), + Aequiv (interp_setcs (canonical_sum_scalar2 l s)) + (Amult (interp_vl l) (interp_setcs s)). 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)))). +simple induction s; simpl in |- *; 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. +Qed. + +Lemma canonical_sum_scalar3_ok : + forall (c:A) (l:varlist) (s:canonical_sum), + Aequiv (interp_setcs (canonical_sum_scalar3 c l s)) + (Amult c (Amult (interp_vl l) (interp_setcs s))). 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))). +simple induction s; simpl in |- *; 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. +Qed. + +Lemma canonical_sum_prod_ok : + forall x y:canonical_sum, + Aequiv (interp_setcs (canonical_sum_prod x y)) + (Amult (interp_setcs x) (interp_setcs y)). 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)). +simple induction x; simpl in |- *; 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. +Qed. + +Theorem setspolynomial_normalize_ok : + forall 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)). +simple induction p; simpl in |- *; 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. +Qed. + +Lemma canonical_sum_simplify_ok : + forall 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)). +simple induction s; simpl in |- *; intros. +trivial. + +generalize (SSR_eq_prop T a Azero). +elim (Aeq a Azero). +simpl in |- *. +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 in |- *. +generalize (SSR_eq_prop T a 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 in |- *. +rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)). +rewrite H. +auto. + +simpl in |- *. +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. +Qed. + +Theorem setspolynomial_simplify_ok : + forall 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. +intro. +unfold setspolynomial_simplify in |- *. +rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)). +exact (setspolynomial_normalize_ok p). +Qed. End semi_setoid_rings. -Implicits Cons_varlist. -Implicits Cons_monom. -Implicits SetSPconst. -Implicits SetSPplus. -Implicits SetSPmult. +Implicit Arguments Cons_varlist. +Implicit Arguments Cons_monom. +Implicit Arguments SetSPconst. +Implicit Arguments SetSPplus. +Implicit Arguments SetSPmult. @@ -1008,134 +998,140 @@ 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. +Variable vm : varmap A. +Variable T : Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq. + +Hint Resolve (STh_plus_comm T). +Hint Resolve (STh_plus_assoc T). +Hint Resolve (STh_plus_assoc2 S T). +Hint Resolve (STh_mult_sym T). +Hint Resolve (STh_mult_assoc T). +Hint Resolve (STh_mult_assoc2 S T). +Hint Resolve (STh_plus_zero_left T). +Hint Resolve (STh_plus_zero_left2 S T). +Hint Resolve (STh_mult_one_left T). +Hint Resolve (STh_mult_one_left2 S T). +Hint Resolve (STh_mult_zero_left S plus_morph mult_morph T). +Hint Resolve (STh_mult_zero_left2 S plus_morph mult_morph T). +Hint Resolve (STh_distr_left T). +Hint Resolve (STh_distr_left2 S T). +Hint Resolve (STh_plus_reg_left S plus_morph T). +Hint Resolve (STh_plus_permute S plus_morph T). +Hint Resolve (STh_mult_permute S mult_morph T). +Hint Resolve (STh_distr_right S plus_morph T). +Hint Resolve (STh_distr_right2 S plus_morph T). +Hint Resolve (STh_mult_zero_right S plus_morph mult_morph T). +Hint Resolve (STh_mult_zero_right2 S plus_morph mult_morph T). +Hint Resolve (STh_plus_zero_right S T). +Hint Resolve (STh_plus_zero_right2 S T). +Hint Resolve (STh_mult_one_right S T). +Hint Resolve (STh_mult_one_right2 S T). +Hint Resolve (STh_plus_reg_right S plus_morph T). +Hint Resolve refl_equal sym_equal trans_equal. (*Hints Resolve refl_eqT sym_eqT trans_eqT.*) -Hints Immediate T. +Hint 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. +Inductive setpolynomial : Type := + | SetPvar : index -> setpolynomial + | SetPconst : A -> setpolynomial + | SetPplus : setpolynomial -> setpolynomial -> setpolynomial + | SetPmult : setpolynomial -> setpolynomial -> setpolynomial + | SetPopp : setpolynomial -> setpolynomial. + +Fixpoint setpolynomial_normalize (x:setpolynomial) : canonical_sum := + match x with + | SetPplus l r => + canonical_sum_merge (setpolynomial_normalize l) + (setpolynomial_normalize r) + | SetPmult l r => + canonical_sum_prod (setpolynomial_normalize l) + (setpolynomial_normalize r) + | SetPconst c => Cons_monom c Nil_var Nil_monom + | SetPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom + | SetPopp p => + canonical_sum_scalar3 (Aopp Aone) Nil_var (setpolynomial_normalize p) + end. + +Definition setpolynomial_simplify (x:setpolynomial) := + canonical_sum_simplify (setpolynomial_normalize x). + +Fixpoint setspolynomial_of (x:setpolynomial) : setspolynomial := + match x with + | SetPplus l r => SetSPplus (setspolynomial_of l) (setspolynomial_of r) + | SetPmult l r => SetSPmult (setspolynomial_of l) (setspolynomial_of r) + | SetPconst c => SetSPconst c + | SetPvar i => SetSPvar i + | SetPopp p => SetSPmult (SetSPconst (Aopp Aone)) (setspolynomial_of p) + end. (*** 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. +Fixpoint interp_setp (p:setpolynomial) : A := + match p with + | SetPconst c => c + | SetPvar i => varmap_find Azero i vm + | SetPplus p1 p2 => Aplus (interp_setp p1) (interp_setp p2) + | SetPmult p1 p2 => Amult (interp_setp p1) (interp_setp p2) + | SetPopp p1 => Aopp (interp_setp p1) + end. (*** 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. +Lemma setspolynomial_of_ok : + forall p:setpolynomial, + Aequiv (interp_setp p) (interp_setsp vm (setspolynomial_of p)). +simple induction p; trivial; simpl in |- *; 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. +Qed. + +Theorem setpolynomial_normalize_ok : + forall p:setpolynomial, + setpolynomial_normalize p = setspolynomial_normalize (setspolynomial_of p). +simple induction p; trivial; simpl in |- *; intros. +rewrite H; rewrite H0; reflexivity. +rewrite H; rewrite H0; reflexivity. +rewrite H; simpl in |- *. +elim + (canonical_sum_scalar3 (Aopp Aone) Nil_var + (setspolynomial_normalize (setspolynomial_of s))); + [ reflexivity + | simpl in |- *; intros; rewrite H0; reflexivity + | simpl in |- *; intros; rewrite H0; reflexivity ]. +Qed. + +Theorem setpolynomial_simplify_ok : + forall p:setpolynomial, + Aequiv (interp_setcs vm (setpolynomial_simplify p)) (interp_setp p). +intro. +unfold setpolynomial_simplify in |- *. +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. +Qed. End setoid_rings. -End setoid. +End setoid.
\ No newline at end of file diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v index d6c19410f2..fecdb294b4 100644 --- a/contrib/ring/Setoid_ring_theory.v +++ b/contrib/ring/Setoid_ring_theory.v @@ -18,9 +18,9 @@ Section Setoid_rings. Variable A : Type. Variable Aequiv : A -> A -> Prop. -Infix Local "==" Aequiv (at level 5, no associativity). +Infix Local "==" := Aequiv (at level 70, no associativity). -Variable S : (Setoid_Theory A Aequiv). +Variable S : Setoid_Theory A Aequiv. Add Setoid A Aequiv S. @@ -31,390 +31,388 @@ 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). +Infix "+" := Aplus (at level 50, left associativity). +Infix "*" := Amult (at level 40, left associativity). Notation "0" := Azero. Notation "1" := Aone. -Notation "- x" := (Aopp x) (at level 0) V8only. +Notation "- x" := (Aopp x). -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. +Variable + plus_morph : forall a a0 a1 a2:A, a == a0 -> a1 == a2 -> a + a1 == a0 + a2. +Variable + mult_morph : forall a a0 a1 a2:A, a == a0 -> a1 == a2 -> a * a1 == a0 * a2. +Variable opp_morph : forall a a0:A, a == a0 -> - a == - a0. Add Morphism Aplus : Aplus_ext. -Exact plus_morph. -Save. +exact plus_morph. +Qed. Add Morphism Amult : Amult_ext. -Exact mult_morph. -Save. +exact mult_morph. +Qed. Add Morphism Aopp : Aopp_ext. -Exact opp_morph. -Save. +exact opp_morph. +Qed. 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 -}. +Record Semi_Setoid_Ring_Theory : Prop := + {SSR_plus_comm : forall n m:A, n + m == m + n; + SSR_plus_assoc : forall n m p:A, n + (m + p) == n + m + p; + SSR_mult_comm : forall n m:A, n * m == m * n; + SSR_mult_assoc : forall n m p:A, n * (m * p) == n * m * p; + SSR_plus_zero_left : forall n:A, 0 + n == n; + SSR_mult_one_left : forall n:A, 1 * n == n; + SSR_mult_zero_left : forall n:A, 0 * n == 0; + SSR_distr_left : forall n m p:A, (n + m) * p == n * p + m * p; + SSR_plus_reg_left : forall n m p:A, n + m == n + p -> m == p; + SSR_eq_prop : forall 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. +Let plus_comm := SSR_plus_comm T. +Let plus_assoc := SSR_plus_assoc T. +Let mult_comm := SSR_mult_comm T. +Let mult_assoc := SSR_mult_assoc T. +Let plus_zero_left := SSR_plus_zero_left T. +Let mult_one_left := SSR_mult_one_left T. +Let mult_zero_left := SSR_mult_zero_left T. +Let distr_left := SSR_distr_left T. +Let plus_reg_left := SSR_plus_reg_left T. +Let equiv_refl := Seq_refl A Aequiv S. +Let equiv_sym := Seq_sym A Aequiv S. +Let equiv_trans := Seq_trans A Aequiv S. + +Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left + mult_one_left mult_zero_left distr_left plus_reg_left + equiv_refl (*equiv_sym*). +Hint 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. +Lemma SSR_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p). +auto. Qed. + +Lemma SSR_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p). +auto. Qed. + +Lemma SSR_plus_zero_left2 : forall n:A, n == 0 + n. +auto. Qed. + +Lemma SSR_mult_one_left2 : forall n:A, n == 1 * n. +auto. Qed. + +Lemma SSR_mult_zero_left2 : forall n:A, 0 == 0 * n. +auto. Qed. + +Lemma SSR_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p. +auto. Qed. + +Lemma SSR_plus_permute : forall n m p:A, n + (m + p) == m + (n + p). +intros. +rewrite (plus_assoc n m p). +rewrite (plus_comm n m). +rewrite <- (plus_assoc m n p). +trivial. +Qed. + +Lemma SSR_mult_permute : forall n m p:A, n * (m * p) == m * (n * p). +intros. +rewrite (mult_assoc n m p). +rewrite (mult_comm n m). +rewrite <- (mult_assoc m n p). +trivial. +Qed. + +Hint Resolve SSR_plus_permute SSR_mult_permute. + +Lemma SSR_distr_right : forall n m p:A, n * (m + p) == n * m + n * p. +intros. +rewrite (mult_comm n (m + p)). +rewrite (mult_comm n m). +rewrite (mult_comm n p). +auto. +Qed. + +Lemma SSR_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p). +intros. +apply equiv_sym. +apply SSR_distr_right. +Qed. + +Lemma SSR_mult_zero_right : forall n:A, n * 0 == 0. +intro; rewrite (mult_comm n 0); auto. +Qed. + +Lemma SSR_mult_zero_right2 : forall n:A, 0 == n * 0. +intro; rewrite (mult_comm n 0); auto. +Qed. + +Lemma SSR_plus_zero_right : forall n:A, n + 0 == n. +intro; rewrite (plus_comm n 0); auto. +Qed. + +Lemma SSR_plus_zero_right2 : forall n:A, n == n + 0. +intro; rewrite (plus_comm n 0); auto. +Qed. + +Lemma SSR_mult_one_right : forall n:A, n * 1 == n. +intro; rewrite (mult_comm n 1); auto. +Qed. + +Lemma SSR_mult_one_right2 : forall n:A, n == n * 1. +intro; rewrite (mult_comm n 1); auto. +Qed. + +Lemma SSR_plus_reg_right : forall n m p:A, m + n == p + n -> m == p. +intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n). +intro; apply plus_reg_left with n; trivial. +Qed. 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 -}. +Record Setoid_Ring_Theory : Prop := + {STh_plus_comm : forall n m:A, n + m == m + n; + STh_plus_assoc : forall n m p:A, n + (m + p) == n + m + p; + STh_mult_sym : forall n m:A, n * m == m * n; + STh_mult_assoc : forall n m p:A, n * (m * p) == n * m * p; + STh_plus_zero_left : forall n:A, 0 + n == n; + STh_mult_one_left : forall n:A, 1 * n == n; + STh_opp_def : forall n:A, n + - n == 0; + STh_distr_left : forall n m p:A, (n + m) * p == n * p + m * p; + STh_eq_prop : forall 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. +Let plus_comm := STh_plus_comm T. +Let plus_assoc := STh_plus_assoc T. +Let mult_comm := STh_mult_sym T. +Let mult_assoc := STh_mult_assoc T. +Let plus_zero_left := STh_plus_zero_left T. +Let mult_one_left := STh_mult_one_left T. +Let opp_def := STh_opp_def T. +Let distr_left := STh_distr_left T. +Let equiv_refl := Seq_refl A Aequiv S. +Let equiv_sym := Seq_sym A Aequiv S. +Let equiv_trans := Seq_trans A Aequiv S. + +Hint Resolve plus_comm plus_assoc mult_comm 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. +Lemma STh_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p). +auto. Qed. + +Lemma STh_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p). +auto. Qed. + +Lemma STh_plus_zero_left2 : forall n:A, n == 0 + n. +auto. Qed. + +Lemma STh_mult_one_left2 : forall n:A, n == 1 * n. +auto. Qed. + +Lemma STh_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p. +auto. Qed. + +Lemma STh_opp_def2 : forall n:A, 0 == n + - n. +auto. Qed. + +Lemma STh_plus_permute : forall n m p:A, n + (m + p) == m + (n + p). +intros. +rewrite (plus_assoc n m p). +rewrite (plus_comm n m). +rewrite <- (plus_assoc m n p). +trivial. +Qed. + +Lemma STh_mult_permute : forall n m p:A, n * (m * p) == m * (n * p). +intros. +rewrite (mult_assoc n m p). +rewrite (mult_comm n m). +rewrite <- (mult_assoc m n p). +trivial. +Qed. + +Hint Resolve STh_plus_permute STh_mult_permute. + +Lemma Saux1 : forall a:A, a + a == a -> a == 0. +intros. +rewrite <- (plus_zero_left a). +rewrite (plus_comm 0 a). +setoid_replace (a + 0) with (a + (a + - a)); auto. +rewrite (plus_assoc a a (- a)). +rewrite H. +apply opp_def. +Qed. + +Lemma STh_mult_zero_left : forall n:A, 0 * n == 0. +intros. +apply Saux1. +rewrite <- (distr_left 0 0 n). +rewrite (plus_zero_left 0). +trivial. +Qed. +Hint Resolve STh_mult_zero_left. + +Lemma STh_mult_zero_left2 : forall n:A, 0 == 0 * n. +auto. +Qed. + +Lemma Saux2 : forall 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_comm z y). +rewrite (plus_assoc x y z). +rewrite H. +auto. +Qed. + +Lemma STh_opp_mult_left : forall x y:A, - (x * y) == - x * y. +intros. +apply Saux2 with (x * y); auto. +rewrite <- (distr_left x (- x) y). +rewrite (opp_def x). +auto. +Qed. +Hint Resolve STh_opp_mult_left. + +Lemma STh_opp_mult_left2 : forall x y:A, - x * y == - (x * y). +auto. +Qed. + +Lemma STh_mult_zero_right : forall n:A, n * 0 == 0. +intro; rewrite (mult_comm n 0); auto. +Qed. + +Lemma STh_mult_zero_right2 : forall n:A, 0 == n * 0. +intro; rewrite (mult_comm n 0); auto. +Qed. + +Lemma STh_plus_zero_right : forall n:A, n + 0 == n. +intro; rewrite (plus_comm n 0); auto. +Qed. + +Lemma STh_plus_zero_right2 : forall n:A, n == n + 0. +intro; rewrite (plus_comm n 0); auto. +Qed. + +Lemma STh_mult_one_right : forall n:A, n * 1 == n. +intro; rewrite (mult_comm n 1); auto. +Qed. + +Lemma STh_mult_one_right2 : forall n:A, n == n * 1. +intro; rewrite (mult_comm n 1); auto. +Qed. + +Lemma STh_opp_mult_right : forall x y:A, - (x * y) == x * - y. +intros. +rewrite (mult_comm x y). +rewrite (mult_comm x (- y)). +auto. +Qed. + +Lemma STh_opp_mult_right2 : forall x y:A, x * - y == - (x * y). +intros. +rewrite (mult_comm x y). +rewrite (mult_comm x (- y)). +auto. +Qed. + +Lemma STh_plus_opp_opp : forall x y:A, - x + - y == - (x + y). +intros. +apply Saux2 with (x + y); auto. +rewrite (STh_plus_permute (x + y) (- x) (- y)). +rewrite <- (plus_assoc x y (- y)). +rewrite (opp_def y); rewrite (STh_plus_zero_right x). +rewrite (STh_opp_def2 x); trivial. +Qed. + +Lemma STh_plus_permute_opp : forall n m p:A, - m + (n + p) == n + (- m + p). +auto. +Qed. + +Lemma STh_opp_opp : forall n:A, - - n == n. +intro. +apply Saux2 with (- n); auto. +rewrite (plus_comm (- n) n); auto. +Qed. +Hint Resolve STh_opp_opp. + +Lemma STh_opp_opp2 : forall n:A, n == - - n. +auto. +Qed. + +Lemma STh_mult_opp_opp : forall x y:A, - x * - y == x * y. +intros. +rewrite (STh_opp_mult_left2 x (- y)). +rewrite (STh_opp_mult_right2 x y). +trivial. +Qed. + +Lemma STh_mult_opp_opp2 : forall x y:A, x * y == - x * - y. +intros. +apply equiv_sym. +apply STh_mult_opp_opp. +Qed. + +Lemma STh_opp_zero : - 0 == 0. +rewrite <- (plus_zero_left (- 0)). +trivial. +Qed. + +Lemma STh_plus_reg_left : forall 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_comm n (- n)). +rewrite <- (plus_assoc (- n) n m). +rewrite <- (plus_assoc (- n) n p). +auto. +Qed. + +Lemma STh_plus_reg_right : forall n m p:A, m + n == p + n -> m == p. +intros. +apply STh_plus_reg_left with n. +rewrite (plus_comm n m); rewrite (plus_comm n p); assumption. +Qed. + +Lemma STh_distr_right : forall n m p:A, n * (m + p) == n * m + n * p. +intros. +rewrite (mult_comm n (m + p)). +rewrite (mult_comm n m). +rewrite (mult_comm n p). +trivial. +Qed. + +Lemma STh_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p). +intros. +apply equiv_sym. +apply STh_distr_right. +Qed. End Theory_of_setoid_rings. -Hints Resolve STh_mult_zero_left STh_plus_reg_left : core. +Hint 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. +intros until 1; case H. +split; intros; simpl in |- *; eauto. Defined. -Coercion Semi_Setoid_Ring_Theory_of : - Setoid_Ring_Theory >-> Semi_Setoid_Ring_Theory. +Coercion Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory >-> + Semi_Setoid_Ring_Theory. @@ -426,4 +424,4 @@ Section power_ring. End power_ring. -End Setoid_rings. +End Setoid_rings.
\ No newline at end of file diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v index cf5e18c5ea..e6a7bf2af7 100644 --- a/contrib/ring/ZArithRing.v +++ b/contrib/ring/ZArithRing.v @@ -12,24 +12,25 @@ Require Export ArithRing. Require Export ZArith_base. -Require Eqdep_dec. +Require Import Eqdep_dec. -Definition Zeq := [x,y:Z] - Cases `x ?= y ` of - EGAL => true +Definition Zeq (x y:Z) := + match (x ?= y)%Z with + | Datatypes.Eq => 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. +Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y. + intros x y H; unfold Zeq in H. + apply Zcompare_Eq_eq. + destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ]. +Qed. -Definition ZTheory : (Ring_Theory Zplus Zmult `1` `0` Zopp Zeq). - Split; Intros; Apply eq2eqT; EAuto with zarith. - Apply eqT2eq; Apply Zeq_prop; Assumption. -Save. +Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq. + split; intros; apply eq2eqT; eauto with zarith. + apply eqT2eq; apply Zeq_prop; assumption. +Qed. (* 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]. +Add Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory + [ Zpos Zneg 0%Z xO xI 1%positive ].
\ No newline at end of file |