Is there a Prolog-like tactic?

Stream: Is there code for X?

[Mr Proof]

Consider the prolog example from Wikipedia:

mother_child(trude, sally).

father_child(tom, sally).
father_child(tom, erica).
father_child(mike, tom).

sibling(X, Y)      :- parent_child(Z, X), parent_child(Z, Y), not(X = Y).

parent_child(X, Y) :- father_child(X, Y).
parent_child(X, Y) :- mother_child(X, Y).

Now, in Prolog one would write:

?- siblings(A, B).

And it would give examples of pairs of siblings.

It is possible to encode the above as Prop statements in Lean. In Lean the equivalent to get the answer would be instead constructing a proof of the existence of a pair:

theorem T1: ∃ x, y: Siblings(x,y) := by....

Now if all the previous propositions are "Horn Clauses", then this is fully provable using a Prolog style search. e.g. if there was a tactic called prolog:

theorem T1: ∃ x, y: Siblings(x,y) := by prolog

And then providing that works:

#print T1

Should be able to reveal which values it chose as witnesses for x and y.

So, in short, is there a prolog-like tactic that can do all this automatically? (I have played around with Prolog interpreters in C# and it can be done in around 200 lines - probably much shorter). Though not sure how fast it would be with Mathlib. (It would only have to look at horne clauses and ignore the rest).

If anyone is able to convert the Wikipedia example into lean and show a tactic automatically finding a pair of siblings that would be nice. Also, it would just be nice to be able to use Lean as an alternative to Prolog.

[Yury G. Kudryashov]

How do you want to encode the inputs? GIve an #mwe, please.

[Mr Proof]

I suppose like this?

-- Define the type of people
inductive Person
| Alice | Bob | Carol | Dan | Eve | Frank
deriving Repr, DecidableEq

open Person

-- Define relations
variable (Parent : Person → Person → Prop)
variable (Siblings : Person → Person → Prop)

-- Horn-clause style axiom:
axiom siblings_from_parent :
  ∀ (p a b : Person), Parent p a → Parent p b → Siblings a b

-- Some facts
axiom parent_alice_bob : Parent Alice Bob
axiom parent_alice_carol : Parent Alice Carol
axiom parent_dan_eve : Parent Dan Eve
axiom parent_dan_frank : Parent Dan Frank

theorem T1 : ∃ x y, Siblings x y := by
  [[[[Would be nice to have a prolog-like single tactic to solve this]]]

#print T1

[Yury G. Kudryashov]

Your axioms imply False, because they generalize over Parent and Siblings.

[Mr Proof]

OK How about this (although it's not really the point of the question):

-- Define the type of people
inductive Person
| Alice | Bob | Carol | Dan | Eve | Frank
deriving Repr, DecidableEq

open Person

-- Parent relation
axiom Parent : Person → Person → Prop

-- Define siblings (same parent, distinct people)
def Siblings (a b : Person) : Prop :=
  ∃ p, Parent p a ∧ Parent p b ∧ a ≠ b

-- Facts
axiom parent_alice_bob   : Parent Alice Bob
axiom parent_alice_carol : Parent Alice Carol
axiom parent_dan_eve     : Parent Dan Eve
axiom parent_dan_frank  : Parent Dan Frank

-- Existence of siblings
theorem T1 : ∃ x y, Siblings x y := by
  ?????

#print T1

I take it there is no prolog-style tactic as yet. When I got time I guess I could try making one.

[Eric Wieser]

@Kim Morrison, I assume grind can't be told to try instantiating data constructors?

[Eric Wieser]

This works with aesop

import Aesop

-- Define the type of people
inductive Person
| Alice | Bob | Carol | Dan | Eve | Frank
deriving Repr, DecidableEq

open Person

-- Parent relation
axiom Parent : Person → Person → Prop

-- Define siblings (same parent, distinct people)
@[simp]
def Siblings (a b : Person) : Prop :=
  ∃ p, Parent p a ∧ Parent p b ∧ a ≠ b

-- Facts
@[simp] axiom parent_alice_bob   : Parent Alice Bob
@[simp] axiom parent_alice_carol : Parent Alice Carol
@[simp] axiom parent_dan_eve     : Parent Dan Eve
@[simp] axiom parent_dan_frank  : Parent Dan Frank

open Lean Elab Tactic

@[aesop tactic unsafe]
def aesopExistsIntroA : TacticM Unit := do evalTactic <| ← `(tactic|refine Exists.intro Alice ?_)
@[aesop tactic unsafe]
def aesopExistsIntroB : TacticM Unit := do evalTactic <| ← `(tactic|refine Exists.intro Bob ?_)
@[aesop tactic unsafe]
def aesopExistsIntroC : TacticM Unit := do evalTactic <| ← `(tactic|refine Exists.intro Carol ?_)
@[aesop tactic unsafe]
def aesopExistsIntroD : TacticM Unit := do evalTactic <| ← `(tactic|refine Exists.intro Dan ?_)
@[aesop tactic unsafe]
def aesopExistsIntroE : TacticM Unit := do evalTactic <| ← `(tactic|refine Exists.intro Eve ?_)
@[aesop tactic unsafe]
def aesopExistsIntroF : TacticM Unit := do evalTactic <| ← `(tactic|refine Exists.intro Frank ?_)

-- Existence of siblings
theorem T1 : ∃ x y, Siblings x y := by
  aesop (config := {maxRuleApplications := 1000})

#print T1

[Eric Wieser]

Maybe @Jannis Limperg can advise on a shorter way to write that

[Mr Proof]

That's great! The theorem that came out was:

theorem T1 : ∃ x y, Siblings x y :=
id
  (Exists.intro Frank
    (Exists.intro Eve
      (Eq.mpr
        (id
          (congrArg Exists
            (funext fun p =>
              congrArg (And (Parent p Frank))
                (Eq.trans
                  (congrArg (And (Parent p Eve))
                    (Eq.trans (congrArg Not (eq_false' fun h => False.elim (noConfusion_of_Nat Person.ctorIdx h)))
                      not_false_eq_true))
                  (and_true (Parent p Eve))))))
        (Exists.intro Dan
          (of_eq_true
            (Eq.trans (congr (congrArg And parent_dan_frank._simp_2) parent_dan_eve._simp_2) (and_self True)))))))

Which translated means "Frank and Eve are siblings (whose parent is Dan)".

Just a note, Prolog does it using depth-first-search, matching and backtracking.

If I were to design a tactic I would call it "prolog" and have it just do whatever prolog can do using the same methods.

Probably not a high priority but being able to do the equivalent of what Prolog can do seems like maybe a useful thing? IDK, it's kind of a fun gimmick anyway.

Although also, it could be a good benchmark to test tactics on databases of prolog examples.:thinking:

[Eric Wieser]

Actually you can get there much faster with your original code plus

attribute [simp] Siblings
attribute [aesop safe apply] parent_alice_bob parent_alice_carol parent_dan_eve parent_dan_frank

-- Existence of siblings
theorem T1 : ∃ x y, Siblings x y := by
  aesop

[Mr Proof]

Yes that gives a shorter proof too:

theorem T1 : ∃ x y, Siblings x y :=
id
  (Exists.intro Bob
    (Exists.intro Carol
      (Exists.intro Alice
        ⟨parent_alice_bob,
          ⟨parent_alice_carol,
            of_eq_true
              (Eq.trans (congrArg Not (eq_false' fun h => False.elim (noConfusion_of_Nat Person.ctorIdx h)))
                not_false_eq_true)⟩⟩)))

This time saying "Bob and Carol are siblings (with parent Alice)"

Actually, this makes me think it might be quite easy to write a small translation app wihch translates basic Prolog files into Lean. (There's probably a good use for this, but I'm not sure what it is yet!)

It would tell you if the expression was satisfiable. It might be a bit trickier to extract the witnesses from the proof. It might not always be the first few Exist terms.

But I would have to try it on some more advanced examples first.

Also on the web editor [aesop safe] seemed to work without "apply".

(BTW my reasons for wanting this is I am making a puzzle solving app, which I needed the power of Type Theory and Prolog combined. Type Theory to "prove" when you get stuck in a dead end. And Prolog to search for solutions so I was investigating if Lean could do both. It might not be the correct solution but it is interesting what it can do).

[Kim Morrison]

I suspect you can also do the same with more light weight tactics such as apply_rules or solve_by_elim.

(This is not what grind intends to cover, at least for now!)

[Mr Proof]

Yes I wouldn't expect grind to do that.

I have seen some SAT solvers and SMT solvers implemented in Lean. (Does Lean/grind make use any of the fast SAT solvers under the hood like Gecode, OR-tools or Z3?)

So it should be possible to solve simple classic-AI puzzles such as 8-queens or knights tour , the zebra puzzle, sliding 15, or even sudokus, and rubiks cube (with IDA* search) with a single tactic one day. So in my humble opinion these classic AI puzzles would make an interesting benchmark for tactic efficiency.

To me this seems a better way for an AI to solve problems as an alternative to the current paradigm which seems to be for an LLM to try to invent the solution and for Lean to check it. The more Lean can solve using it's own search routines the better, I believe.

Knights-Tour-Animation1.gif

Thats just my 2 cents. Appreciate all the hard work. :slight_smile:

[Niels Voss]

I believe there is bv_decide, which I think uses a SAT solver, although it relies upon Lean.ofReduceBool and Lean.trustCompiler.

[Henrik Böving]

bv_decide is capable of solving these when encoded in Lean yes. There is also no need to trust ofReduceBool in order to have bv_decide solve them. You just state the problem as having no solution, it produces a counter example and then you instantiate that counterexample as a solution (which is usually trivial, at least with NP stuff)

[Mr Proof]

That's great. I will watch your video on it to find out more :)
https://www.youtube.com/watch?v=Q1LDavBJ94A&t=85s
BTW, if you would like an idea for a new video/article idea then solving classic logic problems/games using the by_decide (or other) tactic in one go would be really interesting. :slight_smile:
I have been deep-diving into constraint solving and search recently, and have learnt lots of interesting things like CDCL, the "all-different" constraint algorithms, IDA* search, LRTS search. It's like the past 25 years of people have been developing algorithms that are perfect to use as tactics.

Unfortunately there is not yet a language (I think) that combines all these search algorithms AND backs it up with a proof. So it's interesting to see how Lean develops in this area.