summaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/Field_tac.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring/Field_tac.v')
-rw-r--r--plugins/setoid_ring/Field_tac.v89
1 files changed, 49 insertions, 40 deletions
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index 34a3018b..f867c6d0 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -10,55 +10,67 @@ Require Import Ring_tac BinList Ring_polynom InitialRing.
Require Export Field_theory.
(* syntaxification *)
- Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv :=
+ (* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+ (* the tactic could be used to discriminate occurrences of an opaque *)
+ (* constant phi, with (phi 0) not convertible to 0 for instance *)
+ Ltac mkFieldexpr C Cst CstPow rO rI radd rmul rsub ropp rdiv rinv rpow t fv :=
let rec mkP t :=
let f :=
match Cst t with
| InitialRing.NotConstant =>
match t with
+ | rO =>
+ fun _ => constr:(@FEO C)
+ | rI =>
+ fun _ => constr:(@FEI C)
| (radd ?t1 ?t2) =>
fun _ =>
let e1 := mkP t1 in
- let e2 := mkP t2 in constr:(FEadd e1 e2)
+ let e2 := mkP t2 in constr:(@FEadd C e1 e2)
| (rmul ?t1 ?t2) =>
fun _ =>
let e1 := mkP t1 in
- let e2 := mkP t2 in constr:(FEmul e1 e2)
+ let e2 := mkP t2 in constr:(@FEmul C e1 e2)
| (rsub ?t1 ?t2) =>
fun _ =>
let e1 := mkP t1 in
- let e2 := mkP t2 in constr:(FEsub e1 e2)
+ let e2 := mkP t2 in constr:(@FEsub C e1 e2)
| (ropp ?t1) =>
- fun _ => let e1 := mkP t1 in constr:(FEopp e1)
+ fun _ => let e1 := mkP t1 in constr:(@FEopp C e1)
| (rdiv ?t1 ?t2) =>
fun _ =>
let e1 := mkP t1 in
- let e2 := mkP t2 in constr:(FEdiv e1 e2)
+ let e2 := mkP t2 in constr:(@FEdiv C e1 e2)
| (rinv ?t1) =>
- fun _ => let e1 := mkP t1 in constr:(FEinv e1)
+ fun _ => let e1 := mkP t1 in constr:(@FEinv C e1)
| (rpow ?t1 ?n) =>
match CstPow n with
| InitialRing.NotConstant =>
fun _ =>
let p := Find_at t fv in
constr:(@FEX C p)
- | ?c => fun _ => let e1 := mkP t1 in constr:(FEpow e1 c)
+ | ?c => fun _ => let e1 := mkP t1 in constr:(@FEpow C e1 c)
end
| _ =>
fun _ =>
let p := Find_at t fv in
constr:(@FEX C p)
end
- | ?c => fun _ => constr:(FEc c)
+ | ?c => fun _ => constr:(@FEc C c)
end in
f ()
in mkP t.
-Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
+ (* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+ (* the tactic could be used to discriminate occurrences of an opaque *)
+ (* constant phi, with (phi 0) not convertible to 0 for instance *)
+Ltac FFV Cst CstPow rO rI add mul sub opp div inv pow t fv :=
let rec TFV t fv :=
match Cst t with
| InitialRing.NotConstant =>
match t with
+ | rO => fv
+ | rI => fv
| (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
@@ -83,60 +95,60 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
Ltac PackField F req Cst_tac Pow_tac L1 L2 L3 L4 cond_ok pre post :=
let FLD :=
match type of L1 with
- | context [req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
+ | context [req (@FEeval ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
(fun proj =>
proj Cst_tac Pow_tac pre post
- req radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok)
+ req rO rI radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok)
| _ => fail 1 "field anomaly: bad correctness lemma (parse)"
end in
F FLD.
Ltac get_FldPre FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
pre).
Ltac get_FldPost FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
post).
Ltac get_L1 FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
L1).
Ltac get_SimplifyEqLemma FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
L2).
Ltac get_SimplifyLemma FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
L3).
Ltac get_L4 FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
L4).
Ltac get_CondLemma FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
cond_ok).
Ltac get_FldEq FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
req).
@@ -146,33 +158,33 @@ Ltac get_FldCarrier FLD :=
Ltac get_RingFV FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
- FV Cst_tac Pow_tac radd rmul rsub ropp rpow).
+ FV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow).
Ltac get_FFV FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
- FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).
+ FFV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow).
Ltac get_RingMeta FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
- mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow).
+ mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow).
Ltac get_Meta FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
- mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).
+ mkFieldexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow).
Ltac get_Hyp_tac FLD :=
FLD ltac:
- (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+ (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
L1 L2 L3 L4 cond_ok =>
- let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
+ let mkPol := mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow in
fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).
Ltac get_FEeval FLD :=
@@ -180,8 +192,8 @@ Ltac get_FEeval FLD :=
match type of L1 with
| context
[(@FEeval
- ?R ?r0 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] =>
- constr:(@FEeval R r0 add mul sub opp div inv C phi Cpow powphi pow)
+ ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] =>
+ constr:(@FEeval R r0 r1 add mul sub opp div inv C phi Cpow powphi pow)
| _ => fail 1 "field anomaly: bad correctness lemma (get_FEeval)"
end.
@@ -201,8 +213,7 @@ Ltac fold_field_cond req :=
Ltac simpl_PCond FLD :=
let req := get_FldEq FLD in
let lemma := get_CondLemma FLD in
- try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def;
- clear lock_def lock);
+ try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
protect_fv "field_cond";
fold_field_cond req;
try exact I.
@@ -210,8 +221,7 @@ Ltac simpl_PCond FLD :=
Ltac simpl_PCond_BEURK FLD :=
let req := get_FldEq FLD in
let lemma := get_CondLemma FLD in
- try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def;
- clear lock_def lock);
+ (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
protect_fv "field_cond";
fold_field_cond req.
@@ -544,10 +554,9 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in
match s_spec with
| mkhypo ?ss_spec =>
- let field_ok3 := constr:(field_ok2 _ ss_spec) in
match d_spec with
| mkhypo ?dd_spec =>
- let field_ok := constr:(field_ok3 _ dd_spec) in
+ let field_ok := constr:(field_ok2 _ dd_spec) in
let mk_lemma lemma :=
constr:(lemma _ _ _ _ _ _ _ _ _ _
set ext_r inv_m afth
@@ -563,7 +572,7 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
(fun f =>
f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in
cond1_ok cond2_ok)
- | _ => fail 4 "field: bad coefficiant division specification"
+ | _ => fail 4 "field: bad coefficient division specification"
end
| _ => fail 3 "field: bad sign specification"
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 16:50:35 +0000