feat: LambdaCalculus.LocallyNameless.Coc

[matthunz]

Summary

Adds basic syntax and typing judgments for the Calculus of Constructions following Coquand's algorithm. I tried to keep everything as close to other lambda calculi in this project as well as general code style. Some of the lemmas from that paper are noticeably missing but I'm hoping this can be an OK first cut 😃

LambdaCalculus.LocallyNameless.Coc

• Term syntax

inductive Term (Var : Type u) : Type u
  /-- Bound term variables using a de-Bruijn index. -/
  | bvar : ℕ → Term Var
  /-- Free term variables. -/
  | fvar : Var → Term Var
  /-- Function application. -/
  | app : Term Var → Term Var → Term Var
  /-- Lambda abstraction. -/
  | abs : Term Var → Term Var → Term Var
  /-- Pi type. -/
  | pi : Term Var → Term Var → Term Var
  /-- Type universe. -/
  | type : ℕ → Term Var

• Typing judgements

inductive Typing : Env Var → Term Var → Term Var → Prop
  /-- Variable lookup in Γ -/
  | var : Γ.Wf → ⟨x, A⟩ ∈ Γ → Typing Γ (.fvar x) A
  /-- Function application -/
  | app : Typing Γ M (.pi A B) → Typing Γ N A → Typing Γ (.app M N) (B ^ᵗ N)
  /-- Lambda abstraction -/
  | abs (ρ : Finset Var) :
      Typing Γ A K →
      (∀ x ∉ ρ, Typing ({⟨x, A⟩} ∪ Γ) (N ^ᵗ .fvar x) (B ^ᵗ .fvar x)) →
      Typing Γ (.abs A N) (.pi A B)
  /-- Pi type -/
  | pi (ρ : Finset Var) :
      Typing Γ A (.type k) →
      (∀ x ∉ ρ, Typing ({⟨x, A⟩} ∪ Γ) (B ^ᵗ .fvar x) (.type i)) →
      (i = k ∨ i = 0) →
      Typing Γ (.pi A B) (.type i)
  /-- Type universe -/
  | type : Typing Γ (.type s) (.type (s + 1))
  /-- β-conversion -/
  | conv : Typing Γ M A → A =β B → Typing Γ B (.type i) → Typing Γ M B

Cslib.Foundations.Syntax.HasBetaEquiv

• HasBetaEquiv (similar to HasAlphaEquiv) for the notation A =β B

class HasBetaEquiv (t : Type u) where
  /-- β-equivalence relation for type t. -/
  BetaEquiv : t → t → Prop

[chenson2018]

Hi, thanks for your interest in contributing!

Can I ask why the jump to CoC for this named representation of binding? It is a little uncommon to do this style at all, so there's not much else to build off yet. I was hoping that STLC and System F would get filled out first to work out any kinks before more complex type systems.

We are planning to add well scoped indices as an alternative in the next few months or so, but if your interest is formalizing CoC right now would you be interested in doing so in the locally nameless style? This would be much easier to review in comparison to what we already have and prior work in Rocq.

[matthunz]

Hey 👋 thanks so much for the feedback!

I wanted to go the named representation route at first because it felt more natural to me coming from functional programming but I'm definitely unsure of how to prove things like well-formedness with that approach.

I'd be thrilled if we can fit this in here somehow given the current plans, here's what I did for now:

• Changed to locally-nameless AST b3c0b23
• Added the requisite locally-closed and well-formed proofs 8a20752 13ec089

I think the biggest remaining features would now be reduction and the related proofs to tie everything together, which might be a somewhat significant undertaking 😅 happy to defer to your judgement on what the scope of this PR should be

[chenson2018]

Some of this looks good, in particular thank you for mostly following conventions from the System F formalization. There are a few important places however where I'm not sure about the definitions. Because these are tricky to get right I suggest closely following prior work like the formalization from Charguéraud I link below.

[chenson2018]

We probably want this to be ℕ → Term Var as well.

[chenson2018]

I would expect we reuse LocallyNameless.Context instead of this abbrev.

[chenson2018]

We should name this consistently as openRec and open' with the other typesystems.

[chenson2018]

For CoC, the variable σ is a term, as opposed to System F where it was a type. I'd update the variable names accordingly to use t₁ and t₂.

[chenson2018]

This is for decidable equality? I'd rather make this explicit as a typeclass parameter.

[chenson2018]

This definition looks very different from what I expected. See for instance the definition in the Rocq formalization I closely followed for other type systems.

[chenson2018]

I was expecting to see a mutual block also defining well-formed contexts.

[chenson2018]

I don't think this is right. Because of the dependent types aspect, we need a typing derivation before adding to the context, right?

[chenson2018]

I should have mentioned previously. This should use the reduction_sys attribute to get notation, because this is still reduction and not the equivalence (reflexive symmetric transitive closure), right? I would remove the HasBetaEquiv class and use this.