Understanding `nomatch`

Stream: lean4

[Abdalrhman M Mohamed]

I am currently trying to formalize STLC in Lean 4. One of the first theorems I would like to prove is that $\vdash \lambda x : A.\ x \ x : A \rightarrow B$ is not derivable for any types $A$ and $B$. Here is a mwe:

namespace STLC

abbrev Var := Char

inductive type where
  | base  : type
  | arrow : type → type → type

inductive term where
  | var : Var → term
  | lam : Var → type → term → term
  | app : term → term → term

def ctx := List (Var × type)

open type term in
inductive typing : ctx → term → type → Prop where
  | var  : typing ((x, A) :: Γ) (var x) A -- simplified
  | arri : typing ((x, A) :: Γ) M B → typing Γ (lam x A M) (arrow A B)
  | arre : typing Γ M (arrow A B) → typing Γ N A → typing Γ (app M N) B

open type term in
theorem no_δ : ¬ ∃ A B, typing nil (lam x A (app (var x) (var x))) (arrow A B) :=
  fun h => match h with
  | Exists.intro A (Exists.intro B h) => match h with
    | typing.arri h => match h with
      | typing.arre (A := T) h₁ h₂ => match h₂ with
        | typing.var => nomatch h₁

namespace STLC

In the last line, $h_1$ has type typing ((x, A) :: nil) (var x) (arrow A B) which should not be derivable from the typing rules. However, it looks like I am missing something as Lean complains about my use of nomatch and says that I did not account for the typing.var case. But that rule should not be applicable because $A \ne A \rightarrow B$. Can someone tell me what I am doing wrong?

[Leonardo de Moura]

Thanks for reporting the problem. I created an issue: https://github.com/leanprover/lean4/issues/1022
The occurs check test is missing in our dependent eliminator, we will add it as soon as possible.

[Trebor Huang]

By the way, even without the occurs check, you can manually prove that by recursing on $A$.

[Abdalrhman M Mohamed]

By "manually prove that by recursing on $A$", do you mean no_δ or A ≠ arrow A B? If you're talking about the latter, then yes. It's possible to manually prove it. But how does that help me prove no_δ? I don't have an assumption of the form A = arrow A B in my context there...

[Trebor Huang]

I mean the latter. But then you can get that assumption by requiring Lean to generate an equation (which I honestly don't know how in Lean 4). Even if Lean can't do it, you can still generate it manually by strengthening the induction hypothesis, by a technique called Fording.

[Leonardo de Moura]

Leonardo de Moura said:

Thanks for reporting the problem. I created an issue: https://github.com/leanprover/lean4/issues/1022
The occurs check test is missing in our dependent eliminator, we will add it as soon as possible.

Pushed a fix for this.

[Leonardo de Moura]

https://github.com/leanprover/lean4/commit/c5fdd54cd8ad04fe00726ad8f23545cfa276146a