lean4-metaprogramming-book
lean4-metaprogramming-book copied to clipboard
`and_then` is subtly different from `<;>`. The former focuses the goal, whereas the latter does not.
Page 60 suggests that a and_then b
behaves the same as a <;> b
, but this is not the case when b
does not close all goals;
For example, if the second tactic is skip. The <;>
version compiles just fine.
example {x : Nat} : True :=
by
cases x <;> skip
repeat exact True.intro
But, the and_then
version complains about unsolved goals.
macro a:tactic " and_then " b:tactic : tactic =>
`(tactic| $a:tactic; all_goals $b:tactic)
example {x : Nat} : true :=
by
cases x and_then skip -- Error: unsolved goals ...
repeat exact True.intro
I don't readily see how to fix this while keeping it as a simple substitution-macro, but maybe this discrepancy should be pointed out in the text.
The problem was that { $a:tactic; all_goals $b:tactic }
, with curly braces, was explicitly requiring it to close the goals. Removing them solved the problem.
We still want to focus the main goal, before applying a
, so that b
only works on those goals introduced by a
.
example {x y : Nat} : y = 0 ∨ y ≠ 0 :=
by
cases y;
cases x and_then {
apply Or.inl;
rfl
}
apply Or.inr
simp
Turns out focus
does exactly that, so the macro should be
macro a:tactic " and_then " b:tactic : tactic =>
`(tactic|
focus
$a:tactic; all_goals $b:tactic
)
I'd make a PR, but that seems a bit overkill for a change this tiny?
@alexkeizer the PR is highly welcome if you explain the change in the text. We're in the tactics chapter afterall 👍🏼