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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Term
open Proof_type
open Tacmach
open Glob_term
open Refiner
open Genarg
open Tacexpr
open Tactics
open Util
(* Basic tactics *)
let h_intro_move x y =
abstract_tactic (TacIntroMove (x, y)) (intro_move x y)
let h_intro x = h_intro_move (Some x) no_move
let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
let h_assumption = abstract_tactic TacAssumption assumption
let h_exact c = abstract_tactic (TacExact c) (exact_check c)
let h_exact_no_check c =
abstract_tactic (TacExactNoCheck c) (exact_no_check c)
let h_vm_cast_no_check c =
abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c)
let h_apply simple ev cb =
abstract_tactic (TacApply (simple,ev,List.map snd cb,None))
(apply_with_bindings_gen simple ev cb)
let h_apply_in simple ev cb (id,ipat as inhyp) =
abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp))
(apply_in simple ev id cb ipat)
let h_elim ev cb cbo =
abstract_tactic (TacElim (ev,cb,cbo))
(elim ev cb cbo)
let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c)
let h_case ev cb = abstract_tactic (TacCase (ev,cb)) (general_case_analysis ev cb)
let h_case_type c = abstract_tactic (TacCaseType c) (case_type c)
let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n)
let h_mutual_fix b id n l =
abstract_tactic
(TacMutualFix (b,id,n,l))
(mutual_fix id n l 0)
let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido)
let h_mutual_cofix b id l =
abstract_tactic
(TacMutualCofix (b,id,l))
(mutual_cofix id l 0)
let h_cut c = abstract_tactic (TacCut c) (cut c)
let h_generalize_gen cl =
abstract_tactic (TacGeneralize cl)
(generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl))
let h_generalize cl =
h_generalize_gen (List.map (fun c -> ((all_occurrences_expr,c),Names.Anonymous))
cl)
let h_generalize_dep c =
abstract_tactic (TacGeneralizeDep c) (generalize_dep c)
let h_let_tac b na c cl eqpat =
let id = Option.default (dummy_loc,IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
abstract_tactic (TacLetTac (na,c,cl,b,eqpat))
(letin_tac with_eq na c None cl)
let h_let_pat_tac b na c cl eqpat =
let id = Option.default (dummy_loc,IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
abstract_tactic (TacLetTac (na,snd c,cl,b,eqpat))
(letin_pat_tac with_eq na c None cl)
(* Derived basic tactics *)
let h_simple_induction_destruct isrec h =
abstract_tactic (TacSimpleInductionDestruct (isrec,h))
(if isrec then (simple_induct h) else (simple_destruct h))
let h_simple_induction = h_simple_induction_destruct true
let h_simple_destruct = h_simple_induction_destruct false
let out_indarg = function
| ElimOnConstr (_,c) -> ElimOnConstr c
| ElimOnIdent id -> ElimOnIdent id
| ElimOnAnonHyp n -> ElimOnAnonHyp n
let h_induction_destruct isrec ev lcl =
let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in
abstract_tactic (TacInductionDestruct (isrec,ev,lcl'))
(induction_destruct isrec ev lcl)
let h_new_induction ev c idl e cl =
h_induction_destruct true ev ([c,idl],e,cl)
let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl)
let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d)
let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
(* Context management *)
let h_clear b l = abstract_tactic (TacClear (b,l))
((if b then keep else clear) l)
let h_clear_body l = abstract_tactic (TacClearBody l) (clear_body l)
let h_move dep id1 id2 =
abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2)
let h_rename l =
abstract_tactic (TacRename l) (rename_hyp l)
let h_revert l = abstract_tactic (TacRevert l) (revert l)
(* Constructors *)
let h_left ev l = abstract_tactic (TacLeft (ev,l)) (left_with_bindings ev l)
let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_bindings ev l)
let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_bindings ev l)
(* Moved to tacinterp because of dependencies in Tacinterp.interp
let h_any_constructor t =
abstract_tactic (TacAnyConstructor t) (any_constructor t)
*)
let h_constructor ev n l =
abstract_tactic (TacConstructor(ev,ArgArg n,l))(constructor_tac ev None n l)
let h_one_constructor n =
abstract_tactic (TacConstructor(false,ArgArg n,NoBindings)) (one_constructor n NoBindings)
let h_simplest_left = h_left false NoBindings
let h_simplest_right = h_right false NoBindings
(* Conversion *)
let h_reduce r cl =
abstract_tactic (TacReduce (r,cl)) (reduce r cl)
let h_change op c cl =
abstract_tactic (TacChange (op,c,cl)) (change op c cl)
(* Equivalence relations *)
let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity
let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c)
let h_transitivity c =
abstract_tactic (TacTransitivity c)
(intros_transitivity c)
let h_simplest_apply c = h_apply false false [dummy_loc,(c,NoBindings)]
let h_simplest_eapply c = h_apply false true [dummy_loc,(c,NoBindings)]
let h_simplest_elim c = h_elim false (c,NoBindings) None
let h_simplest_case c = h_case false (c,NoBindings)
let h_intro_patterns l = abstract_tactic (TacIntroPattern l) (intro_patterns l)
|
