eblast

Stream: general

[Jesse Michael Han]

I was quite amused to learn that eblast could do essentially all of last week's homework assignment for Jeremy's ITP course (I think finish is, for all practical purposes, stronger, and indeed suffices to replace all calls to eblast below, but I think this is neat demonstration of how far the out-of-the-box SMT tools can get you):

import order.lattice data.nat.gcd

class lattice' (α : Type*) extends lattice.has_inf α, lattice.has_sup α :=
(inf_comm : ∀ x y : α, x ⊓ y = y ⊓ x)
(inf_assoc : ∀ x y z : α, x ⊓ y ⊓ z = x ⊓ (y ⊓ z))
(sup_comm : ∀ x y : α, x ⊔ y = y ⊔ x)
(sup_assoc : ∀ x y z : α, x ⊔ y ⊔ z = x ⊔ (y ⊔ z))
(inf_absorb : ∀ x y : α, x ⊓ (x ⊔ y) = x)
(sup_absorb : ∀ x y : α, x ⊔ (x ⊓ y) = x)

namespace lattice'

attribute [ematch]
  inf_comm inf_assoc sup_comm sup_assoc inf_absorb sup_absorb

-- inside the namespace, you can refer to the axioms without a prefix

variables {α : Type*} [lattice' α]

-- the footnote on Wikipedia tells you how to prove this!
@[ematch]theorem sup_idem (x : α) : x ⊔ x = x :=
by {[smt] eblast} -- :^)

@[ematch]theorem inf_idem (x : α) : x ⊓ x = x :=
by {[smt] eblast}

protected def le (x y : α) := x = x ⊓ y

instance : has_le α := ⟨lattice'.le⟩

@[ematch]lemma le_unfold {x y : α} : x ≤ y ↔ x = x ⊓ y := by refl

@[ematch]theorem le_def (x y : α) : (x ≤ y) = (x = x ⊓ y) := rfl

@[ematch]theorem le_refl (x : α) : x ≤ x :=
by rw [le_def, inf_idem]

-- you can use `rw le_def at *` to unfold the definition everywhere

-- Wikipedia also tells you how to prove this one:

@[ematch]theorem le_def' (x y : α) : (x ≤ y) ↔ (y = x ⊔ y) :=
by {split; intros; {[smt] eblast}}

@[ematch]theorem le_trans {x y z : α} (h : x ≤ y) (h' : y ≤ z) : x ≤ z :=
by {[smt] eblast}

@[ematch]theorem le_antisymm {x y : α} (h : x ≤ y) (h' : y ≤ x) : x = y :=
by {[smt] eblast}

@[ematch]theorem le_sup_left (x y : α) : x ≤ x ⊔ y :=
by {[smt] eblast}

@[ematch]theorem le_sup_right (x y : α) : y ≤ x ⊔ y :=
by {[smt] eblast}

@[ematch]theorem sup_le {x y z : α} (h₁ : x ≤ z) (h₂ : y ≤ z) : x ⊔ y ≤ z :=
by {[smt] eblast}

@[ematch]theorem inf_le_left (x y : α) : x ⊓ y ≤ x :=
by {[smt] eblast}

@[ematch]theorem inf_le_right (x y : α) : x ⊓ y ≤ y :=
by {[smt] eblast}

@[ematch]theorem le_inf {x y z : α} (h₁ : x ≤ y) (h₂ : x ≤ z) : x ≤ y ⊓ z :=
by {[smt] eblast}

end lattice'

[Patrick Massot]

I would really love to understand better what finish is doing. Do you understand this?

[Jesse Michael Han]

The person to ask is really @Jeremy Avigad, but from what I can tell from looking at the source, it is essentially eblast (where ematch is iterated only up to 20 times, each time followed by cc) wrapped with preprocessing and a tableaux prover.

The preprocessor negates the goal and normalizes the hypotheses by calling simp and pushing negations inwards. It also splits conjunctions and cases on existentials.

The final step is auto.done, which first tries contradiction (if your goal is provable using just classical propositional logic then after the preprocessing, this should close it). Otherwise, it essentially runs eblast, which heuristically instantiates ematch lemmas, hoping that enough is in context for cc to close the goal.

[Jesse Michael Han]

(also, finish only parses a list of simp lemmas, while [smt] eblast_using will parse a list of texprs).

[Scott Morrison]

It's a real pity about the bug in eblast, that causes it to choke on any goals which have two instances of a typeclass, parametrised by different types (e.g. ring A and ring B). eblast is super powerful, and would prove a tonne of stuff, e.g. in category theory, but unusable in the presence of non-trivial type classes.

[Scott Morrison]

Hopefully someday someone writes a new version of it!

[Joseph Corneli]

@Jesse Michael Han could you comment on how this built-in SMT support compares with the https://github.com/leanprover/smt2_interface ?

[Jesse Michael Han]

I am not an expert, but I think the built-in SMT support is not quite an SMT solver, while smt2_interface implements a translation from Lean into first-order logic to send out to external SMT solvers, querying them for sat or unsat. I don't think they reconstruct Lean proofs from the proof traces produced by the external solvers, so they add an axiom that lets them treat external solvers like Z3 as oracles.

[Joseph Corneli]

Thanks for the comment @Jesse Michael Han. I tried this example, which follows the style of yours (I think). I suppose I wouldn't actually expect it to work since I'm mostly shooting in the dark, but the debugging message is not particularly informative. Is this very far off working do you think?

import data.real.basic

constant cos : ℝ → ℝ

@[ematch]theorem cos_values (x : ℝ) : cos x ≤ 1 ∧ cos x ≥ -1 := sorry
@[ematch]theorem abs_values (a b : ℝ) : abs a > abs b → a + b ≠ 0 := sorry

@[ematch]theorem cosine_shift (x: ℝ) : cos x + 2 ≠ 0 :=
by {[smt] eblast}

solve1 tactic failed, focused goal has not been solved
state:
x : ℝ
⊢ cos x + 2 ≠ 0

[Joseph Corneli]

For the record I could successfully check the example with z3.

(set-logic AUFLIRA)
(declare-fun cos ( Real ) Real)
(set-option :numeral-as-real true)
;; Two basic rules that should combine to give us our conclusion
(assert (forall (( X Real )) (and (<= (cos  X) 1) (>= (cos  X ) (- 1)))))
(assert (forall (( A Real ) ( B Real )) (=> (> (abs A) (abs B)) (not (= (+ A B) 0)))))
;; negate the desired conclusion because we want to check for unsatisfiablity
(assert (forall (( X Real )) (= (+ (cos X) 2) 0)))
(check-sat)
(exit)

$ z3 -smt2 cosine_variant.smt2
unsat

[Joseph Corneli]

There seems to only be one mention of eblast in mathlib, but I found this set of examples from a 2017 presentation: https://github.com/leanprover/presentations/tree/c2094a9da1fecf065fbf7b70a93ce90747cdfe1a/20170116_POPL/smt -- aside from a bit of code drift that seems like a helpful guide...

[Jesse Michael Han]

eblast is ematch, close on a loop, so you can replace it with ematch, ematch, ... to see which lemmas it instantiates

[Joseph Corneli]

I turned on tracing with set_option trace.smt.ematch true and got this:

[smt.ematch] instance [abs_values], generation: 1
abs (cos x) > abs 2 → cos x + 2 ≠ 0
[smt.ematch] instance [cos_values], generation: 1
cos x ≤ 1 ∧ cos x ≥ -1
[smt.ematch] instance, generation: 1, after preprocessing
abs (cos x) > abs 2 → cos x + 2 ≠ 0
[smt.ematch] instance, generation: 1, after preprocessing
cos x ≤ 1 ∧ cos x ≥ -1
[smt.ematch] instance [le_antisymm'], generation: 2
(:cos x ≤ 1:) → 1 ≤ cos x → cos x = 1
[smt.ematch] instance, generation: 2, after preprocessing
cos x ≤ 1 → 1 ≤ cos x → cos x = 1
[smt.ematch] instance [le_trans], generation: 2
cos x ≤ 1 → 1 ≤ cos x → cos x ≤ cos x
[smt.ematch] instance [le_trans], generation: 3
1 ≤ cos x → cos x ≤ 1 → 1 ≤ 1
[smt.ematch] instance [le_antisymm'], generation: 3
(:1 ≤ cos x:) → cos x ≤ 1 → 1 = cos x
[smt.ematch] instance, generation: 2, after preprocessing
cos x ≤ 1 → 1 ≤ cos x → cos x ≤ cos x
[smt.ematch] instance, generation: 3, after preprocessing
1 ≤ cos x → cos x ≤ 1 → 1 ≤ 1
[smt.ematch] instance, generation: 3, after preprocessing
1 ≤ cos x → cos x ≤ 1 → 1 = cos x
[smt.ematch] instance [le_refl], generation: 3
cos x ≤ cos x
[smt.ematch] instance [le_refl], generation: 4
1 ≤ 1
[smt.ematch] instance [le_trans], generation: 3
1 ≤ cos x → cos x ≤ cos x → 1 ≤ cos x
[smt.ematch] instance [le_trans], generation: 3
cos x ≤ cos x → cos x ≤ cos x → cos x ≤ cos x
[smt.ematch] instance [le_trans], generation: 4
1 ≤ 1 → 1 ≤ cos x → 1 ≤ cos x
[smt.ematch] instance [le_trans], generation: 3
cos x ≤ cos x → cos x ≤ 1 → cos x ≤ 1
[smt.ematch] instance [le_trans], generation: 4
1 ≤ 1 → 1 ≤ 1 → 1 ≤ 1
[smt.ematch] instance [le_trans], generation: 2
cos x ≤ 1 → 1 ≤ 1 → cos x ≤ 1
[smt.ematch] instance [le_antisymm'], generation: 3
(:cos x ≤ cos x:) → cos x ≤ cos x → cos x = cos x
[smt.ematch] instance [le_antisymm'], generation: 4
(:1 ≤ 1:) → 1 ≤ 1 → 1 = 1
[smt.ematch] instance, generation: 3, after preprocessing
cos x ≤ cos x
[smt.ematch] instance, generation: 4, after preprocessing
1 ≤ 1
[smt.ematch] instance, generation: 3, after preprocessing
1 ≤ cos x → cos x ≤ cos x → 1 ≤ cos x
[smt.ematch] instance, generation: 3, after preprocessing
cos x ≤ cos x → cos x ≤ cos x → cos x ≤ cos x
[smt.ematch] instance, generation: 4, after preprocessing
1 ≤ 1 → 1 ≤ cos x → 1 ≤ cos x
[smt.ematch] instance, generation: 3, after preprocessing
cos x ≤ cos x → cos x ≤ 1 → cos x ≤ 1
[smt.ematch] instance, generation: 4, after preprocessing
1 ≤ 1 → 1 ≤ 1 → 1 ≤ 1
[smt.ematch] instance, generation: 2, after preprocessing
cos x ≤ 1 → 1 ≤ 1 → cos x ≤ 1
[smt.ematch] instance, generation: 3, after preprocessing
cos x ≤ cos x → cos x ≤ cos x → cos x = cos x
[smt.ematch] instance, generation: 4, after preprocessing
1 ≤ 1 → 1 ≤ 1 → 1 = 1

[Jesse Michael Han]

right, so ematch just writes all these things down and then prays that close (which is just cc) can chain together these facts to close the goal

[Jesse Michael Han]

there's an option to ask Z3 to produce a proof---maybe you'll see the discrepancy there

[Joseph Corneli]

huh, OK!

[Joseph Corneli]

Well here's the z3 proof, I'm not having a moment of clarity reviewing it.

(proof
(let (($x160 (forall ((X Real) )(! (let (($x154 (>= (- 2.0) (- 1.0))))
 (let (($x151 (<= (- 2.0) 1.0)))
 (and $x151 $x154))) :qid k!6))
 ))
 (let (($x178 (forall ((X Real) )(! false :qid k!6))
 ))
 (let ((?x179 (lambda ((X Real) )(let ((@x173 (monotonicity (rewrite (= (<= (- 2.0) 1.0) true)) (rewrite (= (>= (- 2.0) (- 1.0)) false)) (= (and (<= (- 2.0) 1.0) (>= (- 2.0) (- 1.0))) (and true false)))))
 (trans @x173 (rewrite (= (and true false) false)) (= (and (<= (- 2.0) 1.0) (>= (- 2.0) (- 1.0))) false))))
 ))
 (let ((@x186 (trans (quant-intro (proof-bind ?x179) (= $x160 $x178)) (elim-unused (= $x178 false)) (= $x160 false))))
 (let (($x40 (forall ((X Real) )(! (let ((?x23 (cos X)))
 (let (($x34 (>= ?x23 (- 1.0))))
 (let (($x25 (<= ?x23 1.0)))
 (and $x25 $x34)))) :qid k!6))
 ))
 (let ((?x161 (lambda ((X Real) )(let (($x154 (>= (- 2.0) (- 1.0))))
 (let (($x151 (<= (- 2.0) 1.0)))
 (let (($x157 (and $x151 $x154)))
 (let ((?x23 (cos X)))
 (let (($x34 (>= ?x23 (- 1.0))))
 (let (($x25 (<= ?x23 1.0)))
 (let (($x37 (and $x25 $x34)))
 (let (($x136 (= ?x23 (- 2.0))))
 (let (($x141 (forall ((X Real) )(! (let ((?x23 (cos X)))
 (= ?x23 (- 2.0))) :qid k!9))
 ))
 (let (($x127 (forall ((X Real) )(! (= (+ (cos X) 2.0) 0.0) :qid k!9))
 ))
 (let ((?x142 (lambda ((X Real) )(let (($x126 (= (+ (cos X) 2.0) 0.0)))
 (let ((@x134 (monotonicity (rewrite (= (+ (cos X) 2.0) (+ 2.0 (cos X)))) (= $x126 (= (+ 2.0 (cos X)) 0.0)))))
 (trans @x134 (rewrite (= (= (+ 2.0 (cos X)) 0.0) (= (cos X) (- 2.0)))) (= $x126 (= (cos X) (- 2.0)))))))
 ))
 (let ((@x146 (mp (asserted $x127) (quant-intro (proof-bind ?x142) (= $x127 $x141)) $x141)))
 (let ((@x156 (monotonicity (unit-resolution ((_ quant-inst X) (or (not $x141) $x136)) @x146 $x136) (= $x34 $x154))))
 (let ((@x153 (monotonicity (unit-resolution ((_ quant-inst X) (or (not $x141) $x136)) @x146 $x136) (= $x25 $x151))))
 (monotonicity @x153 @x156 (= $x37 $x157)))))))))))))))))
 ))
 (let (($x29 (forall ((X Real) )(! (let ((?x23 (cos X)))
 (let (($x25 (<= ?x23 1.0)))
 (and $x25 (>= ?x23 (- 1.0))))) :qid k!6))
 ))
 (let ((?x41 (lambda ((X Real) )(let ((?x23 (cos X)))
 (let (($x34 (>= ?x23 (- 1.0))))
 (let (($x25 (<= ?x23 1.0)))
 (let (($x37 (and $x25 $x34)))
 (let ((@x36 (monotonicity (rewrite (= (- 1.0) (- 1.0))) (= (>= ?x23 (- 1.0)) $x34))))
 (monotonicity @x36 (= (and $x25 (>= ?x23 (- 1.0))) $x37))))))))
 ))
 (let ((@x45 (mp (asserted $x29) (quant-intro (proof-bind ?x41) (= $x29 $x40)) $x40)))
 (mp (mp @x45 (quant-intro (proof-bind ?x161) (= $x40 $x160)) $x160) @x186 false)))))))))))

[Jesse Michael Han]

it's probably doing something like, derive false from cos x <= -2 and cos x >= -1

from the ematch trace, we can see that ematch doesn't know how to move 1 to the other side of an inequality (and probably doesn't know how to derive the above contradiction either). I don't think it's very good at this kind of arithmetic; from playing around with it, it looks like marking add_le_add_right or the like as @[ematch] drastically slows down each ematch round

[Joseph Corneli]

Thanks for having a further look @Jesse Michael Han. It sounds like automating a proof inside Lean might need another reasoner that would take the final output from ematch and fiddle around with the arithmetic a bit. However, I also noticed that the ematch trace for this example doesn't have much to say about 2, or -1 whereas it comes up with lots of things to say about 1 and cos x. In this regard even having another "finisher" would not be enough.

Incidentally I find the proof produced by veriT a bit easier to read than the z3 proof, so I've copied it below. veriT required one extra hint (assert (= C (cos A))) to get started, but it doesn't do much with that.

(set-logic AUFLIRA)
(declare-fun cos ( Real ) Real)
(declare-fun A () Real)
(declare-fun C () Real)
(assert (= C (cos A)))
(assert (forall (( X Real )) (and (<= (cos  X) 1) (>= (cos  X ) (- 1)))))
(assert (forall (( A Real ) ( B Real )) (=> (> (abs A) (abs B)) (not (= (+ A B) 0)))))
(assert (forall (( X Real )) (= (+ (cos X) 2) 0)))
(check-sat)

1:(input ((= C (cos A))))
2:(input ((forall  (X Real) (and (<= (cos X) 1) (>= (cos X) (- 1))))))
3:(input ((forall  (A Real) (B Real) (=> (> (abs A) (abs B)) (not (= 0 (+ A B)))))))
4:(input ((forall  (X Real) (= 0 (+ (cos X) 2)))))
5:(tmp_betared ((forall  (@vr0 Real) (and (<= (cos @vr0) 1) (>= (cos @vr0) (- 1))))) 2)
6:(tmp_betared ((forall  (@vr1 Real) (@vr2 Real) (=> (> (abs @vr1) (abs @vr2)) (not (= 0 (+ @vr1 @vr2)))))) 3)
7:(tmp_betared ((forall  (@vr3 Real) (= 0 (+ (cos @vr3) 2)))) 4)
8:(tmp_qnt_tidy ((forall  (@vr4 Real) (and (<= (cos @vr4) 1) (>= (cos @vr4) (- 1))))) 5)
9:(tmp_qnt_tidy ((forall  (@vr4 Real) (@vr5 Real) (=> (> (abs @vr4) (abs @vr5)) (not (= 0 (+ @vr4 @vr5)))))) 6)
10:(tmp_qnt_tidy ((forall  (@vr4 Real) (= 0 (+ (cos @vr4) 2)))) 7)
11:(forall_inst ((or (not (forall  (@vr4 Real) (= 0 (+ (cos @vr4) 2)))) (= 0 (+ (cos A) 2)))))
12:(forall_inst ((or (not (forall  (@vr4 Real) (and (<= (cos @vr4) 1) (>= (cos @vr4) (- 1))))) (and (<= (cos A) 1) (>= (cos A) (- 1))))))
13:(or ((not (forall  (@vr4 Real) (= 0 (+ (cos @vr4) 2)))) (= 0 (+ (cos A) 2))) 11)
14:(resolution ((= 0 (+ (cos A) 2))) 13 10)
15:(and_pos ((not (and (<= (cos A) 1) (>= (cos A) (- 1)))) (<= (cos A) 1)) 0)
16:(and_pos ((not (and (<= (cos A) 1) (>= (cos A) (- 1)))) (>= (cos A) (- 1))) 1)
17:(or ((not (forall  (@vr4 Real) (and (<= (cos @vr4) 1) (>= (cos @vr4) (- 1))))) (and (<= (cos A) 1) (>= (cos A) (- 1)))) 12)
18:(resolution ((and (<= (cos A) 1) (>= (cos A) (- 1)))) 17 8)
19:(resolution ((<= (cos A) 1)) 15 18)
20:(resolution ((>= (cos A) (- 1))) 16 18)
21:(la_generic ((not (>= (cos A) (- 1))) (not (= 0 (+ (cos A) 2)))))
22:(resolution () 21 14 20)

[Joseph Corneli]

@Scott Morrison would the alternative approach you mentioned at https://github.com/leanprover/lean/issues/1940 be relevant to the problem here?

[Joseph Corneli]

Am I correct in thinking that that's the code you have at https://github.com/semorrison/lean-rewrite-search ?

[Jesse Michael Han]

a pleasant example, from one of Pitt's linear algebra prelims:

import tactic.interactive basic

variables {α : Type*} [monoid α] {T : α}

def adj : α → α := sorry

@[ematch]lemma adj_adj (a : α) : adj (adj a) = a := sorry

@[ematch]theorem adj_antimul {a b : α} : adj (a * b) = adj b * adj a := sorry

@[ematch]def is_unitary : α → Prop := (λ a, adj a * a = (1 : α))

attribute [ematch] mul_assoc -- sadly necessary

theorem normal_of_adjoint_eq_unitary_self (T : α) (U : α) (H : is_unitary U) (H : adj T = U * T) :
  T * (adj T) = (adj T) * T :=
by {[smt] eblast}

[Jesse Michael Han]

i'm very pleased that it even knows to insert the 1 and rewrite backwards using is_unitary oops, it only needs to reassociate and then rewrite with is_unitary

[Kevin Buzzard]

You should have seen the automatic theorem provers in action at AITP last week :-)

[Kevin Buzzard]

But IIRC Lean is supposed to be bridging the gap between ATPs and ITPs so this is definitely a step in the right direction :-)

[Scott Morrison]

@Joseph Corneli, no, rewrite_search will not do anything for your cos x + 2 ≠ 0 problem. It searches (rather well, sometimes!) for chains of rewrites.

[Scott Morrison]

Likely normal_of_adjoint_eq_unitary_self could be done, but I haven't checked.

[Joseph Corneli]

@Scott Morrison thanks. I was just starting to read the description of rewrite search in the repo today.

[Joseph Corneli]

I also read the Selsam and de Moura paper about congruence closure in ITT. That's maybe a closer comparison?