## Stream: new members

### Topic: calculus of constructions defined in Lean

#### Patrick Thomas (Oct 10 2020 at 00:36):

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 (Oct 10 2020 at 01:44):

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

#### Chris B (Oct 10 2020 at 02:06):

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

Thank you.

#### Anton Lorenzen (Oct 10 2020 at 07:37):

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 (Oct 10 2020 at 14:05):

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 (Oct 10 2020 at 14:08):

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 (Oct 10 2020 at 14:09):

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

#### Mario Carneiro (Oct 10 2020 at 14:12):

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

#### Mario Carneiro (Oct 10 2020 at 14:12):

or half a dozen other tweaks to the theory

#### Mario Carneiro (Oct 10 2020 at 14:14):

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 (Oct 10 2020 at 14:15):

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

#### Mario Carneiro (Oct 10 2020 at 14:15):

I don't know the strength of it

#### Pedro Minicz (Oct 10 2020 at 14:23):

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

#### Pedro Minicz (Oct 10 2020 at 14:24):

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

#### Mario Carneiro (Oct 10 2020 at 14:25):

oof, F_omega models are weird

Last updated: May 18 2021 at 16:25 UTC