exact? recent regression?

Stream: mathlib4

[RL]

Is exact?broken at the moment? Someting as trivial as:

example (a n : ℕ) (h1 : n = 2 * a + 1) : n = 1 + 2 * a := by
  exact?

cannot be found using exact?. I'm sure it was working well with library_search a few months ago...

I'm using leanprover/lean4:nightly-2023-08-19.

NOTE: should be moved to mathlib4 topic

[Alex J. Best]

Have you seen rw?, I'm not sure I'd expect exact? to find this (what is the single exact blah call you think it should find?)

[Notification Bot]

This topic was moved here from #lean4 > exact? recent regression? by Scott Morrison.

[Scott Morrison]

I don't see why either exact? or rw? should be able to do this.

[Jon Eugster]

I guess one possible proof would be rwa [Nat.add_comm], so one question could be if it is by design that rw?isn't able to suggest this, or at least rank Nat.add_comm higher up (3rd position now)?

[Scott Morrison]

There is nothing in rw? that tries assumption afterwards. There is already something that checks if rfl works afterwards. Checking assumption as well would be a reasonable addition.

[Michael Stoll]

I just observed this:

import Mathlib
lemma ex (x : ℕ) (h : 2 * 2 ∣ x) : 2 ∣ x := by exact? -- Try this: exact dvd_of_mul_left_dvd h

vs.

import Mathlib
lemma ex' (x : ℕ) (h₁ : (x : ZMod 4) = 0) (h : 2 * 2 ∣ x) : 2 ∣ x := by exact?
-- `exact?` could not close the goal. Try `apply?` to see partial suggestions.

It seems a bit strange that adding a hypothesis to the context makes exact? miss the solution it had found before.

[Scott Morrison]

Fascinating: not exact?'s fault per se:

import Mathlib

lemma ex' (x : ℕ) (h₁ : (x : ZMod 4) = 0) (h : 2 * 2 ∣ x) : 2 ∣ x := by
  apply dvd_of_mul_left_dvd
  solve_by_elim* -- failed

[Scott Morrison]

There is a bug in my implementation of src#Lean.MVarId.independent?, and more generally a meta-bug in my implementation of solve_by_elim being terrible.

[Michael Stoll]

Not sure if this is related:

import Mathlib
lemma ex {a : ℕ} (h : (a : ZMod 2) = 0) : 2 ∣ a := by apply?
-- `exact Iff.mp (ZMod.nat_cast_zmod_eq_zero_iff_dvd a 2) h`
lemma ex' {a : ℕ} (h : ((a : ZMod 4) : ZMod 2) = 0) : 2 ∣ a := by apply?
-- long list of essentially useless suggestions (similarly without `h`)

[Scott Morrison]

What answer might you expect there? I think that one is just out of scope for exact?.

[Scott Morrison]

Michael Stoll said:

I just observed this:

import Mathlib
lemma ex (x : ℕ) (h : 2 * 2 ∣ x) : 2 ∣ x := by exact? -- Try this: exact dvd_of_mul_left_dvd h

vs.

import Mathlib
lemma ex' (x : ℕ) (h₁ : (x : ZMod 4) = 0) (h : 2 * 2 ∣ x) : 2 ∣ x := by exact?
-- `exact?` could not close the goal. Try `apply?` to see partial suggestions.

It seems a bit strange that adding a hypothesis to the context makes exact? miss the solution it had found before.

Now fixed in #6862.

[Rob Lewis]

This may not actually be a regression, maybe my mistaken memory... I thought exact? handled negation/False correctly, but this fails.

import Mathlib.Tactic.LibrarySearch

axiom P : Prop
axiom Pfalse : ¬ P
lemma foo (hp : P) : False := by
  -- exact?
  exact Pfalse hp

(library_search gets this in Lean 3.) I didn't see an issue and couldn't turn up any hits on Zulip search, is this known?

[Scott Morrison]

It is known.