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, 0 insertions, 1086 deletions
diff --git a/contrib7/field/Field.v b/contrib7/field/Field.v deleted file mode 100644 index f282e246..00000000 --- a/contrib7/field/Field.v +++ /dev/null @@ -1,15 +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.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 deleted file mode 100644 index 2cc01038..00000000 --- a/contrib7/field/Field_Compl.v +++ /dev/null @@ -1,62 +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_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 deleted file mode 100644 index ffd2aad4..00000000 --- a/contrib7/field/Field_Tactic.v +++ /dev/null @@ -1,397 +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_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 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. |