This repository was archived by the owner on Jun 17, 2026. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 26
Expand file tree
/
Copy pathtactic.lean
More file actions
164 lines (136 loc) · 7.73 KB
/
Copy pathtactic.lean
File metadata and controls
164 lines (136 loc) · 7.73 KB
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
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
This is just a trick to embed the 'tactic language' as a Lean
expression. We should view 'tactic' as automation that when execute
produces a term. tactic.builtin is just a "dummy" for creating the
definitions that are actually implemented in C++
-/
prelude
import init.datatypes init.reserved_notation init.num
inductive tactic :
Type := builtin : tactic
namespace tactic
-- Remark the following names are not arbitrary, the tactic module
-- uses them when converting Lean expressions into actual tactic objects.
-- The bultin 'by' construct triggers the process of converting a
-- a term of type 'tactic' into a tactic that sythesizes a term
definition and_then (t1 t2 : tactic) : tactic := builtin
definition or_else (t1 t2 : tactic) : tactic := builtin
definition par (t1 t2 : tactic) : tactic := builtin
definition fixpoint (f : tactic → tactic) : tactic := builtin
definition repeat (t : tactic) : tactic := builtin
definition at_most (t : tactic) (k : num) : tactic := builtin
definition discard (t : tactic) (k : num) : tactic := builtin
definition focus_at (t : tactic) (i : num) : tactic := builtin
definition try_for (t : tactic) (ms : num) : tactic := builtin
definition all_goals (t : tactic) : tactic := builtin
definition now : tactic := builtin
definition assumption : tactic := builtin
definition eassumption : tactic := builtin
definition state : tactic := builtin
definition fail : tactic := builtin
definition id : tactic := builtin
definition beta : tactic := builtin
definition info : tactic := builtin
definition whnf : tactic := builtin
definition contradiction : tactic := builtin
definition exfalso : tactic := builtin
definition congruence : tactic := builtin
definition rotate_left (k : num) := builtin
definition rotate_right (k : num) := builtin
definition rotate (k : num) := rotate_left k
definition norm_num : tactic := builtin
-- This is just a trick to embed expressions into tactics.
-- The nested expressions are "raw". They tactic should
-- elaborate them when it is executed.
inductive expr : Type :=
builtin : expr
inductive expr_list : Type :=
| nil : expr_list
| cons : expr → expr_list → expr_list
-- auxiliary type used to mark optional list of arguments
definition opt_expr_list := expr_list
-- auxiliary types used to mark that the expression is suppose to be an identifier, optional, or a list.
definition identifier := expr
definition identifier_list := expr_list
definition opt_identifier_list := expr_list
-- Remark: the parser has special support for tactics containing `location` parameters.
-- It will parse the optional `at ...` modifier.
definition location := expr
-- Marker for instructing the parser to parse it as 'with <expr>'
definition with_expr := expr
-- Marker for instructing the parser to parse it as '?(using <expr>)'
definition using_expr := expr
-- Constant used to denote the case were no expression was provided
definition none_expr : expr := expr.builtin
definition apply (e : expr) : tactic := builtin
definition eapply (e : expr) : tactic := builtin
definition fapply (e : expr) : tactic := builtin
definition rename (a b : identifier) : tactic := builtin
definition intro (e : opt_identifier_list) : tactic := builtin
definition generalize_tac (e : expr) (id : identifier) : tactic := builtin
definition clear (e : identifier_list) : tactic := builtin
definition revert (e : identifier_list) : tactic := builtin
definition refine (e : expr) : tactic := builtin
definition exact (e : expr) : tactic := builtin
-- Relaxed version of exact that does not enforce goal type
definition rexact (e : expr) : tactic := builtin
definition check_expr (e : expr) : tactic := builtin
definition trace (s : string) : tactic := builtin
-- rewrite_tac is just a marker for the builtin 'rewrite' notation
-- used to create instances of this tactic.
definition rewrite_tac (e : expr_list) : tactic := builtin
definition xrewrite_tac (e : expr_list) : tactic := builtin
definition krewrite_tac (e : expr_list) : tactic := builtin
definition replace (old : expr) (new : with_expr) (loc : location) : tactic := builtin
-- Arguments:
-- - ls : lemmas to be used (if not provided, then blast will choose them)
-- - ds : definitions that can be unfolded (if not provided, then blast will choose them)
definition blast (ls : opt_identifier_list) (ds : opt_identifier_list) : tactic := builtin
-- with_options_tac is just a marker for the builtin 'with_options' notation
definition with_options_tac (o : expr) (t : tactic) : tactic := builtin
-- with_options_tac is just a marker for the builtin 'with_attributes' notation
definition with_attributes_tac (o : expr) (n : identifier_list) (t : tactic) : tactic := builtin
definition simp : tactic := #tactic with_options [blast.strategy "simp"] blast
definition simp_nohyps : tactic := #tactic with_options [blast.strategy "simp_nohyps"] blast
definition simp_topdown : tactic := #tactic with_options [blast.strategy "simp", simplify.top_down true] blast
definition inst_simp : tactic := #tactic with_options [blast.strategy "ematch_simp"] blast
definition rec_simp : tactic := #tactic with_options [blast.strategy "rec_simp"] blast
definition rec_inst_simp : tactic := #tactic with_options [blast.strategy "rec_ematch_simp"] blast
definition grind : tactic := #tactic with_options [blast.strategy "grind"] blast
definition grind_simp : tactic := #tactic with_options [blast.strategy "grind_simp"] blast
definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin
definition induction (h : expr) (rec : using_expr) (ids : opt_identifier_list) : tactic := builtin
definition intros (ids : opt_identifier_list) : tactic := builtin
definition generalizes (es : expr_list) : tactic := builtin
definition clears (ids : identifier_list) : tactic := builtin
definition reverts (ids : identifier_list) : tactic := builtin
definition change (e : expr) : tactic := builtin
definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
definition note_tac (id : identifier) (e : expr) : tactic := builtin
definition constructor (k : option num) : tactic := builtin
definition fconstructor (k : option num) : tactic := builtin
definition existsi (e : expr) : tactic := builtin
definition split : tactic := builtin
definition left : tactic := builtin
definition right : tactic := builtin
definition injection (e : expr) (ids : opt_identifier_list) : tactic := builtin
definition subst (ids : identifier_list) : tactic := builtin
definition substvars : tactic := builtin
definition reflexivity : tactic := builtin
definition symmetry : tactic := builtin
definition transitivity (e : expr) : tactic := builtin
definition try (t : tactic) : tactic := or_else t id
definition repeat1 (t : tactic) : tactic := and_then t (repeat t)
definition focus (t : tactic) : tactic := focus_at t 0
definition determ (t : tactic) : tactic := at_most t 1
definition trivial : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption
definition do (n : nat) (t : tactic) : tactic :=
nat.rec id (λn t', and_then t t') n
end tactic
tactic_infixl `;`:15 := tactic.and_then
tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
--tactic_notation `replace` s `with` t := tactic.replace_tac s t