blob: 2ac96b826515cde4825f674ec4ab825a171f144a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import Ring_tac.
Require Import InitialRing.
Require Import Field.
(* syntaxification *)
Ltac mkFieldexpr C Cst radd rmul rsub ropp rdiv rinv t fv :=
let rec mkP t :=
match Cst t with
| Ring_tac.NotConstant =>
match t with
| (radd ?t1 ?t2) =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(FEadd C e1 e2)
| (rmul ?t1 ?t2) =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(FEmul C e1 e2)
| (rsub ?t1 ?t2) =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(FEsub C e1 e2)
| (ropp ?t1) =>
let e1 := mkP t1 in constr:(FEopp C e1)
| (rdiv ?t1 ?t2) =>
let e1 := mkP t1 in
let e2 := mkP t2 in constr:(FEdiv C e1 e2)
| (rinv ?t1) =>
let e1 := mkP t1 in constr:(FEinv C e1)
| _ =>
let p := Find_at t fv in constr:(FEX C p)
end
| ?c => constr:(FEc C c)
end
in mkP t.
Ltac FFV Cst add mul sub opp div inv t fv :=
let rec TFV t fv :=
match Cst t with
| Ring_tac.NotConstant =>
match t with
| (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)
| (opp ?t1) => TFV t1 fv
| (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
| (inv ?t1) => TFV t1 fv
| _ => AddFvTail t fv
end
| _ => fv
end
in TFV t fv.
(* simplifying the non-zero condition... *)
Ltac fold_field_cond req rO :=
let rec fold_concl t :=
match t with
?x /\ ?y =>
let fx := fold_concl x in let fy := fold_concl y in constr:(fx/\fy)
| req ?x rO -> False => constr:(~ req x rO)
| _ => t
end in
match goal with
|- ?t => let ft := fold_concl t in change ft
end.
Ltac simpl_PCond req rO :=
protect_fv "field";
try (exact I);
fold_field_cond req rO.
(* Rewriting *)
Ltac Field_rewrite_list lemma Cond_lemma req Cst_tac :=
let Make_tac :=
match type of lemma with
| forall l fe nfe,
_ = nfe ->
PCond _ _ _ _ _ _ _ _ _ _ _ ->
req (FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv ?C ?phi l fe) _ =>
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*)
unfold Pphi_dev in H;simpl in H in
(fun f => f mkFV mkFE simpl_field lemma req;
try (apply Cond_lemma; simpl_PCond req rO))
| _ => fail 1 "field anomaly: bad correctness lemma"
end in
Make_tac ReflexiveRewriteTactic.
(* Pb: second rewrite are applied to non-zero condition of first rewrite... *)
(* 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"
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
let nfrac1 := fresh "frac1" in
let norm_hyp1 := fresh "norm_frac1" in
let nfrac2 := fresh "frac2" in
let norm_hyp2 := fresh "norm_frac2" in
ParseExpr2 (lemma fv fe1 fe2)
ltac:(fun nfrac_val1 nfrac_val2 =>
(compute_assertion norm_hyp1 nfrac1 nfrac_val1;
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 rO];
try clear nfrac1 nfrac2 norm_hyp1 norm_hyp2)) in
ParseLemma ltac:(OnEquation req Main).
Ltac ParseFieldComponents lemma req :=
match type of lemma with
| forall l fe1 fe2 nfe1 nfe2,
_ = nfe1 -> _ = nfe2 -> _ -> PCond _ _ _ _ _ _ _ _ _ _ _ ->
req (FEeval ?R ?rO ?add ?mul ?sub ?opp ?div ?inv ?C ?phi l fe1) _ =>
(fun f => f add mul sub opp div inv C)
| _ => fail 1 "field: bad correctness lemma"
end.
(* solve completely a field equation, leaving non-zero conditions to be
proved *)
Ltac Make_field_tac lemma Cond_lemma req Cst_tac :=
let Main radd rmul rsub ropp rdiv rinv C :=
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 mkFV mkFE Simpl lemma Cond_lemma req in
ParseFieldComponents lemma req Main.
(* transforms a field equation to an equivalent (simplified) ring equation,
and leaves non-zero conditions to be proved *)
Ltac Make_field_simplify_eq_tac lemma Cond_lemma req Cst_tac :=
let Main radd rmul rsub ropp rdiv rinv C :=
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 := (unfold Pphi_dev; simpl) in
Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
ParseFieldComponents lemma req Main.
|
