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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
open Names
open Constr
open Termops
open EConstr
open Inductiveops
open Hipattern
open Tacmach.New
open Tacticals.New
open Clenv
open Tactics
type branch_args = {
branchnum : int; (* the branch number *)
nassums : int; (* number of assumptions/letin to be introduced *)
branchsign : bool list; (* the signature of the branch.
true=assumption, false=let-in *)
branchnames : Tactypes.intro_patterns}
type elim_kind = Case of bool | Elim
(* Find the right elimination suffix corresponding to the sort of the goal *)
(* c should be of type A1->.. An->B with B an inductive definition *)
let general_elim_then_using mk_elim
rec_flag allnames tac predicate (ind, u, args) id =
let open Pp in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sort = Retyping.get_sort_family_of env sigma (Proofview.Goal.concl gl) in
let sigma, elim = match mk_elim with
| Case dep ->
let u = EInstance.kind sigma u in
let (sigma, r) = Indrec.build_case_analysis_scheme env sigma (ind, u) dep sort in
(sigma, EConstr.of_constr r)
| Elim ->
let gr = Indrec.lookup_eliminator env ind sort in
Evd.fresh_global env sigma gr
in
let indclause = mk_clenv_from_env env sigma None (mkVar id, mkApp (mkIndU (ind, u), args)) in
(* applying elimination_scheme just a little modified *)
let elimclause = mk_clenv_from_env env sigma None (elim, Retyping.get_type_of env sigma elim) in
let indmv =
match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
| Meta mv -> mv
| _ -> CErrors.anomaly (str"elimination.")
in
let pmv =
let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in
match EConstr.kind elimclause.evd p with
| Meta p -> p
| _ ->
let name_elim =
match EConstr.kind sigma elim with
| Const _ | Var _ -> str " " ++ Printer.pr_econstr_env env sigma elim
| _ -> mt ()
in
CErrors.user_err ~hdr:"Tacticals.general_elim_then_using"
(str "The elimination combinator " ++ name_elim ++ str " is unknown.")
in
let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag (ind, u) in
let brnames = Tacticals.compute_induction_names false branchsigns allnames in
let flags = Unification.elim_flags () in
let elimclause' =
match predicate with
| None -> elimclause'
| Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
in
let after_tac i =
let ba = { branchsign = branchsigns.(i);
branchnames = brnames.(i);
nassums = List.length branchsigns.(i);
branchnum = i+1; }
in
tac ba
in
let branchtacs = List.init (Array.length branchsigns) after_tac in
Proofview.tclTHEN
(Clenv.res_pf ~flags elimclause')
(Proofview.tclEXTEND [] tclIDTAC branchtacs)
end
(* computing the case/elim combinators *)
let make_elim_branch_assumptions ba hyps =
let assums =
try List.rev (List.firstn ba.nassums hyps)
with Failure _ -> CErrors.anomaly (Pp.str "make_elim_branch_assumptions.") in
assums
let elim_on_ba tac ba =
Proofview.Goal.enter begin fun gl ->
let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
tac branches
end
let elimination_then tac id =
let open Declarations in
Proofview.Goal.enter begin fun gl ->
let ((ind, u), t) = pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl (mkVar id)) in
let _, args = decompose_app_vect (Proofview.Goal.sigma gl) t in
let isrec,mkelim =
match (Global.lookup_mind (fst ind)).mind_record with
| NotRecord -> true, Elim
| FakeRecord | PrimRecord _ -> false, Case true
in
general_elim_then_using mkelim isrec None tac None (ind, u, args) id
end
(* Supposed to be called without as clause *)
let introElimAssumsThen tac ba =
assert (ba.branchnames == []);
let introElimAssums = tclDO ba.nassums intro in
(tclTHEN introElimAssums (elim_on_ba tac ba))
(* Supposed to be called with a non-recursive scheme *)
let introCaseAssumsThen with_evars tac ba =
let n1 = List.length ba.branchsign in
let n2 = List.length ba.branchnames in
let (l1,l2),l3 =
if n1 < n2 then List.chop n1 ba.branchnames, []
else (ba.branchnames, []), List.make (n1-n2) false in
let introCaseAssums =
tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in
(tclTHEN introCaseAssums (elim_on_ba (tac l2) ba))
let case_tac dep names tac elim ind c =
let tac = introCaseAssumsThen false (* ApplyOn not supported by inversion *) tac in
general_elim_then_using (Case dep) false names tac (Some elim) ind c
(* The following tactic Decompose repeatedly applies the
elimination(s) rule(s) of the types satisfying the predicate
``recognizer'' onto a certain hypothesis. For example :
Require Elim.
Require Le.
Goal (y:nat){x:nat | (le O x)/\(le x y)}->{x:nat | (le O x)}.
Intros y H.
Decompose [sig and] H;EAuto.
Qed.
Another example :
Goal (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C.
Intros A B C H; Decompose [and or] H; Assumption.
Qed.
*)
let rec general_decompose_on_hyp recognizer =
ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())
and general_decompose_aux recognizer id =
elimination_then
(introElimAssumsThen
(fun bas ->
tclTHEN (clear [id])
(tclMAP (general_decompose_on_hyp recognizer)
(ids_of_named_context bas))))
id
(* We should add a COMPLETE to be sure that the created hypothesis
doesn't stay if no elimination is possible *)
(* Best strategies but loss of compatibility *)
let tmphyp_name = Id.of_string "_TmpHyp"
let general_decompose recognizer c =
Proofview.Goal.enter begin fun gl ->
let typc = pf_get_type_of gl c in
tclTHENS (cut typc)
[ intro_using_then tmphyp_name (fun id ->
ifOnHyp recognizer (general_decompose_aux recognizer)
(fun id -> clear [id])
id);
exact_no_check c ]
end
let head_in indl t gl =
let sigma = Tacmach.New.project gl in
try
let ity,_ = extract_mrectype sigma t in
List.exists (fun i -> Ind.CanOrd.equal (fst i) (fst ity)) indl
with Not_found -> false
let decompose_these c l =
Proofview.Goal.enter begin fun gl ->
let indl = List.map (fun x -> x, Univ.Instance.empty) l in
general_decompose (fun env sigma (_,t) -> head_in indl t gl) c
end
let decompose_and c =
general_decompose
(fun env sigma (_,t) -> is_record env sigma t)
c
let decompose_or c =
general_decompose
(fun env sigma (_,t) -> is_disjunction env sigma t)
c
let h_decompose l c = decompose_these c l
let h_decompose_or = decompose_or
let h_decompose_and = decompose_and
|
