mathlib sat solvers

Stream: general

[Rob Lewis]

With @Mario Carneiro 's #10744 there are at least 3 SAT+ tactics in mathlib.

• itauto is intuitionistic; itauto! is complete for classical prop logic
• tauto and tauto! both exist. I think it's been claimed that tauto! is complete for classical prop logic. tauto is not intuitionistic but is weaker than tauto!. It seems to have some support for equality, and perhaps some basic first order reasoning/heuristic instantiation? There's no module doc and the tactic doc doesn't seem complete.
• finish and friends are classical. I think (but am not sure) that finish is complete. finish is not complete. At a high level they claim to do the same as what tauto does, but explicitly say that they use the SMT state for e-matching and congruence closure.

[Rob Lewis]

I think this is a confusing zoo of options. One move that I think is a strict improvement: kill tauto and rename tauto! to tauto.

[Rob Lewis]

itauto! is a doubly confusing name, since it's neither i nor tauto (if we keep tauto(!) around).

[Rob Lewis]

Depending on what tauto actually does beyond prop logic, we could delete it and rename itauto! to tauto. (We should check performance of course.) But I suspect it does enough extra, whether intentionally or as a side effect, that this isn't an easy drop-in replacement.

[Rob Lewis]

itauto looks like the cleanest implementation and should be the easiest to port to Lean 4.

[Rob Lewis]

Correction, finish is not complete:

import tactic.finish

example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by finish

[Rob Lewis]

finish has better first-order support than tauto, although both do some:

example (h₁ : ∀ x, p x → q x) (h₂ : ∀ x, p x) : q a :=
by tauto! -- both work

example (h₁ : p a) (h₂ : p b) (h₃ : q b) : ∃ x, p x ∧ q x :=
by tauto! -- only finish works

[Patrick Massot]

In my experience tauto is a lot faster than finish.

[Jeremy Avigad]

finish should be complete for classical propositional logic, but for equality and quantifier instantiation, it is only heuristic.

[Jeremy Avigad]

Oops, I take it back. I think the issue is with the iff: by default, it is not expanded. I think adding iff_def should work. Hold on, I'll check.

[Jeremy Avigad]

This works:

import tactic.finish

example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := by finish [iff_def]

My vague memory is that finish doesn't expand iff because that could blow up goals painfully, but if you do expand them, it should be complete for propositional formulas that use it.

[Rob Lewis]

Indeed, finish with [iff_def] added when needed solves every goal in the tauto test suite except example (p q r : Prop) (h : ¬ p = q) (h' : r = q) : p ↔ ¬ r, where there seems to be a simp loop but simp [iff_def]; finish works.

[Rob Lewis]

I suspect that most of the slowdown from finish is in ematching. In the tauto test suite, setting max_ematch_rounds = 0, finish still solves everything except one, which it solves with max_ematch_rounds = 1.

[Rob Lewis]

In fact, on the tauto tests, finish is faster even without changing max_ematch_rounds.

[Rob Lewis]

I'm harping on this for a few reasons. One, it's confusing right now which tactics do what with what performance profile. Two, some of this will need to get ported, and we should avoid duplicated effort.

[Patrick Massot]

I think that if you're porting you get to choose your favorite tactic.

[Rob Lewis]

Is there real hope for porting finish? If it's sat + cc/e-matching, it can't be ported until (unless) cc/e-matching is. And then it might be better re-implemented on top of itauto! instead of its own sat solver

[Rob Lewis]

Patrick Massot said:

I think that if you're porting you get to choose your favorite tactic.

But if all are used on mathlib now, it would be nice to have drop in Lean 4 replacements. Alternatively (what I'm getting at) we should eliminate usages of some variants in mathlib.

[Patrick Massot]

I'm pretty sure we could remove uses of finish rather easily

[Rob Lewis]

At a very rough count I see ~100 uses of finish in mathlib and spot-checking them, tauto! isn't a drop-in replacement. My two reasons for harping on this conflict here. It would be easier to eliminate tauto with itauto! and finish than it would be to eliminate finish. But finish is the hardest one to port.

[Gabriel Ebner]

Personally, I'd rather not port finish if we can avoid it. Certainly not as a propositional prover (where you don't want to do anything beyond propositional logic so that you get good error messages). Jannis' aesop prover (https://github.com/JLimperg/aesop) aims to do what auto does in Isabelle, which is much more useful for general automation in my eyes.

[Patrick Massot]

I'm sure we can run a "finish finish challenge" and remove finish from mathlib in a couple of days at most. And I don't think Jeremy will complains at all, finish was explicitly an experiment.

[Rob Lewis]

I hadn't seen Jannis' repo yet! That's great

[Rob Lewis]

I suspect that would be close to a drop-in replacement for both finish and tauto in Lean 4.

[Rob Lewis]

I also just poked around some of the mathlib tauto uses, and while finish {use_simp := ff, max_ematch_rounds := 0} is a drop-in replacement, it's still much slower -- the bottleneck seems to be creating the SMT state in the first place.

[Rob Lewis]

Which makes my proposal the following:

• merge #10744
• replace all non-first-order uses of old tauto(!) with itauto(!), pending a comparison of the performance
• replace all non-first-order uses of finish with itauto!
• replace all remaining uses of finish however possible
• delete tauto; rename tauto! to something else that makes the first-orderness explicit
• rename itauto! to tauto

[Rob Lewis]

Porting itauto should be easy. We can figure out what to do with the remaining tauto-fo calls later, depending on how Jannis' work progresses

[Yaël Dillies]

What does that mean for #1083?

[Rob Lewis]

Yaël Dillies said:

What does that mean for #1083?

#1083 is long dead. Anyone is welcome to revive this kind of work in Lean 4, but given the dependence on external tools, I don't think it's relevant here.

[Rob Lewis]

itauto is epsilon slower than tauto on the tauto tests solved by both, and significantly faster on the itauto tests solved by both.

[Rob Lewis]

But the tauto test suite isn't large.

[Eric Rodriguez]

for the last few lines of the proposal, I guess you mean we now want itauto! = tauto, and itauto stays the same, instead of keeping tauto! too?

[Eric Rodriguez]

otherwise I totally agree in general. finish also always had the disadvantage of being a black box, so if it needed speeding up it couldn't be aided like tidy did

[Rob Lewis]

I want:
tauto -> nothing
tauto! -> first_order_something
itauto -> itauto
itauto! -> tauto

[Rob Lewis]

Current tauto! is stronger than itauto!, so I don't want to remove it.

[Rob Lewis]

I also don't want to delete the finish tactic, just remove/ban its use in mathlib

[Rob Lewis]

Where as tauto (non-!) can be deleted. It's neither intuitionistic nor complete, I think it has no advantage over tauto!

[Arthur Paulino]

Rob Lewis said:

Yaël Dillies said:

What does that mean for #1083?

#1083 is long dead. Anyone is welcome to revive this kind of work in Lean 4, but given the dependence on external tools, I don't think it's relevant here.

Wow, I think that an interface with Vampire would make for a cool Lean 4 package, at the very least

[Rob Lewis]

@Jeremy Avigad and @Wojciech Nawrocki (and others?) have done the hookup in one direction, although I don't think they reconstruct Vampire proofs in Lean? https://arxiv.org/abs/2112.02142

[Rob Lewis]

(To be fair, most of the work in #1083 was in the reconstruction)

[Wojciech Nawrocki]

We have a simple language of propositional formulas which can be sent to Vampire, but yes, unfortunately reconstructing proofs is the hard part which we do not do. We also don't have a connection to Expr.

[Arthur Paulino]

#1083 has ~5k lines added (idk how many of them were automatically generated). But it would be a bit sad to lose so much work

[Rob Lewis]

It's entirely undocumented. I have no objection to merging it once it's mathlib-ready. But it doesn't sound like Seul is interested in returning to it.

[Ruben Van de Velde]

I had a tiny bit of finish-removal in an old branch, so I pushed it to https://github.com/leanprover-community/mathlib/compare/finish-finish in case it ends up being useful

[Siddhartha Gadgil]

This may have been discussed before - are there attempts to interface (in Lean 4) with the TPTP language for FOL and SMT-lib for SMT problems to then call external solvers (such an interface avoids committing to a specific solver)?

Thanks

[Gabriel Ebner]

I was working on something like that for Lean 3: https://gebner.org/pdfs/2020-01-08_fomm20_leanhammer.pdf I hope I'll get back to it at some point.

[Jeremy Avigad]

Sorry to be slow to respond. I just got back from a few days visiting my mother in NY. finish was an attempt to do something like Isabelle's auto, and most of the uses in mathlib date back to the very early days, when I was testing it out to see how far it would get. I gave up on it when I decided that it was too limited and there wasn't a way to do what I wanted without having write a lot of code in C++. I am pleased that people have found it useful over the years, but I won't be sorry to see it go. I am counting on Jannis to do it right in Lean 4!

[Jeremy Avigad]

The Vampire connection is fun to play with, but it's not used to construct Lean theorems. I also very much hope that Gabriel will work on this at some point. It will be great to have Isabelle-like automation in Lean.

[Jannis Limperg]

Rob Lewis said:

I suspect [Aesop] would be close to a drop-in replacement for both finish and tauto in Lean 4.

Parity with tauto should be no big problem. In fact, Aesop already does most of the things that tauto does (judging by the doc string and modulo Aesop bugs). For parity with finish, I still need to decide what to do with equations that aren't naturally handled by simp. But that's definitely happening at some point.

[Stuart Presnell]

I've made a start on finishing finish by finding and replacing it in computability/regular_expressions #10811

[Filippo A. E. Nuccio]

+1 for the "start on finishing" :big_smile:

[Rob Lewis]

Rob Lewis said:

Which makes my proposal the following:

• merge #10744
• replace all non-first-order uses of old tauto(!) with itauto(!), pending a comparison of the performance
• replace all non-first-order uses of finish with itauto!
• replace all remaining uses of finish however possible
• delete tauto; rename tauto! to something else that makes the first-orderness explicit
• rename itauto! to tauto

@Mario Carneiro @Gabriel Ebner and any others who might have opinions here: do you agree with this plan?

[Rob Lewis]

And what should we rename tauto! to?

[Gabriel Ebner]

(deleted)

[Mario Carneiro]

itauto! has more in common with itauto than tauto though

[Rob Lewis]

But itauto! is a classical solver, so the i is misleading

[Mario Carneiro]

I'm aware of that, but I'd rather rename itauto in both forms for that

[Mario Carneiro]

It is still basically an intuitionistic prover, it's not a classical sat solver even with the !

[Gabriel Ebner]

But it proves all classical tautologies, right? So tauto is a good name.

[Mario Carneiro]

Suppose we added a more standard sat solver that also proves all classical tautologies. What would you call it?

[Gabriel Ebner]

Probably cdcl.

[Mario Carneiro]

then maybe we should call this one ljt

[Gabriel Ebner]

Or sat.

[Gabriel Ebner]

I'm not against ljt, but we should mention "tautology" in the docstring.

[Gabriel Ebner]

And what should we rename tauto! to?

Do you know what tauto! does exactly (in addition to classical tautologies)?

[Rob Lewis]

Gabriel Ebner said:

And what should we rename tauto! to?

Do you know what tauto! does exactly (in addition to classical tautologies)?

Nope. The tauto docs aren't very detailed and it definitely does things that aren't described.

[Gabriel Ebner]

I just noticed that itauto lacks a key feature of tauto: countermodels. So that's a significant regression if we replace tauto by itauto. When itauto fails, it gives you zero information on why.

import tactic.tauto tactic.itauto

example (a b : Prop) : a → a ∧ b := by tauto -- tells you that h : a ⊢ b is not provable
example (a b : Prop) : a → a ∧ b := by itauto

[Mario Carneiro]

not least because intuitionistic countermodels are hard

[Mario Carneiro]

but if you think it will be useful, I can make the failure case more informative

[Gabriel Ebner]

In intuitionistic logic, you can still return an unprovable sequent.

[Mario Carneiro]

in general there are a bunch of failed searches that contribute to the failure, the easy thing will only report the last failure

[Rob Lewis]

And I think tauto's countermodels are only vaguely present. Like, you could interpret this as a countermodel but it's really not clear.

example (a b : Prop) : a ∧ ¬ a := by tauto

[Gabriel Ebner]

It tells you that it can't prove ⊢ a, so {a ↦ false} is a countermodel.

[Gabriel Ebner]

Mario Carneiro: in general there are a bunch of failed searches that contribute to the failure, the easy thing will only report the last failure

What I meant is that you can return the last sequent after applying the invertible rules. This sequent won't contain any top-level connectives except implication/not on the left, if that makes it clearer.

[Johan Commelin]

cdcl and ljt are mysterioglyphs to me. I would much prefer tauto.

[Mario Carneiro]

Would it be better to have itauto {classical := tt}?

[Gabriel Ebner]

I strongly prefer tauto over that.

[Gabriel Ebner]

Either name it by the calculus, or by the class of goals it solves.

[Mario Carneiro]

The fact that ljt doesn't "mean anything" isn't necessarily an issue; tactics are really just "names" that you have to learn

[Mario Carneiro]

like, you would be just as hard pressed to guess what lia or micromega do

[Mario Carneiro]

on second thought, I think that classical; itauto ends up doing essentially the same thing as itauto!, so maybe it's not needed

[Gabriel Ebner]

Even if it does the same, we should have a tauto alias for it.

[Mario Carneiro]

assuming that we can find the existing name-squatter a better home

[Mario Carneiro]

My general understanding of tauto is that it does solve_by_elim and casesm [/\, \/]

[Gabriel Ebner]

From my cursory reading of the tauto source code it does tautology + exists.intro + exists.cases_on + @[symm].

[Rob Lewis]

With some kind of handling of equality too

[Gabriel Ebner]

Mmmh, apparently it also applies @[symm] lemmas in some way that I don't understand.

[Rob Lewis]

What about tauto! -> auto? Isabelle's auto is much different, but the general idea (logic + heuristics) is similar, and it's only a one character change

[Rob Lewis]

It's hard to name it by the calculus or class of goals it solves if neither is specified

[Gabriel Ebner]

No no no.

[Gabriel Ebner]

Isabelle's auto is something completely different.

[Gabriel Ebner]

How about tauto+ or tauto_plus?

[Rob Lewis]

I don't like the idea of tauto and tauto+ having completely different implementations

[Rob Lewis]

tauto_plus feels slightly better

[Mario Carneiro]

I prefer tauto_plus; I would reserve character sigils for option changes rather than implementation changes

[Mario Carneiro]

(same reason I'm kind of okay with itauto! even though two of the characters are in direct conflict with each other)

[Rob Lewis]

etauto for extended?

[Rob Lewis]

Not sure how confusing it is that the e prefix is used already in eapply...

[Stuart Presnell]

Is there any problem that might arise from this recycling of names, having some of the tactics shift “one chair to the left”? In the very short term it might be tricky to remember what does what, if you’re used to the old names. Are there other problems that might arise (e.g. documentation pertaining to previous versions of mathlib become more confusing)? Is there an argument for just choosing brand new names that don’t collide with the names currently in use?

[Mario Carneiro]

mathlib has zero backward compatibility, so that's not really a concern. If it was difficult to change all existing uses it might be an issue, but for name changes like this it is not difficult.

[Mario Carneiro]

I think for the most part people just try to speak the magic words and see if it solves the goal, in which case it doesn't matter even if the names switch around if your goal is still solved

[Rob Lewis]

If it's a big worry we could acknowledge the change in the error messages for a bit

[Rob Lewis]

There are 100 uses of tauto that can be replaced with itauto, 3 with itauto!, and 122 that can't be replaced with either. Unfortunately this experiment pointed out that itauto doesn't scale as well as tauto. The diff shows a handful of places where tauto worked but itauto times out, generally (always?) because there's too much in the context. https://github.com/leanprover-community/mathlib/compare/tauto-to-itauto

[Mario Carneiro]

Could you extract some stress tests?

[Stuart Presnell]

Stuart Presnell said:

I've made a start on finishing finish by finding and replacing it in computability/regular_expressions #10811

I think my most recent PR (#11136) eliminates the last few instances of finish in the main body of mathlib. The only remaining (non-commented) instances of the string "finish" that I could find are in the scripts, test, tactic, and archive folders, which I haven't touched.

I have five other open PRs (#11099, #11103, #11126, #11130, and #11133), if anyone's interested in hastening the finish of the "finish finish" project. :grinning:

[Johan Commelin]

Thanks for all your efforts!

[Stuart Presnell]

It's been a really rewarding random tour of the library! I've worked on a lot of files that I might never have looked at otherwise.

[Patrick Massot]

Stuart Presnell said:

I have five other open PRs (#11099, #11103, #11126, #11130, and #11133), if anyone's interested in hastening the finish of the "finish finish" project. :grinning:

I'm on it.

[Patrick Massot]

All 5 PRs are now in bors's queue.

[Patrick Massot]

@Rob Lewis have you seen that?

[Stuart Presnell]

Fantastic, thank you!

[Patrick Massot]

Stuart, if you are curious you can have a look at how I simplified many cases. It's not the most interesting part of Lean, but you often learn stuff by seeing code simplification.

[Stuart Presnell]

Thanks very much, I've just skimmed through the changes you've made and already seen that you've made a lot of improvements that I should learn from. I'll take a proper look over them tomorrow.

[Rob Lewis]

Mario Carneiro said:

Could you extract some stress tests?

@Mario Carneiro sorry I missed this question before. Here are a few tests chopped from that experiment. They don't have minimal imports but at least the first one should be relatively low. All of these time out for me without clearing variables first.

import algebra.big_operators.basic
import number_theory.quadratic_reciprocity



example {x y z : ℤ} (m n : ℤ)
  -- (h : pythagorean_triple x y z)
  (hzpos : 0 < z)
  (h2 : x % 2 = 1 ∧ y % 2 = 0)
  (hc : y.gcd x = 1)
  (H : (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨
            y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
         m.gcd n = 1 ∧
           (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)) :
  (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨
       x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) :=
begin
  -- itauto,
end


open_locale big_operators

example {β α : Type}
  [comm_monoid β]
  {s : finset α}
  {f : α → β}
  (_inst : decidable_eq α)
  (_inst_2 : decidable_eq β)
  (s : finset α)
  (ih : ∀ (t : finset α),
          t ⊂ s →
          ∀ (g : Π (a : α), a ∈ t → α),
            (∀ (a : α) (ha : a ∈ t), f a * f (g a ha) = 1) →
            (∀ (a : α) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
            ∀ (g_mem : ∀ (a : α) (ha : a ∈ t), g a ha ∈ t),
              (∀ (a : α) (ha : a ∈ t), g (g a ha) sorry = a) →
              ∏ (x : α) in t, f x = 1)
  (g : Π (a : α), a ∈ s → α)
  (h : ∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1)
  (g_ne : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a)
  (g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s)
  (g_inv : ∀ (a : α) (ha : a ∈ s), g (g a ha) sorry = a)
  (_x : s.nonempty)
  (_fun_match : s.nonempty → ∏ (x : α) in s, f x = 1)
  (x : α)
  (hx : x ∈ s)
  (hmem : ∀ (y : α), y ∈ (s.erase x).erase (g x hx) → y ∈ s)
  (g_inj : ∀ {x : α} {hx : x ∈ s} {y : α} {hy : y ∈ s},
             g x hx = g y hy → x = y)
  (ih' : ∏ (y : α) in (s.erase x).erase (g x hx), f y = 1)
  (hx1 : f x = 1)
  (y : α)
  (hy : y ∈ s)
  (hy₁ : ¬y = g x hx → y = x) :
  y = x ∨ y = g x hx :=
begin
  clear ih _fun_match g_inj ih', -- comment this and it's slow
  itauto,
end


open function finset nat finite_field zmod


example (p q : ℕ) (x : ℕ × ℕ)
  (hq0 : ↑q ≠ 0)
  (hswap : (filter (λ (x : ℕ × ℕ), x.snd * q ≤ x.fst * p)
                ((Ico 1 (q / 2).succ).product (Ico 1 (p / 2).succ))).card =
             (filter (λ (x : ℕ × ℕ), x.fst * q ≤ x.snd * p)
                ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ))).card)
  (hdisj : disjoint
             (filter (λ (x : ℕ × ℕ), x.snd * p ≤ x.fst * q)
                ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)))
             (filter (λ (x : ℕ × ℕ), x.fst * q ≤ x.snd * p)
                ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ))))
  (this : x.snd * p ≤ x.fst * q ∨ x.fst * q ≤ x.snd * p) :
  ((1 ≤ x.fst ∧ x.fst < (p / 2).succ) ∧
           1 ≤ x.snd ∧ x.snd < (q / 2).succ) ∧
        x.snd * p ≤ x.fst * q ∨
      ((1 ≤ x.fst ∧ x.fst < (p / 2).succ) ∧
           1 ≤ x.snd ∧ x.snd < (q / 2).succ) ∧
        x.fst * q ≤ x.snd * p ↔
    (1 ≤ x.fst ∧ x.fst < (p / 2).succ) ∧
      1 ≤ x.snd ∧ x.snd < (q / 2).succ :=
begin
  -- itauto,
end

[Rob Lewis]

Old tauto isn't instant, but the worst is 1.2 seconds on the first one.

[Mario Carneiro]

The first one is instant for me

[Mario Carneiro]

profiler says 38 ms

[Mario Carneiro]

this is on master as of a few days ago

[Mario Carneiro]

updated to master, seems the same. Example 1 in 30 ms, example 2 fails (in 10 ms), example 3 in 16 ms

[Mario Carneiro]

Ah, #10744 never got merged?

[Mario Carneiro]

I don't think the discussion about naming should block that PR

[Rob Lewis]

The problem is with #10744 then

[Rob Lewis]

I was running these tests on top of that. With that change they time out for me

[Rob Lewis]

You're right that they're fast on master

[Rob Lewis]

Didn't check that, I wasn't expecting a regression in plain itauto from that change

[Mario Carneiro]

I think I know the issue behind example 1: Everything there is a decidable proposition so the preprocessor adds a whole bunch of potential applications of em and the main solver gets lost

[Mario Carneiro]

maybe there should be a tactic option to turn off decidability checking

[Rob Lewis]

itauto-?

[Rob Lewis]

In any case, with this performance I don't think it should be used to replace tauto in mathlib3. Maybe this is reason to write a dedicated classical sat tactic for mathlib4

[Mario Carneiro]

@Rob Lewis I've pushed some changes on #10744 that should address the issues. itauto now acts like it does on master, ignoring decidable instances, while itauto* will add all decidable instances and itauto [p] will add selected decidable instances. Also I incorporated @Gabriel Ebner 's suggestion to show partial proofs in the case where the proof search fails.