apply?/exact?/have?/rw? issues

[kim-em]

Please list bugs in these tactics here.

• [ ] invalid apply? suggestion
• [x] rw? errors and panics
• [ ] apply? cache corrupts on update

[kim-em]

Should

example (p q : Prop) : (p ↔ q) ↔ (¬p ↔ ¬q) := by library_search

work? The flipped version successfully finds not_iff_not, and I thought library_search was meant to handle the symmetric versions of lemmas.

[kim-em]

From https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Showing.20that.20a.20structure.20is.20.60Fintype.60

import Mathlib.Data.Fintype.Sigma
import Mathlib.Tactic.LibrarySearch

instance [Fintype α] (f : α ≃ β) : Fintype β := by library_search
-- suggestion: refine { elems := ?_ (id (Equiv.symm f)), complete := (_ : ∀ (x : β), x ∈ ?_) }

[fpvandoorn]

@semorrison I hope you don't mind that I hijacked your first comment here to keep track of some Zulip threads where I reported issues.

[ocfnash]

From https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20fails.20to.20find.20theorem/near/377013391

import Mathlib

example {n : ℕ} : n = 0 ∨ 0 < n := by exact? -- Fails to find `eq_zero_or_pos`

including reply from @dwrensha pointing out that this is a consequence of the isInternal' heuristic here: https://github.com/leanprover-community/mathlib4/blob/a1451be4b1cafd4d5e780a690b9e26c8891d3220/Mathlib/Lean/Expr/Basic.lean#L97

[grhkm21]

import Mathlib.Tactic

example (h : ¬P ∨ Q) (h' : P) : Q := by exact? -- fails
example (h : ¬P ∨ Q) (h' : P) : Q := imp_iff_not_or.mpr h h'

[fpvandoorn]

@grhkm21 I believe this is an intentional limitation: some lemmas apply to every goal, and for performance reasons they are not tried by exact?. Your example is one such lemma.

[kim-em]

But it might well be possible to re-enable trying these universal lemmas, as in the current model they would be tried last, and we have an automatic mechanism to stop before reaching a timeout. Someone should try!

[adomasbaliuka]

import Mathlib

example (x y c : ℝ) (h: 0 < c) : x < y → c * x < c * y := by exact?

suggests the malformed term

  exact fun a =>
    (fun {α} {a b c} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] a0 =>
        (mul_lt_mul_left a0).mpr)
      h a