a cheat-sheet tactic

Stream: new members

[Kevin Lacker]

I was trying to write a simple tactic, to automatically apply the instructions in the "cheat sheet" - https://leanprover-community.github.io//img/lean-tactics.pdf - and running into some parts I couldn't figure out. So far I have a tactic that applies intro1 as much as possible and a couple other bits:

namespace tactic
namespace interactive

meta def cheat_once : tactic unit :=
do t ← target,
(intro1 >> skip) <|> assumption <|> contradiction <|> fail "no cheat-sheet tactic matches"

meta def cheat : tactic unit :=
do cheat_once,
(cheat <|> skip)

end interactive
end tactic

I am working on the next step, to run cases on any of the hypotheses that are ∃ ∨ ∧ expressions. My instinct was, ok I should loop over all the hypotheses, check if they are ∃ ∨ ∧ expressions, and if so then apply cases to that hypothesis. So, questions:

• Is this a reasonable strategy?

• Is looping over all the hypotheses something best done by inspecting the local_context? There are a bunch of undocumented functions in https://leanprover-community.github.io/mathlib_docs/core/init/meta/local_context.html#local_context and I suspect I should use one of them but a pointer would be helpful.

• I can imagine checking if something's a ∃ ∨ ∧ expression by constructing an example one and then seeing if it unifies against the hypothesis. That seems really roundabout, though - I feel like I want to be writing something like if expr.root_operation == ∃`. What's a nice way to do this?

[Scott Morrison]

Have a look at the auto_cases tactic, which does something similar to what you're looking for.

[Kevin Lacker]

ok, very informative tactic. so basically yes local_context is the way to go, no don't use any methods just use it straight, and "unification" isn't really the way to think about it but rather to use the language's built-in matching stuff.

[Kevin Lacker]

so when it looks through local_context, a bunch of those things are just variables like x and y or whatever. but I only want to be looking for hypotheses. I guess to Lean those things are basically the same, they are both local constants, even though some of them are hypotheses and some of them are unbound variables (or is that the right term?) ? should I just be ignoring this distinction because the matching stuff will filter that out anyway?

[Kevin Lacker]

OK cool, i got it working like this:

meta def can_cases : expr → tactic unit
| `(Exists _) := skip
| `(and _ _)  := skip
| `(or _ _)   := skip
| _           := fail "cannot cases this expr"

meta def cases_or_fail (hyp : expr) : tactic unit :=
do t ← infer_type hyp,
can_cases t,
tactic.cases hyp >> skip

-- Run cases on the first thing possible
meta def cases_first : list expr → tactic unit
| (E :: Es) := cases_or_fail E <|> cases_first Es
| []        := fail "cases doesn't apply to anything in the local context"

meta def cases_once : tactic unit :=
do lc ← local_context,
cases_first lc

[Mario Carneiro]

Kevin Lacker said:

so when it looks through local_context, a bunch of those things are just variables like x and y or whatever. but I only want to be looking for hypotheses. I guess to Lean those things are basically the same, they are both local constants, even though some of them are hypotheses and some of them are unbound variables (or is that the right term?) ? should I just be ignoring this distinction because the matching stuff will filter that out anyway?

local_context returns a list of local constants, so they should all just be variables like x, y, h. DTT doesn't distinguish between hypotheses and variables of other types, it's all just variables whose types may depend on other (earlier) variables. So you usually want to use t <- infer_type h to get the type of the variables in the context, and then by looking at that you can figure out more information about what kind of thing it is. Specifically, if you want to know whether it is a hypothesis or a variable of some other kind, you should check if infer_type t returns Prop (which is what is_prop t does), or equivalently use is_proof h, which just calls t <- infer_type h, is_prop t.

[Kevin Lacker]

okay that makes sense. infer_type is defined in the c++ kernel I guess, that is why there's no real code at https://github.com/leanprover-community/lean/blob/cc72964/library/init/meta/tactic.lean#L418 ?

[Reid Barton]

Right, all the meta constants in this and similar files have an implementation magically provided by the C++ code