How to nomatch on a custom less-than type?

Stream: general

[nrs]

Since lt below always has a type mismatch, wouldn't we expect nomatch lt to typecheck?

inductive Pos
  | one : Pos
  | succ : Pos -> Pos

def Pos.toNat : Pos -> Nat
  | .one => 1
  | .succ n => .succ (n.toNat)

inductive LT' : Nat -> Nat -> Type
  | mk : (n : Nat) -> (pos : Pos) -> LT' n (n + pos.toNat)

variable (lt : LT' 0 0)
#check match lt with | .mk nat pos => _ -- type mismatch; has type LT'' nat (nat + pos.toNat) but expected LT'' 0 0
#check match lt with | .mk .. => _ -- type mismatch; has type LT'' 0 (0 + ?m.15735.toNat) : Type but is expected to have type LT'' 0 0 : Type
#check nomatch lt -- missing cases _

[Trebor Huang]

The mismatch is the "Lean doesn't know if it matches" kind, not the "Lean knows it definitely doesn't match" kind. Only the latter warrants a nomatch.

[nrs]

Trebor Huang said:

The mismatch is the "Lean doesn't know if it matches" kind, not the "Lean knows it definitely doesn't match" kind. Only the latter warrants a nomatch.

hm. Is there more information I could provide to obtain a contradiction/an empty type? e.g., is there something that can inhabit LT' 0 0 -> Empty?

[Kyle Miller]

This is a standard sort of example of trying to do pattern matching with indices that aren't just constructor applications. One solution is to change the type to "relax" the index using a propositional equality:

inductive LT' : Nat -> Nat -> Type
  | mk : (n m : Nat) -> (pos : Pos) -> (h : m = n + pos.toNat) -> LT' n m

variable (lt : LT' 0 0)
#check match lt with | .mk 0 _ pos h => by cases pos <;> cases h

[nrs]

Kyle Miller said:

This is a standard sort of example of trying to do pattern matching with indices that aren't just constructor applications. One solution is to change the type to "relax" the index using a propositional equality:

inductive LT' : Nat -> Nat -> Type
  | mk : (n m : Nat) -> (pos : Pos) -> (h : m = n + pos.toNat) -> LT' n m

variable (lt : LT' 0 0)
#check match lt with | .mk 0 _ pos h => by cases pos <;> cases h

Thanks for the reply! I will be studying this example