diff options
Diffstat (limited to 'contrib/field')
| -rw-r--r-- | contrib/field/Field.v | 15 | ||||
| -rw-r--r-- | contrib/field/Field_Compl.v | 61 | ||||
| -rw-r--r-- | contrib/field/Field_Tactic.v | 432 | ||||
| -rw-r--r-- | contrib/field/Field_Theory.v | 645 | ||||
| -rw-r--r-- | contrib/field/field.ml4 | 190 |
5 files changed, 1343 insertions, 0 deletions
diff --git a/contrib/field/Field.v b/contrib/field/Field.v new file mode 100644 index 00000000..7b48e275 --- /dev/null +++ b/contrib/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.6.2.1 2004/07/16 19:30:09 herbelin Exp $ *) + +Require Export Field_Compl. +Require Export Field_Theory. +Require Export Field_Tactic. + +(* Command declarations are moved to the ML side *)
\ No newline at end of file diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v new file mode 100644 index 00000000..cba921f7 --- /dev/null +++ b/contrib/field/Field_Compl.v @@ -0,0 +1,61 @@ +(************************************************************************) +(* 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.8.2.1 2004/07/16 19:30:09 herbelin Exp $ *) + +Inductive listT (A:Type) : Type := + | nilT : listT A + | consT : A -> listT A -> listT A. + +Fixpoint appT (A:Type) (l m:listT A) {struct l} : listT A := + match l with + | 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 (A:Type) (B:Set) + (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2}) + (lst:listT (prodT A B)) {struct lst} : + B -> A -> A := + fun (key:B) (default:A) => + match lst with + | nilT => default + | consT (pairT v e) l => + match eq_dec e key with + | left _ => v + | right _ => assoc_2nd_rec A B eq_dec l key default + end + end). + +Definition fstT (A B:Type) (c:prodT A B) := match c with + | pairT a _ => a + end. + +Definition sndT (A B:Type) (c:prodT A B) := match c with + | pairT _ a => a + end. + +Definition mem := + (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) + (a:A) (l:listT A) {struct l} : bool := + match l with + | nilT => false + | consT a1 l1 => + match eq_dec a a1 with + | 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.
\ No newline at end of file diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v new file mode 100644 index 00000000..c5c06547 --- /dev/null +++ b/contrib/field/Field_Tactic.v @@ -0,0 +1,432 @@ +(************************************************************************) +(* 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.20.2.1 2004/07/16 19:30:09 herbelin Exp $ *) + +Require Import Ring. +Require Export Field_Compl. +Require Export Field_Theory. + +(**** Interpretation A --> ExprA ****) + +Ltac mem_assoc var lvar := + match constr:lvar with + | (nilT _) => constr:false + | (consT _ ?X1 ?X2) => + match constr:(X1 = var) with + | (?X1 = ?X1) => constr:true + | _ => mem_assoc var X2 + end + end. + +Ltac seek_var_aux FT lvar trm := + let AT := eval cbv beta iota delta [A] in (A FT) + with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT) + with AoneT := eval cbv beta iota delta [Aone] in (Aone FT) + with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) + with AmultT := eval cbv beta iota delta [Amult] in (Amult FT) + with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT) + with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in + match constr:trm with + | AzeroT => lvar + | AoneT => lvar + | (AplusT ?X1 ?X2) => + let l1 := seek_var_aux FT lvar X1 in + seek_var_aux FT l1 X2 + | (AmultT ?X1 ?X2) => + let l1 := seek_var_aux FT lvar X1 in + seek_var_aux FT l1 X2 + | (AoppT ?X1) => seek_var_aux FT lvar X1 + | (AinvT ?X1) => seek_var_aux FT lvar X1 + | ?X1 => + let res := mem_assoc X1 lvar in + match constr:res with + | true => lvar + | false => constr:(consT AT X1 lvar) + end + end. + +Ltac seek_var FT trm := + let AT := eval cbv beta iota delta [A] in (A FT) in + seek_var_aux FT (nilT AT) trm. + +Ltac number_aux lvar cpt := + match constr:lvar with + | (nilT ?X1) => constr:(nilT (prodT X1 nat)) + | (consT ?X1 ?X2 ?X3) => + let l2 := number_aux X3 (S cpt) in + constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2) + end. + +Ltac number lvar := number_aux lvar 0. + +Ltac build_varlist FT trm := let lvar := seek_var FT trm in + number lvar. + +Ltac assoc elt lst := + match constr:lst with + | (nilT _) => fail + | (consT (prodT _ nat) (pairT _ nat ?X1 ?X2) ?X3) => + match constr:(elt = X1) with + | (?X1 = ?X1) => constr:X2 + | _ => assoc elt X3 + end + end. + +Ltac interp_A FT lvar trm := + let AT := eval cbv beta iota delta [A] in (A FT) + with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT) + with AoneT := eval cbv beta iota delta [Aone] in (Aone FT) + with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) + with AmultT := eval cbv beta iota delta [Amult] in (Amult FT) + with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT) + with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in + match constr:trm with + | AzeroT => constr:EAzero + | AoneT => constr:EAone + | (AplusT ?X1 ?X2) => + let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in + constr:(EAplus e1 e2) + | (AmultT ?X1 ?X2) => + let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in + constr:(EAmult e1 e2) + | (AoppT ?X1) => + let e := interp_A FT lvar X1 in + constr:(EAopp e) + | (AinvT ?X1) => let e := interp_A FT lvar X1 in + constr:(EAinv e) + | ?X1 => let idx := assoc X1 lvar in + constr:(EAvar idx) + end. + +(************************) +(* Simplification *) +(************************) + +(**** Generation of the multiplier ****) + +Ltac remove e l := + match constr:l with + | (nilT _) => l + | (consT ?X1 e ?X2) => constr:X2 + | (consT ?X1 ?X2 ?X3) => let nl := remove e X3 in + constr:(consT X1 X2 nl) + end. + +Ltac union l1 l2 := + match constr:l1 with + | (nilT _) => l2 + | (consT ?X1 ?X2 ?X3) => + let nl2 := remove X2 l2 in + let nl := union X3 nl2 in + constr:(consT X1 X2 nl) + end. + +Ltac raw_give_mult trm := + match constr:trm with + | (EAinv ?X1) => constr:(consT ExprA X1 (nilT ExprA)) + | (EAopp ?X1) => raw_give_mult X1 + | (EAplus ?X1 ?X2) => + let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in + union l1 l2 + | (EAmult ?X1 ?X2) => + let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in + eval compute in (appT ExprA l1 l2) + | _ => constr:(nilT ExprA) + end. + +Ltac give_mult trm := + let ltrm := raw_give_mult trm in + constr:(mult_of_list ltrm). + +(**** Associativity ****) + +Ltac apply_assoc FT lvar trm := + let t := eval compute in (assoc trm) in + match constr:(t = trm) with + | (?X1 = ?X1) => idtac + | _ => + rewrite <- (assoc_correct FT trm); change (assoc trm) with t in |- * + end. + +(**** Distribution *****) + +Ltac apply_distrib FT lvar trm := + let t := eval compute in (distrib trm) in + match constr:(t = trm) with + | (?X1 = ?X1) => idtac + | _ => + rewrite <- (distrib_correct FT trm); + change (distrib trm) with t in |- * + end. + +(**** Multiplication by the inverse product ****) + +Ltac grep_mult := match goal with + | id:(interp_ExprA _ _ _ <> _) |- _ => id + end. + +Ltac weak_reduce := + match goal with + | |- context [(interp_ExprA ?X1 ?X2 _)] => + cbv beta iota zeta + delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero + Aone Aplus Amult Aopp Ainv] in |- * + end. + +Ltac multiply mul := + match goal with + | |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA ?X1 ?X2 ?X4) => + let AzeroT := eval cbv beta iota delta [Azero X1] in (Azero X1) in + (cut (interp_ExprA X1 X2 mul <> AzeroT); + [ intro; let id := grep_mult in + apply (mult_eq X1 X3 X4 mul X2 id) + | weak_reduce; + let AoneT := eval cbv beta iota delta [Aone X1] in (Aone X1) + with AmultT := eval cbv beta iota delta [Amult X1] in (Amult X1) in + (try + match goal with + | |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r X1) + end; clear X1 X2) ]) + end. + +Ltac apply_multiply FT lvar trm := + let t := eval compute in (multiply trm) in + match constr:(t = trm) with + | (?X1 = ?X1) => idtac + | _ => + rewrite <- (multiply_correct FT trm); + change (multiply trm) with t in |- * + end. + +(**** Permutations and simplification ****) + +Ltac apply_inverse mul FT lvar trm := + let t := eval compute in (inverse_simplif mul trm) in + match constr:(t = trm) with + | (?X1 = ?X1) => idtac + | _ => + rewrite <- (inverse_correct FT trm mul); + [ change (inverse_simplif mul trm) with t in |- * | assumption ] + end. +(**** Inverse test ****) + +Ltac strong_fail tac := first [ tac | fail 2 ]. + +Ltac inverse_test_aux FT trm := + let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) + with AmultT := eval cbv beta iota delta [Amult] in (Amult FT) + with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT) + with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in + match constr:trm with + | (AinvT _) => fail 1 + | (AoppT ?X1) => + strong_fail ltac:(inverse_test_aux FT X1; idtac) + | (AplusT ?X1 ?X2) => + strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2) + | (AmultT ?X1 ?X2) => + strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2) + | _ => idtac + end. + +Ltac inverse_test FT := + let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) in + match goal with + | |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2) + end. + +(**** Field itself ****) + +Ltac apply_simplif sfun := + match goal with + | |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) => + sfun X1 X2 X3 + end; + match goal with + | |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) => + sfun X1 X2 X3 + end. + +Ltac unfolds FT := + match eval cbv beta iota delta [Aminus] in (Aminus FT) with + | (Field_Some _ ?X1) => unfold X1 in |- * + | _ => idtac + end; + match eval cbv beta iota delta [Adiv] in (Adiv FT) with + | (Field_Some _ ?X1) => unfold X1 in |- * + | _ => idtac + end. + +Ltac reduce FT := + let AzeroT := eval cbv beta iota delta [Azero] in (Azero FT) + with AoneT := eval cbv beta iota delta [Aone] in (Aone FT) + with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) + with AmultT := eval cbv beta iota delta [Amult] in (Amult FT) + with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT) + with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in + (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] in |- * || + compute in |- *). + +Ltac field_gen_aux FT := + let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT) in + match goal with + | |- (?X1 = ?X2) => + let lvar := build_varlist FT (AplusT X1 X2) in + let trm1 := interp_A FT lvar X1 with trm2 := interp_A FT lvar X2 in + let mul := give_mult (EAplus trm1 trm2) in + (cut + (let ft := FT in + let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2); + [ compute in |- *; auto + | intros ft vm; apply_simplif apply_distrib; + apply_simplif apply_assoc; multiply mul; + [ apply_simplif apply_multiply; + apply_simplif ltac:(apply_inverse mul); + let id := grep_mult in + clear id; weak_reduce; clear ft vm; first + [ inverse_test FT; ring | field_gen_aux FT ] + | idtac ] ]) + end. + +Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT. + +(*****************************) +(* Term Simplification *) +(*****************************) + +(**** Minus and division expansions ****) + +Ltac init_exp FT trm := + let e := + (match eval cbv beta iota delta [Aminus] in (Aminus FT) with + | (Field_Some _ ?X1) => eval cbv beta delta [X1] in trm + | _ => trm + end) in + match eval cbv beta iota delta [Adiv] in (Adiv FT) with + | (Field_Some _ ?X1) => eval cbv beta delta [X1] in e + | _ => e + end. + +(**** Inverses simplification ****) + +Ltac simpl_inv trm := + match constr:trm with + | (EAplus ?X1 ?X2) => + let e1 := simpl_inv X1 with e2 := simpl_inv X2 in + constr:(EAplus e1 e2) + | (EAmult ?X1 ?X2) => + let e1 := simpl_inv X1 with e2 := simpl_inv X2 in + constr:(EAmult e1 e2) + | (EAopp ?X1) => let e := simpl_inv X1 in + constr:(EAopp e) + | (EAinv ?X1) => SimplInvAux X1 + | ?X1 => constr:X1 + end + with SimplInvAux trm := + match constr:trm with + | (EAinv ?X1) => simpl_inv X1 + | (EAmult ?X1 ?X2) => + let e1 := simpl_inv (EAinv X1) with e2 := simpl_inv (EAinv X2) in + constr:(EAmult e1 e2) + | ?X1 => let e := simpl_inv X1 in + constr:(EAinv e) + end. + +(**** Monom simplification ****) + +Ltac map_tactic fcn lst := + match constr:lst with + | (nilT _) => lst + | (consT ?X1 ?X2 ?X3) => + let r := fcn X2 with t := map_tactic fcn X3 in + constr:(consT X1 r t) + end. + +Ltac build_monom_aux lst trm := + match constr:lst with + | (nilT _) => eval compute in (assoc trm) + | (consT _ ?X1 ?X2) => build_monom_aux X2 (EAmult trm X1) + end. + +Ltac build_monom lnum lden := + let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in + let ltot := eval compute in (appT ExprA lnum ildn) in + let trm := build_monom_aux ltot EAone in + match constr:trm with + | (EAmult _ ?X1) => constr:X1 + | ?X1 => constr:X1 + end. + +Ltac simpl_monom_aux lnum lden trm := + match constr:trm with + | (EAmult (EAinv ?X1) ?X2) => + let mma := mem_assoc X1 lnum in + match constr:mma with + | true => + let newlnum := remove X1 lnum in + simpl_monom_aux newlnum lden X2 + | false => simpl_monom_aux lnum (consT ExprA X1 lden) X2 + end + | (EAmult ?X1 ?X2) => + let mma := mem_assoc X1 lden in + match constr:mma with + | true => + let newlden := remove X1 lden in + simpl_monom_aux lnum newlden X2 + | false => simpl_monom_aux (consT ExprA X1 lnum) lden X2 + end + | (EAinv ?X1) => + let mma := mem_assoc X1 lnum in + match constr:mma with + | true => + let newlnum := remove X1 lnum in + build_monom newlnum lden + | false => build_monom lnum (consT ExprA X1 lden) + end + | ?X1 => + let mma := mem_assoc X1 lden in + match constr:mma with + | true => + let newlden := remove X1 lden in + build_monom lnum newlden + | false => build_monom (consT ExprA X1 lnum) lden + end + end. + +Ltac simpl_monom trm := simpl_monom_aux (nilT ExprA) (nilT ExprA) trm. + +Ltac simpl_all_monomials trm := + match constr:trm with + | (EAplus ?X1 ?X2) => + let e1 := simpl_monom X1 with e2 := simpl_all_monomials X2 in + constr:(EAplus e1 e2) + | ?X1 => simpl_monom X1 + end. + +(**** Associativity and distribution ****) + +Ltac assoc_distrib trm := eval compute in (assoc (distrib trm)). + +(**** The tactic Field_Term ****) + +Ltac eval_weak_reduce trm := + eval + cbv beta iota zeta + delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero Aone Aplus + Amult Aopp Ainv] in trm. + +Ltac field_term FT exp := + let newexp := init_exp FT exp in + let lvar := build_varlist FT newexp in + let trm := interp_A FT lvar newexp in + let tma := eval compute in (assoc trm) in + let tsmp := + simpl_all_monomials + ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in + let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in + (replace exp with trep; [ ring trep | field_gen FT ]).
\ No newline at end of file diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v new file mode 100644 index 00000000..8737fd79 --- /dev/null +++ b/contrib/field/Field_Theory.v @@ -0,0 +1,645 @@ +(************************************************************************) +(* 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.12.2.1 2004/07/16 19:30:09 herbelin Exp $ *) + +Require Import Peano_dec. +Require Import Ring. +Require Import 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 : forall 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 : forall e1 e2:ExprA, {e1 = e2} + {e1 <> e2}. +Proof. + double induction e1 e2; try intros; + try (left; reflexivity) || (try (right; discriminate)). + elim (H1 e0); intro y; elim (H2 e); intro y0; + try + (left; rewrite y; rewrite y0; auto) || + (right; red in |- *; intro; inversion H3; auto). + elim (H1 e0); intro y; elim (H2 e); intro y0; + try + (left; rewrite y; rewrite y0; auto) || + (right; red in |- *; intro; inversion H3; auto). + elim (H0 e); intro y. + left; rewrite y; auto. + right; red in |- *; intro; inversion H1; auto. + elim (H0 e); intro y. + left; rewrite y; auto. + right; red in |- *; intro; inversion H1; auto. + elim (eq_nat_dec n n0); intro y. + left; rewrite y; auto. + right; red in |- *; intro; inversion H; auto. +Defined. + +Definition eq_nat_dec := Eval compute in eq_nat_dec. +Definition eqExprA := Eval compute in eqExprA_O. + +(**** Generation of the multiplier ****) + +Fixpoint mult_of_list (e:listT ExprA) : ExprA := + match e with + | nilT => EAone + | consT e1 l1 => EAmult e1 (mult_of_list l1) + end. + +Section Theory_of_fields. + +Variable T : Field_Theory. + +Let AT := A T. +Let AplusT := Aplus T. +Let AmultT := Amult T. +Let AoneT := Aone T. +Let AzeroT := Azero T. +Let AoppT := Aopp T. +Let AeqT := Aeq T. +Let AinvT := Ainv T. +Let RTT := RT T. +Let 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 : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1. +Proof. + intros; ring. +Qed. + +Lemma AplusT_assoc : + forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3). +Proof. + intros; ring. +Qed. + +Lemma AmultT_sym : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1. +Proof. + intros; ring. +Qed. + +Lemma AmultT_assoc : + forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3). +Proof. + intros; ring. +Qed. + +Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r. +Proof. + intros; ring. +Qed. + +Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r. +Proof. + intros; ring. +Qed. + +Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT. +Proof. + intros; ring. +Qed. + +Lemma AmultT_AplusT_distr : + forall r1 r2 r3:AT, + AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3). +Proof. + intros; ring. +Qed. + +Lemma r_AplusT_plus : forall 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. +Qed. + +Lemma r_AmultT_mult : + forall 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 in |- *; 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 ]. +Qed. + +Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT. +Proof. + intro; ring. +Qed. + +Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT. +Proof. + intro; ring. +Qed. + +Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r. +Proof. + intro; ring. +Qed. + +Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT. +Proof. + intros; rewrite AmultT_sym; apply Th_inv_defT; auto. +Qed. + +Lemma Rmult_neq_0_reg : + forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT. +Proof. + intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; ring. +Qed. + +(************************) +(* Interpretation *) +(************************) + +(**** ExprA --> A ****) + +Fixpoint interp_ExprA (lvar:listT (prodT AT nat)) (e:ExprA) {struct e} : + AT := + match e with + | 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 (e1:ExprA) : ExprA -> ExprA := + fun e2:ExprA => + match e1 with + | EAmult t1 t2 => + match t2 with + | 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 := + match e with + | EAmult e1 e3 => + match e1 with + | 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 (e1:ExprA) : ExprA -> ExprA := + fun e2:ExprA => + match e1 with + | EAplus t1 t2 => + match t2 with + | 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 := + match e with + | EAplus e1 e3 => + match e1 with + | 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 : + forall (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. +simple induction e2; auto; intros. +unfold merge_mult at 1 in |- *; fold merge_mult in |- *; + unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *; + rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *; + fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *; + fold interp_ExprA in |- *; auto. +Qed. + +Lemma merge_mult_correct : + forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)), + interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2). +Proof. +simple induction e1; auto; intros. +elim e0; try (intros; simpl in |- *; 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 in |- *; ring. +ring. +Qed. + +Lemma assoc_mult_correct1 : + forall (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. +simple induction e1; auto; intros. +rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct; + simpl in |- *; rewrite merge_mult_correct; simpl in |- *; + auto. +Qed. + +Lemma assoc_mult_correct : + forall (e:ExprA) (lvar:listT (prodT AT nat)), + interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e. +Proof. +simple induction e; auto; intros. +elim e0; intros. +intros; simpl in |- *; ring. +simpl in |- *; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1))); + rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite merge_mult_correct; simpl in |- *; + rewrite merge_mult_correct; simpl in |- *; rewrite AmultT_assoc; + rewrite assoc_mult_correct1; rewrite H2; simpl in |- *; + rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 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 in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +Qed. + +Lemma merge_plus_correct1 : + forall (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. +simple induction e2; auto; intros. +unfold merge_plus at 1 in |- *; fold merge_plus in |- *; + unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *; + rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *; + fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *; + fold interp_ExprA in |- *; auto. +Qed. + +Lemma merge_plus_correct : + forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)), + interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2). +Proof. +simple induction e1; auto; intros. +elim e0; try intros; try (simpl in |- *; 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 in |- *; ring. +ring. +Qed. + +Lemma assoc_plus_correct : + forall (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. +simple induction e1; auto; intros. +rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct; + simpl in |- *; rewrite merge_plus_correct; simpl in |- *; + auto. +Qed. + +Lemma assoc_correct : + forall (e:ExprA) (lvar:listT (prodT AT nat)), + interp_ExprA lvar (assoc e) = interp_ExprA lvar e. +Proof. +simple induction e; auto; intros. +elim e0; intros. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite merge_plus_correct; simpl in |- *; + rewrite merge_plus_correct; simpl in |- *; rewrite AplusT_assoc; + rewrite assoc_plus_correct; rewrite H2; simpl in |- *; + 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 in |- *; + 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 in |- *; fold assoc in |- *; unfold interp_ExprA in |- *; + fold interp_ExprA in |- *; rewrite assoc_mult_correct; + rewrite (H0 lvar); simpl in |- *; auto. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +simpl in |- *; rewrite (H0 lvar); auto. +unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *; + fold interp_ExprA in |- *; rewrite assoc_mult_correct; + simpl in |- *; auto. +Qed. + +(**** Distribution *****) + +Fixpoint distrib_EAopp (e:ExprA) : ExprA := + match e with + | 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 (e1:ExprA) : ExprA -> ExprA := + fun e2:ExprA => + match e1 with + | EAplus t1 t2 => + EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2) + | _ => EAmult e1 e2 + end). + +Fixpoint distrib_mult_left (e1 e2:ExprA) {struct e1} : ExprA := + match e1 with + | 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 := + match e with + | 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 : + forall (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. +simple induction e1; try intros; simpl in |- *; auto. +rewrite AmultT_sym; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar); + rewrite (H0 e2 lvar); ring. +Qed. + +Lemma distrib_mult_left_correct : + forall (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. +simple induction e1; try intros; simpl in |- *. +rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl in |- *; + apply AmultT_Or. +rewrite distrib_mult_right_correct; simpl in |- *; 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 in |- *; apply AmultT_sym. +rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym. +rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym. +rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym. +Qed. + +Lemma distrib_correct : + forall (e:ExprA) (lvar:listT (prodT AT nat)), + interp_ExprA lvar (distrib e) = interp_ExprA lvar e. +Proof. +simple induction e; intros; auto. +simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar); + unfold distrib in |- *; simpl in |- *; auto. +simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar); + unfold distrib in |- *; simpl in |- *; apply distrib_mult_left_correct. +simpl in |- *; fold AoppT in |- *; rewrite <- (H lvar); + unfold distrib in |- *; simpl in |- *; rewrite distrib_mult_right_correct; + simpl in |- *; fold AoppT in |- *; ring. +Qed. + +(**** Multiplication by the inverse product ****) + +Lemma mult_eq : + forall (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 in |- *; intros; + apply + (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1) + (interp_ExprA lvar e2)); assumption. +Qed. + +Fixpoint multiply_aux (a e:ExprA) {struct e} : ExprA := + match e with + | EAplus e1 e2 => EAplus (EAmult a e1) (multiply_aux a e2) + | _ => EAmult a e + end. + +Definition multiply (e:ExprA) : ExprA := + match e with + | EAmult a e1 => multiply_aux a e1 + | _ => e + end. + +Lemma multiply_aux_correct : + forall (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. +simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct; + auto. + simpl in |- *; rewrite (H0 lvar); ring. +Qed. + +Lemma multiply_correct : + forall (e:ExprA) (lvar:listT (prodT AT nat)), + interp_ExprA lvar (multiply e) = interp_ExprA lvar e. +Proof. + simple induction e; simpl in |- *; auto. + intros; apply multiply_aux_correct. +Qed. + +(**** Permutations and simplification ****) + +Fixpoint monom_remove (a m:ExprA) {struct m} : ExprA := + match m with + | EAmult m0 m1 => + match eqExprA m0 (EAinv a) with + | left _ => m1 + | right _ => EAmult m0 (monom_remove a m1) + end + | _ => + match eqExprA m (EAinv a) with + | left _ => EAone + | right _ => EAmult a m + end + end. + +Definition monom_simplif_rem := + (fix monom_simplif_rem (a:ExprA) : ExprA -> ExprA := + fun m:ExprA => + match a with + | EAmult a0 a1 => monom_simplif_rem a1 (monom_remove a0 m) + | _ => monom_remove a m + end). + +Definition monom_simplif (a m:ExprA) : ExprA := + match m with + | EAmult a' m' => + match eqExprA a a' with + | left _ => monom_simplif_rem a m' + | right _ => m + end + | _ => m + end. + +Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA := + match e with + | EAplus e1 e2 => EAplus (monom_simplif a e1) (inverse_simplif a e2) + | _ => monom_simplif a e + end. + +Lemma monom_remove_correct : + forall (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. +simple induction e; intros. +simpl in |- *; case (eqExprA EAzero (EAinv a)); intros; + [ inversion e0 | simpl in |- *; trivial ]. +simpl in |- *; case (eqExprA EAone (EAinv a)); intros; + [ inversion e0 | simpl in |- *; trivial ]. +simpl in |- *; case (eqExprA (EAplus e0 e1) (EAinv a)); intros; + [ inversion e2 | simpl in |- *; trivial ]. +simpl in |- *; case (eqExprA e0 (EAinv a)); intros. +rewrite e2; simpl in |- *; fold AinvT in |- *. +rewrite <- + (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a)) + (interp_ExprA lvar e1)); rewrite AinvT_r; [ ring | assumption ]. +simpl in |- *; rewrite H0; auto; ring. +simpl in |- *; fold AoppT in |- *; case (eqExprA (EAopp e0) (EAinv a)); + intros; [ inversion e1 | simpl in |- *; trivial ]. +unfold monom_remove in |- *; case (eqExprA (EAinv e0) (EAinv a)); intros. +case (eqExprA e0 a); intros. +rewrite e2; simpl in |- *; fold AinvT in |- *; rewrite AinvT_r; auto. +inversion e1; simpl in |- *; elimtype False; auto. +simpl in |- *; trivial. +unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros; + [ inversion e0 | simpl in |- *; trivial ]. +Qed. + +Lemma monom_simplif_rem_correct : + forall (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. +simple induction a; simpl in |- *; intros; try rewrite monom_remove_correct; + auto. +elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1); + intros. +rewrite (H0 (monom_remove e e1) lvar H3); rewrite monom_remove_correct; auto. +ring. +Qed. + +Lemma monom_simplif_correct : + forall (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. +simple induction e; intros; auto. +simpl in |- *; case (eqExprA a e0); intros. +rewrite <- e2; apply monom_simplif_rem_correct; auto. +simpl in |- *; trivial. +Qed. + +Lemma inverse_correct : + forall (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. +simple induction e; intros; auto. +simpl in |- *; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto. +unfold inverse_simplif in |- *; rewrite monom_simplif_correct; auto. +Qed. + +End Theory_of_fields.
\ No newline at end of file diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 new file mode 100644 index 00000000..32adec66 --- /dev/null +++ b/contrib/field/field.ml4 @@ -0,0 +1,190 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id: field.ml4,v 1.33.2.1 2004/07/16 19:30:09 herbelin Exp $ *) + +open Names +open Pp +open Proof_type +open Tacinterp +open Tacmach +open Term +open Typing +open Util +open Vernacinterp +open Vernacexpr +open Tacexpr + +(* Interpretation of constr's *) +let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c + +(* Construction of constants *) +let constant dir s = Coqlib.gen_constant "Field" ("field"::dir) s + +(* To deal with the optional arguments *) +let constr_of_opt a opt = + let ac = constr_of a in + match opt with + | None -> mkApp ((constant ["Field_Compl"] "Field_None"),[|ac|]) + | Some f -> mkApp ((constant ["Field_Compl"] "Field_Some"),[|ac;constr_of f|]) + +(* Table of theories *) +let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t) + +let lookup env typ = + try Gmap.find typ !th_tab + with Not_found -> + errorlabstrm "field" + (str "No field is declared for type" ++ spc() ++ + Printer.prterm_env env typ) + +let _ = + let init () = th_tab := Gmap.empty in + let freeze () = !th_tab in + let unfreeze fs = th_tab := fs in + Summary.declare_summary "field" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + +let load_addfield _ = () +let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab +let subst_addfield (_,subst,(typ,th as obj)) = + let typ' = subst_mps subst typ in + let th' = subst_mps subst th in + if typ' == typ && th' == th then obj else + (typ',th') +let export_addfield x = Some x + +(* Declaration of the Add Field library object *) +let (in_addfield,out_addfield)= + Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with + Libobject.open_function = (fun i o -> if i=1 then cache_addfield o); + Libobject.cache_function = cache_addfield; + Libobject.subst_function = subst_addfield; + Libobject.classify_function = (fun (_,a) -> Libobject.Substitute a); + Libobject.export_function = export_addfield } + +(* Adds a theory to the table *) +let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth + ainv_l = + begin + (try + Ring.add_theory true true false a None None None aplus amult aone azero + (Some aopp) aeq rth Quote.ConstrSet.empty + with | UserError("Add Semi Ring",_) -> ()); + let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"), + [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in + begin + let _ = type_of (Global.env ()) Evd.empty th in (); + Lib.add_anonymous_leaf (in_addfield (a,th)) + end + end + +(* Vernac command declaration *) +open Extend +open Pcoq +open Genarg + +VERNAC ARGUMENT EXTEND divarg +| [ "div" ":=" constr(adiv) ] -> [ adiv ] +END + +VERNAC ARGUMENT EXTEND minusarg +| [ "minus" ":=" constr(aminus) ] -> [ aminus ] +END + +(* +(* The v7->v8 translator needs printers, then temporary use ARGUMENT EXTEND...*) +VERNAC ARGUMENT EXTEND minus_div_arg +| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ] +| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ] +| [ ] -> [ None, None ] +END +*) + +(* For the translator, otherwise the code above is OK *) +open Ppconstrnew +let pp_minus_div_arg _prc _prt (omin,odiv) = + if omin=None && odiv=None then mt() else + spc() ++ str "with" ++ + pr_opt (fun c -> str "minus := " ++ _prc c) omin ++ + pr_opt (fun c -> str "div := " ++ _prc c) odiv +(* +let () = + Pptactic.declare_extra_genarg_pprule true + (rawwit_minus_div_arg,pp_minus_div_arg) + (globwit_minus_div_arg,pp_minus_div_arg) + (wit_minus_div_arg,pp_minus_div_arg) +*) +ARGUMENT EXTEND minus_div_arg + TYPED AS constr_opt * constr_opt + PRINTED BY pp_minus_div_arg +| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ] +| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ] +| [ ] -> [ None, None ] +END + +VERNAC COMMAND EXTEND Field + [ "Add" "Field" + constr(a) constr(aplus) constr(amult) constr(aone) + constr(azero) constr(aopp) constr(aeq) + constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ] + -> [ let (aminus_o, adiv_o) = md in + add_field + (constr_of a) (constr_of aplus) (constr_of amult) + (constr_of aone) (constr_of azero) (constr_of aopp) + (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o) + (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l) ] +END + +(* Guesses the type and calls field_gen with the right theory *) +let field g = + Library.check_required_library ["Coq";"field";"Field"]; + let ist = { lfun=[]; debug=get_debug () } in + let typ = + match Hipattern.match_with_equation (pf_concl g) with + | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t + | _ -> error "The statement is not built from Leibniz' equality" in + let th = VConstr (lookup (pf_env g) typ) in + (interp_tac_gen [(id_of_string "FT",th)] (get_debug ()) + <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g + +(* Verifies that all the terms have the same type and gives the right theory *) +let guess_theory env evc = function + | c::tl -> + let t = type_of env evc c in + if List.exists (fun c1 -> + not (Reductionops.is_conv env evc t (type_of env evc c1))) tl then + errorlabstrm "Field:" (str" All the terms must have the same type") + else + lookup env t + | [] -> anomaly "Field: must have a non-empty constr list here" + +(* Guesses the type and calls Field_Term with the right theory *) +let field_term l g = + Library.check_required_library ["Coq";"field";"Field"]; + let env = (pf_env g) + and evc = (project g) in + let th = valueIn (VConstr (guess_theory env evc l)) + and nl = List.map (fun x -> valueIn (VConstr x)) (Quote.sort_subterm g l) in + (List.fold_right + (fun c a -> + let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in + Tacticals.tclTHENFIRSTn tac [|a|]) nl Tacticals.tclIDTAC) g + +(* Declaration of Field *) + +TACTIC EXTEND Field +| [ "Field" ] -> [ field ] +| [ "Field" ne_constr_list(l) ] -> [ field_term l ] +END |