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
open Printer
open Pretyping
open Glob_term
open Tacmach
open Ssrmatching_plugin
open Ssrmatching
open Ssrast
open Ssrcommon
(** Backward chaining tactics: apply, exact, congr. *)
(** The "apply" tactic *)
let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
let rc = pf_intern_term ist gl c in
let rcs' = rc :: rcs in
match goclr with
| None -> clr, rcs'
| Some ghyps ->
let clr' = snd (interp_hyps ist gl ghyps) @ clr in
if k <> NoFlag then clr', rcs' else
let loc = rc.CAst.loc in
match DAst.get rc with
| GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
| GRef (Names.GlobRef.VarRef id, _) when not_section_id id ->
SsrHyp (Loc.tag ?loc id) :: clr', rcs'
| _ -> clr', rcs'
let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) (project gl)
let interp_nbargs ist gl rc =
try
let rc6 = mkRApp rc (mkRHoles 6) in
let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc6, None) in
let si = sig_it gl in
let gl = re_sig si sigma in
6 + Ssrcommon.nbargs_open_constr (pf_env gl) t
with _ -> 5
let interp_view_nbimps ist gl rc =
try
let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc, None) in
let si = sig_it gl in
let gl = re_sig si sigma in
let pl, c = splay_open_constr (pf_env gl) t in
if Ssrcommon.isAppInd (pf_env gl) (project gl) c then List.length pl else (-(List.length pl))
with _ -> 0
let interp_agens ist gl gagens =
match List.fold_right (interp_agen ist gl) gagens ([], []) with
| clr, rlemma :: args ->
let n = interp_nbargs ist gl rlemma - List.length args in
let rec loop i =
if i > n then
errorstrm Pp.(str "Cannot apply lemma " ++ pf_pr_glob_constr gl rlemma)
else
try interp_refine ist gl (mkRApp rlemma (mkRHoles i @ args))
with _ -> loop (i + 1) in
clr, loop 0
| _ -> assert false
let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c)
let apply_rconstr ?ist t gl =
let n = match ist, DAst.get t with
| None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs (pf_env gl) (project gl) (EConstr.mkVar id)
| Some ist, _ -> interp_nbargs ist gl t
| _ -> anomaly "apply_rconstr without ist and not RVar" in
let mkRlemma i = mkRApp t (mkRHoles i) in
let cl = pf_concl gl in
let rec loop i =
if i > n then
errorstrm Pp.(str"Cannot apply lemma "++pf_pr_glob_constr gl t)
else try pf_match gl (mkRlemma i) (OfType cl) with _ -> loop (i + 1) in
Proofview.V82.of_tactic (refine_with (loop 0)) gl
let mkRAppView ist gl rv gv =
let nb_view_imps = interp_view_nbimps ist gl rv in
mkRApp rv (mkRHoles (abs nb_view_imps))
let refine_interp_apply_view dbl ist gl gv =
let pair i = List.map (fun x -> i, x) in
let rv = pf_intern_term ist gl gv in
let v = mkRAppView ist gl rv gv in
let interp_with (dbl, hint) =
let i = if dbl = Ssrview.AdaptorDb.Equivalence then 2 else 1 in
interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
let rec loop = function
| [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
| h :: hs -> (try Proofview.V82.of_tactic (refine_with (snd (interp_with h))) gl with _ -> loop hs) in
loop (pair dbl (Ssrview.AdaptorDb.get dbl) @
if dbl = Ssrview.AdaptorDb.Equivalence
then pair Ssrview.AdaptorDb.Backward (Ssrview.AdaptorDb.(get Backward))
else [])
let apply_top_tac =
Proofview.Goal.enter begin fun _ ->
Tacticals.New.tclTHENLIST [
introid top_id;
Proofview.V82.tactic (apply_rconstr (mkRVar top_id));
cleartac [SsrHyp(None,top_id)]
]
end
let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl ->
let _, clr = interp_hyps ist gl gclr in
let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in
let ggenl, tclGENTAC =
if gviews <> [] && ggenl <> [] then
let ggenl= List.map (fun (x,(k,p)) -> x, {kind=k; pattern=p; interpretation= Some ist}) (List.hd ggenl) in
[], Tacticals.tclTHEN (Proofview.V82.of_tactic (genstac (ggenl,[])))
else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in
tclGENTAC (fun gl ->
match gviews, ggenl with
| v :: tl, [] ->
let dbl =
if List.length tl = 1
then Ssrview.AdaptorDb.Equivalence
else Ssrview.AdaptorDb.Backward in
Tacticals.tclTHEN
(List.fold_left (fun acc v ->
Tacticals.tclTHENLAST acc (vtac v dbl))
(vtac v Ssrview.AdaptorDb.Backward) tl)
(old_cleartac clr) gl
| [], [agens] ->
let clr', (sigma, lemma) = interp_agens ist gl agens in
let gl = pf_merge_uc_of sigma gl in
Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr']) gl
| _, _ ->
Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [apply_top_tac; cleartac clr]) gl) gl
)
let apply_top_tac = apply_top_tac