summaryrefslogtreecommitdiff
path: root/contrib/field
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/field')
-rw-r--r--contrib/field/LegacyField.v (renamed from contrib/field/Field.v)10
-rw-r--r--contrib/field/LegacyField_Compl.v (renamed from contrib/field/Field_Compl.v)2
-rw-r--r--contrib/field/LegacyField_Tactic.v (renamed from contrib/field/Field_Tactic.v)35
-rw-r--r--contrib/field/LegacyField_Theory.v (renamed from contrib/field/Field_Theory.v)102
-rw-r--r--contrib/field/field.ml416
5 files changed, 85 insertions, 80 deletions
diff --git a/contrib/field/Field.v b/contrib/field/LegacyField.v
index 3cc097fc..08397d02 100644
--- a/contrib/field/Field.v
+++ b/contrib/field/LegacyField.v
@@ -6,10 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field.v 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: LegacyField.v 9273 2006-10-25 11:30:36Z barras $ *)
-Require Export Field_Compl.
-Require Export Field_Theory.
-Require Export Field_Tactic.
+Require Export LegacyField_Compl.
+Require Export LegacyField_Theory.
+Require Export LegacyField_Tactic.
-(* Command declarations are moved to the ML side *) \ No newline at end of file
+(* Command declarations are moved to the ML side *)
diff --git a/contrib/field/Field_Compl.v b/contrib/field/LegacyField_Compl.v
index f018359e..b37281e9 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/LegacyField_Compl.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field_Compl.v 8866 2006-05-28 16:21:04Z herbelin $ *)
+(* $Id: LegacyField_Compl.v 9273 2006-10-25 11:30:36Z barras $ *)
Require Import List.
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/LegacyField_Tactic.v
index 8d727536..2b6ff5b4 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/LegacyField_Tactic.v
@@ -6,12 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field_Tactic.v 8866 2006-05-28 16:21:04Z herbelin $ *)
+(* $Id: LegacyField_Tactic.v 9319 2006-10-30 12:41:21Z barras $ *)
Require Import List.
-Require Import Ring.
-Require Export Field_Compl.
-Require Export Field_Theory.
+Require Import LegacyRing.
+Require Export LegacyField_Compl.
+Require Export LegacyField_Theory.
(**** Interpretation A --> ExprA ****)
@@ -184,15 +184,15 @@ 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)
+ 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
+ try
match goal with
| |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT)
- end; clear FT X2) ])
+ end; clear FT X2) ]
end.
Ltac apply_multiply FT lvar trm :=
@@ -279,7 +279,7 @@ Ltac field_gen_aux FT :=
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
+ cut
(let ft := FT in
let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2);
[ compute in |- *; auto
@@ -287,13 +287,14 @@ Ltac field_gen_aux FT :=
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 ] ])
+ (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; ring) || field_gen_aux FT.
+Ltac field_gen FT :=
+ unfolds FT; (inverse_test FT; legacy ring) || field_gen_aux FT.
(*****************************)
(* Term Simplification *)
@@ -429,4 +430,4 @@ Ltac field_term FT exp :=
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 ]).
+ (replace exp with trep; [ legacy ring trep | field_gen FT ]).
diff --git a/contrib/field/Field_Theory.v b/contrib/field/LegacyField_Theory.v
index fff3c414..9c3a12fb 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/LegacyField_Theory.v
@@ -6,12 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field_Theory.v 8866 2006-05-28 16:21:04Z herbelin $ *)
+(* $Id: LegacyField_Theory.v 9288 2006-10-26 18:25:06Z herbelin $ *)
Require Import List.
Require Import Peano_dec.
-Require Import Ring.
-Require Import Field_Compl.
+Require Import LegacyRing.
+Require Import LegacyField_Compl.
Record Field_Theory : Type :=
{A : Type;
@@ -88,66 +88,66 @@ 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) (
+Add Legacy 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.
+Add Legacy 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.
+Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1.
Proof.
- intros; ring.
+ intros; legacy ring.
Qed.
Lemma AplusT_assoc :
forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3).
Proof.
- intros; ring.
+ intros; legacy ring.
Qed.
-Lemma AmultT_sym : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1.
+Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1.
Proof.
- intros; ring.
+ intros; legacy ring.
Qed.
Lemma AmultT_assoc :
forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3).
Proof.
- intros; ring.
+ intros; legacy ring.
Qed.
Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r.
Proof.
- intros; ring.
+ intros; legacy ring.
Qed.
Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r.
Proof.
- intros; ring.
+ intros; legacy ring.
Qed.
Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT.
Proof.
- intros; ring.
+ 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; ring.
+ 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).
- ring.
+ legacy ring.
transitivity (AplusT (AplusT (AoppT r) r) r2).
repeat rewrite AplusT_assoc; rewrite <- H; reflexivity.
- ring.
+ legacy ring.
Qed.
Lemma r_AmultT_mult :
@@ -162,28 +162,28 @@ Qed.
Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT.
Proof.
- intro; ring.
+ intro; legacy ring.
Qed.
Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT.
Proof.
- intro; ring.
+ intro; legacy ring.
Qed.
Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r.
Proof.
- intro; ring.
+ intro; legacy 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.
+ 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 in |- *; intro; apply H; rewrite H0; ring.
+ intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; legacy ring.
Qed.
(************************)
@@ -276,7 +276,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 |- *; ring).
+elim e0; try (intros; simpl in |- *; legacy ring).
unfold interp_ExprA in H2; fold interp_ExprA in H2;
cut
(AmultT (interp_ExprA lvar e2)
@@ -286,8 +286,8 @@ 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 |- *; ring.
-ring.
+ simpl in |- *; legacy ring.
+legacy ring.
Qed.
Lemma assoc_mult_correct1 :
@@ -308,7 +308,7 @@ Lemma assoc_mult_correct :
Proof.
simple induction e; auto; intros.
elim e0; intros.
-intros; simpl in |- *; ring.
+intros; simpl in |- *; legacy 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.
@@ -317,9 +317,9 @@ simpl in |- *; rewrite merge_mult_correct; simpl in |- *;
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_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1));
rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc;
- ring.
+ legacy ring.
simpl in |- *; rewrite (H0 lvar); auto.
simpl in |- *; rewrite (H0 lvar); auto.
simpl in |- *; rewrite (H0 lvar); auto.
@@ -344,7 +344,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 |- *; ring).
+elim e0; try intros; try (simpl in |- *; legacy ring).
unfold interp_ExprA in H2; fold interp_ExprA in H2;
cut
(AplusT (interp_ExprA lvar e2)
@@ -354,8 +354,8 @@ 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 |- *; ring.
-ring.
+ simpl in |- *; legacy ring.
+legacy ring.
Qed.
Lemma assoc_plus_correct :
@@ -387,7 +387,7 @@ simpl in |- *; rewrite merge_plus_correct; simpl in |- *;
(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)))
+ (AplusT_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))
; rewrite assoc_plus_correct; rewrite H1; simpl in |- *;
rewrite (H0 lvar);
rewrite <-
@@ -397,10 +397,10 @@ simpl in |- *; rewrite merge_plus_correct; simpl in |- *;
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_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_sym.
+ (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.
@@ -454,8 +454,8 @@ Lemma distrib_mult_right_correct :
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.
+rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
+ rewrite (H0 e2 lvar); legacy ring.
Qed.
Lemma distrib_mult_left_correct :
@@ -466,18 +466,18 @@ 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 distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
+rewrite AmultT_comm;
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 (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_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.
+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.
Qed.
Lemma distrib_correct :
@@ -491,7 +491,7 @@ 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.
+ simpl in |- *; fold AoppT in |- *; legacy ring.
Qed.
(**** Multiplication by the inverse product ****)
@@ -527,7 +527,7 @@ Lemma multiply_aux_correct :
Proof.
simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct;
auto.
- simpl in |- *; rewrite (H0 lvar); ring.
+ simpl in |- *; rewrite (H0 lvar); legacy ring.
Qed.
Lemma multiply_correct :
@@ -595,8 +595,8 @@ 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.
+ (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.
@@ -619,7 +619,7 @@ simple induction a; simpl in |- *; intros; try rewrite monom_remove_correct;
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.
+legacy ring.
Qed.
Lemma monom_simplif_correct :
@@ -644,3 +644,7 @@ unfold inverse_simplif in |- *; 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/contrib/field/field.ml4 b/contrib/field/field.ml4
index 47e583fd..dab5a45c 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: field.ml4 8866 2006-05-28 16:21:04Z herbelin $ *)
+(* $Id: field.ml4 9273 2006-10-25 11:30:36Z barras $ *)
open Names
open Pp
@@ -86,7 +86,7 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
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"),
+ 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 ();
@@ -139,7 +139,7 @@ ARGUMENT EXTEND minus_div_arg
END
VERNAC COMMAND EXTEND Field
- [ "Add" "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) ]
@@ -153,7 +153,7 @@ END
(* Guesses the type and calls field_gen with the right theory *)
let field g =
- Coqlib.check_required_library ["Coq";"field";"Field"];
+ Coqlib.check_required_library ["Coq";"field";"LegacyField"];
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
@@ -175,7 +175,7 @@ let guess_theory env evc = function
(* Guesses the type and calls Field_Term with the right theory *)
let field_term l g =
- Coqlib.check_required_library ["Coq";"field";"Field"];
+ 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))
@@ -187,7 +187,7 @@ let field_term l g =
(* Declaration of Field *)
-TACTIC EXTEND field
-| [ "field" ] -> [ field ]
-| [ "field" ne_constr_list(l) ] -> [ field_term l ]
+TACTIC EXTEND legacy_field
+| [ "legacy" "field" ] -> [ field ]
+| [ "legacy" "field" ne_constr_list(l) ] -> [ field_term l ]
END
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 20:47:38 +0000