prolog-like search?

Stream: new members

[Ranjit Jhala]

Hi folks, can anyone tell me if there is some standard/existing tactic for prolog-like proof search in lean4. As a concrete example, suppose I give you definitions like

inductive peano where
  | Z : peano
  | S : peano -> peano

open peano

inductive even : peano -> Prop where
  | evenZ : even Z
  | evenSS {n} : even n -> even (S (S n))

open even

now suppose I want to prove that

theorem even_4 : even (S (S (S (S Z)))) := by
  prolog_like_search

is there some prolog_like_search tactic I can use that would generate the proof term? By "prolog-like-search" I mean if you write the above in Prolog as (something like)

even(Z).
even(S(S(n))) :- even(n).

and then ask query

even(S(S(S(S(Z))))

I think prolog will say "yes" or such... (having implicitly "synthesized" the proof from the rules/definition of even).

Any pointers will be greatly appreciated!

[Kyle Miller]

Yeah, simp is basically that:

theorem even_4 : even (S (S (S (S Z)))) := by
  simp [evenZ, evenSS]

[Kyle Miller]

You likely need to increase the "maximum discharge depth". By default it's 2, and that's just enough for this example.

simp (config := {maxDischargeDepth := 2}) [evenZ, evenSS]

[Kyle Miller]

Another is the apply_rules tactic, which searches for some sequence of applys that work, which is closer to Prolog:

theorem even_4 : even (S (S (S (S Z)))) := by
  apply_rules [evenZ, evenSS]

[Kyle Miller]

I take that back, it should be solve_by_elim, not apply_rules. The apply_rules tactic doesn't do backtracking.

[Ranjit Jhala]

Thanks very much, I didn't know about apply_rules or solve_by_elim! (Elsewhere someone also pointed me to this aesop system which seems very relevant: https://github.com/leanprover-community/aesop)