diff options
Diffstat (limited to 'plugins/field')
| -rw-r--r-- | plugins/field/LegacyField.v | 14 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Compl.v | 36 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Tactic.v | 431 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Theory.v | 648 | ||||
| -rw-r--r-- | plugins/field/field.ml4 | 191 | ||||
| -rw-r--r-- | plugins/field/field_plugin.mllib | 2 | ||||
| -rw-r--r-- | plugins/field/vo.itarget | 4 |
7 files changed, 0 insertions, 1326 deletions
diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v deleted file mode 100644 index a5a85790..00000000 --- a/plugins/field/LegacyField.v +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Export LegacyField_Compl. -Require Export LegacyField_Theory. -Require Export LegacyField_Tactic. -Declare ML Module "field_plugin". - -(* Command declarations are moved to the ML side *) diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v deleted file mode 100644 index 89f824e5..00000000 --- a/plugins/field/LegacyField_Compl.v +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import List. - -Definition assoc_2nd := - (fix assoc_2nd_rec (A:Type) (B:Set) - (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2}) - (lst:list (prod A B)) {struct lst} : - B -> A -> A := - fun (key:B) (default:A) => - match lst with - | nil => default - | (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 mem := - (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) - (a:A) (l:list A) {struct l} : bool := - match l with - | nil => false - | a1 :: l1 => - match eq_dec a a1 with - | left _ => true - | right _ => mem A eq_dec a l1 - end - end). diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v deleted file mode 100644 index 8a55d582..00000000 --- a/plugins/field/LegacyField_Tactic.v +++ /dev/null @@ -1,431 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import List. -Require Import LegacyRing. -Require Export LegacyField_Compl. -Require Export LegacyField_Theory. - -(**** Interpretation A --> ExprA ****) - -Ltac get_component a s := eval cbv beta iota delta [a] in (a s). - -Ltac body_of s := eval cbv beta iota delta [s] in s. - -Ltac mem_assoc var lvar := - match constr:lvar with - | nil => constr:false - | ?X1 :: ?X2 => - match constr:(X1 = var) with - | (?X1 = ?X1) => constr:true - | _ => mem_assoc var X2 - end - end. - -Ltac number lvar := - let rec number_aux lvar cpt := - match constr:lvar with - | (@nil ?X1) => constr:(@nil (prod X1 nat)) - | ?X2 :: ?X3 => - let l2 := number_aux X3 (S cpt) in - constr:((X2,cpt) :: l2) - end - in number_aux lvar 0. - -Ltac build_varlist FT trm := - let rec seek_var lvar trm := - let AT := get_component A FT - with AzeroT := get_component Azero FT - with AoneT := get_component Aone FT - with AplusT := get_component Aplus FT - with AmultT := get_component Amult FT - with AoppT := get_component Aopp FT - with AinvT := get_component Ainv FT in - match constr:trm with - | AzeroT => lvar - | AoneT => lvar - | (AplusT ?X1 ?X2) => - let l1 := seek_var lvar X1 in - seek_var l1 X2 - | (AmultT ?X1 ?X2) => - let l1 := seek_var lvar X1 in - seek_var l1 X2 - | (AoppT ?X1) => seek_var lvar X1 - | (AinvT ?X1) => seek_var lvar X1 - | ?X1 => - let res := mem_assoc X1 lvar in - match constr:res with - | true => lvar - | false => constr:(X1 :: lvar) - end - end in - let AT := get_component A FT in - let lvar := seek_var (@nil AT) trm in - number lvar. - -Ltac assoc elt lst := - match constr:lst with - | nil => fail - | (?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 := get_component A FT - with AzeroT := get_component Azero FT - with AoneT := get_component Aone FT - with AplusT := get_component Aplus FT - with AmultT := get_component Amult FT - with AoppT := get_component Aopp FT - with AinvT := get_component 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 - | nil => l - | e :: ?X2 => constr:X2 - | ?X2 :: ?X3 => let nl := remove e X3 in constr:(X2 :: nl) - end. - -Ltac union l1 l2 := - match constr:l1 with - | nil => l2 - | ?X2 :: ?X3 => - let nl2 := remove X2 l2 in - let nl := union X3 nl2 in - constr:(X2 :: nl) - end. - -Ltac raw_give_mult trm := - match constr:trm with - | (EAinv ?X1) => constr:(X1 :: nil) - | (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 (app l1 l2) - | _ => constr:(@nil 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 - 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 - 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] - end. - -Ltac multiply mul := - match goal with - | |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) => - let AzeroT := get_component Azero FT in - cut (interp_ExprA FT X2 mul <> AzeroT); - [ intro; (let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id)) - | weak_reduce; - (let AoneT := get_component Aone ltac:(body_of FT) - with AmultT := get_component Amult ltac:(body_of FT) in - try - match goal with - | |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT) - end; clear FT 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 - 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 | assumption ] - end. -(**** Inverse test ****) - -Ltac strong_fail tac := first [ tac | fail 2 ]. - -Ltac inverse_test_aux FT trm := - let AplusT := get_component Aplus FT - with AmultT := get_component Amult FT - with AoppT := get_component Aopp FT - with AinvT := get_component 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 := get_component 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 get_component Aminus FT with - | Some ?X1 => unfold X1 - | _ => idtac - end; - match get_component Adiv FT with - | Some ?X1 => unfold X1 - | _ => idtac - end. - -Ltac reduce FT := - let AzeroT := get_component Azero FT - with AoneT := get_component Aone FT - with AplusT := get_component Aplus FT - with AmultT := get_component Amult FT - with AoppT := get_component Aopp FT - with AinvT := get_component Ainv FT in - (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] || - compute). - -Ltac field_gen_aux FT := - let AplusT := get_component 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; 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; legacy ring | field_gen_aux FT ]) - | idtac ] ] - end. - -Ltac field_gen FT := - unfolds FT; (inverse_test FT; legacy ring) || field_gen_aux FT. - -(*****************************) -(* Term Simplification *) -(*****************************) - -(**** Minus and division expansions ****) - -Ltac init_exp FT trm := - let e := - (match get_component Aminus FT with - | Some ?X1 => eval cbv beta delta [X1] in trm - | _ => trm - end) in - match get_component Adiv FT with - | 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 - | nil => lst - | ?X2 :: ?X3 => - let r := fcn X2 with t := map_tactic fcn X3 in - constr:(r :: t) - end. - -Ltac build_monom_aux lst trm := - match constr:lst with - | nil => eval compute in (assoc trm) - | ?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 (app 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 (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 (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 (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 (X1 :: lnum) lden - end - end. - -Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil 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; [ legacy ring trep | field_gen FT ]). diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v deleted file mode 100644 index 39926f65..00000000 --- a/plugins/field/LegacyField_Theory.v +++ /dev/null @@ -1,648 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import List. -Require Import Peano_dec. -Require Import LegacyRing. -Require Import LegacyField_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 : option (A -> A -> A); - Adiv : option (A -> A -> 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; intro; inversion H3; auto). - elim (H1 e0); intro y; elim (H2 e); intro y0; - try - (left; rewrite y; rewrite y0; auto) || - (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 eq_nat_dec. -Definition eqExprA := Eval compute in eqExprA_O. - -(**** Generation of the multiplier ****) - -Fixpoint mult_of_list (e:list ExprA) : ExprA := - match e with - | nil => EAone - | 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 Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) ( - Azero T) (Aopp T) (Aeq T) (RT T). - -Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT. - -(***************************) -(* Lemmas to be used *) -(***************************) - -Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1. -Proof. - intros; legacy ring. -Qed. - -Lemma AplusT_assoc : - forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3). -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1. -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_assoc : - forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3). -Proof. - intros; legacy ring. -Qed. - -Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r. -Proof. - intros; legacy ring. -Qed. - -Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r. -Proof. - intros; legacy ring. -Qed. - -Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT. -Proof. - intros; legacy 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; legacy 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). - legacy ring. - transitivity (AplusT (AplusT (AoppT r) r) r2). - repeat rewrite AplusT_assoc; rewrite <- H; reflexivity. - legacy 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 ; 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; legacy ring. -Qed. - -Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT. -Proof. - intro; legacy ring. -Qed. - -Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r. -Proof. - intro; legacy ring. -Qed. - -Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT. -Proof. - intros; rewrite AmultT_comm; 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; intro; apply H; rewrite H0; legacy ring. -Qed. - -(************************) -(* Interpretation *) -(************************) - -(**** ExprA --> A ****) - -Fixpoint interp_ExprA (lvar:list (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:list (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; fold merge_mult; - unfold interp_ExprA at 2; fold interp_ExprA; - rewrite (H0 e e3 lvar); unfold interp_ExprA at 1; - fold interp_ExprA; unfold interp_ExprA at 5; - fold interp_ExprA; auto. -Qed. - -Lemma merge_mult_correct : - forall (e1 e2:ExprA) (lvar:list (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; legacy 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; legacy ring. -legacy ring. -Qed. - -Lemma assoc_mult_correct1 : - forall (e1 e2:ExprA) (lvar:list (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; rewrite merge_mult_correct; - simpl; rewrite merge_mult_correct; simpl; - auto. -Qed. - -Lemma assoc_mult_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e. -Proof. -simple induction e; auto; intros. -elim e0; intros. -intros; simpl; legacy 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 interp_ExprA at 3 in H1; - fold interp_ExprA in H1; rewrite (H0 lvar) in H1; - rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1)); - rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc; - legacy ring. -simpl; rewrite (H0 lvar); auto. -simpl; rewrite (H0 lvar); auto. -simpl; rewrite (H0 lvar); auto. -Qed. - -Lemma merge_plus_correct1 : - forall (e1 e2 e3:ExprA) (lvar:list (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; fold merge_plus; - unfold interp_ExprA at 2; fold interp_ExprA; - rewrite (H0 e e3 lvar); unfold interp_ExprA at 1; - fold interp_ExprA; unfold interp_ExprA at 5; - fold interp_ExprA; auto. -Qed. - -Lemma merge_plus_correct : - forall (e1 e2:ExprA) (lvar:list (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; legacy 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; legacy ring. -legacy ring. -Qed. - -Lemma assoc_plus_correct : - forall (e1 e2:ExprA) (lvar:list (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; rewrite merge_plus_correct; - simpl; rewrite merge_plus_correct; simpl; - auto. -Qed. - -Lemma assoc_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (assoc e) = interp_ExprA lvar e. -Proof. -simple 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_comm (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_comm (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_comm. -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. -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:list (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; auto. -rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar); - rewrite (H0 e2 lvar); legacy ring. -Qed. - -Lemma distrib_mult_left_correct : - forall (e1 e2:ExprA) (lvar:list (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. -rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl; - apply AmultT_Or. -rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. -rewrite AmultT_comm; - rewrite - (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e) - (interp_ExprA lvar e0)); - rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e)); - rewrite (AmultT_comm (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_comm. -rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. -Qed. - -Lemma distrib_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (distrib e) = interp_ExprA lvar e. -Proof. -simple 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; legacy ring. -Qed. - -(**** Multiplication by the inverse product ****) - -Lemma mult_eq : - forall (e1 e2 a:ExprA) (lvar:list (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. -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:list (AT * nat)), - interp_ExprA lvar (multiply_aux a e) = - AmultT (interp_ExprA lvar a) (interp_ExprA lvar e). -Proof. -simple induction e; simpl; intros; try rewrite merge_mult_correct; - auto. - simpl; rewrite (H0 lvar); legacy ring. -Qed. - -Lemma multiply_correct : - forall (e:ExprA) (lvar:list (AT * nat)), - interp_ExprA lvar (multiply e) = interp_ExprA lvar e. -Proof. - simple induction e; simpl; 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:list (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; 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; [ legacy ring | assumption ]. -simpl; rewrite H0; auto; legacy 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; exfalso; auto. -simpl; trivial. -unfold monom_remove; case (eqExprA (EAvar n) (EAinv a)); intros; - [ inversion e0 | simpl; trivial ]. -Qed. - -Lemma monom_simplif_rem_correct : - forall (a e:ExprA) (lvar:list (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; 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. -legacy ring. -Qed. - -Lemma monom_simplif_correct : - forall (e a:ExprA) (lvar:list (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; case (eqExprA a e0); intros. -rewrite <- e2; apply monom_simplif_rem_correct; auto. -simpl; trivial. -Qed. - -Lemma inverse_correct : - forall (e a:ExprA) (lvar:list (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; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto. -unfold inverse_simplif; rewrite monom_simplif_correct; auto. -Qed. - -End Theory_of_fields. - -(* Compatibility *) -Notation AplusT_sym := AplusT_comm (only parsing). -Notation AmultT_sym := AmultT_comm (only parsing). diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 deleted file mode 100644 index 089ff1e8..00000000 --- a/plugins/field/field.ml4 +++ /dev/null @@ -1,191 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -open Names -open Pp -open Proof_type -open Tacinterp -open Tacmach -open Term -open Typing -open Util -open Vernacinterp -open Vernacexpr -open Tacexpr -open Mod_subst -open Coqlib - -(* Interpretation of constr's *) -let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c - -(* Construction of constants *) -let constant dir s = gen_constant "Field" ("field"::dir) s -let init_constant s = gen_constant_in_modules "Field" init_modules s - -(* To deal with the optional arguments *) -let constr_of_opt a opt = - let ac = constr_of a in - let ac3 = mkArrow ac (mkArrow ac ac) in - match opt with - | None -> mkApp (init_constant "None",[|ac3|]) - | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|]) - -module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) - -(* Table of theories *) -let th_tab = ref (Cmap.empty : constr Cmap.t) - -let lookup env typ = - try Cmap.find typ !th_tab - with Not_found -> - errorlabstrm "field" - (str "No field is declared for type" ++ spc() ++ - Printer.pr_lconstr_env env typ) - -let _ = - let init () = th_tab := Cmap.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 } - -let load_addfield _ = () -let cache_addfield (_,(typ,th)) = th_tab := Cmap.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') - -(* Declaration of the Add Field library object *) -let in_addfield : types * constr -> Libobject.obj = - 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)} - -(* 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 ["LegacyField_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 Ppconstr -let pp_minus_div_arg _prc _prlc _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" "Legacy" "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 = - Coqlib.check_required_library ["Coq";"field";"LegacyField"]; - let typ = - try match Hipattern.match_with_equation (pf_concl g) with - | _,_,Hipattern.PolymorphicLeibnizEq (t,_,_) -> t - | _ -> raise Exit - with Hipattern.NoEquationFound | Exit -> - 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 = - Coqlib.check_required_library ["Coq";"field";"LegacyField"]; - 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 legacy_field -| [ "legacy" "field" ] -> [ field ] -| [ "legacy" "field" ne_constr_list(l) ] -> [ field_term l ] -END diff --git a/plugins/field/field_plugin.mllib b/plugins/field/field_plugin.mllib deleted file mode 100644 index 3c3e87af..00000000 --- a/plugins/field/field_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Field -Field_plugin_mod diff --git a/plugins/field/vo.itarget b/plugins/field/vo.itarget deleted file mode 100644 index 22b56f33..00000000 --- a/plugins/field/vo.itarget +++ /dev/null @@ -1,4 +0,0 @@ -LegacyField_Compl.vo -LegacyField_Tactic.vo -LegacyField_Theory.vo -LegacyField.vo |