lambda calc formalization

Stream: new members

[cosindine]

Hi all, recently I've been getting into type theory -- more specifically typed lambda calculi. I have quite a number of lambda calc text books at this point, and I figured I should go through one of them and write out some proofs in lean.

here is my current attempt at a representation:

namespace cosindine

universe u
def Set (α: Sort u) := α → Bool
def empty (α: Sort u) : Set α := λx↦ false
def union {α: Sort u} (a b: Set α) : Set α := λx↦ or (a x) (b x)
def intersect {α: Sort u} (a b: Set α) : Set α := λx↦ and (a x) (b x)
def complement {α: Sort u} (a: Set α) : Set α := λx↦ not (a x)

def ite {α: Sort u} (a: Bool) (t e: α) : α :=
  match a with
  | Bool.true => t
  | Bool.false => e

def nat_eq := Nat.beq
def add := Nat.add

inductive Term where
  | var : Nat → Term
  | app : Term → Term → Term
  | lam : Nat → Term → Term

mutual
unsafe def term_ts (t: Term) :=
  match t with
  | Term.var n => toString n
  | Term.app a b => (term_ts_p a) ++ (term_ts b)
  | Term.lam m n => "λ" ++ (toString m) ++ "." ++ (term_ts n)

unsafe def term_ts_p (t: Term) :=
  match t with
  | Term.var n => (toString n) ++ " "
  | _ => "(" ++ (term_ts t) ++ ")"

end

instance : ToString Term where
  toString t := unsafe term_ts t

def var (t: Term) : Set Nat :=
  match t with
  | Term.var n => nat_eq n
  | Term.app a b => union (var a) (var b)
  | Term.lam m n => union (nat_eq m) (var n)

def max_var (t: Term) : Nat :=
  match t with
  | Term.var n => n
  | Term.app a b => max (max_var a) (max_var b)
  | Term.lam m n => max m (max_var n)

def free_var (t: Term) : Set Nat :=
  match t with
  | Term.var n => nat_eq n
  | Term.app a b => union (free_var a) (free_var b)
  | Term.lam m n => λx↦ ite (nat_eq m x) False (free_var n x)

def rename_free (t: Term) (x y: Nat) : Term :=
  match t with
  | Term.var n => ite (nat_eq n x) (Term.var y) (Term.var n)
  | Term.app a b => Term.app (rename_free a x y) (rename_free b x y)
  | Term.lam m n => Term.lam m (ite (nat_eq m x) n (rename_free n x y))

unsafe def subst (t : Term) (x : Nat) (u : Term) : Term :=
  match t with
  | Term.var n => ite (nat_eq n x) u (Term.var n)
  | Term.app a b => Term.app (subst a x u) (subst b x u)
  | Term.lam m n =>
    ite (nat_eq m x)
      (Term.lam m n)
      (ite (free_var u m)
        (
          let e1 := Nat.succ (add (max_var n) (max_var u))
          Term.lam e1 (subst (rename_free n m e1) x u)
        )
        (Term.lam m (subst n x u)))

end consindine

excuse my lack of syntax, its mostly intentional.

it turns out that substitution is more annoying than you would expect!
image.png

my goal is to essentially prove the church rosser theorem and then move on to typed lambda calculi.

My questions are essentially:
should I bother with proving subst is well founded or just add a "gas/fuel" variable?
does the above seem reasonable to work with?
would it be worth representing terms in the de bruijn form?
is the curch rosser theorem provable for untyped lambda calc in lean (with the non-termination and such)?

Thanks!

[Mario Carneiro]

using de bruijn will fix the termination issue in subst

[Mario Carneiro]

but you can prove it in this form if you want

[Mario Carneiro]

your code is not a #mwe, I'm getting several missing references like nat_eq and union (also Set but import Mathlib.Data.Set.Basic fixes that)

[cosindine]

oop, probably should have checked >_<

so the set i've been using is

def Set (α: Sort u) := α → Bool
def empty (α: Sort u) : Set α := λx↦ false
def union {α: Sort u} (a b: Set α) : Set α := λx↦ or (a x) (b x)
def intersect {α: Sort u} (a b: Set α) : Set α := λx↦ and (a x) (b x)
def compliment {α: Sort u} (a: Set α) : Set α := λx↦ not (a x)

and nat_eq is

def nat_eq (a b: Nat) : Bool :=
  match a, b with
  | Nat.zero, Nat.zero => true
  | Nat.succ n, Nat.zero => false
  | Nat.zero, Nat.succ m => false
  | Nat.succ n, Nat.succ m => nat_eq n m

[Mario Carneiro]

in other words you should put this at the top of your first post:

namespace cosindine

universe u
def Set (α: Sort u) := α → Bool
def empty (α: Sort u) : Set α := λx↦ False
def union {α: Sort u} (a b: Set α) : Set α := λx↦ or (a x) (b x)
def intersect {α: Sort u} (a b: Set α) : Set α := λx↦ and (a x) (b x)
def compliment {α: Sort u} (a: Set α) : Set α := λx↦ not (a x)

def nat_eq := Nat.beq
def add := Nat.add

[Mario Carneiro]

BTW compliment is a very nice thing to say about someone, complement is the set of elements not in a given one

[Mario Carneiro]

you're still missing add, I've added that

[Mario Carneiro]

def size : Term → Nat
  | Term.var _ => 1
  | Term.app a b => size a + size b + 1
  | Term.lam _ n => size n + 1

@[simp] theorem rename_free_size (t x y) : size (rename_free t x y) = size t := by
  induction t <;> simp [*, rename_free, size] <;> split <;> simp [*, size]

def subst (t : Term) (x : Nat) (u : Term) : Term :=
  match t with
  | Term.var n => ite (nat_eq n x) u (Term.var n)
  | Term.app a b => Term.app (subst a x u) (subst b x u)
  | Term.lam m n =>
    ite (nat_eq m x)
      (Term.lam m n)
      (ite (free_var u m)
        (
          let e1 := Nat.succ (add (max_var n) (max_var u))
          Term.lam e1 (subst (rename_free n m e1) x u)
        )
        (Term.lam m (subst n x u)))
termination_by size t
decreasing_by all_goals simp [size] <;> omega

[cosindine]

huh doesn't work for me, but thats probably because i've defined ite as

def ite {α: Sort u} (a: Bool) (t e: α) : α :=
  match a with
  | Bool.true => t
  | Bool.false => e

(i'll add it to the thing...)

<---- needs to start using libraries instead of reinventing everything
<---- has way to much fun reinventing everything

[cosindine]

alright I've fixed it with this beauty:

def size : Term → Nat
  | Term.var _ => 1
  | Term.app a b => Nat.succ (add (size a) (size b))
  | Term.lam _ n => Nat.succ (size n)

-- hey man lean is based on CoC
@[simp] theorem rename_free_size (t x y) : size (rename_free t x y) = size t :=
  match t with
  | Term.var n =>
    bool_cases (nat_eq n x)
      (λp1 ↦
        let e1 := Eq.congrFn (Eq.congrFn (Eq.congrArg ite p1) (Term.var y)) (Term.var n)
        let e2 := Eq.trans (Eq.refl (rename_free (Term.var n) x y)) e1
        let e3 := Eq.congrArg size e2
        e3)
      (λp1 ↦
        let e1 := Eq.congrFn (Eq.congrFn (Eq.congrArg ite p1) (Term.var y)) (Term.var n)
        let e2 := Eq.trans (Eq.refl (rename_free (Term.var n) x y)) e1
        let e3 := Eq.congrArg size e2
        e3)
  | Term.app a b =>
    let e1 := rename_free_size a x y
    let e2 := rename_free_size b x y
    Eq.fold add (Eq.fold add e1 e2) (Eq.refl 1)
  | Term.lam m n =>
    bool_cases (nat_eq m x)
      (λp1 ↦
        let e1 := Eq.congrFn (Eq.congrFn (Eq.congrArg ite p1) n) (rename_free n x y)
        Eq.congrArg size (Eq.congrArg (Term.lam m) e1))
      (λp1 ↦
        let e1 := Eq.congrFn (Eq.congrFn (Eq.congrArg ite p1) n) (rename_free n x y)
        let e2 := Eq.congrArg size (Eq.congrArg (Term.lam m) e1)
        let e3 := rename_free_size n x y
        Eq.trans e2 (Eq.congrArg Nat.succ e3))

-- yes i have a definition of add somewhere
@[simp] theorem add_is_add (a b: Nat) : Eq (add a b) (a + b) :=
  match b with
  | Nat.zero => rfl
  | Nat.succ n => Eq.congrArg Nat.succ (add_is_add a n)

<---- still needs to figure out how to use tactics properly

it probably would have been easier to just send my entire file at this point :skull:

[Mario Carneiro]

<---- still needs to figure out how to use tactics properly

Pro tip, try using them

[Mario Carneiro]

Here's a version of the proof for your ite:

@[simp] theorem rename_free_size (t x y) : size (rename_free t x y) = size t := by
  induction t <;> simp [*, rename_free, size] <;> cases nat_eq .. <;> simp [*, ite, size]

[Mario Carneiro]

If you want to write everything from terms like a caveman then why are you using match? That's a tactic you know :grinning_face_with_smiling_eyes:

[Mario Carneiro]

it desugars to an application of Term.recOn

[cosindine]

last time i tried that it complained about not being able to compile it inside of def's or smthn
or maybe that was just Term.rec?

don't remember...

[Mario Carneiro]

Here's a shorter term-only proof of rename_free_size:

@[simp] theorem rename_free_size (t x y) : size (rename_free t x y) = size t :=
  match t with
  | .var _ =>
    match (motive := ∀b, size (ite b ..) = 1) _ with
    | true | false => rfl
  | .app _ _ =>
    congrArg (· + 1) <| congr (congrArg add (rename_free_size ..)) (rename_free_size ..)
  | .lam _ _ =>
    congrArg (· + 1) <|
      match (motive := ∀b, size (ite b ..) = _) _ with
      | true => rfl | false => rename_free_size ..

[Mario Carneiro]

last time i tried that it complained about not being able to compile it inside of def's or smthn
or maybe that was just Term.rec?

yeah, lean doesn't actually want you to use recursors like a caveman

[cosindine]

yeah for size

def size (t: Term) : Nat :=
  Term.recOn t
    (λa ↦ 1)
    (λa b m1 m2↦ Nat.succ (add m1 m2))
    (λm n m1↦ Nat.succ m1)

it complains with

code generator does not support recursor `Term.recOn` yet, consider using `match ... with`  and/or structural recursion

[Mario Carneiro]

you can mark it as noncomputable

[cosindine]

but i want to compute with it :pleading:

[Mario Carneiro]

actually you probably don't care about computing size

[Mario Carneiro]

the default sizeOf function is also noncomputable

[Mario Carneiro]

it's just used in termination arguments

[Mario Carneiro]

note that compute here means like #eval, the kernel can compute with it according to the rules of CIC regardless

[cosindine]

i can't wait for this to be several hundred lines:

theorem double_subst {x y: Nat} {M N L: Term} (p1: Eq (nat_eq x y) false) (p2: Eq (free_var L x) false) :
  Eq (subst (subst M x N) y L) (subst (subst M y L) x (subst N y L)) := sorry

2025-04-11-211108_755x153_scrot.png

[cosindine]

wait why doesn't this work?

theorem subst_var (n x u) : Eq (subst (Term.var n) x u) (ite (nat_eq n x) u (Term.var n)) := rfl

guess we using

theorem subst_var (n x u) : Eq (subst (Term.var n) x u) (ite (nat_eq n x) u (Term.var n)) := subst.eq_def (Term.var n) x u

[Mario Carneiro]

definitions by well founded recursion (i.e. any time you have to use termination_by and/or decreasing_by are generally not defeq to their bodies, because there is a proof under the hood that constructs the function via something like a fuel variable and then proves that you can get rid of it

[cosindine]

alright i've invested in a second tactic

theorem subst_no_free_var {t: Term} {x: Nat} (p1: Eq (free_var t x) false) (u: Term) : Eq (subst t x u) t :=
  match t with
  | Term.var n =>
    let e1 := Eq.congrFn (Eq.congrFn (Eq.congrArg ite p1) u) (Term.var n)
    Eq.trans (subst.eq_def _ _ _) e1
  | Term.app a b =>
    or_is_false p1
      (λp2 p3 ↦
        let e1 := subst_no_free_var p2 u
        let e2 := subst_no_free_var p3 u
        Eq.trans (subst.eq_def _ _ _) (Eq.fold Term.app e1 e2))
  | Term.lam m n =>
    bool_cases (nat_eq m x)
      (λp2 ↦
        let e1 := Eq.congrFn (Eq.congrFn (Eq.congrArg ite p2) _) _
        Eq.trans (subst.eq_def _ _ _) e1)
      (λp2 ↦
        let e1 := (subst.eq_def (Term.lam m n) x u)
        let e4 := Eq.congrFn (Eq.congrFn (Eq.congrArg ite p2) false) (free_var n x)
        let e5 := Eq.trans (Eq.symm e4) p1
        let e6 := subst_no_free_var e5 u
        let e7 := (Eq.congrArg (Term.lam m) e6)
        let e8 : (a b: Term) → Eq (ite false a b) b := λ a b ↦ rfl
        let e9 : (b: Bool) → Eq (and false b) false := λ b ↦ match b with | true => rfl | false => rfl
        let e10 := by simpa [e8, e9, p1, p2] using e1
        Eq.trans e10 e7)