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
|
open Util
open Names
open Term
open Tacinvutils
open Pp
open Libnames
open Tacticals
open Tactics
open Indfun_common
open Tacmach
open Sign
let tac_pattern l =
(Hiddentac.h_reduce
(Rawterm.Pattern l)
Tacticals.onConcl
)
let rec nb_prod x =
let rec count n c =
match kind_of_term c with
Prod(_,_,t) -> count (n+1) t
| LetIn(_,a,_,t) -> count n (subst1 a t)
| Cast(c,_,_) -> count n c
| _ -> n
in count 0 x
let intro_discr_until n tac : tactic =
let rec intro_discr_until acc : tactic =
fun g ->
if nb_prod (pf_concl g) <= n then tac (List.rev acc) g
else
tclTHEN
intro
(fun g' ->
let id,_,t = pf_last_hyp g' in
tclORELSE
(tclABSTRACT None (Extratactics.h_discrHyp (Rawterm.NamedHyp id)))
(intro_discr_until ((id,t)::acc))
g'
)
g
in
intro_discr_until []
let rec discr_rew_in_H hypname idl : tactic =
match idl with
| [] -> (Extratactics.h_discrHyp (Rawterm.NamedHyp hypname))
| ((id,t)::idl') ->
match kind_of_term t with
| App(eq',[| _ ; arg1 ; _ |]) when eq_constr eq' (Lazy.force eq) ->
begin
let constr,_ = decompose_app arg1 in
if isConstruct constr
then
(discr_rew_in_H hypname idl')
else
tclTHEN
(tclTRY (Equality.general_rewrite_in true hypname (mkVar id)))
(discr_rew_in_H hypname idl')
end
| _ -> discr_rew_in_H hypname idl'
let finalize fname hypname idl : tactic =
tclTRY (
(tclTHEN
(Hiddentac.h_reduce
(Rawterm.Unfold [[],EvalConstRef fname])
(Tacticals.onHyp hypname)
)
(discr_rew_in_H hypname idl)
))
let gen_fargs fargs : tactic =
fun g ->
generalize
(List.map
(fun arg ->
let targ = pf_type_of g arg in
let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in
refl_arg
)
(Array.to_list fargs)
)
g
let invfun (hypname:identifier) (fid:identifier) : tactic=
fun g ->
let nprod_goal = nb_prod (pf_concl g) in
let f_ind_id =
(
Indrec.make_elimination_ident
fid
(Tacticals.elimination_sort_of_goal g)
)
in
let fname = const_of_id fid in
let princ = const_of_id f_ind_id in
let princ_info =
let princ_type =
(try (match (Global.lookup_constant princ) with
{Declarations.const_type=t} -> t
)
with _ -> assert false)
in
Tactics.compute_elim_sig princ_type
in
let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
let do_invert fargs appf : tactic =
let frealargs = (snd (array_chop (List.length princ_info.params) fargs))
in
let pat_args =
(List.map (fun e -> ([-1],e)) (Array.to_list frealargs)) @ [[],appf]
in
tclTHENSEQ
[
gen_fargs frealargs;
tac_pattern pat_args;
Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings);
intro_discr_until nprod_goal (finalize fname hypname)
]
in
match kind_of_term typhyp with
| App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) ->
(* let valf = def_of_const (mkConst fname) in *)
let eq_arg1 , eq_arg2 , good_eq_form , fargs =
match kind_of_term arg1 , kind_of_term arg2 with
| App(f, args),_ when eq_constr f (mkConst fname) ->
arg1 , arg2 , tclIDTAC , args
| _,App(f, args) when eq_constr f (mkConst fname) ->
arg2 , arg1 , symmetry_in hypname , args
| _ , _ -> error "inversion impossible"
in
tclTHEN
good_eq_form
(do_invert fargs eq_arg1)
g
| App(f',fargs) when eq_constr f' (mkConst fname) ->
do_invert fargs typhyp g
| _ -> error "inversion impossible"
|
