diff options
Diffstat (limited to 'contrib7/field/Field_Theory.v')
| -rw-r--r-- | contrib7/field/Field_Theory.v | 612 |
1 files changed, 0 insertions, 612 deletions
diff --git a/contrib7/field/Field_Theory.v b/contrib7/field/Field_Theory.v deleted file mode 100644 index 3ba2fbc0..00000000 --- a/contrib7/field/Field_Theory.v +++ /dev/null @@ -1,612 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: Field_Theory.v,v 1.2.2.1 2004/07/16 19:30:17 herbelin Exp $ *) - -Require Peano_dec. -Require Ring. -Require Field_Compl. - -Record Field_Theory : Type := -{ A : Type; - Aplus : A -> A -> A; - Amult : A -> A -> A; - Aone : A; - Azero : A; - Aopp : A -> A; - Aeq : A -> A -> bool; - Ainv : A -> A; - Aminus : (field_rel_option A); - Adiv : (field_rel_option A); - RT : (Ring_Theory Aplus Amult Aone Azero Aopp Aeq); - Th_inv_def : (n:A)~(n=Azero)->(Amult (Ainv n) n)=Aone -}. - -(* The reflexion structure *) -Inductive ExprA : Set := -| EAzero : ExprA -| EAone : ExprA -| EAplus : ExprA -> ExprA -> ExprA -| EAmult : ExprA -> ExprA -> ExprA -| EAopp : ExprA -> ExprA -| EAinv : ExprA -> ExprA -| EAvar : nat -> ExprA. - -(**** Decidability of equality ****) - -Lemma eqExprA_O:(e1,e2:ExprA){e1=e2}+{~e1=e2}. -Proof. - Double Induction e1 e2;Try Intros; - Try (Left;Reflexivity) Orelse Try (Right;Discriminate). - Elim (H1 e0);Intro y;Elim (H2 e);Intro y0; - Try (Left; Rewrite y; Rewrite y0;Auto) - Orelse (Right;Red;Intro;Inversion H3;Auto). - Elim (H1 e0);Intro y;Elim (H2 e);Intro y0; - Try (Left; Rewrite y; Rewrite y0;Auto) - Orelse (Right;Red;Intro;Inversion H3;Auto). - Elim (H0 e);Intro y. - Left; Rewrite y; Auto. - Right;Red; Intro;Inversion H1;Auto. - Elim (H0 e);Intro y. - Left; Rewrite y; Auto. - Right;Red; Intro;Inversion H1;Auto. - Elim (eq_nat_dec n n0);Intro y. - Left; Rewrite y; Auto. - Right;Red;Intro;Inversion H;Auto. -Defined. - -Definition eq_nat_dec := Eval Compute in Peano_dec.eq_nat_dec. -Definition eqExprA := Eval Compute in eqExprA_O. - -(**** Generation of the multiplier ****) - -Fixpoint mult_of_list [e:(listT ExprA)]: ExprA := - Cases e of - | nilT => EAone - | (consT e1 l1) => (EAmult e1 (mult_of_list l1)) - end. - -Section Theory_of_fields. - -Variable T : Field_Theory. - -Local AT := (A T). -Local AplusT := (Aplus T). -Local AmultT := (Amult T). -Local AoneT := (Aone T). -Local AzeroT := (Azero T). -Local AoppT := (Aopp T). -Local AeqT := (Aeq T). -Local AinvT := (Ainv T). -Local RTT := (RT T). -Local Th_inv_defT := (Th_inv_def T). - -Add Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (Azero T) (Aopp T) - (Aeq T) (RT T). - -Add Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT. - -(***************************) -(* Lemmas to be used *) -(***************************) - -Lemma AplusT_sym:(r1,r2:AT)(AplusT r1 r2)=(AplusT r2 r1). -Proof. - Intros;Ring. -Save. - -Lemma AplusT_assoc:(r1,r2,r3:AT)(AplusT (AplusT r1 r2) r3)= - (AplusT r1 (AplusT r2 r3)). -Proof. - Intros;Ring. -Save. - -Lemma AmultT_sym:(r1,r2:AT)(AmultT r1 r2)=(AmultT r2 r1). -Proof. - Intros;Ring. -Save. - -Lemma AmultT_assoc:(r1,r2,r3:AT)(AmultT (AmultT r1 r2) r3)= - (AmultT r1 (AmultT r2 r3)). -Proof. - Intros;Ring. -Save. - -Lemma AplusT_Ol:(r:AT)(AplusT AzeroT r)=r. -Proof. - Intros;Ring. -Save. - -Lemma AmultT_1l:(r:AT)(AmultT AoneT r)=r. -Proof. - Intros;Ring. -Save. - -Lemma AplusT_AoppT_r:(r:AT)(AplusT r (AoppT r))=AzeroT. -Proof. - Intros;Ring. -Save. - -Lemma AmultT_AplusT_distr:(r1,r2,r3:AT)(AmultT r1 (AplusT r2 r3))= - (AplusT (AmultT r1 r2) (AmultT r1 r3)). -Proof. - Intros;Ring. -Save. - -Lemma r_AplusT_plus:(r,r1,r2:AT)(AplusT r r1)=(AplusT r r2)->r1=r2. -Proof. - Intros; Transitivity (AplusT (AplusT (AoppT r) r) r1). - Ring. - Transitivity (AplusT (AplusT (AoppT r) r) r2). - Repeat Rewrite -> AplusT_assoc; Rewrite <- H; Reflexivity. - Ring. -Save. - -Lemma r_AmultT_mult: - (r,r1,r2:AT)(AmultT r r1)=(AmultT r r2)->~r=AzeroT->r1=r2. -Proof. - Intros; Transitivity (AmultT (AmultT (AinvT r) r) r1). - Rewrite Th_inv_defT;[Symmetry; Apply AmultT_1l;Auto|Auto]. - Transitivity (AmultT (AmultT (AinvT r) r) r2). - Repeat Rewrite AmultT_assoc; Rewrite H; Trivial. - Rewrite Th_inv_defT;[Apply AmultT_1l;Auto|Auto]. -Save. - -Lemma AmultT_Or:(r:AT) (AmultT r AzeroT)=AzeroT. -Proof. - Intro; Ring. -Save. - -Lemma AmultT_Ol:(r:AT)(AmultT AzeroT r)=AzeroT. -Proof. - Intro; Ring. -Save. - -Lemma AmultT_1r:(r:AT)(AmultT r AoneT)=r. -Proof. - Intro; Ring. -Save. - -Lemma AinvT_r:(r:AT)~r=AzeroT->(AmultT r (AinvT r))=AoneT. -Proof. - Intros; Rewrite -> AmultT_sym; Apply Th_inv_defT; Auto. -Save. - -Lemma without_div_O_contr: - (r1,r2:AT)~(AmultT r1 r2)=AzeroT ->~r1=AzeroT/\~r2=AzeroT. -Proof. - Intros r1 r2 H; Split; Red; Intro; Apply H; Rewrite H0; Ring. -Save. - -(************************) -(* Interpretation *) -(************************) - -(**** ExprA --> A ****) - -Fixpoint interp_ExprA [lvar:(listT (prodT AT nat));e:ExprA] : AT := - Cases e of - | EAzero => AzeroT - | EAone => AoneT - | (EAplus e1 e2) => (AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2)) - | (EAmult e1 e2) => (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)) - | (EAopp e) => ((Aopp T) (interp_ExprA lvar e)) - | (EAinv e) => ((Ainv T) (interp_ExprA lvar e)) - | (EAvar n) => (assoc_2nd AT nat eq_nat_dec lvar n AzeroT) - end. - -(************************) -(* Simplification *) -(************************) - -(**** Associativity ****) - -Definition merge_mult := - Fix merge_mult {merge_mult [e1:ExprA] : ExprA -> ExprA := - [e2:ExprA]Cases e1 of - | (EAmult t1 t2) => - Cases t2 of - | (EAmult t2 t3) => (EAmult t1 (EAmult t2 (merge_mult t3 e2))) - | _ => (EAmult t1 (EAmult t2 e2)) - end - | _ => (EAmult e1 e2) - end}. - -Fixpoint assoc_mult [e:ExprA] : ExprA := - Cases e of - | (EAmult e1 e3) => - Cases e1 of - | (EAmult e1 e2) => - (merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2)) - (assoc_mult e3)) - | _ => (EAmult e1 (assoc_mult e3)) - end - | _ => e - end. - -Definition merge_plus := - Fix merge_plus {merge_plus [e1:ExprA]:ExprA->ExprA:= - [e2:ExprA]Cases e1 of - | (EAplus t1 t2) => - Cases t2 of - | (EAplus t2 t3) => (EAplus t1 (EAplus t2 (merge_plus t3 e2))) - | _ => (EAplus t1 (EAplus t2 e2)) - end - | _ => (EAplus e1 e2) - end}. - -Fixpoint assoc [e:ExprA] : ExprA := - Cases e of - | (EAplus e1 e3) => - Cases e1 of - | (EAplus e1 e2) => - (merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3)) - | _ => (EAplus (assoc_mult e1) (assoc e3)) - end - | _ => (assoc_mult e) - end. - -Lemma merge_mult_correct1: - (e1,e2,e3:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (merge_mult (EAmult e1 e2) e3))= - (interp_ExprA lvar (EAmult e1 (merge_mult e2 e3))). -Proof. -Intros e1 e2;Generalize e1;Generalize e2;Clear e1 e2. -Induction e2;Auto;Intros. -Unfold 1 merge_mult;Fold merge_mult; - Unfold 2 interp_ExprA;Fold interp_ExprA; - Rewrite (H0 e e3 lvar); - Unfold 1 interp_ExprA;Fold interp_ExprA; - Unfold 5 interp_ExprA;Fold interp_ExprA;Auto. -Save. - -Lemma merge_mult_correct: - (e1,e2:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (merge_mult e1 e2))= - (interp_ExprA lvar (EAmult e1 e2)). -Proof. -Induction e1;Auto;Intros. -Elim e0;Try (Intros;Simpl;Ring). -Unfold interp_ExprA in H2;Fold interp_ExprA in H2; - Cut (AmultT (interp_ExprA lvar e2) (AmultT (interp_ExprA lvar e4) - (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e3))))= - (AmultT (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4)) - (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). -Intro H3;Rewrite H3;Rewrite <-H2; - Rewrite merge_mult_correct1;Simpl;Ring. -Ring. -Save. - -Lemma assoc_mult_correct1:(e1,e2:ExprA)(lvar:(listT (prodT AT nat))) - (AmultT (interp_ExprA lvar (assoc_mult e1)) - (interp_ExprA lvar (assoc_mult e2)))= - (interp_ExprA lvar (assoc_mult (EAmult e1 e2))). -Proof. -Induction e1;Auto;Intros. -Rewrite <-(H e0 lvar);Simpl;Rewrite merge_mult_correct;Simpl; - Rewrite merge_mult_correct;Simpl;Auto. -Save. - -Lemma assoc_mult_correct: - (e:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (assoc_mult e))=(interp_ExprA lvar e). -Proof. -Induction e;Auto;Intros. -Elim e0;Intros. -Intros;Simpl;Ring. -Simpl;Rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1))); - Rewrite (AmultT_1l (interp_ExprA lvar e1)); Apply H0. -Simpl;Rewrite (H0 lvar);Auto. -Simpl;Rewrite merge_mult_correct;Simpl;Rewrite merge_mult_correct;Simpl; - Rewrite AmultT_assoc;Rewrite assoc_mult_correct1;Rewrite H2;Simpl; - Rewrite <-assoc_mult_correct1 in H1; - Unfold 3 interp_ExprA in H1;Fold interp_ExprA in H1; - Rewrite (H0 lvar) in H1; - Rewrite (AmultT_sym (interp_ExprA lvar e3) (interp_ExprA lvar e1)); - Rewrite <-AmultT_assoc;Rewrite H1;Rewrite AmultT_assoc;Ring. -Simpl;Rewrite (H0 lvar);Auto. -Simpl;Rewrite (H0 lvar);Auto. -Simpl;Rewrite (H0 lvar);Auto. -Save. - -Lemma merge_plus_correct1: - (e1,e2,e3:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (merge_plus (EAplus e1 e2) e3))= - (interp_ExprA lvar (EAplus e1 (merge_plus e2 e3))). -Proof. -Intros e1 e2;Generalize e1;Generalize e2;Clear e1 e2. -Induction e2;Auto;Intros. -Unfold 1 merge_plus;Fold merge_plus; - Unfold 2 interp_ExprA;Fold interp_ExprA; - Rewrite (H0 e e3 lvar); - Unfold 1 interp_ExprA;Fold interp_ExprA; - Unfold 5 interp_ExprA;Fold interp_ExprA;Auto. -Save. - -Lemma merge_plus_correct: - (e1,e2:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (merge_plus e1 e2))= - (interp_ExprA lvar (EAplus e1 e2)). -Proof. -Induction e1;Auto;Intros. -Elim e0;Try Intros;Try (Simpl;Ring). -Unfold interp_ExprA in H2;Fold interp_ExprA in H2; - Cut (AplusT (interp_ExprA lvar e2) (AplusT (interp_ExprA lvar e4) - (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e3))))= - (AplusT (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4)) - (interp_ExprA lvar e2)) (interp_ExprA lvar e3)). -Intro H3;Rewrite H3;Rewrite <-H2;Rewrite merge_plus_correct1;Simpl;Ring. -Ring. -Save. - -Lemma assoc_plus_correct:(e1,e2:ExprA)(lvar:(listT (prodT AT nat))) - (AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))= - (interp_ExprA lvar (assoc (EAplus e1 e2))). -Proof. -Induction e1;Auto;Intros. -Rewrite <-(H e0 lvar);Simpl;Rewrite merge_plus_correct;Simpl; - Rewrite merge_plus_correct;Simpl;Auto. -Save. - -Lemma assoc_correct: - (e:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (assoc e))=(interp_ExprA lvar e). -Proof. -Induction e;Auto;Intros. -Elim e0;Intros. -Simpl;Rewrite (H0 lvar);Auto. -Simpl;Rewrite (H0 lvar);Auto. -Simpl;Rewrite merge_plus_correct;Simpl;Rewrite merge_plus_correct; - Simpl;Rewrite AplusT_assoc;Rewrite assoc_plus_correct;Rewrite H2; - Simpl;Apply (r_AplusT_plus (interp_ExprA lvar (assoc e1)) - (AplusT (interp_ExprA lvar (assoc e2)) - (AplusT (interp_ExprA lvar e3) (interp_ExprA lvar e1))) - (AplusT (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e3)) - (interp_ExprA lvar e1)));Rewrite <-AplusT_assoc; - Rewrite (AplusT_sym (interp_ExprA lvar (assoc e1)) - (interp_ExprA lvar (assoc e2))); - Rewrite assoc_plus_correct;Rewrite H1;Simpl;Rewrite (H0 lvar); - Rewrite <-(AplusT_assoc (AplusT (interp_ExprA lvar e2) - (interp_ExprA lvar e1)) - (interp_ExprA lvar e3) (interp_ExprA lvar e1)); - Rewrite (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e1) - (interp_ExprA lvar e3)); - Rewrite (AplusT_sym (interp_ExprA lvar e1) (interp_ExprA lvar e3)); - Rewrite <-(AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3) - (interp_ExprA lvar e1));Apply AplusT_sym. -Unfold assoc;Fold assoc;Unfold interp_ExprA;Fold interp_ExprA; - Rewrite assoc_mult_correct;Rewrite (H0 lvar);Simpl;Auto. -Simpl;Rewrite (H0 lvar);Auto. -Simpl;Rewrite (H0 lvar);Auto. -Simpl;Rewrite (H0 lvar);Auto. -Unfold assoc;Fold assoc;Unfold interp_ExprA;Fold interp_ExprA; - Rewrite assoc_mult_correct;Simpl;Auto. -Save. - -(**** Distribution *****) - -Fixpoint distrib_EAopp [e:ExprA] : ExprA := - Cases e of - | (EAplus e1 e2) => (EAplus (distrib_EAopp e1) (distrib_EAopp e2)) - | (EAmult e1 e2) => (EAmult (distrib_EAopp e1) (distrib_EAopp e2)) - | (EAopp e) => (EAmult (EAopp EAone) (distrib_EAopp e)) - | e => e - end. - -Definition distrib_mult_right := - Fix distrib_mult_right {distrib_mult_right [e1:ExprA]:ExprA->ExprA:= - [e2:ExprA]Cases e1 of - | (EAplus t1 t2) => - (EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2)) - | _ => (EAmult e1 e2) - end}. - -Fixpoint distrib_mult_left [e1:ExprA] : ExprA->ExprA := - [e2:ExprA] - Cases e1 of - | (EAplus t1 t2) => - (EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2)) - | _ => (distrib_mult_right e2 e1) - end. - -Fixpoint distrib_main [e:ExprA] : ExprA := - Cases e of - | (EAmult e1 e2) => (distrib_mult_left (distrib_main e1) (distrib_main e2)) - | (EAplus e1 e2) => (EAplus (distrib_main e1) (distrib_main e2)) - | (EAopp e) => (EAopp (distrib_main e)) - | _ => e - end. - -Definition distrib [e:ExprA] : ExprA := (distrib_main (distrib_EAopp e)). - -Lemma distrib_mult_right_correct: - (e1,e2:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (distrib_mult_right e1 e2))= - (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)). -Proof. -Induction e1;Try Intros;Simpl;Auto. -Rewrite AmultT_sym;Rewrite AmultT_AplusT_distr; - Rewrite (H e2 lvar);Rewrite (H0 e2 lvar);Ring. -Save. - -Lemma distrib_mult_left_correct: - (e1,e2:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (distrib_mult_left e1 e2))= - (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)). -Proof. -Induction e1;Try Intros;Simpl. -Rewrite AmultT_Ol;Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_Or. -Rewrite distrib_mult_right_correct;Simpl; - Apply AmultT_sym. -Rewrite AmultT_sym; - Rewrite (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e) - (interp_ExprA lvar e0)); - Rewrite (AmultT_sym (interp_ExprA lvar e2) (interp_ExprA lvar e)); - Rewrite (AmultT_sym (interp_ExprA lvar e2) (interp_ExprA lvar e0)); - Rewrite (H e2 lvar);Rewrite (H0 e2 lvar);Auto. -Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym. -Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym. -Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym. -Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym. -Save. - -Lemma distrib_correct: - (e:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (distrib e))=(interp_ExprA lvar e). -Proof. -Induction e;Intros;Auto. -Simpl;Rewrite <- (H lvar);Rewrite <- (H0 lvar); Unfold distrib;Simpl;Auto. -Simpl;Rewrite <- (H lvar);Rewrite <- (H0 lvar); Unfold distrib;Simpl; - Apply distrib_mult_left_correct. -Simpl;Fold AoppT;Rewrite <- (H lvar);Unfold distrib;Simpl; - Rewrite distrib_mult_right_correct; - Simpl;Fold AoppT;Ring. -Save. - -(**** Multiplication by the inverse product ****) - -Lemma mult_eq: - (e1,e2,a:ExprA)(lvar:(listT (prodT AT nat))) - ~((interp_ExprA lvar a)=AzeroT)-> - (interp_ExprA lvar (EAmult a e1))=(interp_ExprA lvar (EAmult a e2))-> - (interp_ExprA lvar e1)=(interp_ExprA lvar e2). -Proof. - Simpl;Intros; - Apply (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1) - (interp_ExprA lvar e2));Assumption. -Save. - -Fixpoint multiply_aux [a,e:ExprA] : ExprA := - Cases e of - | (EAplus e1 e2) => - (EAplus (EAmult a e1) (multiply_aux a e2)) - | _ => (EAmult a e) - end. - -Definition multiply [e:ExprA] : ExprA := - Cases e of - | (EAmult a e1) => (multiply_aux a e1) - | _ => e - end. - -Lemma multiply_aux_correct: - (a,e:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (multiply_aux a e))= - (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)). -Proof. -Induction e;Simpl;Intros;Try (Rewrite merge_mult_correct);Auto. - Simpl;Rewrite (H0 lvar);Ring. -Save. - -Lemma multiply_correct: - (e:ExprA)(lvar:(listT (prodT AT nat))) - (interp_ExprA lvar (multiply e))=(interp_ExprA lvar e). -Proof. - Induction e;Simpl;Auto. - Intros;Apply multiply_aux_correct. -Save. - -(**** Permutations and simplification ****) - -Fixpoint monom_remove [a,m:ExprA] : ExprA := - Cases m of - | (EAmult m0 m1) => - (Cases (eqExprA m0 (EAinv a)) of - | (left _) => m1 - | (right _) => (EAmult m0 (monom_remove a m1)) - end) - | _ => - (Cases (eqExprA m (EAinv a)) of - | (left _) => EAone - | (right _) => (EAmult a m) - end) - end. - -Definition monom_simplif_rem := - Fix monom_simplif_rem {monom_simplif_rem/1:ExprA->ExprA->ExprA:= - [a,m:ExprA] - Cases a of - | (EAmult a0 a1) => (monom_simplif_rem a1 (monom_remove a0 m)) - | _ => (monom_remove a m) - end}. - -Definition monom_simplif [a,m:ExprA] : ExprA := - Cases m of - | (EAmult a' m') => - (Cases (eqExprA a a') of - | (left _) => (monom_simplif_rem a m') - | (right _) => m - end) - | _ => m - end. - -Fixpoint inverse_simplif [a,e:ExprA] : ExprA := - Cases e of - | (EAplus e1 e2) => (EAplus (monom_simplif a e1) (inverse_simplif a e2)) - | _ => (monom_simplif a e) - end. - -Lemma monom_remove_correct:(e,a:ExprA) - (lvar:(listT (prodT AT nat)))~((interp_ExprA lvar a)=AzeroT)-> - (interp_ExprA lvar (monom_remove a e))= - (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)). -Proof. -Induction e; Intros. -Simpl;Case (eqExprA EAzero (EAinv a));Intros;[Inversion e0|Simpl;Trivial]. -Simpl;Case (eqExprA EAone (EAinv a));Intros;[Inversion e0|Simpl;Trivial]. -Simpl;Case (eqExprA (EAplus e0 e1) (EAinv a));Intros;[Inversion e2| - Simpl;Trivial]. -Simpl;Case (eqExprA e0 (EAinv a));Intros. -Rewrite e2;Simpl;Fold AinvT. -Rewrite <-(AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a)) - (interp_ExprA lvar e1)); - Rewrite AinvT_r;[Ring|Assumption]. -Simpl;Rewrite H0;Auto; Ring. -Simpl;Fold AoppT;Case (eqExprA (EAopp e0) (EAinv a));Intros;[Inversion e1| - Simpl;Trivial]. -Unfold monom_remove;Case (eqExprA (EAinv e0) (EAinv a));Intros. -Case (eqExprA e0 a);Intros. -Rewrite e2;Simpl;Fold AinvT;Rewrite AinvT_r;Auto. -Inversion e1;Simpl;ElimType False;Auto. -Simpl;Trivial. -Unfold monom_remove;Case (eqExprA (EAvar n) (EAinv a));Intros; - [Inversion e0|Simpl;Trivial]. -Save. - -Lemma monom_simplif_rem_correct:(a,e:ExprA) - (lvar:(listT (prodT AT nat)))~((interp_ExprA lvar a)=AzeroT)-> - (interp_ExprA lvar (monom_simplif_rem a e))= - (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)). -Proof. -Induction a;Simpl;Intros; Try Rewrite monom_remove_correct;Auto. -Elim (without_div_O_contr (interp_ExprA lvar e) - (interp_ExprA lvar e0) H1);Intros. -Rewrite (H0 (monom_remove e e1) lvar H3);Rewrite monom_remove_correct;Auto. -Ring. -Save. - -Lemma monom_simplif_correct:(e,a:ExprA) - (lvar:(listT (prodT AT nat)))~((interp_ExprA lvar a)=AzeroT)-> - (interp_ExprA lvar (monom_simplif a e))=(interp_ExprA lvar e). -Proof. -Induction e;Intros;Auto. -Simpl;Case (eqExprA a e0);Intros. -Rewrite <-e2;Apply monom_simplif_rem_correct;Auto. -Simpl;Trivial. -Save. - -Lemma inverse_correct: - (e,a:ExprA)(lvar:(listT (prodT AT nat)))~((interp_ExprA lvar a)=AzeroT)-> - (interp_ExprA lvar (inverse_simplif a e))=(interp_ExprA lvar e). -Proof. -Induction e;Intros;Auto. -Simpl;Rewrite (H0 a lvar H1); Rewrite monom_simplif_correct ; Auto. -Unfold inverse_simplif;Rewrite monom_simplif_correct ; Auto. -Save. - -End Theory_of_fields. |