Inductive definition with "less than" requirement

Stream: new members

[MrQubo]

Hello!

I want to create inductive type for lambda terms. I want to ensure in the type that bounded variables are indeed bounded by lambda term.

Here are my two attempts:

inductive LamB : Nat -> Type
| bvar : ∀ {n}, (m : Nat) -> {_ : m < n} -> LamB n
| fvar : ∀ {n}, String -> LamB n
| app : ∀ {n}, LamB n -> LamB n -> LamB n
| lam : ∀ {n}, LamB (n.succ) -> LamB n
deriving Repr
open LamB

#eval @app 0 (lam (@bvar _ 0 (by simp))) (fvar "x")

This one requires explicitly passing proof of m < n.

inductive LamB : Nat -> Type
| bvar : (m : Nat) -> ∀ {n}, LamB (m + n).succ
| fvar : ∀ {n}, String -> LamB n
| app : ∀ {n}, LamB n -> LamB n -> LamB n
| lam : ∀ {n}, LamB (n.succ) -> LamB n
deriving Repr
open LamB

#eval @app (0+0) (lam (bvar 0)) (fvar "x")

This one results in a type LamB (0+0) which lean doesn't consider to be the same as LamB 0.

Is there a better solution to want I want to accomplish? Ideally, I would want that #eval @app 0 (lam (bvar 0)) (fvar "x") works, and #eval @app 0 (lam (bvar 1)) (fvar "x") doesn't.

[A.]

This seems to work:

inductive LamB : Nat -> Type
| bvar : ∀ {n}, (m : Nat) -> (_ : m < n := by omega) -> LamB n
| fvar : ∀ {n}, String -> LamB n
| app : ∀ {n}, LamB n -> LamB n -> LamB n
| lam : ∀ {n}, LamB (n.succ) -> LamB n
deriving Repr
open LamB

#eval @app 0 (lam (bvar 0)) (fvar "x")