aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/field/LegacyField_Tactic.v22
-rw-r--r--contrib/setoid_ring/Field_tac.v74
-rw-r--r--contrib/setoid_ring/Ring_tac.v18
3 files changed, 42 insertions, 72 deletions
diff --git a/contrib/field/LegacyField_Tactic.v b/contrib/field/LegacyField_Tactic.v
index a52a1f205..63d9bdda6 100644
--- a/contrib/field/LegacyField_Tactic.v
+++ b/contrib/field/LegacyField_Tactic.v
@@ -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,10 +287,10 @@ 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; legacy 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 :=
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index 91ccf2216..786654abb 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -93,63 +93,31 @@ Ltac Field_simplify lemma Cond_lemma req Cst_tac :=
let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
let simpl_field H := protect_fv "field" in H in
- (fun f rl => (f mkFV mkFE simpl_field lemma req rl;
- try (apply Cond_lemma; simpl_PCond req)))
+ fun f rl => f mkFV mkFE simpl_field lemma req rl;
+ try (apply Cond_lemma; simpl_PCond req)
| _ => fail 1 "field anomaly: bad correctness lemma (rewr)"
end in
Make_tac ReflexiveRewriteTactic.
(* Pb: second rewrite are applied to non-zero condition of first rewrite... *)
Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
- field_lookup (fun req cst_tac _ _ field_simplify_ok cond_ok pre post rl =>
- (pre(); Field_simplify field_simplify_ok cond_ok req cst_tac; post())).
+ field_lookup
+ (fun req cst_tac _ _ field_simplify_ok cond_ok pre post rl =>
+ pre(); Field_simplify field_simplify_ok cond_ok req cst_tac rl; post()).
(* Generic form of field tactics *)
Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
- let ParseLemma :=
- match type of lemma with
- | forall l fe1 fe2 nfe1 nfe2, _ = nfe1 -> _ = nfe2 -> _ ->
- PCond _ _ _ _ _ _ _ _ _ ->
- req (@FEeval ?R ?rO _ _ _ _ _ _ _ _ l fe1) _ =>
- (fun f => f R rO)
- | _ => fail 1 "field anomaly: bad correctness lemma (scheme)"
- end in
- let ParseExpr2 ilemma :=
- match type of ilemma with
- forall nfe1 nfe2, ?fe1 = nfe1 -> ?fe2 = nfe2 -> _ => (fun f => f fe1 fe2)
- | _ => fail 1 "field anomaly: cannot find norm expression"
- end in
- let Main r1 r2 R rO :=
- let fv := FV_tac r1 (@List.nil R) in
- let fv := FV_tac r2 fv in
- let fe1 := SYN_tac r1 fv in
- let fe2 := SYN_tac r2 fv in
- ParseExpr2 (lemma fv fe1 fe2)
- ltac:(fun nfrac_val1 nfrac_val2 =>
- (let nfrac1 := fresh "frac1" in
- let norm_hyp1 := fresh "norm_frac1" in
- (compute_assertion norm_hyp1 nfrac1 nfrac_val1;
- let nfrac2 := fresh "frac2" in
- let norm_hyp2 := fresh "norm_frac2" in
- (compute_assertion norm_hyp2 nfrac2 nfrac_val2;
- (apply (lemma fv fe1 fe2 nfrac1 nfrac2 norm_hyp1 norm_hyp2)
- || fail "field anomaly: failed in applying lemma");
- [ SIMPL_tac | apply Cond_lemma; simpl_PCond req];
- try clear nfrac1 nfrac2 norm_hyp1 norm_hyp2)))) in
- ParseLemma ltac:(OnEquation req Main).
-
-Ltac Field_Scheme_n FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
let R := match type of req with ?R -> _ => R end in
let rec ParseExpr ilemma :=
match type of ilemma with
forall nfe, ?fe = nfe -> _ =>
(fun t =>
- (let x := fresh "fld_expr" in
+ let x := fresh "fld_expr" in
let H := fresh "norm_fld_expr" in
- (compute_assertion H x fe;
- ParseExpr (ilemma x H) t;
- try clear x H)))
+ compute_assertion H x fe;
+ ParseExpr (ilemma x H) t;
+ try clear x H)
| _ => (fun t => t ilemma)
end in
let Main r1 r2 :=
@@ -159,8 +127,8 @@ Ltac Field_Scheme_n FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
let fe2 := SYN_tac r2 fv in
ParseExpr (lemma fv fe1 fe2)
ltac:(fun ilemma =>
- ((apply ilemma || fail "field anomaly: failed in applying lemma");
- [ SIMPL_tac | apply Cond_lemma; simpl_PCond req])) in
+ apply ilemma || fail "field anomaly: failed in applying lemma";
+ [ SIMPL_tac | apply Cond_lemma; simpl_PCond req]) in
OnEquation req Main.
(* solve completely a field equation, leaving non-zero conditions to be
@@ -170,13 +138,14 @@ Ltac Field lemma Cond_lemma req Cst_tac :=
let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
let Simpl :=
- vm_compute; (reflexivity || fail "not a valid field equation") in
- Field_Scheme_n mkFV mkFE Simpl lemma Cond_lemma req in
+ vm_compute; reflexivity || fail "not a valid field equation" in
+ Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
ParseFieldComponents lemma req Main.
Tactic Notation (at level 0) "field" :=
- field_lookup (fun req cst_tac field_ok _ _ cond_ok pre post rl =>
- (pre(); Field field_ok cond_ok req cst_tac; post())).
+ field_lookup
+ (fun req cst_tac field_ok _ _ cond_ok pre post rl =>
+ pre(); Field field_ok cond_ok req cst_tac; post()).
(* transforms a field equation to an equivalent (simplified) ring equation,
and leaves non-zero conditions to be proved (field_simplify_eq) *)
@@ -185,13 +154,14 @@ Ltac Field_simplify_eq lemma Cond_lemma req Cst_tac :=
let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
let Simpl := (protect_fv "field") in
- Field_Scheme_n mkFV mkFE Simpl lemma Cond_lemma req in
+ Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
ParseFieldComponents lemma req Main.
-Tactic Notation (at level 0) "field_simplify_eq" constr_list(rl) :=
- field_lookup (fun req cst_tac _ field_simplify_eq_ok _ cond_ok pre post rl =>
- (pre(); Field_simplify_eq field_simplify_eq_ok cond_ok req cst_tac;
- post())) rl.
+Tactic Notation (at level 0) "field_simplify_eq" :=
+ field_lookup
+ (fun req cst_tac _ field_simplify_eq_ok _ cond_ok pre post rl =>
+ pre(); Field_simplify_eq field_simplify_eq_ok cond_ok req cst_tac;
+ post()).
(* Adding a new field *)
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index ec09d4f0b..95efde7f5 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -28,7 +28,7 @@ Ltac OnMainSubgoal H ty :=
match ty with
| _ -> ?ty' =>
let subtac := OnMainSubgoal H ty' in
- (fun tac => (lapply H; [clear H; intro H; subtac tac | idtac]))
+ fun tac => lapply H; [clear H; intro H; subtac tac | idtac]
| _ => (fun tac => tac)
end.
@@ -59,7 +59,7 @@ Ltac ReflexiveRewriteTactic FV_tac SYN_tac SIMPL_tac lemma2 req rl :=
list_iter
ltac:(fun r =>
let ast := SYN_tac r fv in
- (try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast))
+ try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast)
rl).
(********************************************************)
@@ -117,18 +117,18 @@ Ltac FV Cst add mul sub opp t fv :=
req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe1) _ =>
let mkFV := FV Cst_tac add mul sub opp in
let mkPol := mkPolexpr C Cst_tac add mul sub opp in
- (fun f => f R mkFV mkPol)
+ fun f => f R mkFV mkPol
| _ => fail 1 "ring anomaly: bad correctness lemma"
end in
let Main r1 r2 R mkFV mkPol :=
let fv := mkFV r1 (@List.nil R) in
let fv := mkFV r2 fv in
- (check_fv fv;
- let pe1 := mkPol r1 fv in
+ check_fv fv;
+ (let pe1 := mkPol r1 fv in
let pe2 := mkPol r2 fv in
- (apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring");
+ apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring";
vm_compute;
- (exact (refl_equal true) || fail "not a valid ring equation")) in
+ exact (refl_equal true) || fail "not a valid ring equation") in
Make_tac ltac:(OnEquation req Main).
Ltac Ring_simplify Cst_tac lemma2 req rl :=
@@ -149,12 +149,12 @@ Ltac Ring_simplify Cst_tac lemma2 req rl :=
Tactic Notation (at level 0) "ring" :=
ring_lookup
(fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
- (pre(); Ring cst_tac lemma1 req)).
+ pre(); Ring cst_tac lemma1 req).
Tactic Notation (at level 0) "ring_simplify" constr_list(rl) :=
ring_lookup
(fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
- (pre(); Ring_simplify cst_tac lemma2 req rl; post())) rl.
+ pre(); Ring_simplify cst_tac lemma2 req rl; post()) rl.
(* A simple macro tactic to be prefered to ring_simplify *)
Ltac ring_replace t1 t2 := replace t1 with t2 by ring.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 01:33:08 +0000