How to explore all branches using repeat or otherwise

Stream: new members

[Lars Ericson]

I am doing an exercise in the Theorem Proving in Lean 4 book, to get a one-line version of a proof. First I supply a multi-line proof:

example (p q r : Prop) (hp : p)
        : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := by
  apply And.intro
  apply Or.inl
  exact hp
  apply And.intro
  apply Or.inr
  apply Or.inl
  exact hp
  apply Or.inr
  apply Or.inr

The obvious one-liner doesn't work:

example (p q r : Prop) (hp : p)
        : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := by
  repeat (any_goals (first | apply And.intro | apply Or.inl | apply Or.inr | exact hp))

It leaves me in this state:

pqr: Prop
hp: p
⊢ q
pqr: Prop
hp: p
⊢ q

It can get here because many combinations of the list of tactics in the first can lead to ⊢ q or ⊢ r but fewer branches lead to ⊢ p.

How would I change the above so that it would recursively explore every non-failing sequence of applications of the list of tactics in the first until it found a sequence that worked or exhausted all sequences?

[Richard Copley]

You won't find many examples of people trying to build algorithms out of tactic combinators. Is that your real aim, or would any kind of one-liner satisfy you? Here's one:

import Mathlib.Tactic.Tauto
example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) :=
  by tauto

If the exercise asks for a one-line proof, chances are it means you to translate your proof into term mode. I've done that in two stylistic variations, with no clever tricks, in the spoiler tag.

example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) :=
  And.intro (Or.inl hp) (And.intro (Or.inr (Or.inl hp)) (Or.inr (Or.inr hp)))

example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) :=
  ⟨.inl hp, .inr <| .inl hp, .inr <| .inr hp⟩

[Lars Ericson]

@Richard Copley and @Martin Dvořák, term proofs were the topic of the previous chapters. The tactics chapter is about tactic proofs and introduces repeat in the Tactics Combinator section and after that rewriting, extending simp and split. The exercise starts with "Use tactic combinators". Your Spoiler proofs do not address the "use tactic combinator" requirement. That is why I am fussing with repeat. I need a combinator or two, but not too many to fit in one line. tauto feels like dodging the pedagogical intent, in the context of the chapter.

[Matt Diamond]

@Lars Ericson interesting exercise! here's a solution I found:

example (p q r : Prop) (hp : p)
        : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := by
  repeat (first | apply And.intro | apply Or.inl; exact hp | apply Or.inr | exact hp)

[Matt Diamond]

the key is to write the combinator so that applying Or.inl is considered a failure if we're not able to close the goal with hp immediately afterward

[Matt Diamond]

(also I removed your use of any_goals because it didn't seem necessary)

[Matt Diamond]

it seems like a good rule of thumb when using repeat and first is to ask, for each branch, "would this ever cause a problem if it succeeded? if so, how can I make it more specific so that it fails in those cases?"

[Lars Ericson]

Thanks! Is there a less insightful way to write this with my initial list of tactics so that Lean does a brute force depth first search of the possible combinations in the list, backing up when it reaches a non-empty goal state for which no tactic in the list applies? I understand this search could be intractable. I am just curious if it is possible to express it.

[Kyle Miller]

I'm not sure there's a way to do this without making a recursive tactic macro.

syntax "my_tauto" : tactic

macro_rules
  | `(tactic| my_tauto) =>
    `(tactic|
        first
        | done
        | assumption
        | apply Or.inl <;> my_tauto
        | apply Or.inr <;> my_tauto
        | apply And.intro <;> my_tauto)


example (p q r : Prop) (hp : p)
        : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := by
  my_tauto

[Lars Ericson]

@Kyle Miller that's great, the last sections on defining new tactics scared me a little. This gives me a good guide. I had kind of assumed that there would be a recursive search macro already designed in Lean since it seems like it would be a core idea. I'm glad to see how to do it. For the exact problem in the text @Matt Diamond 's answer seems closest to the intent of the problem.

[Lars Ericson]

I.e. instead of first a macro called recursive_repeat_first, like your my_tauto but taking a list of tactics as an argument like first.