aesop can't prove ¬ p ∨ q from p → q

Stream: general

[Yaël Dillies]

I just stumbled upon this puzzling example, which came up when trying to get aesop to prove a lemma of the form ¬ Property ↔ a ≠ b ∨ c = d from an existing lemma saying Property ↔ a = b ∧ c ≠ d:

import Aesop

example {p q : Prop} (hpq : p → q) : ¬ p ∨ q := by aesop

[Aaron Liu]

This is a goal for tauto

[Peter Nelson]

Why is this outside the intended scope of aesop?

[Aaron Liu]

You could have aesop call tauto, but that might be slow for complicated goals

[Yaël Dillies]

Aaron Liu said:

This is a goal for tauto

I am aware that tauto can prove this goal :smile: but it cannot prove the lemma ¬ Property ↔ a ≠ b ∨ c = d by calling the lemma Property ↔ a = b ∧ c ≠ d (because it does not know how to call lemmas, by design)

[Aaron Liu]

The solution is to have the lemma you want

[Aaron Liu]

or rw since it's an iff

[Yaël Dillies]

Again, I am aware

[Kevin Buzzard]

For me the big problem with Aesop as a general tool for doing basic stuff, is that for it to work like that, a ton of things need to be tagged @aesop. Probably you can tag some logic lemmas with @aesop and this will fix the problem. I think that where Aesop has shown its real utility is being the general tool powering tactics like aesop_cat, and maybe what is happening here is that one could make another tactic aesop_tauto which would solve this goal. But my mental model of aesop is that it will prove goals which can be proved with cases, simp and solve_by_elim, and that you might not want to expect too much more from "out of the box" aesop, because the Great Tag Every Lemma With Aesop project never happened (and it was never really clear to me whether it was supposed to happen).

[Jireh Loreaux]

Kevin Buzzard said:

is that for it to work like that, a ton of things need to be tagged @aesop.

I think this just means you need to do the tagging. For instance, I was recently preparing a presentation and looking at the proof, I had this goal (extracted) with this proof.

theorem extracted {F A B : Type*} [CStarAlgebra A] [CStarAlgebra B] [FunLike F A B]
    [AlgHomClass F ℂ A B] [StarHomClass F A B] {a : A} (ha : IsSelfAdjoint a) (φ : F)
    (hφ : Function.Injective φ)
    (h_spec : spectrum ℝ (StarAlgHom.restrictScalars ℝ (φ : A →⋆ₐ[ℂ] B) a) ⊆ spectrum ℝ a)
    (x : ℝ) (hx : x ∈ spectrum ℝ a) (hx' : x ∉ spectrum ℝ (φ a)) (f : C(ℝ, ℝ))
    (h_eqOn : Set.EqOn (⇑f) 0 (spectrum ℝ (φ a))) (h_eqOn_x : Set.EqOn (⇑f) 1 {x})
    (this : Set.EqOn (⇑f) 0 (spectrum ℝ a)) :
    False := by
  exact zero_ne_one <| calc
  0 = f x := (this hx).symm
  _ = 1 := h_eqOn_x <| Set.mem_singleton x

I really didn't want to tel my audience that we didn't have automation that could handle it. The goal boils down to this, which I hope we can all agree is something aesop should be able to prove, but it couldn't at the time because the forward rule it now uses below didn't exist / wasn't tagged. The solution was to create / tag it.

example {α 𝕜 : Type*} [Field 𝕜] {f : α → 𝕜} {x : α} {s : Set α}
    (h_mem : x ∈ s) (h_eqOn : s.EqOn f 0) (h_eqOn_x : Set.EqOn f 1 {x}) :
    False := by
  aesop?
  /-
  simp_all only [Set.eqOn_singleton, Pi.one_apply]
  have fwd : f x = (0 : α → 𝕜) x := Set.EqOn.eq_of_mem (s := s) h_eqOn h_mem
  simp_all only [Pi.zero_apply, zero_ne_one]
  -/

Aside: currently aesop can't prove the extracted goal above either, but this is due to a separate bug in the new stateful reasoning engine. It can be done with stateful reasoning disabled.

  -- first line required due to a new bug in aesop: https://github.com/leanprover-community/aesop/issues/207
  set_option aesop.dev.statefulForward false in
  aesop

[Jannis Limperg]

Yael's original example is definitely in scope for Aesop. Really, Aesop should be complete for classical (or constructive) propositional logic, so it should be able to replace tauto. But making it so requires someone to think about how to do this (efficiently); it's not just a matter of tagging more stuff. I hope I'll get to it eventually.

[Jireh Loreaux]

:up: :thumbs_up: indeed, I was more pushing back against Kevin's remark:
Kevin Buzzard said:

For me the big problem with Aesop as a general tool for doing basic stuff ...

[Kevin Buzzard]

So should more stuff be tagged Aesop? The power of simp is that it knows so many lemmas. Aesop can use apply so has far more potential but in practice I'm using simp 100 times more often than Aesop in eg FLT I should think

[Yury G. Kudryashov]

We should definitely tag more lemmas with @[aesop].

[Jireh Loreaux]

When I'm reviewing PRs and/or proofs, I often ask myself if aesop works. If I think it should but it doesn't, that generally means there is a missing tag.

[Edison Xie]

Kevin Buzzard said:

So should more stuff be tagged Aesop? The power of simp is that it knows so many lemmas. Aesop can use apply so has far more potential but in practice I'm using simp 100 times more often than Aesop in eg FLT I should think

aesop tries simp in its proof right?