Zulip Chat Archive

Stream: new members

Topic: calculus of constructions defined in Lean


view this post on Zulip 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))

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Thomas (Oct 10 2020 at 02:37):

Thank you.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Pedro Minicz (Oct 10 2020 at 14:09):

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

view this post on Zulip Mario Carneiro (Oct 10 2020 at 14:12):

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

view this post on Zulip Mario Carneiro (Oct 10 2020 at 14:12):

or half a dozen other tweaks to the theory

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 10 2020 at 14:15):

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

view this post on Zulip Mario Carneiro (Oct 10 2020 at 14:15):

I don't know the strength of it

view this post on Zulip Pedro Minicz (Oct 10 2020 at 14:23):

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

view this post on Zulip Pedro Minicz (Oct 10 2020 at 14:24):

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

view this post on Zulip Mario Carneiro (Oct 10 2020 at 14:25):

oof, F_omega models are weird


Last updated: May 18 2021 at 16:25 UTC