Tactic backtracking

Stream: lean4

[Paolo G. Giarrusso]

Hi all! Lean4 newbie and Coq expert here. I'm wondering if Lean4 plans to support real logic-programming-style backtracking across tactics, to fix the 2nd/3rd example (like in Coq >= 8.4):

example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) := by repeat constructor <;> assumption -- works
example (p q r : Prop) (hp : p) : (q ∨ p ∨ r) := by repeat constructor <;> assumption -- fails
example (p q r : Prop) (hp : p) : (q ∨ p ∨ r) := by
  repeat (mplus | apply Or.inl | apply Or.inr) <;> assumption -- pseudocode

I'm aware of MonadBacktrack and TC search, but I'm not sure either's an answer — and while in mathlib this might not matter, it seems useful enough in syntactic proofs that are useful in proof theory / programming languages / (metatheory of) program verification

[Paolo G. Giarrusso]

I also appreciate that sort-of backtracking is exponential, but that doesn't always make it "too" slow

[Paolo G. Giarrusso]

(what's "too slow" varies, but in practice I'm bothered by tactics taking more than >= 0.1s)

[Mario Carneiro]

mplus is spelled first btw

[Paolo G. Giarrusso]

not quite, first isn't a sufficient mplus:

example (p q r : Prop) (hp : p) : (q ∨ p ∨ r) := by
  repeat (first | apply Or.inl | apply Or.inr) <;> assumption -- fails

[Mario Carneiro]

Can you describe in words how you want the search to proceed?

[Mario Carneiro]

it's not immediately obvious to me what semantics you want from that syntax

[Mario Carneiro]

One way to do a recursive backtracking search here is with a recursive macro:

syntax "stuff" : tactic
macro_rules
  | `(tactic| stuff) => `(tactic| first | assumption | apply Or.inl; stuff | apply Or.inr; stuff)
example (p q r : Prop) (hp : p) : (q ∨ p ∨ r) := by stuff

[Mario Carneiro]

I think there is a way to do this with one of the repeat combinators but I haven't thought too hard about it

[Mario Carneiro]

you can also use a multiply-defined macro to similar effect:

syntax "stuff" : tactic
macro_rules | `(tactic| stuff) => `(tactic| assumption)
macro_rules | `(tactic| stuff) => `(tactic| (apply Or.inl; stuff))
macro_rules | `(tactic| stuff) => `(tactic| (apply Or.inr; stuff))
example (p q r : Prop) (hp : p) : (q ∨ p ∨ r) := by stuff

[Mario Carneiro]

There is certainly no difficulty in defining a combinator that has backtracking behavior, but <;> and repeat do not backtrack

[Paolo G. Giarrusso]

applying mplus (a; b) <;> c on a goal would attempt a, then attempt c, and if that fails backtrack to try b then c.

[Paolo G. Giarrusso]

If there is no difficulty, can you define mplus? Your examples encode the specific example, but I'm not sure they generalize

[Paolo G. Giarrusso]

I guess it's possible to define LogicTacticM by stacking an actual logic monad with backtracking on top of TacticM, lifting all tactics to LogicTacticM, and adapting tactics to be multi-success where appropriate, but that seems invasive.

[Mario Carneiro]

This does what your description says, but it doesn't seem to be correct, since there is no recursion involved

syntax "mplus " withPosition((colGe "|" tacticSeq)+)
  " => " tacticSeq : tactic

macro_rules
  | `(tactic| mplus $[| $tac]* => $after) => do
    let tac ← tac.mapM fun t => `(tactic| (($t); ($after)))
    `(tactic| first $[| $tac:tactic]*)

example (p q r : Prop) (hp : p) : (q ∨ p ∨ r) := by
  mplus | apply Or.inl | apply Or.inr => assumption

[Paolo G. Giarrusso]

while your workaround lets me define a new tactic for any fixed mplus (a; b) <;> c, but I don't see how to write a first-class mplus (a; b) — the correct denotational semantics supports returning multiple successes.

[Mario Carneiro]

Note that we have to take over the <;> tactic here, since as I said that tactic doesn't backtrack and the way you have nested things makes it impossible for <;> to do its work after mplus is done

[Mario Carneiro]

You could have a special backtrackingTactic syntax class and define all these combinators, but as you say that would be invasive. Do you have an example that can't be trivially rewritten so that the repetition can't be lifted to an explicit tactic combinator call?

[Mario Carneiro]

That is, this is easy if you allow putting mplus as the root combinator and nesting <;> c inside it, the problem is only with having mplus passing multiple results and having everything after it get transparently run multiple times. This was an explicit design decision of the tactic language; we were aware of this behavior in Isabelle and Coq and chose not to replicate it because it leads to more difficult to understand control flow

[Paolo G. Giarrusso]

are you asking for evidence that (pure) Prolog doesn't trivially translate to functional programming? I'll admit I don't have a compelling one ready, mostly because I'd have to reverse-engineer old proofs

[Mario Carneiro]

I think the general version I posted above is equivalent in power to your mplus (a; b), you just have to pass the rest of the block (the scope of stuff that should be run multiple times) in the =>, CPS style

[Paolo G. Giarrusso]

ah, that could work

[Paolo G. Giarrusso]

yeah, I buy that CPS is systematically sufficient. I'd have to reimplement needed tactics (here, constructor and repeat), but it should be doable as needed.

[Mario Carneiro]

do I understand correctly that constructor nondeterministically picks a constructor to apply and repeat nondeterministically decides how many times to iterate?

[Mario Carneiro]

I'm not sure exactly how repeat interacts with the nondeterminism here

[Paolo G. Giarrusso]

I expect Coq's repeat is greedy, but constructor is multi-success

[Mario Carneiro]

but if you want to make a language out of this I think you could generalize the mplus combinator above to

syntax "nondet" nondetTactic " => " tacticSeq : tactic
syntax "constructor" : nondetTactic
syntax  "any" withPosition((colGe "|" tacticSeq)+) : nondetTactic
-- etc

[Paolo G. Giarrusso]

thank you; I'll need a bunch of reading to follow that, but this is good enough for now

[Paolo G. Giarrusso]

I guess the reading will need "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages" and/or https://leanprover.github.io/lean4/doc/macro_overview.html.

I hope I won't need the videos in https://leanprover.github.io/lean4/doc/elaborators.html...

[Sebastian Ullrich]

Hey Paolo! You might also find the community-authored https://github.com/arthurpaulino/lean4-metaprogramming-book/ useful