diff options
Diffstat (limited to 'contrib7/field/Field_Theory.v')
| -rw-r--r-- | contrib7/field/Field_Theory.v | 612 |
1 files changed, 612 insertions, 0 deletions
diff --git a/contrib7/field/Field_Theory.v b/contrib7/field/Field_Theory.v new file mode 100644 index 00000000..3ba2fbc0 --- /dev/null +++ b/contrib7/field/Field_Theory.v @@ -0,0 +1,612 @@ +(************************************************************************) +(* 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. |