calculus of constructions defined in Lean

Stream: new members

[Patrick Thomas]

A while ago with a lot of help I came up with the following definitions for the untyped lambda calculus in Lean. Is it feasible to do the same for the typed lambda calculus on up to the calculus of constructions? I'm hoping it might be useful for my understanding of it.

import data.set
open set


def var := ℕ

inductive pre_term : Type
| var : var → pre_term
| app : pre_term → pre_term → pre_term
| abs : var → pre_term → pre_term


def FV : pre_term → set var
| (pre_term.var x) := {x}
| (pre_term.app P Q) := (FV P) ∪ (FV Q)
| (pre_term.abs x P) := (FV P) \ {x}


-- sub_is_def M x N means M [ x := N ] is defined
inductive sub_is_def : pre_term → var → pre_term → Prop

-- y [ x := N ] is defined
| var (y : var) (x : var) (N : pre_term) :
  sub_is_def (pre_term.var y) x N

-- P [ x := N ] is defined → Q [ x := N ] is defined → (P Q) [ x := N ] is defined
| app (P : pre_term) (Q : pre_term) (x : var) (N : pre_term) :
  sub_is_def P x N → sub_is_def Q x N → sub_is_def (pre_term.app P Q) x N

-- x = y → ( λ y . P ) [ x := N ] is defined
| abs_same (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x = y → sub_is_def (pre_term.abs y P) x N

-- x ≠ y → x ∉ FV ( λ y . P ) → ( λ y . P ) [ x := N ] is defined
| abs_diff_nel (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x ≠ y → x ∉ FV (pre_term.abs y P) → sub_is_def (pre_term.abs y P) x N

-- x ≠ y → y ∉ FV ( N ) → P [ x := N ] is defined → ( λ y . P ) [ x := N ] is defined
| abs_diff (y : var) (P : pre_term) (x : var) (N : pre_term) :
  x ≠ y → y ∉ FV N → sub_is_def P x N → sub_is_def (pre_term.abs y P) x N



-- M [ x := N ]
def sub : pre_term → var → pre_term → pre_term
-- if x = y then y [ x := N ] = N else y [ x := N ] = y
| (pre_term.var y) x N := if (x = y) then N else (pre_term.var y)

-- (P Q) [ x := N ] = (P [ x := N ] Q [ x := N ])
| (pre_term.app P Q) x N := pre_term.app (sub P x N) (sub Q x N)

-- if x = y then ( λ y . P ) [ x := N ] = ( λ y . P ) else ( λ y . P ) [ x := N ] = ( λ y . P [ x := N ] )
| (pre_term.abs y P) x N := if x = y then (pre_term.abs y P) else (pre_term.abs y (sub P x N))

[Patrick Thomas]

I guess that would violate not being able to prove things about a theory inside that theory?

[Chris B]

I'm just passing by while doing some procrastinating, but @Anton Lorenzen made a model of CoC in Lean that might be of interest. https://github.com/anfelor/coc-lean

[Patrick Thomas]

Thank you.

[Anton Lorenzen]

Don't be afraid to hit me up. It was my first lean project and there is quite a bit I would do differently this time around.

[Pedro Minicz]

Patrick Thomas said:

I guess that would violate not being able to prove things about a theory inside that theory?

This won't be a problem, as Lean's type theory is a lot more powerful than plain CC.

[Pedro Minicz]

Just by having an infinite universe hierarchy, Lean should be able to prove many interesting things about CC and even about more complicated lambda calculi, like the Calculus of Dependent Lambda Eliminations (basis for the Cedille proof assistant, it is a very small and elegant extension of CC which makes induction derivable for Mendler-style lambda encoded data types).

[Pedro Minicz]

Although this is just a hunch. @Mario Carneiro should know how to answer this better.

[Mario Carneiro]

That sounds right, although the term CC/CoC/CIC is sometimes overloaded to include the universes

[Mario Carneiro]

or half a dozen other tweaks to the theory

[Mario Carneiro]

But it's certainly possible (though complicated) to define the full theory of Lean inside Lean. The only thing you won't be able to prove is that the embedded theory doesn't prove false, although you can do it if you add an axiom to lean asserting the existence of a sufficiently large cardinal

[Mario Carneiro]

@Pedro Minicz Is there a consistency proof for CDLE somewhere?

[Mario Carneiro]

I don't know the strength of it

[Pedro Minicz]

Yes, there is. It involves translating CDLE to $F_\omega$. I don't really understand all the details of the proof.

[Pedro Minicz]

It can be found here, page 18, section 6.

[Mario Carneiro]

oof, F_omega models are weird