lambda-terms by S, K combinators

Stream: new members

[Horatiu Cheval]

Hello, I am trying to implement a version of the SKI calculus, and I got stuck at defining λ-terms by combinators. What I have is

inductive type
| ground : type
| compose : type → type → type

infixr `>>` := type.compose

-- for each type τ, variables of type τ are represented by natural indices
inductive var (τ : type)
| mk : ℕ → var


inductive term : type → Type
| of_var : ∀ {τ : type}, var τ → term τ
| app : ∀ {τ σ : type}, term (τ >> σ) → term τ → term σ
| K : ∀ {τ σ : type}, term $ τ >> σ >> τ
| S : ∀ {τ σ ρ : type}, term $ (τ >> σ >> ρ) >> (τ >> σ) >> τ >> ρ

-- is_free_var x t means that x occurs in t
-- Probably needed for the following definition, I left out its body
inductive is_free_var : ∀ {τ σ : type}, var σ → term τ → Prop

instance decidable_is_free_var : ∀ {τ σ : type} {t : term τ} {x : var σ}, decidable $ is_free_var x t := sorry

Now, for variables x and terms t of any type, we define a termλ x . t by
λ x . x := S K K
λ x . a := K a, if x is not a variable in a
λ x . (a x) := a, if x is not a variable in a
λ x . (a b) := S (λ x . a) (λ x. b), otherwise
for combinators of appropriate types. I've been trying for some time to implement this definition

def lambda : ∀ {τ σ : type}, var τ → term σ → term (τ >> σ) := sorry

The main problem is that the definition does not follow the inductive structure of terms, so I end up with a lot of nested case-checks (which can't even be easily written for variables, since I cannot write x = y with x : var τ and y : var σ), which end up not typechecking, or rendering Lean unable to prove the recursions are terminating or other errors. I can post some of my unsuccessful attempts if it helps. Am I missing a cleaner way of writing this definition?