a7b895525b
@dselsam `simp` now supports lemmas containing metavariables. The metavariables are automatically converted into tmp metavars. The new test contains a few examples.
1005 lines
36 KiB
Text
1005 lines
36 KiB
Text
/-
|
||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic
|
||
import init.meta.smt.congruence_closure init.category.combinators
|
||
import init.meta.interactive_base
|
||
|
||
open lean
|
||
open lean.parser
|
||
|
||
local postfix `?`:9001 := optional
|
||
local postfix *:9001 := many
|
||
|
||
namespace tactic
|
||
/- allows metavars -/
|
||
meta def i_to_expr (q : pexpr) : tactic expr :=
|
||
to_expr q tt
|
||
|
||
/- allow metavars and no subgoals -/
|
||
meta def i_to_expr_no_subgoals (q : pexpr) : tactic expr :=
|
||
to_expr q tt ff
|
||
|
||
/- doesn't allows metavars -/
|
||
meta def i_to_expr_strict (q : pexpr) : tactic expr :=
|
||
to_expr q ff
|
||
|
||
/- Auxiliary version of i_to_expr for apply-like tactics.
|
||
This is a workaround for comment
|
||
https://github.com/leanprover/lean/issues/1342#issuecomment-307912291
|
||
at issue #1342.
|
||
|
||
In interactive mode, given a tactic
|
||
|
||
apply f
|
||
|
||
we want the apply tactic to create all metavariables. The following
|
||
definition will return `@f` for `f`. That is, it will **not** create
|
||
metavariables for implicit arguments.
|
||
|
||
Before we added `i_to_expr_for_apply`, the tactic
|
||
|
||
apply le_antisymm
|
||
|
||
would first elaborate `le_antisymm`, and create
|
||
|
||
@le_antisymm ?m_1 ?m_2 ?m_3 ?m_4
|
||
|
||
The type class resolution problem
|
||
?m_2 : weak_order ?m_1
|
||
by the elaborator since ?m_1 is not assigned yet, and the problem is
|
||
discarded.
|
||
|
||
Then, we would invoke `apply_core`, which would create two
|
||
new metavariables for the explicit arguments, and try to unify the resulting
|
||
type with the current target. After the unification,
|
||
the metavariables ?m_1, ?m_3 and ?m_4 are assigned, but we lost
|
||
the information about the pending type class resolution problem.
|
||
|
||
With `i_to_expr_for_apply`, `le_antisymm` is elaborate into `@le_antisymm`,
|
||
the apply_core tactic creates all metavariables, and solves the ones that
|
||
can be solved by type class resolution.
|
||
|
||
Another possible fix: we modify the elaborator to return pending
|
||
type class resolution problems, and store them in the tactic_state.
|
||
-/
|
||
meta def i_to_expr_for_apply (q : pexpr) : tactic expr :=
|
||
let aux (n : name) : tactic expr := do
|
||
p ← resolve_name n,
|
||
match p with
|
||
| (expr.const c []) := do r ← mk_const c, save_type_info r q, return r
|
||
| _ := i_to_expr p
|
||
end
|
||
in match q with
|
||
| (expr.const c []) := aux c
|
||
| (expr.local_const c _ _ _) := aux c
|
||
| _ := i_to_expr q
|
||
end
|
||
|
||
namespace interactive
|
||
open interactive interactive.types expr
|
||
|
||
/--
|
||
itactic: parse a nested "interactive" tactic. That is, parse
|
||
`{` tactic `}`
|
||
-/
|
||
meta def itactic : Type :=
|
||
tactic unit
|
||
|
||
/--
|
||
This tactic applies to a goal that is either a Pi/forall or starts with a let binder.
|
||
|
||
If the current goal is a Pi/forall `∀ x:T, U` (resp `let x:=t in U`) then intro puts `x:T` (resp `x:=t`) in the local context. The new subgoal target is `U`.
|
||
|
||
If the goal is an arrow `T → U`, then it puts in the local context either `h:T`, and the new goal target is `U`.
|
||
|
||
If the goal is neither a Pi/forall nor starting with a let definition,
|
||
the tactic `intro` applies the tactic `whnf` until the tactic `intro` can be applied or the goal is not `head-reducible`.
|
||
-/
|
||
meta def intro : parse ident_? → tactic unit
|
||
| none := intro1 >> skip
|
||
| (some h) := tactic.intro h >> skip
|
||
|
||
/--
|
||
Similar to `intro` tactic. The tactic `intros` will keep introducing new hypotheses until the goal target is not a Pi/forall or let binder.
|
||
The variant `intros h_1 ... h_n` introduces `n` new hypotheses using the given identifiers to name them.
|
||
-/
|
||
meta def intros : parse ident_* → tactic unit
|
||
| [] := tactic.intros >> skip
|
||
| hs := intro_lst hs >> skip
|
||
|
||
/--
|
||
The tactic introv allows to automatically introduce the variables of a theorem and explicitly name the hypotheses involved.
|
||
The given names are used to name non-dependent hypotheses.
|
||
Examples:
|
||
```
|
||
example : ∀ a b : nat, a = b → b = a :=
|
||
begin
|
||
introv h,
|
||
exact h.symm
|
||
end
|
||
```
|
||
The state after `introv h` is
|
||
```
|
||
a b : ℕ,
|
||
h : a = b
|
||
⊢ b = a
|
||
```
|
||
```
|
||
example : ∀ a b : nat, a = b → ∀ c, b = c → a = c :=
|
||
begin
|
||
introv h₁ h₂,
|
||
exact h₁.trans h₂
|
||
end
|
||
```
|
||
The state after `introv h₁ h₂` is
|
||
```
|
||
a b : ℕ,
|
||
h₁ : a = b,
|
||
c : ℕ,
|
||
h₂ : b = c
|
||
⊢ a = c
|
||
```
|
||
-/
|
||
meta def introv (ns : parse ident_*) : tactic unit :=
|
||
tactic.introv ns >> return ()
|
||
|
||
/--
|
||
The tactic `rename h₁ h₂` renames hypothesis `h₁` into `h₂` in the current local context.
|
||
-/
|
||
meta def rename : parse ident → parse ident → tactic unit :=
|
||
tactic.rename
|
||
|
||
/--
|
||
This tactic applies to any goal.
|
||
The argument term is a term well-formed in the local context of the main goal.
|
||
The tactic apply tries to match the current goal against the conclusion of the type of term.
|
||
If it succeeds, then the tactic returns as many subgoals as the number of premises
|
||
that have not been fixed by type inference or type class resolution.
|
||
Non dependent premises are added before dependent ones.
|
||
|
||
The tactic `apply` uses higher-order pattern matching, type class resolution, and
|
||
first-order unification with dependent types.
|
||
-/
|
||
meta def apply (q : parse texpr) : tactic unit :=
|
||
i_to_expr_for_apply q >>= tactic.apply
|
||
|
||
/--
|
||
Similar to the `apply` tactic, but it also creates subgoals for dependent premises
|
||
that have not been fixed by type inference or type class resolution.
|
||
-/
|
||
meta def fapply (q : parse texpr) : tactic unit :=
|
||
i_to_expr_for_apply q >>= tactic.fapply
|
||
|
||
/--
|
||
Similar to the `apply` tactic, but it only creates subgoals for non dependent premises
|
||
that have not been fixed by type inference or type class resolution.
|
||
-/
|
||
meta def eapply (q : parse texpr) : tactic unit :=
|
||
i_to_expr_for_apply q >>= tactic.eapply
|
||
|
||
/--
|
||
Similar to the `apply` tactic, but allows the user to provide a `apply_cfg` configuration object.
|
||
-/
|
||
meta def apply_with (q : parse qexpr) (cfg : apply_cfg) : tactic unit :=
|
||
do e ← i_to_expr_for_apply q, tactic.apply e cfg
|
||
|
||
/--
|
||
This tactic tries to close the main goal `... |- U` using type class resolution.
|
||
It succeeds if it generates a term of type `U` using type class resolution.
|
||
-/
|
||
meta def apply_instance : tactic unit :=
|
||
tactic.apply_instance
|
||
|
||
/--
|
||
This tactic applies to any goal. It behaves like `exact` with a big difference:
|
||
the user can leave some holes `_` in the term.
|
||
`refine` will generate as many subgoals as there are holes in the term.
|
||
Note that some holes may be implicit.
|
||
The type of holes must be either synthesized by the system or declared by
|
||
an explicit type ascription like (e.g., `(_ : nat → Prop)`).
|
||
-/
|
||
meta def refine (q : parse texpr) : tactic unit :=
|
||
tactic.refine q
|
||
|
||
/--
|
||
This tactic looks in the local context for an hypothesis which type is equal to the goal target.
|
||
If it is the case, the subgoal is proved. Otherwise, it fails.
|
||
-/
|
||
meta def assumption : tactic unit :=
|
||
tactic.assumption
|
||
|
||
private meta def change_core (e : expr) : option expr → tactic unit
|
||
| none := tactic.change e
|
||
| (some h) :=
|
||
do num_reverted : ℕ ← revert h,
|
||
expr.pi n bi d b ← target,
|
||
tactic.change $ expr.pi n bi e b,
|
||
intron num_reverted
|
||
|
||
/--
|
||
This tactic applies to any goal. `change U` replaces the main goal target `T` with `U`
|
||
providing that `U` is well-formed with respect to the main goal local context,
|
||
and `T` and `U` are definitionally equal. `change U at h` will change a local hypothesis
|
||
with `U`. `change A with B at h1 h2 ...` will replace `A` with `B` in all the supplied
|
||
hypotheses (or `*`), or in the goal if no `at` clause is specified, provided that
|
||
`A` and `B` are definitionally equal.
|
||
-/
|
||
meta def change (q : parse texpr) : parse (tk "with" *> texpr)? → parse location → tactic unit
|
||
| none (loc.ns []) := do e ← i_to_expr q, change_core e none
|
||
| none (loc.ns [h]) := do eq ← i_to_expr q, eh ← get_local h, change_core eq (some eh)
|
||
| none _ := fail "change-at does not support multiple locations"
|
||
| (some w) l :=
|
||
do hs ← l.get_locals,
|
||
u ← mk_meta_univ,
|
||
ty ← mk_meta_var (sort u),
|
||
eq ← i_to_expr ``(%%q : %%ty),
|
||
ew ← i_to_expr ``(%%w : %%ty),
|
||
let repl := λe : expr, e.replace (λ a n, if a = eq then some ew else none),
|
||
hs.mmap' (λh, do e ← infer_type h, change_core (repl e) (some h)),
|
||
if l.include_goal then do g ← target, change_core (repl g) none else skip
|
||
|
||
/--
|
||
This tactic applies to any goal. It gives directly the exact proof
|
||
term of the goal. Let `T` be our goal, let `p` be a term of type `U` then
|
||
`exact p` succeeds iff `T` and `U` are definitionally equal.
|
||
-/
|
||
meta def exact (q : parse texpr) : tactic unit :=
|
||
do tgt : expr ← target,
|
||
i_to_expr_strict ``(%%q : %%tgt) >>= tactic.exact
|
||
/--
|
||
Like `exact`, but takes a list of terms and checks that all goals
|
||
are discharged after the tactic.
|
||
-/
|
||
meta def exacts : parse qexpr_list_or_texpr → tactic unit
|
||
| [] := done
|
||
| (t :: ts) := exact t >> exacts ts
|
||
|
||
/--
|
||
`revert h₁ ... hₙ` applies to any goal with hypotheses `h₁` ... `hₙ`.
|
||
It moves the hypotheses and its dependencies to the goal target.
|
||
This tactic is the inverse of `intro`.
|
||
-/
|
||
meta def revert (ids : parse ident*) : tactic unit :=
|
||
do hs ← mmap tactic.get_local ids, revert_lst hs, skip
|
||
|
||
private meta def resolve_name' (n : name) : tactic expr :=
|
||
do {
|
||
p ← resolve_name n,
|
||
match p with
|
||
| expr.const n _ := mk_const n -- create metavars for universe levels
|
||
| _ := i_to_expr p
|
||
end
|
||
}
|
||
|
||
/- Version of to_expr that tries to bypass the elaborator if `p` is just a constant or local constant.
|
||
This is not an optimization, by skipping the elaborator we make sure that no unwanted resolution is used.
|
||
Example: the elaborator will force any unassigned ?A that must have be an instance of (has_one ?A) to nat.
|
||
Remark: another benefit is that auxiliary temporary metavariables do not appear in error messages. -/
|
||
private meta def to_expr' (p : pexpr) : tactic expr :=
|
||
match p with
|
||
| (const c []) := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
|
||
| (local_const c _ _ _) := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
|
||
| _ := i_to_expr p
|
||
end
|
||
|
||
meta structure rw_rule :=
|
||
(pos : pos)
|
||
(symm : bool)
|
||
(rule : pexpr)
|
||
|
||
meta instance rw_rule.reflect : has_reflect rw_rule :=
|
||
λ ⟨p, s, r⟩, `(_)
|
||
|
||
private meta def get_rule_eqn_lemmas (r : rw_rule) : tactic (list name) :=
|
||
let aux (n : name) : tactic (list name) := do {
|
||
p ← resolve_name n,
|
||
-- unpack local refs
|
||
let e := p.erase_annotations.get_app_fn.erase_annotations,
|
||
match e with
|
||
| const n _ := get_eqn_lemmas_for tt n
|
||
| _ := return []
|
||
end } <|> return [] in
|
||
match r.rule with
|
||
| const n _ := aux n
|
||
| local_const n _ _ _ := aux n
|
||
| _ := return []
|
||
end
|
||
|
||
private meta def rw_goal (m : transparency) (rs : list rw_rule) : tactic unit :=
|
||
rs.mfor' $ λ r, do
|
||
save_info r.pos,
|
||
eq_lemmas ← get_rule_eqn_lemmas r,
|
||
orelse'
|
||
(to_expr' r.rule >>= rewrite_core m tt tt occurrences.all r.symm)
|
||
(eq_lemmas.mfirst $ λ n, mk_const n >>= rewrite_core m tt tt occurrences.all r.symm)
|
||
(eq_lemmas.empty)
|
||
|
||
private meta def rw_hyp (m : transparency) (rs : list rw_rule) (hname : name) : tactic unit :=
|
||
rs.mfor' $ λ r,
|
||
do h ← get_local hname,
|
||
save_info r.pos,
|
||
eq_lemmas ← get_rule_eqn_lemmas r,
|
||
orelse'
|
||
(do e ← to_expr' r.rule, rewrite_at_core m tt tt occurrences.all r.symm e h)
|
||
(eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_at_core m tt tt occurrences.all r.symm e h)
|
||
(eq_lemmas.empty)
|
||
|
||
private meta def rw_hyps (m : transparency) (rs : list rw_rule) (hs : list name) : tactic unit :=
|
||
hs.mfor' (rw_hyp m rs)
|
||
|
||
meta def rw_rule_p (ep : parser pexpr) : parser rw_rule :=
|
||
rw_rule.mk <$> cur_pos <*> (option.is_some <$> (tk "-")?) <*> ep
|
||
|
||
meta structure rw_rules_t :=
|
||
(rules : list rw_rule)
|
||
(end_pos : option pos)
|
||
|
||
meta instance rw_rules_t.reflect : has_reflect rw_rules_t :=
|
||
λ ⟨rs, p⟩, `(_)
|
||
|
||
-- accepts the same content as `qexpr_list_or_texpr`, but with correct goal info pos annotations
|
||
meta def rw_rules : parser rw_rules_t :=
|
||
(tk "[" *>
|
||
rw_rules_t.mk <$> sep_by (skip_info (tk ",")) (set_goal_info_pos $ rw_rule_p (qexpr 0))
|
||
<*> (some <$> cur_pos <* set_goal_info_pos (tk "]")))
|
||
<|> rw_rules_t.mk <$> (list.ret <$> rw_rule_p texpr) <*> return none
|
||
|
||
private meta def rw_core (m : transparency) (rs : parse rw_rules) (loca : parse location) : tactic unit :=
|
||
match loca with
|
||
| loc.wildcard := fail "wildcard not allowed with rewrite"
|
||
| loc.ns [] := rw_goal m rs.rules
|
||
| loc.ns hs := rw_hyps m rs.rules hs
|
||
end >> try (reflexivity reducible)
|
||
>> (returnopt rs.end_pos >>= save_info <|> skip)
|
||
|
||
meta def rewrite : parse rw_rules → parse location → tactic unit :=
|
||
rw_core reducible
|
||
|
||
meta def rw : parse rw_rules → parse location → tactic unit :=
|
||
rewrite
|
||
|
||
/- rewrite followed by assumption -/
|
||
meta def rwa (q : parse rw_rules) (l : parse location) : tactic unit :=
|
||
rewrite q l >> try assumption
|
||
|
||
meta def erewrite : parse rw_rules → parse location → tactic unit :=
|
||
rw_core semireducible
|
||
|
||
meta def erw : parse rw_rules → parse location → tactic unit :=
|
||
erewrite
|
||
|
||
private meta def get_type_name (e : expr) : tactic name :=
|
||
do e_type ← infer_type e >>= whnf,
|
||
(const I ls) ← return $ get_app_fn e_type,
|
||
return I
|
||
|
||
precedence `generalizing` : 0
|
||
meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list)
|
||
(revert : parse $ (tk "generalizing" *> ident*)?) : tactic unit :=
|
||
do e ← i_to_expr p,
|
||
locals ← mmap tactic.get_local $ revert.get_or_else [],
|
||
n ← revert_lst locals,
|
||
tactic.induction e ids rec_name,
|
||
all_goals (intron n)
|
||
|
||
meta def cases (p : parse texpr) (ids : parse with_ident_list) : tactic unit :=
|
||
do e ← i_to_expr p,
|
||
tactic.cases e ids
|
||
|
||
private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indices : nat) : option expr → expr → option (expr × expr)
|
||
| case e := if e.has_meta_var then match e with
|
||
| (mvar _ _) :=
|
||
do case ← case,
|
||
guard $ e ∈ goals,
|
||
pure (case, e)
|
||
| (app _ _) :=
|
||
let idx :=
|
||
match e.get_app_fn with
|
||
| const (name.mk_string rec ty') _ :=
|
||
guard (ty' = ty) >>
|
||
match mk_simple_name rec with
|
||
| `drec := some idx | `rec := some idx
|
||
-- indices + major premise
|
||
| `dcases_on := some (idx + num_indices + 1) | `cases_on := some (idx + num_indices + 1)
|
||
| _ := none
|
||
end
|
||
| _ := none
|
||
end in
|
||
match idx with
|
||
| none := list.foldl (<|>) (find_case case e.get_app_fn) $ e.get_app_args.map (find_case case)
|
||
| some idx :=
|
||
let args := e.get_app_args in
|
||
do arg ← args.nth idx,
|
||
args.enum.foldl
|
||
(λ acc ⟨i, arg⟩, match acc with
|
||
| some _ := acc
|
||
| _ := if i ≠ idx then find_case none arg else none
|
||
end)
|
||
-- start recursion with likely case
|
||
(find_case (some arg) arg)
|
||
end
|
||
| (lam _ _ _ e) := find_case case e
|
||
| (macro n args) := list.foldl (<|>) none $ args.map (find_case case)
|
||
| _ := none
|
||
end else none
|
||
|
||
private meta def rename_lams : expr → list name → tactic unit
|
||
| (lam n _ _ e) (n'::ns) := (rename n n' >> rename_lams e ns) <|> rename_lams e (n'::ns)
|
||
| _ _ := skip
|
||
|
||
/-- Focuses on the `induction`/`cases` subgoal corresponding to the given introduction rule,
|
||
optionally renaming introduced locals. -/
|
||
meta def case (ctor : parse ident) (ids : parse ident_*) (tac : itactic) : tactic unit :=
|
||
do r ← result,
|
||
env ← get_env,
|
||
ctor ← resolve_constant ctor
|
||
<|> fail ("'" ++ to_string ctor ++ "' is not a constructor"),
|
||
ty ← (env.inductive_type_of ctor).to_monad
|
||
<|> fail ("'" ++ to_string ctor ++ "' is not a constructor"),
|
||
let ctors := env.constructors_of ty,
|
||
let idx := env.inductive_num_params ty + /- motive -/ 1 +
|
||
list.index_of ctor ctors,
|
||
gs ← get_goals,
|
||
(case, g) ← (find_case gs ty idx (env.inductive_num_indices ty) none r ).to_monad
|
||
<|> fail "could not find open goal of given case",
|
||
set_goals $ g :: gs.filter (≠ g),
|
||
rename_lams case ids,
|
||
solve1 tac
|
||
|
||
meta def destruct (p : parse texpr) : tactic unit :=
|
||
i_to_expr p >>= tactic.destruct
|
||
|
||
meta def generalize (p : parse qexpr) (x : parse ident) : tactic unit :=
|
||
do e ← i_to_expr p,
|
||
tactic.generalize e x
|
||
|
||
meta def generalize2 (p : parse qexpr) (x : parse ident) (h : parse ident) : tactic unit :=
|
||
do tgt ← target,
|
||
e ← to_expr p,
|
||
let e' := tgt.replace $ λa n, if a = e then some (var n.succ) else none,
|
||
tgt' ← (do
|
||
tgt' ← to_expr ``(Π x, %%e = x → %%e'),
|
||
type_check tgt',
|
||
return tgt') <|> to_expr ``(Π x, %%e = x → %%tgt),
|
||
assert h tgt',
|
||
swap,
|
||
t ← get_local h,
|
||
exact ``(%%t %%p rfl),
|
||
intro x,
|
||
intro h
|
||
|
||
meta def ginduction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : tactic unit :=
|
||
do x ← mk_fresh_name,
|
||
let (h, hs) := (match ids with
|
||
| [] := (`_h, [])
|
||
| (h :: hs) := (h, hs)
|
||
end : name × list name),
|
||
generalize2 p x h,
|
||
t ← get_local x,
|
||
induction (to_pexpr t) rec_name hs ([] : list name)
|
||
|
||
meta def trivial : tactic unit :=
|
||
tactic.triv <|> tactic.reflexivity <|> tactic.contradiction <|> fail "trivial tactic failed"
|
||
|
||
/-- Closes the main goal using sorry. -/
|
||
meta def admit : tactic unit := tactic.admit
|
||
|
||
/--
|
||
This tactic applies to any goal. The contradiction tactic attempts to find in the current local context an hypothesis that is equivalent to
|
||
an empty inductive type (e.g. `false`), a hypothesis of the form `c_1 ... = c_2 ...` where `c_1` and `c_2` are distinct constructors,
|
||
or two contradictory hypotheses.
|
||
-/
|
||
meta def contradiction : tactic unit :=
|
||
tactic.contradiction
|
||
|
||
meta def repeat : itactic → tactic unit :=
|
||
tactic.repeat
|
||
|
||
meta def try : itactic → tactic unit :=
|
||
tactic.try
|
||
|
||
meta def skip : tactic unit :=
|
||
tactic.skip
|
||
|
||
meta def solve1 : itactic → tactic unit :=
|
||
tactic.solve1
|
||
|
||
meta def abstract (id : parse ident? ) (tac : itactic) : tactic unit :=
|
||
tactic.abstract tac id
|
||
|
||
meta def all_goals : itactic → tactic unit :=
|
||
tactic.all_goals
|
||
|
||
meta def any_goals : itactic → tactic unit :=
|
||
tactic.any_goals
|
||
|
||
meta def focus (tac : itactic) : tactic unit :=
|
||
tactic.focus [tac]
|
||
|
||
meta def «assume» (p : parse parse_binders) : tactic unit :=
|
||
list.mfor' p $ λ b,
|
||
do t ← target,
|
||
when (not $ t.is_pi ∨ t.is_let) whnf_target,
|
||
when (not $ t.is_pi ∨ t.is_let) $
|
||
fail "assume tactic failed, Pi/let expression expected",
|
||
ty ← i_to_expr b.local_type,
|
||
unify ty t.binding_domain,
|
||
intro_core b.local_pp_name
|
||
|
||
meta def «suppose» (h : parse ident?) (q : parse (tk ":" *> texpr)?) : tactic unit :=
|
||
let h := h.get_or_else `this in
|
||
match q with
|
||
| some e := do
|
||
uniq_name ← mk_fresh_name,
|
||
let l := expr.local_const uniq_name h binder_info.default e,
|
||
«assume» [l]
|
||
| none := intro h
|
||
end
|
||
|
||
/--
|
||
This tactic applies to any goal.
|
||
- `have h : T := p` adds the hypothesis `h : T` to the current goal if `p` a term of type `T`.
|
||
If `T` is omitted, it will be inferred.
|
||
- `have h : T` adds the hypothesis `h : T` to the current goal and opens a new subgoal with target `T`.
|
||
The new subgoal becomes the main goal. If `T` is omitted, it will be replaced by a fresh meta variable.
|
||
|
||
If `h` is omitted, it defaults to `this`.
|
||
-/
|
||
meta def «have» (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
|
||
let h := h.get_or_else `this in
|
||
match q₁, q₂ with
|
||
| some e, some p := do
|
||
t ← i_to_expr e,
|
||
v ← i_to_expr ``(%%p : %%t),
|
||
tactic.assertv h t v
|
||
| none, some p := do
|
||
p ← i_to_expr p,
|
||
tactic.note h none p
|
||
| some e, none := i_to_expr e >>= tactic.assert h
|
||
| none, none := do
|
||
u ← mk_meta_univ,
|
||
e ← mk_meta_var (sort u),
|
||
tactic.assert h e
|
||
end >> skip
|
||
|
||
/--
|
||
This tactic applies to any goal.
|
||
- `let h : T := p` adds the hypothesis `h : T := p` to the current goal if `p` a term of type `T`.
|
||
If `T` is omitted, it will be inferred.
|
||
- `let h : T` adds the hypothesis `h : T := ?M` to the current goal and opens a new subgoal `?M : T`.
|
||
The new subgoal becomes the main goal. If `T` is omitted, it will be replaced by a fresh meta variable.
|
||
|
||
If `h` is omitted, it defaults to `this`.
|
||
-/
|
||
meta def «let» (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
|
||
let h := h.get_or_else `this in
|
||
match q₁, q₂ with
|
||
| some e, some p := do
|
||
t ← i_to_expr e,
|
||
v ← i_to_expr ``(%%p : %%t),
|
||
tactic.definev h t v
|
||
| none, some p := do
|
||
p ← i_to_expr p,
|
||
tactic.pose h none p
|
||
| some e, none := i_to_expr e >>= tactic.define h
|
||
| none, none := do
|
||
u ← mk_meta_univ,
|
||
e ← mk_meta_var (sort u),
|
||
tactic.define h e
|
||
end >> skip
|
||
|
||
|
||
/--
|
||
This tactic displays the current state in the tracing buffer.
|
||
-/
|
||
meta def trace_state : tactic unit :=
|
||
tactic.trace_state
|
||
|
||
/--
|
||
`trace a` displays `a` in the tracing buffer.
|
||
-/
|
||
meta def trace {α : Type} [has_to_tactic_format α] (a : α) : tactic unit :=
|
||
tactic.trace a
|
||
|
||
meta def existsi : parse qexpr_list_or_texpr → tactic unit
|
||
| [] := return ()
|
||
| (p::ps) := i_to_expr p >>= tactic.existsi >> existsi ps
|
||
|
||
/--
|
||
This tactic applies to a goal such that its conclusion is an inductive type (say `I`).
|
||
It tries to apply each constructor of `I` until it succeeds.
|
||
-/
|
||
meta def constructor : tactic unit :=
|
||
tactic.constructor
|
||
|
||
/-- Similar to `constructor`, but only non dependent premises are added as new goals. -/
|
||
meta def econstructor : tactic unit :=
|
||
tactic.econstructor
|
||
|
||
meta def left : tactic unit :=
|
||
tactic.left
|
||
|
||
meta def right : tactic unit :=
|
||
tactic.right
|
||
|
||
meta def split : tactic unit :=
|
||
tactic.split
|
||
|
||
meta def exfalso : tactic unit :=
|
||
tactic.exfalso
|
||
|
||
/--
|
||
The injection tactic is based on the fact that constructors of inductive datatypes are injections.
|
||
That means that if `c` is a constructor of an inductive datatype,
|
||
and if `(c t₁)` and `(c t₂)` are two terms that are equal then `t₁` and `t₂` are equal too.
|
||
|
||
If `q` is a proof of a statement of conclusion `t₁ = t₂`,
|
||
then injection applies injectivity to derive the equality of all arguments of `t₁` and `t₂` placed in the same positions.
|
||
For example, from `(a::b) = (c::d)` we derive `a=c` and `b=d`.
|
||
To use this tactic `t₁` and `t₂` should be constructor applications of the same constructor.
|
||
|
||
Given `h : a::b = c::d`, the tactic `injection h` adds to new hypothesis with types `a = c` and `b = d`
|
||
to the main goal. The tactic `injection h with h₁ h₂` uses the names `h₁` an `h₂` to name the new
|
||
hypotheses.
|
||
-/
|
||
meta def injection (q : parse texpr) (hs : parse with_ident_list) : tactic unit :=
|
||
do e ← i_to_expr q, tactic.injection_with e hs, try assumption
|
||
|
||
meta def injections (hs : parse with_ident_list) : tactic unit :=
|
||
do tactic.injections_with hs, try assumption
|
||
|
||
end interactive
|
||
|
||
section mk_simp_set
|
||
open expr
|
||
|
||
private meta def add_simps : simp_lemmas → list name → tactic simp_lemmas
|
||
| s [] := return s
|
||
| s (n::ns) := do s' ← s.add_simp n, add_simps s' ns
|
||
|
||
private meta def report_invalid_simp_lemma {α : Type} (n : name): tactic α :=
|
||
fail ("invalid simplification lemma '" ++ to_string n ++ "' (use command 'set_option trace.simp_lemmas true' for more details)")
|
||
|
||
private meta def simp_lemmas.resolve_and_add (s : simp_lemmas) (n : name) (ref : pexpr) : tactic simp_lemmas :=
|
||
do
|
||
p ← resolve_name n,
|
||
-- unpack local refs
|
||
let e := p.erase_annotations.get_app_fn.erase_annotations,
|
||
match e with
|
||
| const n _ :=
|
||
(do b ← is_valid_simp_lemma_cnst reducible n, guard b, save_const_type_info n ref, s.add_simp n)
|
||
<|>
|
||
(do eqns ← get_eqn_lemmas_for tt n, guard (eqns.length > 0), save_const_type_info n ref, add_simps s eqns)
|
||
<|>
|
||
report_invalid_simp_lemma n
|
||
| _ :=
|
||
(do e ← i_to_expr_no_subgoals p, b ← is_valid_simp_lemma reducible e, guard b, try (save_type_info e ref), s.add e)
|
||
<|>
|
||
report_invalid_simp_lemma n
|
||
end
|
||
|
||
private meta def simp_lemmas.add_pexpr (s : simp_lemmas) (p : pexpr) : tactic simp_lemmas :=
|
||
match p with
|
||
| (const c []) := simp_lemmas.resolve_and_add s c p
|
||
| (local_const c _ _ _) := simp_lemmas.resolve_and_add s c p
|
||
| _ := do new_e ← i_to_expr_no_subgoals p, s.add new_e
|
||
end
|
||
|
||
private meta def simp_lemmas.append_pexprs : simp_lemmas → list pexpr → tactic simp_lemmas
|
||
| s [] := return s
|
||
| s (l::ls) := do new_s ← simp_lemmas.add_pexpr s l, simp_lemmas.append_pexprs new_s ls
|
||
|
||
meta def mk_simp_set (no_dflt : bool) (attr_names : list name) (hs : list pexpr) (ex : list name) : tactic simp_lemmas :=
|
||
do s₀ ← join_user_simp_lemmas no_dflt attr_names,
|
||
s₁ ← simp_lemmas.append_pexprs s₀ hs,
|
||
-- add equational lemmas, if any
|
||
ex ← ex.mfor (λ n, list.cons n <$> get_eqn_lemmas_for tt n),
|
||
return $ simp_lemmas.erase s₁ $ ex.join
|
||
|
||
end mk_simp_set
|
||
|
||
namespace interactive
|
||
open interactive interactive.types expr
|
||
|
||
private meta def simp_goal (cfg : simp_config) : simp_lemmas → tactic unit
|
||
| s := do
|
||
(new_target, pr) ← target >>= simplify_core cfg s `eq,
|
||
replace_target new_target pr
|
||
|
||
private meta def simp_hyp (cfg : simp_config) (s : simp_lemmas) (h_name : name) : tactic unit :=
|
||
do h ← get_local h_name,
|
||
h_type ← infer_type h,
|
||
(h_new_type, pr) ← simplify_core cfg s `eq h_type,
|
||
replace_hyp h h_new_type pr,
|
||
return ()
|
||
|
||
private meta def simp_hyps (cfg : simp_config) : simp_lemmas → list name → tactic unit
|
||
| s [] := skip
|
||
| s (h::hs) := simp_hyp cfg s h >> simp_hyps s hs
|
||
|
||
private meta def simp_core (cfg : simp_config) (no_dflt : bool) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (locat : loc) : tactic unit :=
|
||
do s ← mk_simp_set no_dflt attr_names hs ids,
|
||
s ← s.append ctx,
|
||
match locat : _ → tactic unit with
|
||
| loc.wildcard :=
|
||
do ls ← local_context,
|
||
let loc_names := ls.map expr.local_pp_name,
|
||
revert_lst ls,
|
||
simp_intro_aux cfg ff s ff loc_names,
|
||
return ()
|
||
| (loc.ns []) := simp_goal cfg s
|
||
| (loc.ns hs) := simp_hyps cfg s hs
|
||
end,
|
||
try tactic.triv, try (tactic.reflexivity reducible)
|
||
|
||
/--
|
||
This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.
|
||
It has many variants.
|
||
|
||
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
|
||
|
||
- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.
|
||
The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.
|
||
This is a convenient way to "unfold" `f`.
|
||
|
||
- `simp only [h_1, ..., h_n]` is like `simp [h_1, ..., h_n]` but does not use `[simp]` lemmas
|
||
|
||
- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,
|
||
but removes the ones named `id_i`s.
|
||
|
||
- `simp at h_1 ... h_n` simplifies the non dependent hypotheses `h_1 : T_1` ... `h_n : T : n`. The tactic fails if the target or another hypothesis depends on one of them.
|
||
|
||
- `simp at *` simplifies all the hypotheses and the goal.
|
||
|
||
- `simp with attr_1 ... attr_n` simplifies the main goal target using the lemmas tagged with any of the attributes `[attr_1]`, ..., `[attr_n]` or `[simp]`.
|
||
-/
|
||
meta def simp (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (locat : parse location)
|
||
(cfg : simp_config := {}) : tactic unit :=
|
||
simp_core cfg no_dflt [] hs attr_names ids locat
|
||
|
||
/-- Simplify the whole context, and use simplified hypotheses to simplify other hypotheses. -/
|
||
meta def simp_all (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
|
||
(ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit :=
|
||
do s ← mk_simp_set no_dflt attr_names hs ids,
|
||
ls ← local_context,
|
||
revert_lst ls,
|
||
let ns := ls.map expr.local_pp_name,
|
||
simp_intro_aux cfg tt s ff ns,
|
||
try tactic.triv, try (tactic.reflexivity reducible)
|
||
|
||
/--
|
||
Similar to the `simp` tactic, but adds all applicable hypotheses as simplification rules.
|
||
-/
|
||
meta def simp_using_hs (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list)
|
||
(cfg : simp_config := {}) : tactic unit :=
|
||
do ctx ← collect_ctx_simps,
|
||
simp_core cfg no_dflt ctx hs attr_names ids (loc.ns [])
|
||
|
||
meta def simph (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list)
|
||
(cfg : simp_config := {}) : tactic unit :=
|
||
simp_using_hs no_dflt hs attr_names ids cfg
|
||
|
||
meta def simp_intros (ids : parse ident_*) (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
|
||
(wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit :=
|
||
do s ← mk_simp_set no_dflt attr_names hs wo_ids,
|
||
match ids with
|
||
| [] := simp_intros_using s cfg
|
||
| ns := simp_intro_lst_using ns s cfg
|
||
end,
|
||
try triv >> try (reflexivity reducible)
|
||
|
||
meta def simph_intros (ids : parse ident_*) (no_dflt : parse only_flag) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
|
||
(wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit :=
|
||
do s ← mk_simp_set no_dflt attr_names hs wo_ids,
|
||
match ids with
|
||
| [] := simph_intros_using s cfg
|
||
| ns := simph_intro_lst_using ns s cfg
|
||
end,
|
||
try triv >> try (reflexivity reducible)
|
||
|
||
private meta def dsimp_hyps (s : simp_lemmas) (hs : list name) : tactic unit :=
|
||
hs.mfor' (λ h, get_local h >>= dsimp_at_core s)
|
||
|
||
meta def dsimp (no_dflt : parse only_flag) (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : parse location → tactic unit
|
||
| (loc.ns []) := do s ← mk_simp_set no_dflt attr_names es ids, tactic.dsimp_core s
|
||
| (loc.ns hs) := do s ← mk_simp_set no_dflt attr_names es ids, dsimp_hyps s hs
|
||
| (loc.wildcard) := do ls ← local_context,
|
||
n ← revert_lst ls,
|
||
s ← mk_simp_set no_dflt attr_names es ids,
|
||
tactic.dsimp_core s,
|
||
intron n
|
||
|
||
/--
|
||
This tactic applies to a goal that has the form `t ~ u` where `~` is a reflexive relation.
|
||
That is, a relation which has a reflexivity lemma tagged with the attribute `[refl]`.
|
||
The tactic checks whether `t` and `u` are definitionally equal and then solves the goal.
|
||
-/
|
||
meta def reflexivity : tactic unit :=
|
||
tactic.reflexivity
|
||
|
||
/--
|
||
Shorter name for the tactic `reflexivity`.
|
||
-/
|
||
meta def refl : tactic unit :=
|
||
tactic.reflexivity
|
||
|
||
meta def symmetry : tactic unit :=
|
||
tactic.symmetry
|
||
|
||
meta def transitivity (q : parse texpr?) : tactic unit :=
|
||
tactic.transitivity >> match q with
|
||
| none := skip
|
||
| some q :=
|
||
do (r, lhs, rhs) ← target_lhs_rhs,
|
||
i_to_expr q >>= unify rhs
|
||
end
|
||
|
||
meta def ac_reflexivity : tactic unit :=
|
||
tactic.ac_refl
|
||
|
||
meta def ac_refl : tactic unit :=
|
||
tactic.ac_refl
|
||
|
||
meta def cc : tactic unit :=
|
||
tactic.cc
|
||
|
||
meta def subst (q : parse texpr) : tactic unit :=
|
||
i_to_expr q >>= tactic.subst >> try (tactic.reflexivity reducible)
|
||
|
||
meta def clear : parse ident* → tactic unit :=
|
||
tactic.clear_lst
|
||
|
||
private meta def to_qualified_name_core : name → list name → tactic name
|
||
| n [] := fail $ "unknown declaration '" ++ to_string n ++ "'"
|
||
| n (ns::nss) := do
|
||
curr ← return $ ns ++ n,
|
||
env ← get_env,
|
||
if env.contains curr then return curr
|
||
else to_qualified_name_core n nss
|
||
|
||
private meta def to_qualified_name (n : name) : tactic name :=
|
||
do env ← get_env,
|
||
if env.contains n then return n
|
||
else do
|
||
ns ← open_namespaces,
|
||
to_qualified_name_core n ns
|
||
|
||
private meta def to_qualified_names : list name → tactic (list name)
|
||
| [] := return []
|
||
| (c::cs) := do new_c ← to_qualified_name c, new_cs ← to_qualified_names cs, return (new_c::new_cs)
|
||
|
||
private meta def dunfold_hyps : list name → list name → tactic unit
|
||
| cs [] := skip
|
||
| cs (h::hs) := get_local h >>= dunfold_at cs >> dunfold_hyps cs hs
|
||
|
||
meta def dunfold : parse ident* → parse location → tactic unit
|
||
| cs (loc.ns []) := do new_cs ← to_qualified_names cs, tactic.dunfold new_cs
|
||
| cs (loc.ns hs) := do new_cs ← to_qualified_names cs, dunfold_hyps new_cs hs
|
||
| cs (loc.wildcard) := do ls ← tactic.local_context,
|
||
n ← revert_lst ls,
|
||
new_cs ← to_qualified_names cs,
|
||
tactic.dunfold new_cs,
|
||
intron n
|
||
|
||
/- TODO(Leo): add support for non-refl lemmas -/
|
||
meta def unfold : parse ident* → parse location → tactic unit :=
|
||
dunfold
|
||
|
||
private meta def dunfold_hyps_occs : name → occurrences → list name → tactic unit
|
||
| c occs [] := skip
|
||
| c occs (h::hs) := get_local h >>= dunfold_core_at occs [c] >> dunfold_hyps_occs c occs hs
|
||
|
||
meta def dunfold_occs : parse ident → parse location → list nat → tactic unit
|
||
| c (loc.ns []) ps := do new_c ← to_qualified_name c, tactic.dunfold_occs_of ps new_c
|
||
| c (loc.ns hs) ps := do new_c ← to_qualified_name c, dunfold_hyps_occs new_c (occurrences.pos ps) hs
|
||
| c (loc.wildcard) ps := fail "wildcard not allowed when unfolding occurences"
|
||
|
||
/- TODO(Leo): add support for non-refl lemmas -/
|
||
meta def unfold_occs : parse ident → parse location → list nat → tactic unit :=
|
||
dunfold_occs
|
||
|
||
private meta def delta_hyps : list name → list name → tactic unit
|
||
| cs [] := skip
|
||
| cs (h::hs) := get_local h >>= delta_at cs >> dunfold_hyps cs hs
|
||
|
||
meta def delta : parse ident* → parse location → tactic unit
|
||
| cs (loc.ns []) := do new_cs ← to_qualified_names cs, tactic.delta new_cs
|
||
| cs (loc.ns hs) := do new_cs ← to_qualified_names cs, delta_hyps new_cs hs
|
||
| cs (loc.wildcard) := do ls ← tactic.local_context,
|
||
n ← revert_lst ls,
|
||
new_cs ← to_qualified_names cs,
|
||
tactic.delta new_cs,
|
||
intron n
|
||
|
||
private meta def unfold_projections_hyps : list name → tactic unit
|
||
| [] := skip
|
||
| (h::hs) := get_local h >>= unfold_projections_at >> unfold_projections_hyps hs
|
||
|
||
/--
|
||
This tactic unfolds all structure projections.
|
||
-/
|
||
meta def unfold_projections : parse location → tactic unit
|
||
| (loc.ns []) := tactic.unfold_projections
|
||
| (loc.ns hs) := unfold_projections_hyps hs
|
||
| (loc.wildcard) := do ls ← local_context, unfold_projections_hyps (ls.map expr.local_pp_name)
|
||
|
||
meta def apply_opt_param : tactic unit :=
|
||
tactic.apply_opt_param
|
||
|
||
meta def apply_auto_param : tactic unit :=
|
||
tactic.apply_auto_param
|
||
|
||
meta def fail_if_success (tac : itactic) : tactic unit :=
|
||
tactic.fail_if_success tac
|
||
|
||
meta def success_if_fail (tac : itactic) : tactic unit :=
|
||
tactic.success_if_fail tac
|
||
|
||
meta def guard_expr_eq (t : expr) (p : parse $ tk ":=" *> texpr) : tactic unit :=
|
||
do e ← to_expr p, guard (alpha_eqv t e)
|
||
|
||
meta def guard_target (p : parse texpr) : tactic unit :=
|
||
do t ← target, guard_expr_eq t p
|
||
|
||
meta def by_cases (q : parse texpr) (n : parse (tk "with" *> ident)?): tactic unit :=
|
||
do p ← tactic.to_expr_strict q,
|
||
tactic.by_cases p (n.get_or_else `h)
|
||
|
||
meta def by_contradiction : tactic unit :=
|
||
tactic.by_contradiction >> return ()
|
||
|
||
meta def by_contra : tactic unit :=
|
||
tactic.by_contradiction >> return ()
|
||
|
||
/-- Type check the given expression, and trace its type. -/
|
||
meta def type_check (p : parse texpr) : tactic unit :=
|
||
do e ← to_expr p, tactic.type_check e, infer_type e >>= trace
|
||
|
||
/-- Fail if there are unsolved goals. -/
|
||
meta def done : tactic unit :=
|
||
tactic.done
|
||
|
||
private meta def show_aux (p : pexpr) : list expr → list expr → tactic unit
|
||
| [] r := fail "show tactic failed"
|
||
| (g::gs) r := do
|
||
do {set_goals [g], g_ty ← target, ty ← i_to_expr p, unify g_ty ty, set_goals (g :: r.reverse ++ gs), tactic.change ty}
|
||
<|>
|
||
show_aux gs (g::r)
|
||
|
||
meta def «show» (q : parse texpr) : tactic unit :=
|
||
do gs ← get_goals,
|
||
show_aux q gs []
|
||
|
||
end interactive
|
||
end tactic
|
||
|
||
section add_interactive
|
||
open tactic
|
||
|
||
/- See add_interactive -/
|
||
private meta def add_interactive_aux (new_namespace : name) : list name → command
|
||
| [] := return ()
|
||
| (n::ns) := do
|
||
env ← get_env,
|
||
d_name ← resolve_constant n,
|
||
(declaration.defn _ ls ty val hints trusted) ← env.get d_name,
|
||
(name.mk_string h _) ← return d_name,
|
||
let new_name := `tactic.interactive <.> h,
|
||
add_decl (declaration.defn new_name ls ty (expr.const d_name (ls.map level.param)) hints trusted),
|
||
add_interactive_aux ns
|
||
|
||
/--
|
||
Copy a list of meta definitions in the current namespace to
|
||
tactic.interactive.
|
||
|
||
This command is useful when we want to update tactic.interactive
|
||
without closing the current namespace.
|
||
-/
|
||
meta def add_interactive (ns : list name) (p : name := `tactic.interactive) : command :=
|
||
add_interactive_aux p ns
|
||
|
||
end add_interactive
|