Matching and unknown constant

Stream: lean4

[Martin Dvořák]

import Mathlib.Tactic

example {a : ℕ} (ha : a = 37) :
    (match matcha : a with
      | 42 => False.elim (by rw [ha] at matcha; norm_num at matcha)
      | n => n
    ) = 37 := by
  aesop

example {a : ℕ → ℕ} (ha : a 0 = 37) :
    (match matcha : a 0 with
      | 42 => False.elim (by rw [ha] at matcha; norm_num at matcha)
      | n => n
    ) = 37 := by
  aesop

The first example is fine.
The second example gives me "unknown constant" and some _private garbage.
Note that the error happens only after the proof is finished.

[Henrik Böving]

@Jannis Limperg this sounds like one for you

[Martin Dvořák]

I see that aesop? produces

  simp_all only [Nat.succ.injEq,
    OfNat.one_ne_ofNat,
    IsEmpty.forall_iff,
    _example.match_1.eq_2]

while it should be

  simp_all only [Nat.succ.injEq,
    OfNat.one_ne_ofNat,
    IsEmpty.forall_iff]

only.

[Jannis Limperg]

Very interesting bug, thanks. Without Mathlib:

import Aesop

example {a : Nat} (ha : a = 37) :
    (match matcha : a with
      | 42 => False.elim (by rw [ha] at matcha; sorry)
      | n => n
    ) = 37 := by
  aesop

example {a : Nat → Nat} (ha : a 0 = 37) :
    (match matcha : a 0 with
      | 42 => False.elim (by rw [ha] at matcha; sorry)
      | n => n
    ) = 37 := by
  aesop

[Jannis Limperg]

aesop#126