diff options
Diffstat (limited to 'plugins/field')
| -rw-r--r-- | plugins/field/LegacyField.v | 4 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Compl.v | 4 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Tactic.v | 24 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Theory.v | 184 | ||||
| -rw-r--r-- | plugins/field/field.ml4 | 16 |
5 files changed, 112 insertions, 120 deletions
diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v index 9017f8d5..504304c6 100644 --- a/plugins/field/LegacyField.v +++ b/plugins/field/LegacyField.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyField.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Export LegacyField_Compl. Require Export LegacyField_Theory. Require Export LegacyField_Tactic. diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v index 52e049a5..5e9ae430 100644 --- a/plugins/field/LegacyField_Compl.v +++ b/plugins/field/LegacyField_Compl.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyField_Compl.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import List. Definition assoc_2nd := diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v index f6626e4a..41d2998c 100644 --- a/plugins/field/LegacyField_Tactic.v +++ b/plugins/field/LegacyField_Tactic.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyField_Tactic.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import List. Require Import LegacyRing. Require Export LegacyField_Compl. @@ -152,7 +150,7 @@ Ltac apply_assoc FT lvar trm := match constr:(t = trm) with | (?X1 = ?X1) => idtac | _ => - rewrite <- (assoc_correct FT trm); change (assoc trm) with t in |- * + rewrite <- (assoc_correct FT trm); change (assoc trm) with t end. (**** Distribution *****) @@ -163,7 +161,7 @@ Ltac apply_distrib FT lvar trm := | (?X1 = ?X1) => idtac | _ => rewrite <- (distrib_correct FT trm); - change (distrib trm) with t in |- * + change (distrib trm) with t end. (**** Multiplication by the inverse product ****) @@ -177,7 +175,7 @@ Ltac weak_reduce := | |- 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 |- * + Aone Aplus Amult Aopp Ainv] end. Ltac multiply mul := @@ -201,7 +199,7 @@ Ltac apply_multiply FT lvar trm := | (?X1 = ?X1) => idtac | _ => rewrite <- (multiply_correct FT trm); - change (multiply trm) with t in |- * + change (multiply trm) with t end. (**** Permutations and simplification ****) @@ -212,7 +210,7 @@ Ltac apply_inverse mul FT lvar trm := | (?X1 = ?X1) => idtac | _ => rewrite <- (inverse_correct FT trm mul); - [ change (inverse_simplif mul trm) with t in |- * | assumption ] + [ change (inverse_simplif mul trm) with t | assumption ] end. (**** Inverse test ****) @@ -254,11 +252,11 @@ Ltac apply_simplif sfun := Ltac unfolds FT := match get_component Aminus FT with - | Some ?X1 => unfold X1 in |- * + | Some ?X1 => unfold X1 | _ => idtac end; match get_component Adiv FT with - | Some ?X1 => unfold X1 in |- * + | Some ?X1 => unfold X1 | _ => idtac end. @@ -269,8 +267,8 @@ Ltac reduce 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] in |- * || - compute 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 @@ -282,7 +280,7 @@ Ltac field_gen_aux FT := cut (let ft := FT in let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2); - [ compute in |- *; auto + [ compute; auto | intros ft vm; apply_simplif apply_distrib; apply_simplif apply_assoc; multiply mul; [ apply_simplif apply_multiply; diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v index 8d10bc8e..1d581a8f 100644 --- a/plugins/field/LegacyField_Theory.v +++ b/plugins/field/LegacyField_Theory.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyField_Theory.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import List. Require Import Peano_dec. Require Import LegacyRing. @@ -46,20 +44,20 @@ Proof. elim (H1 e0); intro y; elim (H2 e); intro y0; try (left; rewrite y; rewrite y0; auto) || - (right; red in |- *; intro; inversion H3; 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 in |- *; intro; inversion H3; auto). + (right; red; intro; inversion H3; auto). elim (H0 e); intro y. left; rewrite y; auto. - right; red in |- *; intro; inversion H1; auto. + right; red; intro; inversion H1; auto. elim (H0 e); intro y. left; rewrite y; auto. - right; red in |- *; intro; inversion H1; auto. + right; red; intro; inversion H1; auto. elim (eq_nat_dec n n0); intro y. left; rewrite y; auto. - right; red in |- *; intro; inversion H; auto. + right; red; intro; inversion H; auto. Defined. Definition eq_nat_dec := Eval compute in eq_nat_dec. @@ -154,7 +152,7 @@ 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 ]. + 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 ]. @@ -183,7 +181,7 @@ 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; legacy ring. + intros r1 r2 H; split; red; intro; apply H; rewrite H0; legacy ring. Qed. (************************) @@ -264,11 +262,11 @@ Lemma merge_mult_correct1 : 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. +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 : @@ -276,7 +274,7 @@ Lemma merge_mult_correct : 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 |- *; legacy ring). +elim e0; try (intros; simpl; legacy ring). unfold interp_ExprA in H2; fold interp_ExprA in H2; cut (AmultT (interp_ExprA lvar e2) @@ -286,7 +284,7 @@ unfold interp_ExprA in H2; fold interp_ExprA in H2; (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 |- *; legacy ring. + simpl; legacy ring. legacy ring. Qed. @@ -297,8 +295,8 @@ Lemma assoc_mult_correct1 : 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 |- *; +rewrite <- (H e0 lvar); simpl; rewrite merge_mult_correct; + simpl; rewrite merge_mult_correct; simpl; auto. Qed. @@ -308,21 +306,21 @@ Lemma assoc_mult_correct : Proof. simple induction e; auto; intros. elim e0; intros. -intros; simpl in |- *; legacy ring. -simpl in |- *; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1))); +intros; simpl; legacy ring. +simpl; 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 |- *; +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 in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. -simpl in |- *; rewrite (H0 lvar); auto. +simpl; rewrite (H0 lvar); auto. +simpl; rewrite (H0 lvar); auto. +simpl; rewrite (H0 lvar); auto. Qed. Lemma merge_plus_correct1 : @@ -332,11 +330,11 @@ Lemma merge_plus_correct1 : 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. +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 : @@ -344,7 +342,7 @@ Lemma merge_plus_correct : 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 |- *; legacy ring). +elim e0; try intros; try (simpl; legacy ring). unfold interp_ExprA in H2; fold interp_ExprA in H2; cut (AplusT (interp_ExprA lvar e2) @@ -354,7 +352,7 @@ unfold interp_ExprA in H2; fold interp_ExprA in H2; (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 |- *; legacy ring. + simpl; legacy ring. legacy ring. Qed. @@ -364,8 +362,8 @@ Lemma assoc_plus_correct : 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 |- *; +rewrite <- (H e0 lvar); simpl; rewrite merge_plus_correct; + simpl; rewrite merge_plus_correct; simpl; auto. Qed. @@ -375,11 +373,11 @@ Lemma assoc_correct : 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 |- *; +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)) @@ -388,7 +386,7 @@ simpl in |- *; rewrite merge_plus_correct; simpl in |- *; (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 in |- *; + ; rewrite assoc_plus_correct; rewrite H1; simpl; rewrite (H0 lvar); rewrite <- (AplusT_assoc (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e1)) @@ -401,15 +399,15 @@ simpl in |- *; rewrite merge_plus_correct; simpl in |- *; rewrite <- (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3) (interp_ExprA lvar e1)); apply AplusT_comm. -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. +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 *****) @@ -453,7 +451,7 @@ Lemma distrib_mult_right_correct : 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. +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. @@ -463,10 +461,10 @@ Lemma distrib_mult_left_correct : 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 |- *; +simple induction e1; try intros; simpl. +rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl; apply AmultT_Or. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. +rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. rewrite AmultT_comm; rewrite (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e) @@ -474,10 +472,10 @@ rewrite AmultT_comm; 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 in |- *; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm. -rewrite distrib_mult_right_correct; simpl in |- *; 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. +rewrite distrib_mult_right_correct; simpl; apply AmultT_comm. Qed. Lemma distrib_correct : @@ -485,13 +483,13 @@ Lemma distrib_correct : 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 |- *; legacy ring. +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 ****) @@ -502,7 +500,7 @@ Lemma mult_eq : interp_ExprA lvar (EAmult a e1) = interp_ExprA lvar (EAmult a e2) -> interp_ExprA lvar e1 = interp_ExprA lvar e2. Proof. - simpl in |- *; intros; + simpl; intros; apply (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1) (interp_ExprA lvar e2)); assumption. @@ -525,16 +523,16 @@ Lemma multiply_aux_correct : 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; +simple induction e; simpl; intros; try rewrite merge_mult_correct; auto. - simpl in |- *; rewrite (H0 lvar); legacy ring. + 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 in |- *; auto. + simple induction e; simpl; auto. intros; apply multiply_aux_correct. Qed. @@ -585,27 +583,27 @@ Lemma monom_remove_correct : 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 |- *. +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 in |- *; rewrite H0; auto; legacy 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. +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 in |- *; fold AinvT in |- *; rewrite AinvT_r; auto. -inversion e1; simpl in |- *; exfalso; auto. -simpl in |- *; trivial. -unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros; - [ inversion e0 | simpl in |- *; trivial ]. +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 : @@ -614,7 +612,7 @@ Lemma monom_simplif_rem_correct : 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; +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. @@ -628,9 +626,9 @@ Lemma monom_simplif_correct : interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e. Proof. simple induction e; intros; auto. -simpl in |- *; case (eqExprA a e0); intros. +simpl; case (eqExprA a e0); intros. rewrite <- e2; apply monom_simplif_rem_correct; auto. -simpl in |- *; trivial. +simpl; trivial. Qed. Lemma inverse_correct : @@ -639,8 +637,8 @@ Lemma inverse_correct : 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. +simpl; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto. +unfold inverse_simplif; rewrite monom_simplif_correct; auto. Qed. End Theory_of_fields. diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 37aa457d..6c9fd325 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: field.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Names open Pp open Proof_type @@ -39,18 +37,20 @@ let constr_of_opt a opt = | 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 (Gmap.empty : (constr,constr) Gmap.t) +let th_tab = ref (Cmap.empty : constr Cmap.t) let lookup env typ = - try Gmap.find typ !th_tab + 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 := Gmap.empty in + let init () = th_tab := Cmap.empty in let freeze () = !th_tab in let unfreeze fs = th_tab := fs in Summary.declare_summary "field" @@ -59,7 +59,7 @@ let _ = Summary.init_function = init } let load_addfield _ = () -let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab +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 @@ -67,7 +67,7 @@ let subst_addfield (subst,(typ,th as obj)) = (typ',th') (* Declaration of the Add Field library object *) -let (in_addfield,out_addfield)= +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; |