diff options
Diffstat (limited to 'contrib7/field')
| -rw-r--r-- | contrib7/field/Field.v | 15 | ||||
| -rw-r--r-- | contrib7/field/Field_Compl.v | 62 | ||||
| -rw-r--r-- | contrib7/field/Field_Tactic.v | 397 | ||||
| -rw-r--r-- | contrib7/field/Field_Theory.v | 612 |
4 files changed, 1086 insertions, 0 deletions
diff --git a/contrib7/field/Field.v b/contrib7/field/Field.v new file mode 100644 index 00000000..f282e246 --- /dev/null +++ b/contrib7/field/Field.v @@ -0,0 +1,15 @@ +(************************************************************************) +(* 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.v,v 1.1.2.1 2004/07/16 19:30:17 herbelin Exp $ *) + +Require Export Field_Compl. +Require Export Field_Theory. +Require Export Field_Tactic. + +(* Command declarations are moved to the ML side *) diff --git a/contrib7/field/Field_Compl.v b/contrib7/field/Field_Compl.v new file mode 100644 index 00000000..2cc01038 --- /dev/null +++ b/contrib7/field/Field_Compl.v @@ -0,0 +1,62 @@ +(************************************************************************) +(* 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_Compl.v,v 1.2.2.1 2004/07/16 19:30:17 herbelin Exp $ *) + +Inductive listT [A:Type] : Type := + nilT : (listT A) | consT : A->(listT A)->(listT A). + +Fixpoint appT [A:Type][l:(listT A)] : (listT A) -> (listT A) := + [m:(listT A)] + Cases l of + | nilT => m + | (consT a l1) => (consT A a (appT A l1 m)) + end. + +Inductive prodT [A,B:Type] : Type := + pairT: A->B->(prodT A B). + +Definition assoc_2nd := +Fix assoc_2nd_rec + {assoc_2nd_rec + [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(listT (prodT A B))] + : B->A->A:= + [key:B;default:A] + Cases lst of + | nilT => default + | (consT (pairT v e) l) => + (Cases (eq_dec e key) of + | (left _) => v + | (right _) => (assoc_2nd_rec A B eq_dec l key default) + end) + end}. + +Definition fstT [A,B:Type;c:(prodT A B)] := + Cases c of + | (pairT a _) => a + end. + +Definition sndT [A,B:Type;c:(prodT A B)] := + Cases c of + | (pairT _ a) => a + end. + +Definition mem := +Fix mem {mem [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(listT A)] : bool := + Cases l of + | nilT => false + | (consT a1 l1) => + Cases (eq_dec a a1) of + | (left _) => true + | (right _) => (mem A eq_dec a l1) + end + end}. + +Inductive field_rel_option [A:Type] : Type := + | Field_None : (field_rel_option A) + | Field_Some : (A -> A -> A) -> (field_rel_option A). diff --git a/contrib7/field/Field_Tactic.v b/contrib7/field/Field_Tactic.v new file mode 100644 index 00000000..ffd2aad4 --- /dev/null +++ b/contrib7/field/Field_Tactic.v @@ -0,0 +1,397 @@ +(************************************************************************) +(* 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_Tactic.v,v 1.2.2.1 2004/07/16 19:30:17 herbelin Exp $ *) + +Require Ring. +Require Export Field_Compl. +Require Export Field_Theory. + +(**** Interpretation A --> ExprA ****) + +Recursive Tactic Definition MemAssoc var lvar := + Match lvar With + | [(nilT ?)] -> false + | [(consT ? ?1 ?2)] -> + (Match ?1=var With + | [?1=?1] -> true + | _ -> (MemAssoc var ?2)). + +Recursive Tactic Definition SeekVarAux FT lvar trm := + Let AT = Eval Cbv Beta Delta [A] Iota in (A FT) + And AzeroT = Eval Cbv Beta Delta [Azero] Iota in (Azero FT) + And AoneT = Eval Cbv Beta Delta [Aone] Iota in (Aone FT) + And AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) + And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT) + And AoppT = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT) + And AinvT = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In + Match trm With + | [(AzeroT)] -> lvar + | [(AoneT)] -> lvar + | [(AplusT ?1 ?2)] -> + Let l1 = (SeekVarAux FT lvar ?1) In + (SeekVarAux FT l1 ?2) + | [(AmultT ?1 ?2)] -> + Let l1 = (SeekVarAux FT lvar ?1) In + (SeekVarAux FT l1 ?2) + | [(AoppT ?1)] -> (SeekVarAux FT lvar ?1) + | [(AinvT ?1)] -> (SeekVarAux FT lvar ?1) + | [?1] -> + Let res = (MemAssoc ?1 lvar) In + Match res With + | [(true)] -> lvar + | [(false)] -> '(consT AT ?1 lvar). + +Tactic Definition SeekVar FT trm := + Let AT = Eval Cbv Beta Delta [A] Iota in (A FT) In + (SeekVarAux FT '(nilT AT) trm). + +Recursive Tactic Definition NumberAux lvar cpt := + Match lvar With + | [(nilT ?1)] -> '(nilT (prodT ?1 nat)) + | [(consT ?1 ?2 ?3)] -> + Let l2 = (NumberAux ?3 '(S cpt)) In + '(consT (prodT ?1 nat) (pairT ?1 nat ?2 cpt) l2). + +Tactic Definition Number lvar := (NumberAux lvar O). + +Tactic Definition BuildVarList FT trm := + Let lvar = (SeekVar FT trm) In + (Number lvar). +V7only [ +(*Used by contrib Maple *) +Tactic Definition build_var_list := BuildVarList. +]. + +Recursive Tactic Definition Assoc elt lst := + Match lst With + | [(nilT ?)] -> Fail + | [(consT (prodT ? nat) (pairT ? nat ?1 ?2) ?3)] -> + Match elt= ?1 With + | [?1= ?1] -> ?2 + | _ -> (Assoc elt ?3). + +Recursive Meta Definition interp_A FT lvar trm := + Let AT = Eval Cbv Beta Delta [A] Iota in (A FT) + And AzeroT = Eval Cbv Beta Delta [Azero] Iota in (Azero FT) + And AoneT = Eval Cbv Beta Delta [Aone] Iota in (Aone FT) + And AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) + And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT) + And AoppT = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT) + And AinvT = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In + Match trm With + | [(AzeroT)] -> EAzero + | [(AoneT)] -> EAone + | [(AplusT ?1 ?2)] -> + Let e1 = (interp_A FT lvar ?1) + And e2 = (interp_A FT lvar ?2) In + '(EAplus e1 e2) + | [(AmultT ?1 ?2)] -> + Let e1 = (interp_A FT lvar ?1) + And e2 = (interp_A FT lvar ?2) In + '(EAmult e1 e2) + | [(AoppT ?1)] -> + Let e = (interp_A FT lvar ?1) In + '(EAopp e) + | [(AinvT ?1)] -> + Let e = (interp_A FT lvar ?1) In + '(EAinv e) + | [?1] -> + Let idx = (Assoc ?1 lvar) In + '(EAvar idx). + +(************************) +(* Simplification *) +(************************) + +(**** Generation of the multiplier ****) + +Recursive Tactic Definition Remove e l := + Match l With + | [(nilT ?)] -> l + | [(consT ?1 e ?2)] -> ?2 + | [(consT ?1 ?2 ?3)] -> + Let nl = (Remove e ?3) In + '(consT ?1 ?2 nl). + +Recursive Tactic Definition Union l1 l2 := + Match l1 With + | [(nilT ?)] -> l2 + | [(consT ?1 ?2 ?3)] -> + Let nl2 = (Remove ?2 l2) In + Let nl = (Union ?3 nl2) In + '(consT ?1 ?2 nl). + +Recursive Tactic Definition RawGiveMult trm := + Match trm With + | [(EAinv ?1)] -> '(consT ExprA ?1 (nilT ExprA)) + | [(EAopp ?1)] -> (RawGiveMult ?1) + | [(EAplus ?1 ?2)] -> + Let l1 = (RawGiveMult ?1) + And l2 = (RawGiveMult ?2) In + (Union l1 l2) + | [(EAmult ?1 ?2)] -> + Let l1 = (RawGiveMult ?1) + And l2 = (RawGiveMult ?2) In + Eval Compute in (appT ExprA l1 l2) + | _ -> '(nilT ExprA). + +Tactic Definition GiveMult trm := + Let ltrm = (RawGiveMult trm) In + '(mult_of_list ltrm). + +(**** Associativity ****) + +Tactic Definition ApplyAssoc FT lvar trm := + Let t=Eval Compute in (assoc trm) In + Match t=trm With + | [ ?1=?1 ] -> Idtac + | _ -> Rewrite <- (assoc_correct FT trm); Change (assoc trm) with t. + +(**** Distribution *****) + +Tactic Definition ApplyDistrib FT lvar trm := + Let t=Eval Compute in (distrib trm) In + Match t=trm With + | [ ?1=?1 ] -> Idtac + | _ -> Rewrite <- (distrib_correct FT trm); Change (distrib trm) with t. + +(**** Multiplication by the inverse product ****) + +Tactic Definition GrepMult := + Match Context With + | [ id: ~(interp_ExprA ? ? ?)= ? |- ?] -> id. + +Tactic Definition WeakReduce := + Match Context With + | [|-[(interp_ExprA ?1 ?2 ?)]] -> + Cbv Beta Delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list ?1 ?2 A + Azero Aone Aplus Amult Aopp Ainv] Zeta Iota. + +Tactic Definition Multiply mul := + Match Context With + | [|-(interp_ExprA ?1 ?2 ?3)=(interp_ExprA ?1 ?2 ?4)] -> + Let AzeroT = Eval Cbv Beta Delta [Azero ?1] Iota in (Azero ?1) In + Cut ~(interp_ExprA ?1 ?2 mul)=AzeroT; + [Intro; + Let id = GrepMult In + Apply (mult_eq ?1 ?3 ?4 mul ?2 id) + |WeakReduce; + Let AoneT = Eval Cbv Beta Delta [Aone ?1] Iota in (Aone ?1) + And AmultT = Eval Cbv Beta Delta [Amult ?1] Iota in (Amult ?1) In + Try (Match Context With + | [|-[(AmultT ? AoneT)]] -> Rewrite (AmultT_1r ?1));Clear ?1 ?2]. + +Tactic Definition ApplyMultiply FT lvar trm := + Let t=Eval Compute in (multiply trm) In + Match t=trm With + | [ ?1=?1 ] -> Idtac + | _ -> Rewrite <- (multiply_correct FT trm); Change (multiply trm) with t. + +(**** Permutations and simplification ****) + +Tactic Definition ApplyInverse mul FT lvar trm := + Let t=Eval Compute in (inverse_simplif mul trm) In + Match t=trm With + | [ ?1=?1 ] -> Idtac + | _ -> Rewrite <- (inverse_correct FT trm mul); + [Change (inverse_simplif mul trm) with t|Assumption]. +(**** Inverse test ****) + +Tactic Definition StrongFail tac := First [tac|Fail 2]. + +Recursive Tactic Definition InverseTestAux FT trm := + Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) + And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT) + And AoppT = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT) + And AinvT = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In + Match trm With + | [(AinvT ?)] -> Fail 1 + | [(AoppT ?1)] -> StrongFail ((InverseTestAux FT ?1);Idtac) + | [(AplusT ?1 ?2)] -> + StrongFail ((InverseTestAux FT ?1);(InverseTestAux FT ?2)) + | [(AmultT ?1 ?2)] -> + StrongFail ((InverseTestAux FT ?1);(InverseTestAux FT ?2)) + | _ -> Idtac. + +Tactic Definition InverseTest FT := + Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) In + Match Context With + | [|- ?1=?2] -> (InverseTestAux FT '(AplusT ?1 ?2)). + +(**** Field itself ****) + +Tactic Definition ApplySimplif sfun := + (Match Context With + | [|- (interp_ExprA ?1 ?2 ?3)=(interp_ExprA ? ? ?)] -> + (sfun ?1 ?2 ?3)); + (Match Context With + | [|- (interp_ExprA ? ? ?)=(interp_ExprA ?1 ?2 ?3)] -> + (sfun ?1 ?2 ?3)). + +Tactic Definition Unfolds FT := + (Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With + | [(Field_Some ? ?1)] -> Unfold ?1 + | _ -> Idtac); + (Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With + | [(Field_Some ? ?1)] -> Unfold ?1 + | _ -> Idtac). + +Tactic Definition Reduce FT := + Let AzeroT = Eval Cbv Beta Delta [Azero] Iota in (Azero FT) + And AoneT = Eval Cbv Beta Delta [Aone] Iota in (Aone FT) + And AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) + And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT) + And AoppT = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT) + And AinvT = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In + Cbv Beta Delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] Zeta Iota + Orelse Compute. + +Recursive Tactic Definition Field_Gen_Aux FT := + Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) In + Match Context With + | [|- ?1=?2] -> + Let lvar = (BuildVarList FT '(AplusT ?1 ?2)) In + Let trm1 = (interp_A FT lvar ?1) + And trm2 = (interp_A FT lvar ?2) In + Let mul = (GiveMult '(EAplus trm1 trm2)) In + Cut [ft:=FT][vm:=lvar](interp_ExprA ft vm trm1)=(interp_ExprA ft vm trm2); + [Compute;Auto + |Intros ft vm;(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc); + (Multiply mul);[(ApplySimplif ApplyMultiply); + (ApplySimplif (ApplyInverse mul)); + (Let id = GrepMult In Clear id);WeakReduce;Clear ft vm; + First [(InverseTest FT);Ring|(Field_Gen_Aux FT)]|Idtac]]. + +Tactic Definition Field_Gen FT := + Unfolds FT;((InverseTest FT);Ring) Orelse (Field_Gen_Aux FT). +V7only [Tactic Definition field_gen := Field_Gen.]. + +(*****************************) +(* Term Simplification *) +(*****************************) + +(**** Minus and division expansions ****) + +Meta Definition InitExp FT trm := + Let e = + (Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With + | [(Field_Some ? ?1)] -> Eval Cbv Beta Delta [?1] in trm + | _ -> trm) In + Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With + | [(Field_Some ? ?1)] -> Eval Cbv Beta Delta [?1] in e + | _ -> e. +V7only [ +(*Used by contrib Maple *) +Tactic Definition init_exp := InitExp. +]. + +(**** Inverses simplification ****) + +Recursive Meta Definition SimplInv trm:= + Match trm With + | [(EAplus ?1 ?2)] -> + Let e1 = (SimplInv ?1) + And e2 = (SimplInv ?2) In + '(EAplus e1 e2) + | [(EAmult ?1 ?2)] -> + Let e1 = (SimplInv ?1) + And e2 = (SimplInv ?2) In + '(EAmult e1 e2) + | [(EAopp ?1)] -> Let e = (SimplInv ?1) In '(EAopp e) + | [(EAinv ?1)] -> (SimplInvAux ?1) + | [?1] -> ?1 +And SimplInvAux trm := + Match trm With + | [(EAinv ?1)] -> (SimplInv ?1) + | [(EAmult ?1 ?2)] -> + Let e1 = (SimplInv '(EAinv ?1)) + And e2 = (SimplInv '(EAinv ?2)) In + '(EAmult e1 e2) + | [?1] -> Let e = (SimplInv ?1) In '(EAinv e). + +(**** Monom simplification ****) + +Recursive Meta Definition Map fcn lst := + Match lst With + | [(nilT ?)] -> lst + | [(consT ?1 ?2 ?3)] -> + Let r = (fcn ?2) + And t = (Map fcn ?3) In + '(consT ?1 r t). + +Recursive Meta Definition BuildMonomAux lst trm := + Match lst With + | [(nilT ?)] -> Eval Compute in (assoc trm) + | [(consT ? ?1 ?2)] -> BuildMonomAux ?2 '(EAmult trm ?1). + +Recursive Meta Definition BuildMonom lnum lden := + Let ildn = (Map (Fun e -> '(EAinv e)) lden) In + Let ltot = Eval Compute in (appT ExprA lnum ildn) In + Let trm = (BuildMonomAux ltot EAone) In + Match trm With + | [(EAmult ? ?1)] -> ?1 + | [?1] -> ?1. + +Recursive Meta Definition SimplMonomAux lnum lden trm := + Match trm With + | [(EAmult (EAinv ?1) ?2)] -> + Let mma = (MemAssoc ?1 lnum) In + (Match mma With + | [true] -> + Let newlnum = (Remove ?1 lnum) In SimplMonomAux newlnum lden ?2 + | [false] -> SimplMonomAux lnum '(consT ExprA ?1 lden) ?2) + | [(EAmult ?1 ?2)] -> + Let mma = (MemAssoc ?1 lden) In + (Match mma With + | [true] -> + Let newlden = (Remove ?1 lden) In SimplMonomAux lnum newlden ?2 + | [false] -> SimplMonomAux '(consT ExprA ?1 lnum) lden ?2) + | [(EAinv ?1)] -> + Let mma = (MemAssoc ?1 lnum) In + (Match mma With + | [true] -> + Let newlnum = (Remove ?1 lnum) In BuildMonom newlnum lden + | [false] -> BuildMonom lnum '(consT ExprA ?1 lden)) + | [?1] -> + Let mma = (MemAssoc ?1 lden) In + (Match mma With + | [true] -> + Let newlden = (Remove ?1 lden) In BuildMonom lnum newlden + | [false] -> BuildMonom '(consT ExprA ?1 lnum) lden). + +Meta Definition SimplMonom trm := + SimplMonomAux '(nilT ExprA) '(nilT ExprA) trm. + +Recursive Meta Definition SimplAllMonoms trm := + Match trm With + | [(EAplus ?1 ?2)] -> + Let e1 = (SimplMonom ?1) + And e2 = (SimplAllMonoms ?2) In + '(EAplus e1 e2) + | [?1] -> SimplMonom ?1. + +(**** Associativity and distribution ****) + +Meta Definition AssocDistrib trm := Eval Compute in (assoc (distrib trm)). + +(**** The tactic Field_Term ****) + +Tactic Definition EvalWeakReduce trm := + Eval Cbv Beta Delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero + Aone Aplus Amult Aopp Ainv] Zeta Iota in trm. + +Tactic Definition Field_Term FT exp := + Let newexp = (InitExp FT exp) In + Let lvar = (BuildVarList FT newexp) In + Let trm = (interp_A FT lvar newexp) In + Let tma = Eval Compute in (assoc trm) In + Let tsmp = (SimplAllMonoms (AssocDistrib (SimplAllMonoms + (SimplInv tma)))) In + Let trep = (EvalWeakReduce '(interp_ExprA FT lvar tsmp)) In + Replace exp with trep;[Ring trep|Field_Gen FT]. 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. |