Logics and lambda calculi

Stream: Type theory

[Sky Wilshaw]

I'm starting a formalisation of logics and lambda calculi in Lean 4, and my hope is that it can be upstreamed to mathlib. The target is to formalise the beta-normal form theorem, the Church-Rosser theorem, and the unique typing theorem for all of the systems in Barendregt's lambda cube. I also want the underlying logical foundations to be general enough to model general noncommutative linear logics. I've written some base code here, I would greatly appreciate feedback! (Yaël recommended that I tag @Mario Carneiro)

import Mathlib.Tactic

structure Judgment (α β : Type _) where
  /-- The antecedents of the judgment. This is also called the context. -/
  left : List α
  /-- The consequent of the judgment. -/
  right : β

-- I don't know what priority this should be.
notation:10 l " ⊢ " r => Judgment.mk l r

/-- A deduction system, with given antecedent and consequent types,
assigns a type to each judgment, which is the type of proofs of that judgment.
If the universe parameter is `0`, the proofs of each judgment are propositions. -/
class DeductionSystem.{u} (α β : Type _) where
  proof : Judgment α β → Sort u

export DeductionSystem (proof)

variable [DeductionSystem α β]

/-- A deduction system has *permutation* if proofs are stable under permutation of the context. -/
class Permutation (α β : Type _) [DeductionSystem α β] where
  permute (Γ₁ : List α) (Γ₂ : List α) {C : β} (h : Γ₁ ~ Γ₂) :
    proof (Γ₁ ⊢ C) ≃ proof (Γ₂ ⊢ C)

export Permutation (permute)

section Permutation

variable [Permutation α β] {Γ Γ₁ Γ₂ : List α} {γ γ₁ γ₂ : α} {C : β}

/-- A way to cast between proofs where the contexts are equal only propositionally.
This has better computational properties than just using `Equiv.cast`. -/
def castProof (h : Γ₁ = Γ₂ := by simp) : proof (Γ₁ ⊢ C) ≃ proof (Γ₂ ⊢ C) :=
  permute Γ₁ Γ₂ (List.Perm.of_eq h)

def permuteSwap :
    proof (γ₁ :: γ₂ :: Γ ⊢ C) ≃ proof (γ₂ :: γ₁ :: Γ ⊢ C) :=
  permute _ _ (List.Perm.swap γ₂ γ₁ Γ)

def permuteMiddle :
    proof (Γ₁ ++ γ :: Γ₂ ⊢ C) ≃ proof (γ :: (Γ₁ ++ Γ₂) ⊢ C) :=
  permute _ _ List.perm_middle

def permuteAppend :
    proof (Γ₁ ++ Γ₂ ⊢ C) ≃ proof (Γ₂ ++ Γ₁ ⊢ C) :=
  permute _ _ (List.perm_append_comm)

end Permutation

/-- A deduction system has *weakening* if proofs are stable under increasing the context. -/
class Weakening (α β : Type _) [DeductionSystem α β] where
  weaken' (Γ₁ Γ₂ : List α) (C : β) :
    proof (Γ₁ ⊢ C) → proof (Γ₂ ++ Γ₁ ⊢ C)

/-- A deduction system has *contraction* if a duplicate hypothesis can be removed. -/
class Contraction (α β : Type _) [DeductionSystem α β] where
  contract' (Γ : List α) (γ : α) (C : β) (h : γ ∈ Γ) :
    proof (γ :: Γ₁ ⊢ C) → proof (Γ₁ ⊢ C)

export Contraction (contract')

/-- The *contraction* rule for multiple hypotheses. -/
def contract [Contraction α β] :
    (Γ₁ Γ₂ : List α) → (C : β) → (h : Γ₁ ⊆ Γ₂) →
    proof (Γ₁ ++ Γ₂ ⊢ C) → proof (Γ₂ ⊢ C)
  | [], _, _, _, pf => pf
  | γ :: Γ₁, Γ₂, C, h, pf =>
      contract Γ₁ Γ₂ C (by aesop) (contract' (Γ₁ ++ Γ₂) γ C (by aesop) pf)

/-- The *weakening* rule, expressed using contraction and permutation:
we can weaken the hypotheses of a proof to any superset of hypotheses.
Note that the list subset operation does not count multiplicity, so we need contraction. -/
def weaken [Weakening α β] [Permutation α β] [Contraction α β]
    (Γ₁ Γ₂ : List α) (C : β) (h : Γ₁ ⊆ Γ₂) :
    proof (Γ₁ ⊢ C) → proof (Γ₂ ⊢ C) :=
  contract Γ₁ Γ₂ C h ∘ permuteAppend ∘ Weakening.weaken' Γ₁ Γ₂ C

/-- Note: The `outParam` markers on this class ensure that typeclass synthesis depends on
the type of terms. This has the downside that we can't extend a `DeductionSystem α β`. -/
class TypeSystemData (α β : outParam <| Type _) (Λ : Type _) (V T : outParam <| Type _) where
  /-- A proposition representing the assertion that a variable has a given type. -/
  varTy : V → T → α
  /-- A proposition representing the assertion that a term has a given type. -/
  termTy : Λ → T → β

  /-- Each variable is naturally a term. -/
  var : V → Λ
  /-- The set of free variables of a term. -/
  free : Λ → Set V
  /-- Substitute a variable for a term inside another term. -/
  subst : V → Λ → Λ → Λ

export TypeSystemData (var free)

-- I don't know what priority these should be.
-- I also don't really like the elaboration of variable typing assertions.
notation:60 v " ∶[" Λ "] " τ => TypeSystemData.varTy Λ v τ
notation:60 t " ∶ " τ => TypeSystemData.termTy t τ
notation:80 t "[" v " := " s "]" => TypeSystemData.subst v s t

class TypeSystem (α β : outParam <| Type _) (Λ : Type _) (V T : outParam <| Type _)
    [DeductionSystem α β] extends TypeSystemData α β Λ V T where
  ax {v : V} : proof ([v ∶[Λ] τ] ⊢ var v ∶ τ)
  free_var : free (var v) = {v}
  subst_var : (var v)[v := t] = t
  subst_var_ne : v ≠ w → (var w)[v := t] = var w
  subst_eq_of_not_free : v ∉ free t → t[v := s] = t
  free_subst_of_free : v ∈ free t → free (t[v := s]) = (free t \ {v}) ∪ free s

export TypeSystem (free_var subst_var subst_var_ne subst_eq_of_not_free free_subst_of_free)

attribute [simp] free_var subst_var

variable [DeductionSystem α β] [TypeSystem α β Λ V T]

theorem free_subst_of_not_free {t : Λ} (h : v ∉ free t) : free (t[v := s]) = free t :=
  by rw [subst_eq_of_not_free h]

theorem free_subst_eq {t : Λ} :
    free (t[v := s]) = (free t \ {v}) ∪ {w ∈ free s | v ∈ free t} := by
  by_cases h : v ∈ free t
  · simp [free_subst_of_free, h]
  · simp [subst_eq_of_not_free, h]

theorem not_mem_free_of_subst {t : Λ} (h : v ∉ free s) : v ∉ free (t[v := s]) := by
  rw [free_subst_eq]
  simp_all

[Notification Bot]

This topic was moved here from #lean4 > Logics and lambda calculi by Mario Carneiro.

[Mario Carneiro]

I think designing meta-frameworks for logics and type systems is incredibly difficult, because so little of the work can actually be reused from one theory to another. It is way too easy to design a framework and then realize that it doesn't apply to type systems in the wild. For an example which is fresh on my mind, consider the lean 4 logic formalized here. Would this framework be able to accomodate it? I think not, because varTy and termTy are contextless (not to mention the more fundamental difference that it uses de bruijn variables and not named variables)

[Sky Wilshaw]

varTy is the type of some things that appear in a context, and termTy is a consequent of a judgment, so I think that isn't too big of an issue. We can use varTy assumptions to deduce termTys.

[Sky Wilshaw]

I also assumed that we wouldn't be able to properly define de Bruijn indexing in a meta-framework, because we don't know what the function types look like.

[Sky Wilshaw]

Also note that α and β don't just need to be comprised of varTy/termTy things - you can also put definitional equality assertions in those types.

[Sky Wilshaw]

I am a bit concerned about how portable results will actually be, though - I don't know what can really be proven in this generality.

[Sky Wilshaw]

I've had a look and I think that all of the typing rules in the paper version of #leantt can be represented in this framework.

[Mario Carneiro]

Sky Wilshaw said:

I also assumed that we wouldn't be able to properly define de Bruijn indexing in a meta-framework, because we don't know what the function types look like.

You don't need to know what function types look like to have a concept of lift and subst and how they interact

[Mario Carneiro]

I would be inclined to stay away from judgments, those are rather free form in practice

[Mario Carneiro]

except maybe for having something like a context with a weakening rule

[Mario Carneiro]

I would not do anything with "assumptions", this is part of the judgment

[Mario Carneiro]

I suspect what is really needed here is some metaprogramming facilities to autogenerate definitions and proofs for things like lift and subst

[Sky Wilshaw]

Mario Carneiro said:

I would not do anything with "assumptions", this is part of the judgment

I agree, I'm being a bit sloppy with my wording.

[Sky Wilshaw]

Mario Carneiro said:

I suspect what is really needed here is some metaprogramming facilities to autogenerate definitions and proofs for things like lift and subst

This sounds like it could be very useful.

[Mario Carneiro]

it might also be worth looking into Nominal Isabelle, which is a framework for doing formal metatheory, although it is built around "nominal types" which are based on the named variable approach, so it instead automates things like fresh variables and alpha equivalence

[Sky Wilshaw]

Sounds interesting, thanks for the pointer!

[Joachim Breitner]

Nominal Lean when? :-)

[Sky Wilshaw]

In light of the discussion above, I've designed a different system that I think is more amenable to actually proving things, but is a lot less general. Instead of building a lambda calculus up using typeclasses, I declare a collection of parameters at the start, and build a lambda calculus based on those parameters. We can then use the recursion principle for these lambda terms to actually prove concrete things.

import Mathlib.Tactic

/-- A collection of Boolean parameters that determine which features of the λ-calculus we construct
should be enabled. See `BoxIntegral.IntegrationParams` for an application of this idea that is
already in mathlib. -/
@[ext]
structure LambdaParams where
  /-- This λ-calculus has λ-abstractions and applications. -/
  lambda : Bool
  /-- This λ-calculus has binary products and projections. -/
  prod : Bool
  /-- This λ-calculus has binary coproducts and a case split construction. -/
  coprod : Bool
  /-- This λ-calculus has a unit type and a constructor for that element. -/
  unit : Bool
  /-- This λ-calculus has an empty type and a recursor for it. -/
  empty : Bool

/-- Types of terms in a λ-calculus with parameters `p` and primitive types `U`. -/
inductive LambdaType (p : LambdaParams) (U : Type _)
| prim    : U → LambdaType p U
| lambda  : p.lambda  → LambdaType p U → LambdaType p U → LambdaType p U
| prod    : p.prod    → LambdaType p U → LambdaType p U → LambdaType p U
| coprod  : p.coprod  → LambdaType p U → LambdaType p U → LambdaType p U
| unit    : p.unit    → LambdaType p U
| empty   : p.empty   → LambdaType p U

/-- Terms in a λ-calculus with parameters `p`, primitive types `U` and opaque constants `C`. -/
inductive LambdaTerm (p : LambdaParams) (U : Type _) (C : Type _) : Type _
/-- An opaque constant. -/
| const : C → LambdaTerm p U C
/-- A local variable of a given de Bruijn index. -/
| var : ℕ → LambdaTerm p U C
/-- A λ-abstraction. -/
| lambda : p.lambda → LambdaType p U → LambdaTerm p U C → LambdaTerm p U C
/-- A λ-application. -/
| app : p.lambda → LambdaTerm p U C → LambdaTerm p U C → LambdaTerm p U C
/-- The pairing operation. -/
| pair : p.prod → LambdaTerm p U C → LambdaTerm p U C → LambdaTerm p U C
/-- The left projection of a product. -/
| fst : p.prod → LambdaTerm p U C → LambdaTerm p U C
/-- The right projection of a product. -/
| snd : p.prod → LambdaTerm p U C → LambdaTerm p U C
/-- The left injection of a coproduct. The type of the right factor is also given. -/
| inl : p.coprod → LambdaType p U → LambdaTerm p U C → LambdaTerm p U C
/-- The right injection of a coproduct. The type of the left factor is also given. -/
| inr : p.coprod → LambdaType p U → LambdaTerm p U C → LambdaTerm p U C
/-- Case splitting. If the parameters are `l`, `r`, `x`, then this term β-reduces to `l t` if
`x = inl t`, and β-reduces to `r t` if `x = inr t`. This matches `Sum.rec`. -/
| case : p.coprod → LambdaTerm p U C → LambdaTerm p U C → LambdaTerm p U C → LambdaTerm p U C
/-- The inhabitant of the unit type. -/
| star : p.unit → LambdaTerm p U C
/-- The recursor for the empty type. This eliminates an element of `empty` into any given type. -/
| elim : p.empty → LambdaType p U → LambdaTerm p U C → LambdaTerm p U C

[Sky Wilshaw]

The typing relation is then defined with an additional parameter C -> LambdaType p U which declares the type of each opaque constant.