summaryrefslogtreecommitdiff
path: root/contrib/field
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/field')
-rw-r--r--contrib/field/Field_Compl.v39
-rw-r--r--contrib/field/Field_Tactic.v76
-rw-r--r--contrib/field/Field_Theory.v53
-rw-r--r--contrib/field/field.ml411
4 files changed, 80 insertions, 99 deletions
diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index 774b3084..f018359e 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -6,56 +6,33 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field_Compl.v 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: Field_Compl.v 8866 2006-05-28 16:21:04Z herbelin $ *)
-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.
+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:listT (prodT A B)) {struct lst} :
+ (lst:list (prod A B)) {struct lst} :
B -> A -> A :=
fun (key:B) (default:A) =>
match lst with
- | nilT => default
- | consT (pairT v e) l =>
+ | 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 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 :=
+ (a:A) (l:list A) {struct l} : bool :=
match l with
- | nilT => false
- | consT a1 l1 =>
+ | nil => false
+ | 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
index afa0a814..8d727536 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -6,8 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field_Tactic.v 8134 2006-03-05 16:39:17Z herbelin $ *)
+(* $Id: Field_Tactic.v 8866 2006-05-28 16:21:04Z herbelin $ *)
+Require Import List.
Require Import Ring.
Require Export Field_Compl.
Require Export Field_Theory.
@@ -20,8 +21,8 @@ Ltac body_of s := eval cbv beta iota delta [s] in s.
Ltac mem_assoc var lvar :=
match constr:lvar with
- | (nilT _) => constr:false
- | (consT _ ?X1 ?X2) =>
+ | nil => constr:false
+ | ?X1 :: ?X2 =>
match constr:(X1 = var) with
| (?X1 = ?X1) => constr:true
| _ => mem_assoc var X2
@@ -31,10 +32,10 @@ Ltac mem_assoc var lvar :=
Ltac number lvar :=
let rec number_aux lvar cpt :=
match constr:lvar with
- | (nilT ?X1) => constr:(nilT (prodT X1 nat))
- | (consT ?X1 ?X2 ?X3) =>
+ | (@nil ?X1) => constr:(@nil (prod X1 nat))
+ | ?X2 :: ?X3 =>
let l2 := number_aux X3 (S cpt) in
- constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2)
+ constr:((X2,cpt) :: l2)
end
in number_aux lvar 0.
@@ -62,17 +63,17 @@ Ltac build_varlist FT trm :=
let res := mem_assoc X1 lvar in
match constr:res with
| true => lvar
- | false => constr:(consT AT X1 lvar)
+ | false => constr:(X1 :: lvar)
end
end in
let AT := get_component A FT in
- let lvar := seek_var (nilT AT) trm in
+ let lvar := seek_var (@nil AT) trm in
number lvar.
Ltac assoc elt lst :=
match constr:lst with
- | (nilT _) => fail
- | (consT (prodT _ nat) (pairT _ nat ?X1 ?X2) ?X3) =>
+ | nil => fail
+ | (?X1,?X2) :: ?X3 =>
match constr:(elt = X1) with
| (?X1 = ?X1) => constr:X2
| _ => assoc elt X3
@@ -113,32 +114,31 @@ Ltac interp_A FT lvar trm :=
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)
+ | 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
- | (nilT _) => l2
- | (consT ?X1 ?X2 ?X3) =>
+ | nil => l2
+ | ?X2 :: ?X3 =>
let nl2 := remove X2 l2 in
let nl := union X3 nl2 in
- constr:(consT X1 X2 nl)
+ constr:(X2 :: nl)
end.
Ltac raw_give_mult trm :=
match constr:trm with
- | (EAinv ?X1) => constr:(consT ExprA X1 (nilT ExprA))
+ | (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 (appT ExprA l1 l2)
- | _ => constr:(nilT ExprA)
+ eval compute in (app l1 l2)
+ | _ => constr:(@nil ExprA)
end.
Ltac give_mult trm :=
@@ -254,13 +254,13 @@ Ltac apply_simplif sfun :=
Ltac unfolds FT :=
match get_component Aminus FT with
- | (Field_Some _ ?X1) => unfold X1 in |- *
+ | Some ?X1 => unfold X1 in |- *
| _ => idtac
end;
- match get_component Adiv FT with
- | (Field_Some _ ?X1) => unfold X1 in |- *
- | _ => idtac
- end.
+ match get_component Adiv FT with
+ | Some ?X1 => unfold X1 in |- *
+ | _ => idtac
+ end.
Ltac reduce FT :=
let AzeroT := get_component Azero FT
@@ -304,11 +304,11 @@ Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT.
Ltac init_exp FT trm :=
let e :=
(match get_component Aminus FT with
- | (Field_Some _ ?X1) => eval cbv beta delta [X1] in trm
+ | Some ?X1 => eval cbv beta delta [X1] in trm
| _ => trm
end) in
match get_component Adiv FT with
- | (Field_Some _ ?X1) => eval cbv beta delta [X1] in e
+ | Some ?X1 => eval cbv beta delta [X1] in e
| _ => e
end.
@@ -341,21 +341,21 @@ Ltac simpl_inv trm :=
Ltac map_tactic fcn lst :=
match constr:lst with
- | (nilT _) => lst
- | (consT ?X1 ?X2 ?X3) =>
+ | nil => lst
+ | ?X2 :: ?X3 =>
let r := fcn X2 with t := map_tactic fcn X3 in
- constr:(consT X1 r t)
+ constr:(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)
+ | 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 (appT ExprA lnum ildn) 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
@@ -370,7 +370,7 @@ Ltac simpl_monom_aux lnum lden trm :=
| true =>
let newlnum := remove X1 lnum in
simpl_monom_aux newlnum lden X2
- | false => simpl_monom_aux lnum (consT ExprA X1 lden) X2
+ | false => simpl_monom_aux lnum (X1 :: lden) X2
end
| (EAmult ?X1 ?X2) =>
let mma := mem_assoc X1 lden in
@@ -378,7 +378,7 @@ Ltac simpl_monom_aux lnum lden trm :=
| true =>
let newlden := remove X1 lden in
simpl_monom_aux lnum newlden X2
- | false => simpl_monom_aux (consT ExprA X1 lnum) lden X2
+ | false => simpl_monom_aux (X1 :: lnum) lden X2
end
| (EAinv ?X1) =>
let mma := mem_assoc X1 lnum in
@@ -386,7 +386,7 @@ Ltac simpl_monom_aux lnum lden trm :=
| true =>
let newlnum := remove X1 lnum in
build_monom newlnum lden
- | false => build_monom lnum (consT ExprA X1 lden)
+ | false => build_monom lnum (X1 :: lden)
end
| ?X1 =>
let mma := mem_assoc X1 lden in
@@ -394,11 +394,11 @@ Ltac simpl_monom_aux lnum lden trm :=
| true =>
let newlden := remove X1 lden in
build_monom lnum newlden
- | false => build_monom (consT ExprA X1 lnum) lden
+ | false => build_monom (X1 :: lnum) lden
end
end.
-Ltac simpl_monom trm := simpl_monom_aux (nilT ExprA) (nilT ExprA) trm.
+Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil ExprA) trm.
Ltac simpl_all_monomials trm :=
match constr:trm with
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 2c954652..fff3c414 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -6,8 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field_Theory.v 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: Field_Theory.v 8866 2006-05-28 16:21:04Z herbelin $ *)
+Require Import List.
Require Import Peano_dec.
Require Import Ring.
Require Import Field_Compl.
@@ -21,8 +22,8 @@ Record Field_Theory : Type :=
Aopp : A -> A;
Aeq : A -> A -> bool;
Ainv : A -> A;
- Aminus : field_rel_option A;
- Adiv : field_rel_option 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}.
@@ -66,10 +67,10 @@ Definition eqExprA := Eval compute in eqExprA_O.
(**** Generation of the multiplier ****)
-Fixpoint mult_of_list (e:listT ExprA) : ExprA :=
+Fixpoint mult_of_list (e:list ExprA) : ExprA :=
match e with
- | nilT => EAone
- | consT e1 l1 => EAmult e1 (mult_of_list l1)
+ | nil => EAone
+ | e1 :: l1 => EAmult e1 (mult_of_list l1)
end.
Section Theory_of_fields.
@@ -191,7 +192,7 @@ Qed.
(**** ExprA --> A ****)
-Fixpoint interp_ExprA (lvar:listT (prodT AT nat)) (e:ExprA) {struct e} :
+Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} :
AT :=
match e with
| EAzero => AzeroT
@@ -257,7 +258,7 @@ Fixpoint assoc (e:ExprA) : ExprA :=
end.
Lemma merge_mult_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -271,7 +272,7 @@ unfold merge_mult at 1 in |- *; fold merge_mult in |- *;
Qed.
Lemma merge_mult_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -290,7 +291,7 @@ ring.
Qed.
Lemma assoc_mult_correct1 :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ 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)).
@@ -302,7 +303,7 @@ rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct;
Qed.
Lemma assoc_mult_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e.
Proof.
simple induction e; auto; intros.
@@ -325,7 +326,7 @@ simpl in |- *; rewrite (H0 lvar); auto.
Qed.
Lemma merge_plus_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -339,7 +340,7 @@ unfold merge_plus at 1 in |- *; fold merge_plus in |- *;
Qed.
Lemma merge_plus_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -358,7 +359,7 @@ ring.
Qed.
Lemma assoc_plus_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -369,7 +370,7 @@ rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct;
Qed.
Lemma assoc_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (assoc e) = interp_ExprA lvar e.
Proof.
simple induction e; auto; intros.
@@ -448,7 +449,7 @@ Fixpoint distrib_main (e:ExprA) : ExprA :=
Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e).
Lemma distrib_mult_right_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -458,7 +459,7 @@ rewrite AmultT_sym; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
Qed.
Lemma distrib_mult_left_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -480,7 +481,7 @@ rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym.
Qed.
Lemma distrib_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (distrib e) = interp_ExprA lvar e.
Proof.
simple induction e; intros; auto.
@@ -496,7 +497,7 @@ Qed.
(**** Multiplication by the inverse product ****)
Lemma mult_eq :
- forall (e1 e2 a:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -520,7 +521,7 @@ Definition multiply (e:ExprA) : ExprA :=
end.
Lemma multiply_aux_correct :
- forall (a e:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -530,7 +531,7 @@ simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct;
Qed.
Lemma multiply_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
interp_ExprA lvar (multiply e) = interp_ExprA lvar e.
Proof.
simple induction e; simpl in |- *; auto.
@@ -578,7 +579,7 @@ Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA :=
end.
Lemma monom_remove_correct :
- forall (e a:ExprA) (lvar:listT (prodT AT nat)),
+ 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).
@@ -608,7 +609,7 @@ unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros;
Qed.
Lemma monom_simplif_rem_correct :
- forall (a e:ExprA) (lvar:listT (prodT AT nat)),
+ 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).
@@ -622,7 +623,7 @@ ring.
Qed.
Lemma monom_simplif_correct :
- forall (e a:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -633,7 +634,7 @@ simpl in |- *; trivial.
Qed.
Lemma inverse_correct :
- forall (e a:ExprA) (lvar:listT (prodT AT nat)),
+ 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.
@@ -642,4 +643,4 @@ 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
+End Theory_of_fields.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 35591f23..47e583fd 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: field.ml4 7837 2006-01-11 09:47:32Z herbelin $ *)
+(* $Id: field.ml4 8866 2006-05-28 16:21:04Z herbelin $ *)
open Names
open Pp
@@ -22,19 +22,22 @@ 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 = Coqlib.gen_constant "Field" ("field"::dir) s
+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 ((constant ["Field_Compl"] "Field_None"),[|ac|])
- | Some f -> mkApp ((constant ["Field_Compl"] "Field_Some"),[|ac;constr_of f|])
+ | None -> mkApp (init_constant "None",[|ac3|])
+ | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|])
(* Table of theories *)
let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 06:14:54 +0000