exact? failure with broad pattern

Stream: lean4

[Floris van Doorn]

I think the following failure of exact? happens because it doesn't index lemmas which have too broad DiscrTree-patterns. Is that correct? I think I lobbied for this before, to get speed over completeness. That said, these failures are unfortunate.

I'm still confused why the last example works, where the lemma is an implication instead of a bi-implication. Does it use a different pattern in that case?

import Mathlib.Data.Real.Basic

example (a b : ℝ) (h : a - b = 0) : a = b := by
  exact? -- fails
  -- exact sub_eq_zero.mp h

example {G} [AddGroup G] (a b : G) (h : a - b = 0) : a = b := by
  exact? -- fails
  -- exact sub_eq_zero.mp h

example (a b : ℤ) (h : a - b = 0) : a = b := by
  exact? -- exact Int.eq_of_sub_eq_zero h

[Michael Stoll]

This seems to be a general phenomenon with bi-implications:

import Mathlib

example {X : Type} {S : Set (Set X)} {B : Set X} (H : B ∉ S ↔ Bᶜ ∈ S) (hB : B ∉ S) :
    Bᶜ ∈ S := by
  /- `exact?` could not close the goal. Try `apply?` to see partial suggestions. -/
  exact?
  -- exact H.mp hB -- works

example {X : Type} {S : Set (Set X)} {B : Set X} (H : B ∉ S → Bᶜ ∈ S) (hB : B ∉ S) :
    Bᶜ ∈ S := by
  /- Try this: exact H hB -/
  exact?

It would be nice if that could be made to work. (The #discr_tree_key of H above seems to be
Iff (Not (@Membership.mem (Set _) (Set (Set _)) _ _ _)) (@Membership.mem (Set _) (Set (Set _)) _ _ (@compl (Set _) _ _)),
which looks sufficiently specific to my eyes.)

[Michael Stoll]

I imagine one solution could be to include the two implications separately in the discrimination tree when indexing a statement whose conclusion is a bi-implication. Would this be reasonable?

[Jovan Gerbscheid]

These are two separate problems: exact? only deals with bi-implications of global statements, not local hypotheses. This does work:

import Mathlib

axiom X : Type
axiom S : Set (Set X)
axiom B : Set X
axiom H : B ∉ S ↔ Bᶜ ∈ S

example (H : B ∉ S ↔ Bᶜ ∈ S) (hB : B ∉ S) :
    Bᶜ ∈ S := by
  /- Try this: exact _root_.H.mp hB -/
  exact?

[Jovan Gerbscheid]

The other problem is that exact? purposefully doesn't index any theorem with the discrimination tree pattern Eq * * *. That explains why it finds Int.eq_of_sub_eq_zero (pattern Eq Int * *). But there apparently isn't such a lemma specialized to real numbers.

[Jovan Gerbscheid]

Similarly, this example works for Nat and Int, but not in general:

import Mathlib

example (x y : Rat) (h : x ≤ y) (h' : y ≤ x) : x = y := by
  exact?