apply? ignores previous lemma

Stream: lean4

[Stepan Holub]

I am puzzled by the fact that apply? finds nothing even if the identical theorem has just been proven. Has this anything to do with "non-classical" nature of the theorem?

theorem dne {p : Prop} (h : ¬¬p) : p :=
  Or.elim (Classical.em p)
    (fun hp : p => hp)
    (fun hnp : ¬p => absurd hnp h)

theorem dne1 {p : Prop} (h : ¬¬p) : p := by
  -- apply? didn't find any relevant lemmas
  exact dne h

[Shreyas Srinivas]

Being classical or not has nothing to do with it. The following works:

theorem dne1 {p : Prop} (h : ¬¬p) : p := by
  have dne {p : Prop} (h : ¬¬p) : p :=
  Or.elim (Classical.em p)
    (fun hp : p => hp)
    (fun hnp : ¬p => absurd hnp h)
  apply?

This must be a bug in the way apply? looks for theorems

[Stepan Holub]

Indeed. But apply? works in most cases. The bug has a strange blind spot for classical reasoning.

[Shreyas Srinivas]

Do you have a different example without classical

[Eric Wieser]

Yes,

theorem foo {p : Prop} (h : p = True) : p := sorry

theorem bar {p : Prop} (h : p = True) : p := by
  apply?

[Eric Wieser]

The problem is likely that the goal is a free variable, so there is nothing to match on

[Eric Wieser]

Indeed, #discr_tree_key foo is just _

[Stepan Holub]

Good point. Not _ is already fine

  theorem foo {p : Prop} (h : p = False) : ¬ p := by
      apply?