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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
open Names
open Termops
open EConstr
open Inductiveops
open Hipattern
open Tacmach.New
open Tacticals.New
open Tactics
open Proofview.Notations
module NamedDecl = Context.Named.Declaration
(* Supposed to be called without as clause *)
let introElimAssumsThen tac ba =
assert (ba.Tacticals.branchnames == []);
let introElimAssums = tclDO ba.Tacticals.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.Tacticals.branchsign in
let n2 = List.length ba.Tacticals.branchnames in
let (l1,l2),l3 =
if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, []
else (ba.Tacticals.branchnames, []), List.make (n1-n2) false in
let introCaseAssums =
tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in
(tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
(* 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 elimHypThen tac id =
elimination_then tac (mkVar id)
let rec general_decompose_on_hyp recognizer =
ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())
and general_decompose_aux recognizer id =
elimHypThen
(introElimAssumsThen
(fun bas ->
tclTHEN (clear [id])
(tclMAP (general_decompose_on_hyp recognizer)
(ids_of_named_context bas.Tacticals.assums))))
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 up_to_delta = ref false (* true *)
let general_decompose recognizer c =
Proofview.Goal.enter { enter = begin fun gl ->
let type_of = pf_unsafe_type_of gl in
let sigma = project gl in
let typc = type_of c in
tclTHENS (cut typc)
[ tclTHEN (intro_using tmphyp_name)
(onLastHypId
(ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma))
(fun id -> clear [id])));
exact_no_check c ]
end }
let head_in indl t gl =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
try
let ity,_ =
if !up_to_delta
then find_mrectype env sigma t
else extract_mrectype sigma t
in List.exists (fun i -> eq_ind (fst i) (fst ity)) indl
with Not_found -> false
let decompose_these c l =
Proofview.Goal.enter { enter = begin fun gl ->
let indl = List.map (fun x -> x, Univ.Instance.empty) l in
general_decompose (fun sigma (_,t) -> head_in indl t gl) c
end }
let decompose_and c =
general_decompose
(fun sigma (_,t) -> is_record sigma t)
c
let decompose_or c =
general_decompose
(fun sigma (_,t) -> is_disjunction sigma t)
c
let h_decompose l c = decompose_these c l
let h_decompose_or = decompose_or
let h_decompose_and = decompose_and
(* The tactic Double performs a double induction *)
let simple_elimination c =
elimination_then (fun _ -> tclIDTAC) c
let induction_trailer abs_i abs_j bargs =
tclTHEN
(tclDO (abs_j - abs_i) intro)
(onLastHypId
(fun id ->
Proofview.Goal.enter { enter = begin fun gl ->
let idty = pf_unsafe_type_of gl (mkVar id) in
let fvty = global_vars (pf_env gl) (project gl) idty in
let possible_bring_hyps =
(List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
in
let (hyps,_) =
List.fold_left
(fun (bring_ids,leave_ids) d ->
let cid = NamedDecl.get_id d in
if not (List.mem cid leave_ids)
then (d::bring_ids,leave_ids)
else (bring_ids,cid::leave_ids))
([],fvty) possible_bring_hyps
in
let ids = List.rev (ids_of_named_context hyps) in
(tclTHENLIST
[revert ids; simple_elimination (mkVar id)])
end }
))
let double_ind h1 h2 =
Proofview.Goal.enter { enter = begin fun gl ->
let abs_i = depth_of_quantified_hypothesis true h1 gl in
let abs_j = depth_of_quantified_hypothesis true h2 gl in
let abs =
if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else
tclZEROMSG (Pp.str "Both hypotheses are the same.") in
abs >>= fun (abs_i,abs_j) ->
(tclTHEN (tclDO abs_i intro)
(onLastHypId
(fun id ->
elimination_then
(introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
end }
let h_double_induction = double_ind
|
