diff options
Diffstat (limited to 'contrib7/field/Field_Tactic.v')
-rw-r--r-- | contrib7/field/Field_Tactic.v | 397 |
1 files changed, 397 insertions, 0 deletions
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]. |