# Zulip Chat Archive

## Stream: general

### Topic: eblast

#### Jesse Michael Han (Mar 06 2019 at 18:44):

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 (Mar 06 2019 at 20:52):

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

#### Jesse Michael Han (Mar 06 2019 at 23:12):

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 (Mar 06 2019 at 23:23):

(also, `finish`

only parses a list of `simp`

lemmas, while `[smt] eblast_using`

will parse a list of `texpr`

s).

#### Scott Morrison (Mar 07 2019 at 00:14):

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 (Mar 07 2019 at 00:14):

Hopefully someday someone writes a new version of it!

#### Joseph Corneli (Apr 15 2019 at 11:31):

@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 (Apr 15 2019 at 14:21):

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 (Apr 16 2019 at 12:23):

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 (Apr 16 2019 at 12:25):

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 (Apr 16 2019 at 12:45):

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 (Apr 16 2019 at 12:46):

`eblast`

is `ematch, close`

on a loop, so you can replace it with `ematch, ematch, ...`

to see which lemmas it instantiates

#### Joseph Corneli (Apr 16 2019 at 12:47):

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 (Apr 16 2019 at 12:48):

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 (Apr 16 2019 at 12:49):

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

#### Joseph Corneli (Apr 16 2019 at 12:49):

huh, OK!

#### Joseph Corneli (Apr 16 2019 at 13:01):

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 (Apr 16 2019 at 15:33):

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 (Apr 17 2019 at 10:23):

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 (Apr 17 2019 at 10:31):

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

#### Joseph Corneli (Apr 17 2019 at 10:44):

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

#### Jesse Michael Han (Apr 17 2019 at 22:08):

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 (Apr 17 2019 at 22:09):

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

and rewrite backwards using `is_unitary`

`is_unitary`

#### Kevin Buzzard (Apr 17 2019 at 22:10):

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

#### Kevin Buzzard (Apr 17 2019 at 22:10):

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 (Apr 29 2019 at 23:03):

@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 (Apr 29 2019 at 23:03):

Likely `normal_of_adjoint_eq_unitary_self`

could be done, but I haven't checked.

#### Joseph Corneli (May 01 2019 at 13:17):

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

#### Joseph Corneli (May 01 2019 at 13:27):

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

Last updated: Aug 03 2023 at 10:10 UTC