From 042be24ce5c9dfff0d5127e780d5c2e1a20658e2 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Wed, 13 Aug 2025 17:14:05 +0200 Subject: [PATCH 01/13] Add well-scoped Fsub --- .../LambdaCalculus/WellScoped/FSub.lean | 33 ++ .../WellScoped/FSub/Debruijn.lean | 118 +++++ .../WellScoped/FSub/RebindTheory/Core.lean | 63 +++ .../FSub/RebindTheory/TypeSystem.lean | 52 ++ .../WellScoped/FSub/Reduce.lean | 17 + .../WellScoped/FSub/RetypeTheory/Core.lean | 124 +++++ .../FSub/RetypeTheory/TypeSystem.lean | 44 ++ .../WellScoped/FSub/Substitution.lean | 2 + .../WellScoped/FSub/Substitution/Core.lean | 69 +++ .../FSub/Substitution/Properties.lean | 483 ++++++++++++++++++ .../WellScoped/FSub/Syntax.lean | 3 + .../WellScoped/FSub/Syntax/Context.lean | 32 ++ .../WellScoped/FSub/Syntax/Core.lean | 74 +++ .../WellScoped/FSub/Syntax/Subst.lean | 23 + .../FSub/TypeSoundness/Canonical.lean | 352 +++++++++++++ .../FSub/TypeSoundness/Preservation.lean | 42 ++ .../FSub/TypeSoundness/Progress.lean | 50 ++ .../WellScoped/FSub/TypeSystem.lean | 44 ++ 18 files changed, 1625 insertions(+) create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean new file mode 100644 index 00000000..01ed3080 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean @@ -0,0 +1,33 @@ +/- +# Type soundness of System F<: + +This is a mechanized type soundness proof of System F<: in what I call _well-scoped_ style. + +The main idea is to: +- Use intrinsically scoped de Bruijn indices. Specifically, de Bruijn indices are indexed by a signature describing available binders in the type context. This way, syntactic constructs are well-scoped (and therefore well-formed) by construction. +- Use context morphisms, which are mappings between type contexts that preserve types. This way, all theorems concerning context operations (weakening, narrowing, substitution) can be proven in a uniform way. + +There are two kinds of context morphisms where the latter depends on the former. +- The first is _rebinding morphisms_. A rebinding morphism `f` from `Γ` to `Δ` maps each `x:T ∈ Γ` to a corresponding binder `f(x) : f(T) ∈ Δ`. Then, we show that typing is preserved under such morphisms. +- The second is _retypeing morphisms_. A retypeing morphism `g` from `Γ` to `Δ` maps each `x: T ∈ Γ` into a typing derivation `Δ ⊢ g(x) : g(T)`. This is of course stronger than the first kind, and its proof relies on that of the first kind. We show that typing is preserved under this kind of morphisms too. + +With this context morphism infrastructure, we can prove a variety of theorems regarding context manipulation, including weakening, narrowing, substitution, and any other context operations that can be formulated as a context morphism. +-/ + +-- This module defines the intrinsically scoped de Bruijn indices. +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Debruijn + +-- The following modules define Syetem F<:. +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Reduce + +-- The following modules define context morphisms and prove their theory. +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.Core +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.TypeSystem +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem + +-- Main type soundness results. +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Preservation +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Progress diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean new file mode 100644 index 00000000..efa2cb0a --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean @@ -0,0 +1,118 @@ +import Mathlib.Tactic + +inductive Sig : Type where +| empty : Sig +| cons_var : Sig -> Sig +| cons_tvar : Sig -> Sig + +@[simp] +instance : EmptyCollection Sig := ⟨Sig.empty⟩ + +theorem Sig.empty_eq : {} = Sig.empty := rfl + +postfix:50 ",x" => Sig.cons_var +postfix:50 ",X" => Sig.cons_tvar + +inductive Var : Sig -> Type where +| here : Var (s,x) +| there_var : Var s -> Var (s,x) +| there_tvar : Var s -> Var (s,X) + +inductive TVar : Sig -> Type where +| here : TVar (s,X) +| there_var : TVar s -> TVar (s,x) +| there_tvar : TVar s -> TVar (s,X) + +structure Rename (s1 s2 : Sig) where + var : Var s1 -> Var s2 + tvar : TVar s1 -> TVar s2 + +def Rename.liftVar (f : Rename s1 s2) : Rename (s1,x) (s2,x) := by + constructor + case var => + intro x; cases x + case here => exact .here + case there_var x0 => exact .there_var (f.var x0) + case tvar => + intro X; cases X + case there_var X0 => exact .there_var (f.tvar X0) + +def Rename.liftTVar (f : Rename s1 s2) : Rename (s1,X) (s2,X) := by + constructor + case tvar => + intro X; cases X + case here => exact .here + case there_tvar X0 => exact .there_tvar (f.tvar X0) + case var => + intro x; cases x + case there_tvar x0 => exact .there_tvar (f.var x0) + +def Rename.succVar : Rename s1 (s1,x) := + { var := fun x => x.there_var, tvar := fun X => X.there_var } + +def Rename.succTVar : Rename s1 (s1,X) := + { var := fun x => x.there_tvar, tvar := fun X => X.there_tvar } + +def Rename.id : Rename s s := + { var := fun x => x, tvar := fun X => X } + +def Rename.comp (f1 : Rename s1 s2) (f2 : Rename s2 s3) : Rename s1 s3 := + { var := fun x => f2.var (f1.var x), tvar := fun X => f2.tvar (f1.tvar X) } + +theorem Rename.funext {f g : Rename s1 s2} + (var : ∀ x, f.var x = g.var x) + (tvar : ∀ X, f.tvar X = g.tvar X) : f = g := by + cases f; cases g + simp + constructor + { funext x; aesop } + { funext X; aesop } + +@[simp] +theorem Rename.id_liftVar_eq_id : Rename.id.liftVar = (Rename.id (s:=(s,x))) := by + apply Rename.funext + case var => intro x; cases x <;> rfl + case tvar => intro X; cases X; rfl + +@[simp] +theorem Rename.id_liftTVar_eq_id : Rename.id.liftTVar = (Rename.id (s:=(s,X))) := by + apply Rename.funext + case var => intro x; cases x; rfl + case tvar => intro X; cases X <;> rfl + +theorem Rename.comp_liftTVar {f1 : Rename s1 s2} {f2 : Rename s2 s3} : + (f1.comp f2).liftTVar = f1.liftTVar.comp f2.liftTVar := by + apply Rename.funext + case var => intro x; cases x; rfl + case tvar => intro X; cases X <;> rfl + +theorem Rename.comp_liftVar {f1 : Rename s1 s2} {f2 : Rename s2 s3} : + (f1.comp f2).liftVar = f1.liftVar.comp f2.liftVar := by + apply Rename.funext + case var => intro x; cases x <;> rfl + case tvar => intro X; cases X; rfl + +theorem Rename.rename_succVar_comm {f : Rename s1 s2} : + (f.comp Rename.succVar) = Rename.succVar.comp f.liftVar := by + apply Rename.funext + case var => intro x; rfl + case tvar => intro X; rfl + +theorem Rename.rename_succTVar_comm {f : Rename s1 s2} : + (f.comp Rename.succTVar) = Rename.succTVar.comp f.liftTVar := by + apply Rename.funext + case var => intro x; rfl + case tvar => intro X; rfl + +def Sig.append : Sig -> Sig -> Sig +| s1, .empty => s1 +| s1, .cons_var s2 => .cons_var (s1.append s2) +| s1, .cons_tvar s2 => .cons_tvar (s1.append s2) + +@[simp] +instance : Append Sig := ⟨Sig.append⟩ + +def Rename.lift : Rename s1 s2 -> (s : Sig) -> Rename (s1 ++ s) (s2 ++ s) +| f, .empty => f +| f, .cons_var s => (f.lift s).liftVar +| f, .cons_tvar s => (f.lift s).liftTVar diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean new file mode 100644 index 00000000..1b5f2467 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean @@ -0,0 +1,63 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax + +structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where + var : ∀ x T, Ctx.LookupVar Γ x T -> Ctx.LookupVar Δ (f.var x) (T.rename f) + tvar : ∀ X T, Ctx.LookupTVar Γ X T -> Ctx.LookupTVar Δ (f.tvar X) (T.rename f) + +def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.rename f) := by + constructor + case var => + intro x P hb + cases hb + case here => simp [<-Ty.rename_succVar_comm]; constructor + case there_var hb => + simp [<-Ty.rename_succVar_comm] + constructor + apply ρ.var _ _ hb + case tvar => + intro X S hb + cases hb + case there_var hb => + simp [<-Ty.rename_succVar_comm] + constructor + apply ρ.tvar _ _ hb + +def Rebind.liftTVar (ρ : Rebind Γ f Δ) : Rebind (Γ,X<:T) (f.liftTVar) (Δ,X<:T.rename f) := by + constructor + case tvar => + intro X S hb + cases hb + case here => simp [<-Ty.rename_succTVar_comm]; constructor + case there_tvar hb => + simp [<-Ty.rename_succTVar_comm] + constructor + apply ρ.tvar _ _ hb + case var => + intro x P hb + cases hb + case there_tvar hb => + simp [<-Ty.rename_succTVar_comm] + constructor + apply ρ.var _ _ hb + +def Rebind.succVar : Rebind Γ Rename.succVar (Γ,x:T) := by + constructor + case var => + intro x P hb + constructor + exact hb + case tvar => + intro X S hb + constructor + exact hb + +def Rebind.succTVar : Rebind Γ Rename.succTVar (Γ,X<:T) := by + constructor + case tvar => + intro X S hb + constructor + exact hb + case var => + intro x P hb + constructor + exact hb diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean new file mode 100644 index 00000000..e8ff80ec --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean @@ -0,0 +1,52 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.Core +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties + +theorem Subtyp.rebind {f : Rename s1 s2} + (hs : Subtyp Γ T1 T2) + (ρ : Rebind Γ f Δ) : + Subtyp Δ (T1.rename f) (T2.rename f) := by + induction hs generalizing s2 + case top => constructor + case refl => constructor + case trans => + apply Subtyp.trans <;> aesop + case tvar hb => + apply Subtyp.tvar + apply ρ.tvar _ _ hb + case arrow ih1 ih2 => + apply Subtyp.arrow + { apply ih1 ρ } + { apply ih2 ρ } + case poly ih1 ih2 => + apply Subtyp.poly + { apply ih1 ρ } + { apply ih2 ρ.liftTVar } + +theorem HasType.rebind {f : Rename s1 s2} + (ht : HasType Γ t T) + (ρ : Rebind Γ f Δ) : + HasType Δ (t.rename f) (T.rename f) := by + induction ht generalizing s2 + case var hb => + apply HasType.var + apply ρ.var _ _ hb + case sub hsub _ ih => + apply sub + { apply hsub.rebind ρ } + { apply ih ρ } + case abs ih => + apply HasType.abs + simp [Ty.rename_succVar_comm] + apply ih ρ.liftVar + case tabs ih => + apply HasType.tabs + apply ih ρ.liftTVar + case app ih1 ih2 => + apply HasType.app + { apply ih1 ρ } + { apply ih2 ρ } + case tapp ih => + simp [Ty.open_tvar_rename_comm] + apply tapp + aesop diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean new file mode 100644 index 00000000..89333fea --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean @@ -0,0 +1,17 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax + +inductive Reduce : Exp s -> Exp s -> Prop where +| red_app_fun : + Reduce e1 e1' -> + Reduce (.app e1 e2) (.app e1' e2) +| red_app_arg : + Exp.IsVal v1 -> + Reduce e2 e2' -> + Reduce (.app v1 e2) (.app v1 e2') +| red_app : + Reduce (.app (.abs T e1) e2) (e1.open_var e2) +| red_tapp_fun : + Reduce e e' -> + Reduce (.tapp e T) (.tapp e' T) +| red_tapp : + Reduce (.tapp (.tabs T' e) T) (e.open_tvar T) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean new file mode 100644 index 00000000..4863f858 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean @@ -0,0 +1,124 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.TypeSystem + +structure Retype (Γ : Ctx s1) (σ : Subst s1 s2) (Δ : Ctx s2) where + var : + ∀ x T, + Γ.LookupVar x T -> + HasType Δ (σ.var x) (T.subst σ) + + tvar : + ∀ X S, + Γ.LookupTVar X S -> + Subtyp Δ (σ.tvar X) (S.subst σ) + +def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P.subst σ) := by + constructor + case var => + intro x T hb + cases hb + case here => + apply HasType.var + simp [<-Ty.subst_succVar_comm_base] + constructor + case there_var hb0 => + have h0 := ρ.var _ _ hb0 + simp [<-Ty.subst_succVar_comm_base] + apply h0.rebind Rebind.succVar + case tvar => + intro X S hb + cases hb + case there_var hb0 => + have h0 := ρ.tvar _ _ hb0 + simp [<-Ty.subst_succVar_comm_base] + apply h0.rebind Rebind.succVar + +def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ,X<:P.subst σ) := by + constructor + case var => + intro x T hb + cases hb + case there_tvar hb0 => + have h0 := ρ.var _ _ hb0 + simp [<-Ty.subst_succTVar_comm_base] + apply h0.rebind Rebind.succTVar + case tvar => + intro X S hb + cases hb + case here => + apply Subtyp.tvar + simp [<-Ty.subst_succTVar_comm_base] + constructor + case there_tvar hb0 => + have h0 := ρ.tvar _ _ hb0 + simp [<-Ty.subst_succTVar_comm_base] + apply h0.rebind Rebind.succTVar + +def Retype.open_var + (ht : HasType Γ e T) : + Retype (Γ,x:T) (Subst.open_var e) Γ := by + constructor + case var => + intro x T hb + cases hb + case here => + simp [Ty.rename_succVar_open_var] + exact ht + case there_var hb0 => + simp [Ty.rename_succVar_open_var] + apply HasType.var + exact hb0 + case tvar => + intro X S hb + cases hb + case there_var hb0 => + simp [Ty.rename_succVar_open_var] + apply Subtyp.tvar + exact hb0 + +def Retype.narrow_tvar + (hs : Subtyp Γ S1 S2) : + Retype (Γ,X<:S2) Subst.id (Γ,X<:S1) := by + constructor + case var => + intro x T hb + simp [Ty.subst_id] + constructor + cases hb + constructor + trivial + case tvar => + intro X S hb + cases hb + case here => + apply Subtyp.trans + { apply Subtyp.tvar; constructor } + { simp [Ty.subst_id]; apply hs.rebind Rebind.succTVar } + case there_tvar hb0 => + apply Subtyp.tvar + simp [Ty.subst_id] + constructor + exact hb0 + +def Retype.open_tvar + (hs : Subtyp Γ R S) : + Retype (Γ,X<:S) (Subst.open_tvar R) Γ := by + constructor + case var => + intro x T hb + cases hb + case there_tvar hb0 => + simp [Ty.rename_succTVar_open_tvar] + apply HasType.var + exact hb0 + case tvar => + intro X0 S0 hb + cases hb + case here => + simp [Ty.rename_succTVar_open_tvar] + exact hs + case there_tvar hb0 => + simp [Ty.rename_succTVar_open_tvar] + apply Subtyp.tvar + exact hb0 diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean new file mode 100644 index 00000000..045176d1 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean @@ -0,0 +1,44 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core + +def Subtyp.retype {σ : Subst s1 s2} + (hsub : Subtyp Γ T1 T2) + (ρ : Retype Γ σ Δ) : + Subtyp Δ (T1.subst σ) (T2.subst σ) := by + induction hsub generalizing s2 + case top => constructor + case refl => constructor + case trans ih1 ih2 => + apply Subtyp.trans <;> aesop + case tvar hb => + apply ρ.tvar _ _ hb + case arrow => apply arrow <;> aesop + case poly ih1 ih2 => + apply poly + { apply ih1 ρ } + { apply ih2 ρ.liftTVar } + +theorem HasType.retype {σ : Subst s1 s2} + (ht : HasType Γ t T) + (ρ : Retype Γ σ Δ) : + HasType Δ (t.subst σ) (T.subst σ) := by + induction ht generalizing s2 + case var hb => apply ρ.var _ _ hb + case sub hsub _ ih => + apply sub + { apply hsub.retype ρ } + { apply ih ρ } + case abs ih => + apply HasType.abs + simp [Ty.subst_succVar_comm_base] + apply ih ρ.liftVar + case tabs ih => + apply HasType.tabs + apply ih ρ.liftTVar + case app ih1 ih2 => + apply HasType.app + { apply ih1 ρ } + { apply ih2 ρ } + case tapp ih => + simp [Ty.open_tvar_subst_comm] + apply HasType.tapp + apply ih ρ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean new file mode 100644 index 00000000..3ffaee7d --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean @@ -0,0 +1,2 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean new file mode 100644 index 00000000..b4c40fb7 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean @@ -0,0 +1,69 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core + +structure Subst (s1 s2 : Sig) where + var : Var s1 -> Exp s2 + tvar : TVar s1 -> Ty s2 + +def Subst.liftVar (s : Subst s1 s2) : Subst (s1,x) (s2,x) := by + constructor + case var => + intro x; cases x + case here => exact .var .here + case there_var x0 => exact (s.var x0).rename Rename.succVar + case tvar => + intro X; cases X + case there_var X0 => exact (s.tvar X0).rename Rename.succVar + +def Subst.liftTVar (s : Subst s1 s2) : Subst (s1,X) (s2,X) := by + constructor + case tvar => + intro X; cases X + case here => exact .tvar .here + case there_tvar X0 => exact (s.tvar X0).rename Rename.succTVar + case var => + intro x; cases x + case there_tvar x0 => exact (s.var x0).rename Rename.succTVar + +def Subst.open_var (e : Exp s) : Subst (s,x) s := by + constructor + case var => + intro x; cases x + case here => exact e + case there_var x0 => exact .var x0 + case tvar => + intro X; cases X + case there_var X0 => exact .tvar X0 + +def Subst.open_tvar (T : Ty s) : Subst (s,X) s := by + constructor + case var => + intro x; cases x + case there_tvar x0 => exact .var x0 + case tvar => + intro X; cases X + case here => exact T + case there_tvar X0 => exact .tvar X0 + +def Rename.asSubst (f : Rename s1 s2) : Subst s1 s2 := by + constructor + case var => intro x; exact .var (f.var x) + case tvar => intro X; exact .tvar (f.tvar X) + +theorem Subst.funext {σ1 σ2 : Subst s1 s2} + (var : ∀ x, σ1.var x = σ2.var x) + (tvar : ∀ X, σ1.tvar X = σ2.tvar X) : σ1 = σ2 := by + cases σ1; cases σ2 + simp + constructor + { funext x; aesop } + { funext X; aesop } + +def Subst.lift : Subst s1 s2 -> (s : Sig) -> Subst (s1 ++ s) (s2 ++ s) +| σ, .empty => σ +| σ, .cons_var s => (σ.lift s).liftVar +| σ, .cons_tvar s => (σ.lift s).liftTVar + +def Subst.id : Subst s s := by + constructor + case var => intro x; exact .var x + case tvar => intro X; exact .tvar X diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean new file mode 100644 index 00000000..09ec22cc --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean @@ -0,0 +1,483 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Subst + +def Subst.comp (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : Subst s1 s3 := by + constructor + case var => + intro x; exact (σ1.var x).subst σ2 + case tvar => + intro X; exact (σ1.tvar X).subst σ2 + +theorem Subst.tvar_there_var_liftVar {σ : Subst s1 s2} : + (σ.liftVar.tvar (.there_var X)) = (σ.tvar X).rename Rename.succVar := rfl + +theorem Subst.tvar_there_tvar_liftTVar {σ : Subst s1 s2} : + (σ.liftTVar.tvar (.there_tvar X)) = (σ.tvar X).rename Rename.succTVar := rfl + +theorem Subst.var_there_tvar_liftTVar {σ : Subst s1 s2} : + (σ.liftTVar.var (.there_tvar x)) = (σ.var x).rename Rename.succTVar := rfl + +theorem Ty.tvar_subst_succVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) : + ((tvar X).subst (σ.lift s0)).rename (Rename.succVar.lift s0) = + ((tvar X).rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by + induction s0 + case empty => rfl + case cons_var s0 ih => + cases X + case there_var X0 => + simp [Subst.lift, Ty.subst] + conv => lhs; simp [Subst.liftVar] + conv => + rhs; simp [Ty.rename, Rename.lift, Rename.liftVar] + simp [Ty.subst] + simp [Subst.tvar_there_var_liftVar] + simp [Rename.lift] + simp [<-Ty.rename_succVar_comm] + congr + exact (ih (X:=X0)) + case cons_tvar s0 ih => + cases X + case here => rfl + case there_tvar X0 => + conv => lhs; simp [Subst.lift, Ty.subst] + conv => lhs; simp [Subst.liftTVar, Rename.lift] + simp [<-Ty.rename_succTVar_comm] + congr + exact (ih (X:=X0)) + +theorem Ty.tvar_subst_succTVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) : + ((tvar X).subst (σ.lift s0)).rename (Rename.succTVar.lift s0) = + ((tvar X).rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by + induction s0 + case empty => rfl + case cons_var s0 ih => + cases X + case there_var X0 => + conv => lhs; simp [Subst.lift, Ty.subst] + conv => lhs; simp [Subst.liftVar, Rename.lift] + simp [<-Ty.rename_succVar_comm] + congr + exact (ih (X:=X0)) + case cons_tvar s0 ih => + cases X + case here => rfl + case there_tvar X0 => + conv => lhs; simp [Subst.lift, Ty.subst] + conv => lhs; simp [Subst.liftTVar, Rename.lift] + simp [<-Ty.rename_succTVar_comm] + congr + exact (ih (X:=X0)) + +theorem Ty.subst_succVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) : + (T.subst (σ.lift s0)).rename (Rename.succVar.lift s0) = + (T.rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by + match T with + | .top => rfl + | .tvar X => simp [Ty.tvar_subst_succVar_comm] + | .arrow T1 T2 => + have ih1 := Ty.subst_succVar_comm (T:=T1) (σ:=σ) + have ih2 := Ty.subst_succVar_comm (T:=T2) (σ:=σ) + simp [Ty.subst, Ty.rename] + simp [ih1, ih2] + | .poly T1 T2 => + have ih1 := Ty.subst_succVar_comm (T:=T1) (σ:=σ) + have ih2 := Ty.subst_succVar_comm (s0:=s0,X) (T:=T2) (σ:=σ) + simp [Ty.subst, Ty.rename] + simp [ih1] + exact ih2 + +theorem Ty.subst_succTVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) : + (T.subst (σ.lift s0)).rename (Rename.succTVar.lift s0) = + (T.rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by + match T with + | .top => rfl + | .tvar X => simp [Ty.tvar_subst_succTVar_comm] + | .arrow T1 T2 => + have ih1 := Ty.subst_succTVar_comm (T:=T1) (σ:=σ) + have ih2 := Ty.subst_succTVar_comm (T:=T2) (σ:=σ) + simp [Ty.subst, Ty.rename] + simp [ih1, ih2] + | .poly T1 T2 => + have ih1 := Ty.subst_succTVar_comm (T:=T1) (σ:=σ) + have ih2 := Ty.subst_succTVar_comm (s0:=s0,X) (T:=T2) (σ:=σ) + simp [Ty.subst, Ty.rename] + simp [ih1] + exact ih2 + +theorem Ty.subst_succVar_comm_base {T : Ty s1} (σ : Subst s1 s2) : + (T.subst σ).rename Rename.succVar = (T.rename Rename.succVar).subst (σ.liftVar) := by + exact Ty.subst_succVar_comm (T:=T) (σ:=σ) (s0:=Sig.empty) + +theorem Ty.subst_succTVar_comm_base {T : Ty s1} (σ : Subst s1 s2) : + (T.subst σ).rename Rename.succTVar = (T.rename Rename.succTVar).subst (σ.liftTVar) := by + exact Ty.subst_succTVar_comm (T:=T) (σ:=σ) (s0:=Sig.empty) + +theorem Exp.rename_succTVar_comm {e : Exp s1} {f : Rename s1 s2} : + (e.rename f).rename Rename.succTVar = + (e.rename Rename.succTVar).rename f.liftTVar := by + simp [Exp.rename_comp, Rename.rename_succTVar_comm] + +theorem Exp.rename_succVar_comm {e : Exp s1} {f : Rename s1 s2} : + (e.rename f).rename Rename.succVar = + (e.rename Rename.succVar).rename f.liftVar := by + simp [Exp.rename_comp, Rename.rename_succVar_comm] + +theorem Exp.var_subst_succTVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) : + ((var x).subst (σ.lift s0)).rename (Rename.succTVar.lift s0) = + ((var x).rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by + induction s0 + case empty => rfl + case cons_var s0 ih => + cases x + case here => rfl + case there_var x0 => + conv => lhs; simp [Subst.lift, Exp.subst] + conv => lhs; simp [Subst.liftVar, Rename.lift] + simp [<-Exp.rename_succVar_comm] + congr + exact (ih (x:=x0)) + case cons_tvar s0 ih => + cases x + case there_tvar x0 => + conv => lhs; simp [Subst.liftTVar] + conv => lhs; simp [Subst.liftVar, Subst.lift, Rename.lift] + conv => lhs; simp [Exp.subst, Subst.liftTVar] + simp [<-Exp.rename_succTVar_comm] + congr + exact (ih (x:=x0)) + +theorem Exp.var_subst_succVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) : + ((var x).subst (σ.lift s0)).rename (Rename.succVar.lift s0) = + ((var x).rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by + induction s0 + case empty => rfl + case cons_var s0 ih => + cases x + case here => rfl + case there_var x0 => + conv => lhs; simp [Subst.lift, Exp.subst] + conv => lhs; simp [Subst.liftVar, Rename.lift] + simp [<-Exp.rename_succVar_comm] + congr + exact (ih (x:=x0)) + case cons_tvar s0 ih => + cases x + case there_tvar x0 => + conv => lhs; simp [Subst.lift, Exp.subst] + conv => lhs; simp [Subst.liftTVar, Rename.lift] + simp [<-Exp.rename_succTVar_comm] + congr + exact (ih (x:=x0)) + +theorem Exp.subst_succTVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) : + (e.subst (σ.lift s0)).rename (Rename.succTVar.lift s0) = + (e.rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by + match e with + | .var x => simp [Exp.var_subst_succTVar_comm] + | .abs A t => + have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ) + have ih2 := Exp.subst_succTVar_comm (s0:=s0,x) (e:=t) (σ:=σ) + simp [Exp.subst, Exp.rename] + simp [ih1] + congr + | .tabs A t => + have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ) + have ih2 := Exp.subst_succTVar_comm (s0:=s0,X) (e:=t) (σ:=σ) + simp [Exp.subst, Exp.rename, ih1] + congr + | .app t1 t2 => + have ih1 := Exp.subst_succTVar_comm (e:=t1) (σ:=σ) + have ih2 := Exp.subst_succTVar_comm (e:=t2) (σ:=σ) + simp [Exp.subst, Exp.rename] + simp [ih1, ih2] + | .tapp t A => + have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ) + have ih2 := Exp.subst_succTVar_comm (s0:=s0) (e:=t) (σ:=σ) + simp [Exp.subst, Exp.rename, ih1, ih2] + +theorem Exp.subst_succVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) : + (e.subst (σ.lift s0)).rename (Rename.succVar.lift s0) = + (e.rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by + match e with + | .var x => simp [Exp.var_subst_succVar_comm] + | .abs A t => + have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ) + have ih2 := Exp.subst_succVar_comm (s0:=s0,x) (e:=t) (σ:=σ) + simp [Exp.subst, Exp.rename] + simp [ih1] + congr + | .tabs A t => + have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ) + have ih2 := Exp.subst_succVar_comm (s0:=s0,X) (e:=t) (σ:=σ) + simp [Exp.subst, Exp.rename, ih1] + congr + | .app t1 t2 => + have ih1 := Exp.subst_succVar_comm (e:=t1) (σ:=σ) + have ih2 := Exp.subst_succVar_comm (e:=t2) (σ:=σ) + simp [Exp.subst, Exp.rename, ih1, ih2] + | .tapp t A => + have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ) + have ih2 := Exp.subst_succVar_comm (s0:=s0) (e:=t) (σ:=σ) + simp [Exp.subst, Exp.rename, ih1, ih2] + +theorem Subst.liftTVar_comp {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : + (σ1.comp σ2).liftTVar = σ1.liftTVar.comp σ2.liftTVar := by + apply Subst.funext + case var => + intro x; cases x + case there_tvar x0 => + simp [Subst.comp, Subst.liftTVar] + simpa [Subst.lift, Rename.lift] using + (Exp.subst_succTVar_comm (s0:=Sig.empty) (σ:=σ2)) + case tvar => + intro X; cases X + case here => rfl + case there_tvar X0 => + simp [Subst.comp, Subst.liftTVar] + simpa [Subst.lift, Rename.lift] using + (Ty.subst_succTVar_comm (s0:=Sig.empty) (T:=σ1.tvar X0) (σ:=σ2)) + +theorem Subst.liftVar_comp {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : + (σ1.comp σ2).liftVar = σ1.liftVar.comp σ2.liftVar := by + apply Subst.funext + case var => + intro x; cases x + case there_var x0 => + simp [Subst.comp, Subst.liftVar] + simpa [Subst.lift, Rename.lift] using + (Exp.subst_succVar_comm (s0:=Sig.empty) (σ:=σ2)) + case here => rfl + case tvar => + intro X; cases X + case there_var X0 => + simp [Subst.comp] + simpa [Subst.lift, Rename.lift] using + (Ty.subst_succVar_comm (s0:=Sig.empty) (T:=σ1.tvar X0) (σ:=σ2)) + +theorem Ty.subst_comp {T : Ty s1} (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : + (T.subst σ1).subst σ2 = T.subst (σ1.comp σ2) := by + induction T generalizing s2 s3 + case top => rfl + case tvar X => rfl + case arrow T1 T2 ih1 ih2 => + simp [Ty.subst] + simp [ih1, ih2] + case poly T1 T2 ih1 ih2 => + simp [Ty.subst] + simp [ih1] + simp [Subst.liftTVar_comp] + simp [ih2] + +theorem Exp.subst_comp {e : Exp s1} (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : + (e.subst σ1).subst σ2 = e.subst (σ1.comp σ2) := by + induction e generalizing s2 s3 + case var x => rfl + case abs A t ih => + simp [Exp.subst] + simp [Ty.subst_comp] + simp [Subst.liftVar_comp] + simp [ih] + case tabs A t ih => + simp [Exp.subst] + simp [Ty.subst_comp] + simp [Subst.liftTVar_comp] + simp [ih] + case app t1 t2 ih1 ih2 => + simp [Exp.subst] + simp [ih1] + simp [ih2] + case tapp t A ih => + simp [Exp.subst] + simp [Ty.subst_comp] + simp [ih] + +theorem Rename.asSubst_liftTVar_comm {f : Rename s1 s2} : + (f.asSubst).liftTVar = f.liftTVar.asSubst := by + apply Subst.funext + case var => + intro x; cases x + case there_tvar x0 => rfl + case tvar => + intro X; cases X + case here => rfl + case there_tvar X0 => rfl + +theorem Rename.asSubst_liftVar_comm {f : Rename s1 s2} : + (f.asSubst).liftVar = f.liftVar.asSubst := by + apply Subst.funext + case var => + intro x; cases x + case here => rfl + case there_var x0 => rfl + case tvar => intro X; cases X; rfl + +theorem Ty.subst_asSubst {T : Ty s1} {f : Rename s1 s2} : + T.subst f.asSubst = T.rename f := by + induction T generalizing s2 + case top => rfl + case tvar => rfl + case arrow T1 T2 ih1 ih2 => simp [Ty.subst, Ty.rename, ih1, ih2] + case poly T1 T2 ih1 ih2 => + simp [Ty.subst, Ty.rename] + simp [ih1] + simp [Rename.asSubst_liftTVar_comm] + simp [ih2] + +theorem Exp.subst_asSubst {e : Exp s1} {f : Rename s1 s2} : + e.subst f.asSubst = e.rename f := by + induction e generalizing s2 + case var x => rfl + case abs A t ih => + simp [Exp.subst, Exp.rename, Ty.subst_asSubst] + simp [Rename.asSubst_liftVar_comm] + simp [ih] + case tabs A t ih => + simp [Exp.subst, Exp.rename, Ty.subst_asSubst] + simp [Rename.asSubst_liftTVar_comm] + simp [ih] + case app t1 t2 ih1 ih2 => + simp [Exp.subst, Exp.rename, ih1, ih2] + case tapp t A ih => + simp [Exp.subst, Exp.rename, Ty.subst_asSubst] + simp [ih] + +theorem Subst.id_liftVar : + (Subst.id (s:=s)).liftVar = Subst.id := by + apply Subst.funext + case var => intro x; cases x <;> rfl + case tvar => intro X; cases X; rfl + +theorem Subst.id_liftTVar : + (Subst.id (s:=s)).liftTVar = Subst.id := by + apply Subst.funext + case var => intro x; cases x; rfl + case tvar => intro X; cases X <;> rfl + +theorem Ty.subst_id {T : Ty s} : T.subst Subst.id = T := by + induction T + case top => rfl + case tvar => rfl + case arrow T1 T2 ih1 ih2 => + simp [Ty.subst, ih1, ih2] + case poly T1 T2 ih1 ih2 => + simp [Ty.subst, ih1] + simp [Subst.id_liftTVar] + simp [ih2] + +theorem Exp.subst_id {e : Exp s} : e.subst Subst.id = e := by + induction e + case var x => rfl + case abs A t ih => + simp [Exp.subst, Ty.subst_id] + simp [Subst.id_liftVar] + simp [ih] + case tabs A t ih => + simp [Exp.subst, Ty.subst_id] + simp [Subst.id_liftTVar] + simp [ih] + case app t1 t2 ih1 ih2 => + simp [Exp.subst, ih1, ih2] + case tapp t A ih => + simp [Exp.subst, Ty.subst_id] + simp [ih] + +theorem Subst.open_tvar_rename_comm {T : Ty s} {f : Rename s s'} : + (Subst.open_tvar T).comp (f.asSubst) + = f.liftTVar.asSubst.comp (Subst.open_tvar (T.rename f)) := by + apply Subst.funext + case var => + intro x + cases x + case there_tvar x0 => rfl + case tvar => + intro X + cases X + case here => + simp [Subst.comp] + conv => lhs; simp [Subst.open_tvar] + conv => + rhs; simp [Rename.asSubst, Rename.liftTVar, Ty.subst] + simp [Subst.open_tvar] + simp [Ty.subst_asSubst] + case there_tvar X0 => rfl + +theorem Ty.open_tvar_rename_comm {T : Ty (s,X)} {U : Ty s} {f : Rename s s'} : + (T.open_tvar U).rename f = (T.rename f.liftTVar).open_tvar (U.rename f) := by + simp [Ty.open_tvar, <-Ty.subst_asSubst] + simp [Ty.subst_comp] + simp [Subst.open_tvar_rename_comm] + simp [Ty.subst_asSubst] + +theorem Subst.succTVar_open_tvar {T : Ty s} : + Rename.succTVar.asSubst.comp (Subst.open_tvar T) = Subst.id := by + apply Subst.funext + case var => intro x; rfl + case tvar => intro X; rfl + +theorem Exp.rename_succTVar_open_tvar {e : Exp s} : + (e.rename Rename.succTVar).subst (Subst.open_tvar X) = + e := by + simp [<-Exp.subst_asSubst] + simp [Exp.subst_comp] + simp [Subst.succTVar_open_tvar] + simp [Exp.subst_id] + +theorem Ty.rename_succTVar_open_tvar {T : Ty s} : + (T.rename Rename.succTVar).subst (Subst.open_tvar X) = + T := by + simp [<-Ty.subst_asSubst] + simp [Ty.subst_comp] + simp [Subst.succTVar_open_tvar] + simp [Ty.subst_id] + +theorem Subst.succVar_open_var {e : Exp s} : + Rename.succVar.asSubst.comp (Subst.open_var e) = Subst.id := by + apply Subst.funext + case var => intro x; rfl + case tvar => intro X; rfl + +theorem Exp.rename_succVar_open_var {e : Exp s} : + (e.rename Rename.succVar).subst (Subst.open_var X) = + e := by + simp [<-Exp.subst_asSubst] + simp [Exp.subst_comp] + simp [Subst.succVar_open_var] + simp [Exp.subst_id] + +theorem Ty.rename_succVar_open_var {T : Ty s} : + (T.rename Rename.succVar).subst (Subst.open_var X) = + T := by + simp [<-Ty.subst_asSubst] + simp [Ty.subst_comp] + simp [Subst.succVar_open_var] + simp [Ty.subst_id] + +theorem Subst.open_tvar_subst_comm {T : Ty s} {σ : Subst s s'} : + (Subst.open_tvar T).comp σ = σ.liftTVar.comp (Subst.open_tvar (T.subst σ)) := by + apply Subst.funext + case var => + intro x + cases x + conv => lhs; simp [Subst.comp, Subst.open_tvar] + conv => + rhs + simp [Subst.comp, Subst.liftTVar] + simp [Exp.rename_succTVar_open_tvar] + rfl + case tvar => + intro X + cases X + case here => rfl + case there_tvar X0 => + conv => lhs; simp [Subst.comp, Subst.open_tvar] + conv => + rhs + simp [Subst.comp, Subst.liftTVar] + simp [Ty.rename_succTVar_open_tvar] + rfl + +theorem Ty.open_tvar_subst_comm {T : Ty (s,X)} {U : Ty s} {σ : Subst s s'} : + (T.open_tvar U).subst σ = (T.subst σ.liftTVar).open_tvar (U.subst σ) := by + simp [Ty.open_tvar] + simp [Ty.subst_comp] + simp [Subst.open_tvar_subst_comm] diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean new file mode 100644 index 00000000..5cc6f61b --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean @@ -0,0 +1,3 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Context +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Subst diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean new file mode 100644 index 00000000..221ca0d1 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean @@ -0,0 +1,32 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core + +inductive Ctx : Sig -> Type where +| empty : Ctx {} +| cons_var : Ctx s -> Ty s -> Ctx (s,x) +| cons_tvar : Ctx s -> Ty s -> Ctx (s,X) + +infixl:50 ",x:" => Ctx.cons_var +infixl:50 ",X<:" => Ctx.cons_tvar + +inductive Ctx.LookupVar : Ctx s -> Var s -> Ty s -> Prop where +| here : + Ctx.LookupVar (Γ,x:T) .here (T.rename Rename.succVar) +| there_var : + Ctx.LookupVar Γ x T -> + Ctx.LookupVar (Γ,x:U) (x.there_var) (T.rename Rename.succVar) +| there_tvar : + Ctx.LookupVar Γ x T -> + Ctx.LookupVar (Γ,X<:S) (x.there_tvar) (T.rename Rename.succTVar) + +inductive Ctx.LookupTVar : Ctx s -> TVar s -> Ty s -> Prop where +| here : + Ctx.LookupTVar (Γ,X<:T) .here (T.rename Rename.succTVar) +| there_var : + Ctx.LookupTVar Γ X T -> + Ctx.LookupTVar (Γ,x:U) X.there_var (T.rename Rename.succVar) +| there_tvar : + Ctx.LookupTVar Γ X T -> + Ctx.LookupTVar (Γ,X<:S) X.there_tvar (T.rename Rename.succTVar) + +@[simp] +instance : EmptyCollection (Ctx {}) := ⟨Ctx.empty⟩ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean new file mode 100644 index 00000000..d4211550 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean @@ -0,0 +1,74 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Debruijn + +inductive Ty : Sig -> Type where +| top : Ty s +| tvar : TVar s -> Ty s +| arrow : Ty s -> Ty s -> Ty s +| poly : Ty s -> Ty (s,X) -> Ty s + +def Ty.rename : Ty s1 -> Rename s1 s2 -> Ty s2 +| .top, _ => .top +| .tvar X, ρ => .tvar (ρ.tvar X) +| .arrow A B, ρ => .arrow (A.rename ρ) (B.rename ρ) +| .poly A B, ρ => .poly (A.rename ρ) (B.rename ρ.liftTVar) + +inductive Exp : Sig -> Type where +| var : Var s -> Exp s +| abs : Ty s -> Exp (s,x) -> Exp s +| tabs : Ty s -> Exp (s,X) -> Exp s +| app : Exp s -> Exp s -> Exp s +| tapp : Exp s -> Ty s -> Exp s + +def Exp.rename : Exp s1 -> Rename s1 s2 -> Exp s2 +| .var x, ρ => .var (ρ.var x) +| .abs A e, ρ => .abs (A.rename ρ) (e.rename ρ.liftVar) +| .tabs A e, ρ => .tabs (A.rename ρ) (e.rename ρ.liftTVar) +| .app e1 e2, ρ => .app (e1.rename ρ) (e2.rename ρ) +| .tapp e A, ρ => .tapp (e.rename ρ) (A.rename ρ) + +theorem Ty.rename_id {T : Ty s} : T.rename Rename.id = T := by + induction T + case top => rfl + case tvar => rfl + case arrow A B ihA ihB => simp [Ty.rename, ihA, ihB] + case poly A B ihA ihB => simp [Ty.rename, ihA, ihB] + +theorem Exp.rename_id {e : Exp s} : e.rename Rename.id = e := by + induction e + case var => rfl + case abs A e ih => simp [Exp.rename, ih, Ty.rename_id] + case tabs A e ih => simp [Exp.rename, ih, Ty.rename_id] + case app e1 e2 ih1 ih2 => simp [Exp.rename, ih1, ih2] + case tapp e A ih => simp [Exp.rename, ih, Ty.rename_id] + +theorem Ty.rename_comp {T : Ty s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} : + (T.rename f1).rename f2 = T.rename (f1.comp f2) := by + induction T generalizing s2 s3 + case top => rfl + case tvar => rfl + case arrow A B ihA ihB => simp [Ty.rename, ihA, ihB] + case poly A B ihA ihB => + simp [Ty.rename, ihA] + simp [Rename.comp_liftTVar] + simp [ihB] + +theorem Exp.rename_comp {e : Exp s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} : + (e.rename f1).rename f2 = e.rename (f1.comp f2) := by + induction e generalizing s2 s3 + case var => rfl + case abs A e ih => simp [Exp.rename, ih, Ty.rename_comp, Rename.comp_liftVar] + case tabs A e ih => simp [Exp.rename, ih, Ty.rename_comp, Rename.comp_liftTVar] + case app e1 e2 ih1 ih2 => simp [Exp.rename, ih1, ih2] + case tapp e A ih => simp [Exp.rename, ih, Ty.rename_comp] + +theorem Ty.rename_succVar_comm {T : Ty s} : + (T.rename f).rename Rename.succVar = (T.rename Rename.succVar).rename f.liftVar := by + simp [Ty.rename_comp, Rename.rename_succVar_comm] + +theorem Ty.rename_succTVar_comm {T : Ty s} : + (T.rename f).rename Rename.succTVar = (T.rename Rename.succTVar).rename f.liftTVar := by + simp [Ty.rename_comp, Rename.rename_succTVar_comm] + +inductive Exp.IsVal : Exp s -> Prop where +| abs : IsVal (.abs T e) +| tabs : IsVal (.tabs T e) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean new file mode 100644 index 00000000..802ab078 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean @@ -0,0 +1,23 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core + +def Ty.subst : Ty s1 -> Subst s1 s2 -> Ty s2 +| .top, _ => .top +| .tvar X, s => s.tvar X +| .arrow A B, s => .arrow (A.subst s) (B.subst s) +| .poly A B, s => .poly (A.subst s) (B.subst s.liftTVar) + +def Exp.subst : Exp s1 -> Subst s1 s2 -> Exp s2 +| .var x, s => s.var x +| .abs A e, s => .abs (A.subst s) (e.subst s.liftVar) +| .tabs A e, s => .tabs (A.subst s) (e.subst s.liftTVar) +| .app e1 e2, s => .app (e1.subst s) (e2.subst s) +| .tapp e A, s => .tapp (e.subst s) (A.subst s) + +def Ty.open_tvar (T : Ty (s,X)) (U : Ty s) : Ty s := + T.subst (Subst.open_tvar U) + +def Exp.open_var (e : Exp (s,x)) (U : Exp s) : Exp s := + e.subst (Subst.open_var U) + +def Exp.open_tvar (e : Exp (s,X)) (U : Ty s) : Exp s := + e.subst (Subst.open_tvar U) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean new file mode 100644 index 00000000..ca1b2996 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean @@ -0,0 +1,352 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem + +inductive Ctx.IsEmpty : Ctx s -> Prop where +| empty_is_empty : Ctx.IsEmpty .empty + +theorem HasType.app_inv + (ht : HasType Γ (.app e1 e2) T) : + ∃ T1 T2, + HasType Γ e1 (.arrow T1 T2) + ∧ HasType Γ e2 T1 + ∧ Subtyp Γ T2 T := by + generalize he0 : Exp.app e1 e2 = e at ht + induction ht <;> cases he0 + case app T1 U1 _ ht1 ht2 _ _ => + use T1, U1 + split_ands + { exact ht1 } + { exact ht2 } + { apply Subtyp.refl } + case sub hsub _ ih => + have ⟨T1, T2, ht1, ht2, hs0⟩ := ih rfl + use T1, T2 + split_ands + { exact ht1 } + { exact ht2 } + { apply Subtyp.trans hs0 hsub } + +theorem Subtyp.top_inv + (hsub : Subtyp Γ .top T) : + T = .top := by + generalize he0 : Ty.top = T at hsub + induction hsub <;> cases he0 + case top => rfl + case refl => rfl + case trans => aesop + +theorem Subtyp.arrow_inv_left + (hsub : Subtyp Γ (.arrow T1 U1) T) : + (∃ T2 U2, T = .arrow T2 U2) ∨ T = .top := by + generalize he0 : Ty.arrow T1 U1 = T at hsub + induction hsub <;> cases he0 + case top => right; rfl + case refl => left; aesop + case arrow => left; aesop + case trans ih1 _ ih2 => + specialize ih2 rfl + cases ih2 + case inl ih2 => + aesop + case inr ih2 => + cases ih2 + rename_i hsub _ + have heq := Subtyp.top_inv hsub + aesop + +theorem Subtyp.poly_inv_left + (hsub : Subtyp Γ (.poly T1 T2) T) : + (∃ T3 T4, T = .poly T3 T4) ∨ T = .top := by + generalize he0 : Ty.poly T1 T2 = T at hsub + induction hsub <;> cases he0 + case top => right; rfl + case refl => left; aesop + case poly => left; aesop + case trans ih1 _ ih2 => + specialize ih2 rfl + cases ih2 + case inl ih2 => + aesop + case inr ih2 => + cases ih2 + rename_i hsub _ + have heq := Subtyp.top_inv hsub + aesop + +theorem Subtype.tvar_inv_right + (hsub : Subtyp Γ T (.tvar X)) : + ∃ X0, T = .tvar X0 := by + generalize he0 : Ty.tvar X = T0 at hsub + induction hsub <;> cases he0 + case refl => aesop + case trans => aesop + case tvar => aesop + +theorem Subtyp.arrow_inv_right + (hsub : Subtyp Γ T (.arrow T2 U2)) : + (∃ T1 U1, T = .arrow T1 U1) ∨ (∃ X, T = .tvar X) := by + generalize he0 : Ty.arrow T2 U2 = T0 at hsub + induction hsub <;> cases he0 + case refl => aesop + case tvar => aesop + case arrow => aesop + case trans ih1 _ ih2 => + specialize ih2 rfl + cases ih2 + case inl ih2 => + have ⟨T2, U2, h⟩ := ih2 + cases h + specialize ih1 rfl + aesop + case inr ih2 => + have ⟨X, h⟩ := ih2 + cases h + rename_i hsub _ + have := Subtype.tvar_inv_right hsub + aesop + +theorem Subtyp.poly_inv_right + (hsub : Subtyp Γ T (.poly T2 U2)) : + (∃ T1 U1, T = .poly T1 U1) ∨ (∃ X, T = .tvar X) := by + generalize he0 : Ty.poly T2 U2 = T0 at hsub + induction hsub <;> cases he0 + case refl => aesop + case tvar => aesop + case poly => aesop + case trans ih1 _ ih2 => + specialize ih2 rfl + cases ih2 + case inl ih2 => + have ⟨T2, U2, h⟩ := ih2 + cases h + specialize ih1 rfl + aesop + case inr ih2 => + have ⟨X, h⟩ := ih2 + cases h + rename_i hsub _ + have := Subtype.tvar_inv_right hsub + aesop + +theorem Subtyp.arrow_inv + (hsub : Subtyp Γ (.arrow T1 U1) (.arrow T2 U2)) : + Subtyp Γ T2 T1 ∧ Subtyp Γ U1 U2 := by + generalize he1 : Ty.arrow T1 U1 = P1 at hsub + generalize he2 : Ty.arrow T2 U2 = P2 at hsub + induction hsub <;> cases he1 <;> cases he2 + case refl => constructor <;> apply Subtyp.refl + case trans hs1 ih1 hs2 ih2 => + have := Subtyp.arrow_inv_left hs1 + cases this + case inr h => + cases h + have := Subtyp.top_inv hs2 + contradiction + case inl h => + have ⟨T3, U3, h⟩ := h + cases h + specialize ih1 rfl rfl + specialize ih2 rfl rfl + have ⟨ih11, ih12⟩ := ih1 + have ⟨ih21, ih22⟩ := ih2 + constructor + { apply Subtyp.trans ih21 ih11 } + { apply Subtyp.trans ih12 ih22 } + case arrow => aesop + +theorem Subtyp.poly_inv + (hsub : Subtyp Γ (.poly T1 U1) (.poly T2 U2)) : + Subtyp Γ T2 T1 ∧ Subtyp (Γ,X<:T2) U1 U2 := by + generalize he1 : Ty.poly T1 U1 = P1 at hsub + generalize he2 : Ty.poly T2 U2 = P2 at hsub + induction hsub <;> cases he1 <;> cases he2 + case refl => constructor <;> apply Subtyp.refl + case poly => aesop + case trans hs1 ih1 hs2 ih2 => + have := Subtyp.poly_inv_left hs1 + cases this + case inl h => + have ⟨T3, T4, h⟩ := h + cases h + specialize ih1 rfl rfl + specialize ih2 rfl rfl + have ⟨ih11, ih12⟩ := ih1 + have ⟨ih21, ih22⟩ := ih2 + constructor + { apply Subtyp.trans ih21 ih11 } + { have ih12' := ih12.retype (Retype.narrow_tvar ih21) + simp [Ty.subst_id] at ih12' + apply Subtyp.trans ih12' ih22 } + case inr h => + cases h + have := Subtyp.top_inv hs2 + contradiction + +theorem Subtyp.non_tvar_left_inv + (hsub : Subtyp Γ T1 T2) + (hnt : ∀ X, T1 ≠ .tvar X) : + ∀ X, T2 ≠ .tvar X := by + induction hsub + case top => aesop + case refl => aesop + case tvar => + rename_i X _ _ + specialize hnt X + contradiction + case trans ih1 ih2 => aesop + case arrow => aesop + case poly => aesop + +theorem HasType.value_typing + (hv : Exp.IsVal v) + (ht : HasType Γ v T) : + ∀ X, T ≠ .tvar X := by + induction ht <;> try (solve | cases hv) + case sub hsub _ ih => + specialize ih hv + apply Subtyp.non_tvar_left_inv hsub + exact ih + case abs => aesop + case tabs => aesop + +theorem HasType.abs_inv {Γ : Ctx s} + (ht : HasType Γ (.abs T0 e) (.arrow T1 U1)) : + ∃ U0, + HasType (Γ,x:T0) e (U0.rename Rename.succVar) ∧ + Subtyp Γ T1 T0 ∧ + Subtyp Γ U0 U1 := by + generalize he1 : Exp.abs T0 e = t at ht + generalize he2 : Ty.arrow T1 U1 = P at ht + induction ht <;> cases he1 <;> cases he2 + case abs T0 t0 U0 ht _ => + use U0 + split_ands + { exact ht } + { apply Subtyp.refl } + { apply Subtyp.refl } + case sub hsub => + have := Subtyp.arrow_inv_right hsub + cases this + case inl h => + have ⟨T1, U1, h⟩ := h + cases h + rename_i ih + specialize ih rfl rfl + have ⟨U0, ih1, ih2, ih3⟩ := ih + have ⟨h1, h2⟩ := Subtyp.arrow_inv hsub + use U0 + split_ands + { exact ih1 } + { apply Subtyp.trans h1 ih2 } + { apply Subtyp.trans ih3 h2 } + case inr h => + have ⟨X, h⟩ := h + rename_i hv _ _ + have := HasType.value_typing (by constructor) hv + aesop + +theorem HasType.tapp_inv + (ht : HasType Γ (.tapp e T) U) : + ∃ T2, + HasType Γ e (.poly T T2) + ∧ Subtyp Γ (T2.open_tvar T) U := by + generalize he1 : Exp.tapp e T = t0 at ht + induction ht <;> cases he1 + case tapp => + rename_i T2 ht _ + use T2 + split_ands + { exact ht } + { apply Subtyp.refl } + case sub hs _ ih => + specialize ih rfl + have ⟨T2, ih1, ih2⟩ := ih + use T2 + split_ands + { exact ih1 } + { apply Subtyp.trans ih2 hs } + +theorem HasType.tabs_inv + (ht : HasType Γ (.tabs T0 e) (.poly T1 U1)) : + ∃ U0, + HasType (Γ,X<:T0) e U0 + ∧ Subtyp Γ T1 T0 + ∧ Subtyp (Γ,X<:T1) U0 U1 := by + generalize he1 : Exp.tabs T0 e = t0 at ht + generalize he2 : Ty.poly T1 U1 = P at ht + induction ht <;> cases he1 <;> cases he2 + case tabs T _ U h _ => + use U + split_ands + { exact h } + { apply Subtyp.refl } + { apply Subtyp.refl } + case sub ht ih hs => + have := Subtyp.poly_inv_right hs + cases this + case inl h => + have ⟨T2, U2, h⟩ := h + cases h + rename_i ih + specialize ih rfl rfl + have ⟨U0, ih1, ih2, ih3⟩ := ih + have ⟨h1, h2⟩ := Subtyp.poly_inv hs + use U0 + split_ands + { exact ih1 } + { apply Subtyp.trans h1 ih2 } + { have ih3' := ih3.retype (Retype.narrow_tvar h1) + simp [Ty.subst_id] at ih3' + apply Subtyp.trans ih3' h2 } + case inr h => + have ⟨X, h⟩ := h + cases h + rename_i ht _ + have := HasType.value_typing (by constructor) ht + aesop + +theorem HasType.value_typing_arrow_inv + (hv : Exp.IsVal v) + (ht : HasType Γ v (.arrow T U)) : + ∃ T0 e0, v = .abs T0 e0 := by + generalize he : Ty.arrow T U = P at ht + induction ht <;> try (solve | cases he | cases hv) + case sub ih => + cases he + rename_i hs + have := Subtyp.arrow_inv_right hs + cases this + case inl h => + have ⟨T1, U1, h⟩ := h + cases h + specialize ih hv rfl + trivial + case inr h => + have ⟨X, h⟩ := h + rename_i hvt _ + have := HasType.value_typing hv hvt + aesop + case abs => aesop + +theorem HasType.value_typing_poly_inv + (hv : Exp.IsVal v) + (ht : HasType Γ v (.poly T U)) : + ∃ T0 e0, v = .tabs T0 e0 := by + generalize he : Ty.poly T U = P at ht + induction ht <;> try (solve | cases he | cases hv) + case sub ih => + cases he + rename_i hs + have := Subtyp.poly_inv_right hs + cases this + case inl h => + have ⟨T1, U1, h⟩ := h + cases h + specialize ih hv rfl + trivial + case inr h => + have ⟨X, h⟩ := h + rename_i hvt _ + have := HasType.value_typing hv hvt + aesop + case tabs => aesop diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean new file mode 100644 index 00000000..e23dbd13 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean @@ -0,0 +1,42 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Reduce +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Canonical + +theorem preservation + (ht : HasType .empty t T) + (hred : Reduce t t') : + HasType .empty t' T := by + induction hred generalizing T + case red_app_fun ih => + have ⟨T1, T2, ht1, ht2, hs0⟩ := HasType.app_inv ht + have ih := ih ht1 + apply HasType.sub hs0 + apply HasType.app ih ht2 + case red_app_arg ih => + have ⟨T1, T2, ht1, ht2, hs0⟩ := HasType.app_inv ht + have ih := ih ht2 + apply HasType.sub hs0 + apply HasType.app ht1 ih + case red_app => + have ⟨T1, T2, ht1, ht2, hs0⟩ := HasType.app_inv ht + have ⟨U0, h1, h2, h3⟩ := HasType.abs_inv ht1 + have ht2' := HasType.sub h2 ht2 + have h1' := h1.retype (Retype.open_var ht2') + simp [Ty.rename_succVar_open_var] at h1' + apply HasType.sub _ h1' + apply Subtyp.trans h3 hs0 + case red_tapp_fun ih => + have ⟨T2, ht1, hs2⟩ := HasType.tapp_inv ht + have ih := ih ht1 + apply HasType.sub hs2 + apply HasType.tapp ih + case red_tapp => + have ⟨T2, ht1, hs2⟩ := HasType.tapp_inv ht + have ⟨U0, h1, h2, h3⟩ := HasType.tabs_inv ht1 + have h1' := h1.retype (Retype.open_tvar h2) + rename_i R + have h3' := h3.retype (Retype.open_tvar Subtyp.refl) + apply HasType.sub _ h1' + apply Subtyp.trans h3' hs2 diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean new file mode 100644 index 00000000..282dc878 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean @@ -0,0 +1,50 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Reduce +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Canonical + +theorem progress + (ht : HasType Γ t T) (hem : Ctx.IsEmpty Γ) : + (∃ t', Reduce t t') ∨ t.IsVal := by + induction ht + case var hb => + cases hem + cases hb + case sub ih => aesop + case abs => right; constructor + case tabs => right; constructor + case app ih1 ih2 => + specialize ih1 hem + cases ih1 + case inl ih1 => + have ⟨t1', ih1⟩ := ih1 + left + constructor + apply Reduce.red_app_fun + exact ih1 + case inr ih1 => + rename_i hvt _ + have := HasType.value_typing_arrow_inv ih1 hvt + have ⟨T0, e0, h⟩ := this + cases h + left + constructor + apply Reduce.red_app + case tapp ih => + specialize ih hem + cases ih + case inl ih => + have ⟨t1', ih⟩ := ih + left + constructor + apply Reduce.red_tapp_fun + exact ih + case inr ih => + rename_i hvt + have := HasType.value_typing_poly_inv ih hvt + have ⟨T0, e0, h⟩ := this + cases h + left + constructor + apply Reduce.red_tapp diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean new file mode 100644 index 00000000..a605a2e4 --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean @@ -0,0 +1,44 @@ +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax + +inductive Subtyp : Ctx s -> Ty s -> Ty s -> Prop where +| top : + Subtyp Γ T .top +| refl : + Subtyp Γ T T +| trans : + Subtyp Γ A B -> + Subtyp Γ B C -> + Subtyp Γ A C +| tvar : + Ctx.LookupTVar Γ X T -> + Subtyp Γ (.tvar X) T +| arrow : + Subtyp Γ T2 T1 -> + Subtyp Γ U1 U2 -> + Subtyp Γ (.arrow T1 U1) (.arrow T2 U2) +| poly : + Subtyp Γ T2 T1 -> + Subtyp (Γ,X<:T2) U1 U2 -> + Subtyp Γ (.poly T1 U1) (.poly T2 U2) + +inductive HasType : Ctx s -> Exp s -> Ty s -> Prop where +| var : + Ctx.LookupVar Γ x T -> + HasType Γ (.var x) T +| sub : + Subtyp Γ T1 T2 -> + HasType Γ t T1 -> + HasType Γ t T2 +| abs : + HasType (Γ,x:T) t (U.rename Rename.succVar) -> + HasType Γ (.abs T t) (.arrow T U) +| tabs : + HasType (Γ,X<:T) t U -> + HasType Γ (.tabs T t) (.poly T U) +| app : + HasType Γ t1 (.arrow T1 U1) -> + HasType Γ t2 T1 -> + HasType Γ (.app t1 t2) U1 +| tapp : + HasType Γ t (.poly T U) -> + HasType Γ (.tapp t T) (U.open_tvar T) From 27277c54fb84cee431109d85bf472bea306a5328 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sat, 13 Sep 2025 23:36:48 +0200 Subject: [PATCH 02/13] Add documents, simplify the proofs --- .../LambdaCalculus/WellScoped/FSub.lean | 32 +- .../WellScoped/FSub/Debruijn.lean | 119 ++++-- .../LambdaCalculus/WellScoped/FSub/Eval.lean | 36 ++ .../WellScoped/FSub/RebindTheory/Core.lean | 93 +++-- .../FSub/RebindTheory/TypeSystem.lean | 14 +- .../WellScoped/FSub/Reduce.lean | 13 + .../WellScoped/FSub/RetypeTheory/Core.lean | 125 +++--- .../FSub/RetypeTheory/TypeSystem.lean | 39 +- .../WellScoped/FSub/Substitution.lean | 7 + .../WellScoped/FSub/Substitution/Core.lean | 124 +++--- .../FSub/Substitution/Properties.lean | 365 +++++++----------- .../WellScoped/FSub/Syntax.lean | 11 + .../WellScoped/FSub/Syntax/Context.lean | 24 ++ .../WellScoped/FSub/Syntax/Core.lean | 86 +++-- .../WellScoped/FSub/Syntax/Subst.lean | 11 + .../FSub/TypeSoundness/Canonical.lean | 291 +++----------- .../FSub/TypeSoundness/Preservation.lean | 26 +- .../FSub/TypeSoundness/Progress.lean | 40 +- .../WellScoped/FSub/TypeSystem.lean | 51 +++ 19 files changed, 760 insertions(+), 747 deletions(-) create mode 100644 Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean index 01ed3080..b19f479b 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub.lean @@ -1,17 +1,28 @@ /- # Type soundness of System F<: -This is a mechanized type soundness proof of System F<: in what I call _well-scoped_ style. +This mechanizes type soundness for System F<: using intrinsically scoped de Bruijn indices +and context morphisms. -The main idea is to: -- Use intrinsically scoped de Bruijn indices. Specifically, de Bruijn indices are indexed by a signature describing available binders in the type context. This way, syntactic constructs are well-scoped (and therefore well-formed) by construction. -- Use context morphisms, which are mappings between type contexts that preserve types. This way, all theorems concerning context operations (weakening, narrowing, substitution) can be proven in a uniform way. +The formalization uses intrinsically scoped de Bruijn indices. +De Bruijn indices are indexed by signatures describing available binders in the type context. +Syntactic constructs are well-scoped by construction. -There are two kinds of context morphisms where the latter depends on the former. -- The first is _rebinding morphisms_. A rebinding morphism `f` from `Γ` to `Δ` maps each `x:T ∈ Γ` to a corresponding binder `f(x) : f(T) ∈ Δ`. Then, we show that typing is preserved under such morphisms. -- The second is _retypeing morphisms_. A retypeing morphism `g` from `Γ` to `Δ` maps each `x: T ∈ Γ` into a typing derivation `Δ ⊢ g(x) : g(T)`. This is of course stronger than the first kind, and its proof relies on that of the first kind. We show that typing is preserved under this kind of morphisms too. +Context morphisms are mappings between type contexts that preserve types. +All theorems concerning context operations (weakening, narrowing, substitution) +are proven uniformly using these morphisms. -With this context morphism infrastructure, we can prove a variety of theorems regarding context manipulation, including weakening, narrowing, substitution, and any other context operations that can be formulated as a context morphism. +Two kinds of context morphisms exist: + +Rebinding morphisms map each `x:T ∈ Γ` to a corresponding binder `f(x) : f(T) ∈ Δ`. +Typing is preserved under rebinding morphisms. + +Retyping morphisms map each `x: T ∈ Γ` to a typing derivation `Δ ⊢ g(x) : g(T)`. +This is stronger than rebinding morphisms. +The proof builds on rebinding morphism preservation. + +This infrastructure enables proofs for context manipulation operations including +weakening, narrowing, substitution, and any context operations expressible as context morphisms. -/ -- This module defines the intrinsically scoped de Bruijn indices. @@ -21,6 +32,11 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Debruijn import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Reduce +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Eval + +-- The following defines parallel substitution and proves its properties. +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties -- The following modules define context morphisms and prove their theory. import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.Core diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean index efa2cb0a..daf1d5c1 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean @@ -1,118 +1,171 @@ +/- +# Intrinsically scoped de Bruijn indices + +This module defines the foundation for intrinsically scoped de Bruijn indices used throughout +the System F<: mechanization. +Instead of using raw natural numbers for de Bruijn indices, +variables and type variables are indexed by a signature (`Sig`) that describes +the available binders in the context. + +This approach ensures that syntactic constructs are well-scoped by construction, +eliminating the possibility of free variables and making theorems easier to state and prove. + +The module defines: +- `Sig`: Signatures that describe the structure of typing contexts +- `Var` and `TVar`: Intrinsically scoped variables and type variables +- `Rename`: Renamings between different signatures +- Context lifting operations for working under binders +-/ + import Mathlib.Tactic +/-- A signature describes the structure of a typing context, tracking both + term variables and type variables in the order they were introduced. -/ inductive Sig : Type where | empty : Sig -| cons_var : Sig -> Sig -| cons_tvar : Sig -> Sig +/-- Extend signature with a term variable -/ +| push_var : Sig -> Sig +/-- Extend signature with a type variable -/ +| push_tvar : Sig -> Sig @[simp] instance : EmptyCollection Sig := ⟨Sig.empty⟩ theorem Sig.empty_eq : {} = Sig.empty := rfl -postfix:50 ",x" => Sig.cons_var -postfix:50 ",X" => Sig.cons_tvar +/-- Convenient syntax for extending a signature with a term variable -/ +postfix:50 ",x" => Sig.push_var +/-- Convenient syntax for extending a signature with a type variable -/ +postfix:50 ",X" => Sig.push_tvar +/-- Term variables indexed by signatures. A `Var s` represents a term variable + that is valid in signature `s`. The constructors correspond to different ways + a variable can be accessed from the current context. -/ inductive Var : Sig -> Type where +/-- The most recently bound term variable -/ | here : Var (s,x) +/-- Skip over the most recent term variable -/ | there_var : Var s -> Var (s,x) +/-- Skip over the most recent type variable -/ | there_tvar : Var s -> Var (s,X) +/-- Type variables indexed by signatures. A `TVar s` represents a type variable + that is valid in signature `s`. -/ inductive TVar : Sig -> Type where +/-- The most recently bound type variable -/ | here : TVar (s,X) +/-- Skip over the most recent term variable -/ | there_var : TVar s -> TVar (s,x) +/-- Skip over the most recent type variable -/ | there_tvar : TVar s -> TVar (s,X) +/-- A renaming between signatures `s1` and `s2` specifies how to map variables + from `s1` to variables in `s2`. This is the foundation for all variable + renamings in the mechanization. -/ structure Rename (s1 s2 : Sig) where + /-- How to rename term variables -/ var : Var s1 -> Var s2 + /-- How to rename type variables -/ tvar : TVar s1 -> TVar s2 -def Rename.liftVar (f : Rename s1 s2) : Rename (s1,x) (s2,x) := by - constructor - case var => - intro x; cases x - case here => exact .here - case there_var x0 => exact .there_var (f.var x0) - case tvar => - intro X; cases X - case there_var X0 => exact .there_var (f.tvar X0) - -def Rename.liftTVar (f : Rename s1 s2) : Rename (s1,X) (s2,X) := by - constructor - case tvar => - intro X; cases X - case here => exact .here - case there_tvar X0 => exact .there_tvar (f.tvar X0) - case var => - intro x; cases x - case there_tvar x0 => exact .there_tvar (f.var x0) - +/-- Lift a renaming to work under a new term variable binder. The new term variable + is mapped to itself, while existing variables are renamed and shifted. -/ +def Rename.liftVar (f : Rename s1 s2) : Rename (s1,x) (s2,x) := + { var := fun x => match x with + | .here => .here + | .there_var x0 => .there_var (f.var x0) + tvar := fun X => match X with + | .there_var X0 => .there_var (f.tvar X0) } + +/-- Lift a renaming to work under a new type variable binder. The new type variable + is mapped to itself, while existing variables are renamed and shifted. -/ +def Rename.liftTVar (f : Rename s1 s2) : Rename (s1,X) (s2,X) := + { tvar := fun X => match X with + | .here => .here + | .there_tvar X0 => .there_tvar (f.tvar X0) + var := fun x => match x with + | .there_tvar x0 => .there_tvar (f.var x0) } + +/-- Weakening renaming that adds a new term variable to the context. + All existing variables are shifted to account for the new binding. -/ def Rename.succVar : Rename s1 (s1,x) := { var := fun x => x.there_var, tvar := fun X => X.there_var } +/-- Weakening renaming that adds a new type variable to the context. + All existing variables are shifted to account for the new binding. -/ def Rename.succTVar : Rename s1 (s1,X) := { var := fun x => x.there_tvar, tvar := fun X => X.there_tvar } +/-- The identity renaming that maps each variable to itself. -/ def Rename.id : Rename s s := { var := fun x => x, tvar := fun X => X } +/-- Composition of renamings. If `f1` renames from `s1` to `s2` and `f2` renames + from `s2` to `s3`, then their composition renames from `s1` to `s3`. -/ def Rename.comp (f1 : Rename s1 s2) (f2 : Rename s2 s3) : Rename s1 s3 := { var := fun x => f2.var (f1.var x), tvar := fun X => f2.tvar (f1.tvar X) } +/-- Two renamings are equal if they map variables in the same way. -/ theorem Rename.funext {f g : Rename s1 s2} (var : ∀ x, f.var x = g.var x) (tvar : ∀ X, f.tvar X = g.tvar X) : f = g := by - cases f; cases g - simp - constructor - { funext x; aesop } - { funext X; aesop } + cases f; cases g; simp + split_ands <;> aesop +/-- Lifting the identity renaming gives the identity renaming. -/ @[simp] theorem Rename.id_liftVar_eq_id : Rename.id.liftVar = (Rename.id (s:=(s,x))) := by apply Rename.funext case var => intro x; cases x <;> rfl case tvar => intro X; cases X; rfl +/-- Lifting the identity renaming gives the identity renaming. -/ @[simp] theorem Rename.id_liftTVar_eq_id : Rename.id.liftTVar = (Rename.id (s:=(s,X))) := by apply Rename.funext case var => intro x; cases x; rfl case tvar => intro X; cases X <;> rfl +/-- Composition commutes with lifting over type variables. -/ theorem Rename.comp_liftTVar {f1 : Rename s1 s2} {f2 : Rename s2 s3} : (f1.comp f2).liftTVar = f1.liftTVar.comp f2.liftTVar := by apply Rename.funext case var => intro x; cases x; rfl case tvar => intro X; cases X <;> rfl +/-- Composition commutes with lifting over term variables. -/ theorem Rename.comp_liftVar {f1 : Rename s1 s2} {f2 : Rename s2 s3} : (f1.comp f2).liftVar = f1.liftVar.comp f2.liftVar := by apply Rename.funext case var => intro x; cases x <;> rfl case tvar => intro X; cases X; rfl +/-- Composing with variable weakening commutes with lifting. -/ theorem Rename.rename_succVar_comm {f : Rename s1 s2} : (f.comp Rename.succVar) = Rename.succVar.comp f.liftVar := by apply Rename.funext case var => intro x; rfl case tvar => intro X; rfl +/-- Composing with type variable weakening commutes with lifting. -/ theorem Rename.rename_succTVar_comm {f : Rename s1 s2} : (f.comp Rename.succTVar) = Rename.succTVar.comp f.liftTVar := by apply Rename.funext case var => intro x; rfl case tvar => intro X; rfl +/-- Append two signatures, concatenating their binder sequences. -/ def Sig.append : Sig -> Sig -> Sig | s1, .empty => s1 -| s1, .cons_var s2 => .cons_var (s1.append s2) -| s1, .cons_tvar s2 => .cons_tvar (s1.append s2) +| s1, .push_var s2 => .push_var (s1.append s2) +| s1, .push_tvar s2 => .push_tvar (s1.append s2) @[simp] instance : Append Sig := ⟨Sig.append⟩ +/-- Lift a renaming to work under multiple binders specified by a signature. + This is the generalization of `liftVar` and `liftTVar` to arbitrary sequences of binders. -/ def Rename.lift : Rename s1 s2 -> (s : Sig) -> Rename (s1 ++ s) (s2 ++ s) | f, .empty => f -| f, .cons_var s => (f.lift s).liftVar -| f, .cons_tvar s => (f.lift s).liftTVar +| f, .push_var s => (f.lift s).liftVar +| f, .push_tvar s => (f.lift s).liftTVar diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean new file mode 100644 index 00000000..cec1543a --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean @@ -0,0 +1,36 @@ +/- +# Big-step evaluator for System F<: +-/ + +import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax + +/-- The result of evaluating an expression. Evaluation may succeed with a value, + fail with an error, or exhaust its fuel allocation. -/ +inductive Result (s : Sig) where +/-- Successful evaluation to a value -/ +| ok : Exp s -> Result s +/-- Runtime error (e.g., free variable, type mismatch) -/ +| err : Result s +/-- Evaluation did not terminate within fuel limit -/ +| nonterm : Result s + +/-- Big-step evaluator with fuel-based termination. -/ +def eval : Nat -> Exp s -> Result s +| 0, _ => .nonterm +| _, .var _ => .err +| _, .abs A e => .ok (.abs A e) +| _, .tabs S e => .ok (.tabs S e) +| fuel+1, .app e1 e2 => + match eval fuel e1 with + | .ok (.abs _ t1) => + eval fuel (t1.open_var e2) + | .ok _ => .err + | .err => .err + | .nonterm => .nonterm +| fuel+1, .tapp e A => + match eval fuel e with + | .ok (.tabs _ t) => + eval fuel (t.open_tvar A) + | .ok _ => .err + | .err => .err + | .nonterm => .nonterm diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean index 1b5f2467..f4ec250d 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean @@ -1,63 +1,82 @@ +/- +# Rebinding morphisms + +This module defines rebinding morphisms, which enable systematic reasoning about +context transformations in the well-scoped approach to System F<:. +Rebinding morphisms are structure-preserving maps between typing contexts +that maintain relationships between variables and their types. + +A rebinding morphism `ρ : Rebind Γ f Δ` consists of: +- A renaming `f : s₁ → s₂` between signatures +- Contexts `Γ : Ctx s₁` and `Δ : Ctx s₂` +- Proofs that bound types are preserved under renaming + +If `x : T ∈ Γ` then `f(x) : f(T) ∈ Δ`, where `f(T)` denotes the renaming of type `T` under `f`. + +Rebinding theory forms the first layer in a hierarchy of context morphisms. +Retyping morphisms build upon this foundation. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax +/-- A rebinding morphism `Rebind Γ f Δ` witnesses that contexts `Γ` and `Δ` are + related by the renaming `f` in a type-preserving way. + + This structure encodes the fundamental principle that context transformations + must preserve the variable and type bindings in the context. -/ structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where + /-- Term variable preservation: x:T in Γ implies f(x):f(T) in Δ -/ var : ∀ x T, Ctx.LookupVar Γ x T -> Ctx.LookupVar Δ (f.var x) (T.rename f) + /-- Type variable preservation: X<:T in Γ implies f(X)<:f(T) in Δ -/ tvar : ∀ X T, Ctx.LookupTVar Γ X T -> Ctx.LookupTVar Δ (f.tvar X) (T.rename f) -def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.rename f) := by - constructor - case var => - intro x P hb +/-- **Lifting rebinding morphisms over term variable binders**. + + If ρ witnesses that Γ and Δ are related by f, then ρ.liftVar witnesses + that Γ,x:T and Δ,x:f(T) are related by f.liftVar. -/ +def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.rename f) where + var := fun x P hb => by cases hb case here => simp [<-Ty.rename_succVar_comm]; constructor case there_var hb => simp [<-Ty.rename_succVar_comm] constructor apply ρ.var _ _ hb - case tvar => - intro X S hb + tvar := fun X S hb => by cases hb case there_var hb => simp [<-Ty.rename_succVar_comm] constructor apply ρ.tvar _ _ hb -def Rebind.liftTVar (ρ : Rebind Γ f Δ) : Rebind (Γ,X<:T) (f.liftTVar) (Δ,X<:T.rename f) := by - constructor - case tvar => - intro X S hb +/-- **Lifting rebinding morphisms over type variable binders**. + + If ρ witnesses that Γ and Δ are related by f, then ρ.liftTVar witnesses + that Γ,X<:T and Δ,X<:f(T) are related by f.liftTVar. -/ +def Rebind.liftTVar (ρ : Rebind Γ f Δ) : Rebind (Γ,X<:T) (f.liftTVar) (Δ,X<:T.rename f) where + tvar := fun X S hb => by cases hb case here => simp [<-Ty.rename_succTVar_comm]; constructor case there_tvar hb => simp [<-Ty.rename_succTVar_comm] constructor apply ρ.tvar _ _ hb - case var => - intro x P hb + var := fun x P hb => by cases hb - case there_tvar hb => - simp [<-Ty.rename_succTVar_comm] - constructor - apply ρ.var _ _ hb + case there_tvar hb => simp [<-Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb + +/-- **Term variable weakening morphism**. + + The standard weakening operation that extends a context with a new term variable + is a rebinding morphism. -/ +def Rebind.succVar : Rebind Γ Rename.succVar (Γ,x:T) where + var := by intro x P hb; constructor; exact hb + tvar := by intro X S hb; constructor; exact hb + +/-- **Type variable weakening morphism**. -def Rebind.succVar : Rebind Γ Rename.succVar (Γ,x:T) := by - constructor - case var => - intro x P hb - constructor - exact hb - case tvar => - intro X S hb - constructor - exact hb - -def Rebind.succTVar : Rebind Γ Rename.succTVar (Γ,X<:T) := by - constructor - case tvar => - intro X S hb - constructor - exact hb - case var => - intro x P hb - constructor - exact hb + The standard weakening operation that extends a context with a new type variable + is a rebinding morphism. -/ +def Rebind.succTVar : Rebind Γ Rename.succTVar (Γ,X<:T) where + tvar := by intro X S hb; constructor; exact hb + var := by intro x P hb; constructor; exact hb diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean index e8ff80ec..4585fe2d 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean @@ -6,21 +6,15 @@ theorem Subtyp.rebind {f : Rename s1 s2} (hs : Subtyp Γ T1 T2) (ρ : Rebind Γ f Δ) : Subtyp Δ (T1.rename f) (T2.rename f) := by - induction hs generalizing s2 - case top => constructor - case refl => constructor - case trans => - apply Subtyp.trans <;> aesop + induction hs generalizing s2 <;> try (solve | constructor) + case trans => apply Subtyp.trans <;> aesop case tvar hb => apply Subtyp.tvar apply ρ.tvar _ _ hb case arrow ih1 ih2 => - apply Subtyp.arrow - { apply ih1 ρ } - { apply ih2 ρ } + apply Subtyp.arrow <;> grind case poly ih1 ih2 => - apply Subtyp.poly - { apply ih1 ρ } + apply Subtyp.poly <;> try grind { apply ih2 ρ.liftTVar } theorem HasType.rebind {f : Rename s1 s2} diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean index 89333fea..aac43dad 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean @@ -1,17 +1,30 @@ +/- +# Operational semantics for System F<: + +This module defines the small-step operational semantics for System F<:. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax +/-- The small-step reduction relation for System F<:. `Reduce e₁ e₂` means that + expression `e₁` can take a single computational step to become `e₂`. -/ inductive Reduce : Exp s -> Exp s -> Prop where +/-- Evaluate function position: if e₁ ⟶ e₁', then (e₁ e₂) ⟶ (e₁' e₂) -/ | red_app_fun : Reduce e1 e1' -> Reduce (.app e1 e2) (.app e1' e2) +/-- Evaluate argument position: if v₁ is a value and e₂ ⟶ e₂', then (v₁ e₂) ⟶ (v₁ e₂') -/ | red_app_arg : Exp.IsVal v1 -> Reduce e2 e2' -> Reduce (.app v1 e2) (.app v1 e2') +/-- Beta reduction: (λx:T.e₁) e₂ ⟶ e₁[x := e₂] -/ | red_app : Reduce (.app (.abs T e1) e2) (e1.open_var e2) +/-- Evaluate polymorphic expression: if e ⟶ e', then (e [T]) ⟶ (e' [T]) -/ | red_tapp_fun : Reduce e e' -> Reduce (.tapp e T) (.tapp e' T) +/-- Type application: (ΛX<:T'.e) [T] ⟶ e[X := T] -/ | red_tapp : Reduce (.tapp (.tabs T' e) T) (e.open_tvar T) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean index 4863f858..50dd4041 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean @@ -1,22 +1,36 @@ +/- +# Retyping morphisms + +This module defines retyping morphisms, which are the second layer in the hierarchy +of context morphisms for System F<:. +Retyping morphisms extend rebinding morphisms by mapping variables to typing derivations +rather than just renamed variables. + +A retyping morphism `ρ : Retype Γ σ Δ` consists of: +- A parallel substitution `σ : s₁ → s₂` +- Contexts `Γ : Ctx s₁` and `Δ : Ctx s₂` +- Proofs that each variable in Γ maps to a well-typed term in Δ +- Proofs that each type variable in Γ maps to a subtype in Δ + +More precisely, if `x : T ∈ Γ` then `Δ ⊢ σ(x) : σ(T)`, +and if `X <: S ∈ Γ` then `Δ ⊢ σ(X) <: σ(S)`. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.TypeSystem -structure Retype (Γ : Ctx s1) (σ : Subst s1 s2) (Δ : Ctx s2) where - var : - ∀ x T, - Γ.LookupVar x T -> - HasType Δ (σ.var x) (T.subst σ) +/-- A retyping morphism `Retype Γ σ Δ` witnesses that contexts `Γ` and `Δ` are + related by the substitution `σ` in a type-preserving way. - tvar : - ∀ X S, - Γ.LookupTVar X S -> - Subtyp Δ (σ.tvar X) (S.subst σ) + Unlike rebinding morphisms, retyping morphisms map variables to typing derivations. -/ +structure Retype (Γ : Ctx s1) (σ : Subst s1 s2) (Δ : Ctx s2) where + var : ∀ x T, Γ.LookupVar x T -> HasType Δ (σ.var x) (T.subst σ) + tvar : ∀ X S, Γ.LookupTVar X S -> Subtyp Δ (σ.tvar X) (S.subst σ) -def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P.subst σ) := by - constructor - case var => - intro x T hb +/-- Extends a retyping morphism to contexts with an additional term variable. -/ +def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P.subst σ) where + var := fun x T hb => by cases hb case here => apply HasType.var @@ -26,99 +40,64 @@ def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P have h0 := ρ.var _ _ hb0 simp [<-Ty.subst_succVar_comm_base] apply h0.rebind Rebind.succVar - case tvar => - intro X S hb + tvar := fun X S hb => by cases hb case there_var hb0 => have h0 := ρ.tvar _ _ hb0 simp [<-Ty.subst_succVar_comm_base] apply h0.rebind Rebind.succVar -def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ,X<:P.subst σ) := by - constructor - case var => - intro x T hb +/-- Extends a retyping morphism to contexts with an additional type variable. -/ +def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ,X<:P.subst σ) where + var := fun x T hb => by cases hb case there_tvar hb0 => have h0 := ρ.var _ _ hb0 simp [<-Ty.subst_succTVar_comm_base] apply h0.rebind Rebind.succTVar - case tvar => - intro X S hb + tvar := fun X S hb => by cases hb case here => apply Subtyp.tvar - simp [<-Ty.subst_succTVar_comm_base] - constructor + grind [Ty.subst_succTVar_comm_base] case there_tvar hb0 => have h0 := ρ.tvar _ _ hb0 simp [<-Ty.subst_succTVar_comm_base] apply h0.rebind Rebind.succTVar +/-- Creates a retyping morphism that substitutes an expression for the newest term variable. -/ def Retype.open_var (ht : HasType Γ e T) : - Retype (Γ,x:T) (Subst.open_var e) Γ := by - constructor - case var => - intro x T hb + Retype (Γ,x:T) (Subst.open_var e) Γ where + var := fun x T hb => by cases hb - case here => - simp [Ty.rename_succVar_open_var] - exact ht - case there_var hb0 => - simp [Ty.rename_succVar_open_var] - apply HasType.var - exact hb0 - case tvar => - intro X S hb + case here => simpa [Ty.rename_succVar_open_var] + case there_var hb0 => apply HasType.var; simpa [Ty.rename_succVar_open_var] + tvar := fun X S hb => by cases hb - case there_var hb0 => - simp [Ty.rename_succVar_open_var] - apply Subtyp.tvar - exact hb0 + case there_var hb0 => apply Subtyp.tvar; simpa [Ty.rename_succVar_open_var] +/-- Creates a retyping morphism that narrows the bound of the newest type variable. -/ def Retype.narrow_tvar (hs : Subtyp Γ S1 S2) : - Retype (Γ,X<:S2) Subst.id (Γ,X<:S1) := by - constructor - case var => - intro x T hb - simp [Ty.subst_id] - constructor - cases hb - constructor - trivial - case tvar => - intro X S hb + Retype (Γ,X<:S2) Subst.id (Γ,X<:S1) where + var := fun x T hb => by cases hb; constructor; grind [Ty.subst_id] + tvar := fun X S hb => by cases hb case here => apply Subtyp.trans { apply Subtyp.tvar; constructor } { simp [Ty.subst_id]; apply hs.rebind Rebind.succTVar } - case there_tvar hb0 => - apply Subtyp.tvar - simp [Ty.subst_id] - constructor - exact hb0 + case there_tvar hb0 => apply Subtyp.tvar; grind [Ty.subst_id] +/-- Creates a retyping morphism that substitutes a type for the newest type variable. -/ def Retype.open_tvar (hs : Subtyp Γ R S) : - Retype (Γ,X<:S) (Subst.open_tvar R) Γ := by - constructor - case var => - intro x T hb + Retype (Γ,X<:S) (Subst.open_tvar R) Γ where + var := fun x T hb => by cases hb - case there_tvar hb0 => - simp [Ty.rename_succTVar_open_tvar] - apply HasType.var - exact hb0 - case tvar => - intro X0 S0 hb + case there_tvar hb0 => apply HasType.var; grind [Ty.rename_succTVar_open_tvar] + tvar := fun X0 S0 hb => by cases hb - case here => - simp [Ty.rename_succTVar_open_tvar] - exact hs - case there_tvar hb0 => - simp [Ty.rename_succTVar_open_tvar] - apply Subtyp.tvar - exact hb0 + case here => simpa [Ty.rename_succTVar_open_tvar] + case there_tvar hb0 => apply Subtyp.tvar; simpa [Ty.rename_succTVar_open_tvar] diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean index 045176d1..e66c5d02 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean @@ -1,22 +1,19 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core +/-- Context retyping preserves subtyping judgments. -/ def Subtyp.retype {σ : Subst s1 s2} (hsub : Subtyp Γ T1 T2) (ρ : Retype Γ σ Δ) : Subtyp Δ (T1.subst σ) (T2.subst σ) := by - induction hsub generalizing s2 - case top => constructor - case refl => constructor - case trans ih1 ih2 => - apply Subtyp.trans <;> aesop - case tvar hb => - apply ρ.tvar _ _ hb + induction hsub generalizing s2 <;> try (solve | constructor) + case trans ih1 ih2 => apply Subtyp.trans <;> aesop + case tvar hb => apply ρ.tvar _ _ hb case arrow => apply arrow <;> aesop case poly ih1 ih2 => - apply poly - { apply ih1 ρ } + apply poly <;> try grind { apply ih2 ρ.liftTVar } +/-- Context retyping preserves typing judgments. -/ theorem HasType.retype {σ : Subst s1 s2} (ht : HasType Γ t T) (ρ : Retype Γ σ Δ) : @@ -24,21 +21,9 @@ theorem HasType.retype {σ : Subst s1 s2} induction ht generalizing s2 case var hb => apply ρ.var _ _ hb case sub hsub _ ih => - apply sub - { apply hsub.retype ρ } - { apply ih ρ } - case abs ih => - apply HasType.abs - simp [Ty.subst_succVar_comm_base] - apply ih ρ.liftVar - case tabs ih => - apply HasType.tabs - apply ih ρ.liftTVar - case app ih1 ih2 => - apply HasType.app - { apply ih1 ρ } - { apply ih2 ρ } - case tapp ih => - simp [Ty.open_tvar_subst_comm] - apply HasType.tapp - apply ih ρ + apply sub <;> try aesop + apply hsub.retype ρ + case abs ih => apply HasType.abs; simpa [Ty.subst_succVar_comm_base] using ih ρ.liftVar + case tabs ih => apply HasType.tabs; apply ih ρ.liftTVar + case app ih1 ih2 => apply HasType.app <;> aesop + case tapp ih => simp [Ty.open_tvar_subst_comm]; apply HasType.tapp; aesop diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean index 3ffaee7d..105aec17 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean @@ -1,2 +1,9 @@ +/- +# Parallel substitution for System F<: + +This module provides the complete parallel substitution theory for System F<:. +It imports both the core substitution definitions and their properties. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean index b4c40fb7..0aade90a 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean @@ -1,54 +1,84 @@ +/- +# Parallel substitution for System F<: + +This module defines parallel substitution operations, which allow simultaneous +substitution of multiple variables. +This provides a uniform way to handle variable binding and substitution. + +The module defines: +- `Subst`: A parallel substitution that maps variables from signature s₁ to + expressions/types in signature s₂ +- Lifting operations that extend substitutions to work under binders +- Opening operations for single-variable substitution +- Identity substitution and conversion from renamings + +Parallel substitutions generalize both renamings and single-variable substitutions. +The lifting operations extend substitutions to work under binders +while respecting the scoping disciplines of the intrinsically scoped syntax. + +A substitution σ : s₁ → s₂ assigns to each variable x ∈ s₁ an expression σ(x) +with variables in s₂, and to each type variable X ∈ s₁ a type σ(X) with variables in s₂. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core +/-- A parallel substitution maps term variables to expressions and type variables + to types. This allows simultaneous substitution of multiple variables while + preserving well-scopedness. -/ structure Subst (s1 s2 : Sig) where + /-- How to substitute term variables -/ var : Var s1 -> Exp s2 + /-- How to substitute type variables -/ tvar : TVar s1 -> Ty s2 -def Subst.liftVar (s : Subst s1 s2) : Subst (s1,x) (s2,x) := by - constructor - case var => - intro x; cases x - case here => exact .var .here - case there_var x0 => exact (s.var x0).rename Rename.succVar - case tvar => - intro X; cases X - case there_var X0 => exact (s.tvar X0).rename Rename.succVar +/-- Lift a substitution to work under a term variable binder. The newly bound + variable is mapped to itself, while existing variables are substituted and + then weakened to account for the new binding. -/ +def Subst.liftVar (s : Subst s1 s2) : Subst (s1,x) (s2,x) := + { var := fun x => match x with + | .here => .var .here + | .there_var x0 => (s.var x0).rename Rename.succVar + tvar := fun X => match X with + | .there_var X0 => (s.tvar X0).rename Rename.succVar } -def Subst.liftTVar (s : Subst s1 s2) : Subst (s1,X) (s2,X) := by - constructor - case tvar => - intro X; cases X - case here => exact .tvar .here - case there_tvar X0 => exact (s.tvar X0).rename Rename.succTVar - case var => - intro x; cases x - case there_tvar x0 => exact (s.var x0).rename Rename.succTVar +/-- Lift a substitution to work under a type variable binder. The newly bound + type variable is mapped to itself, while existing variables are substituted + and then weakened to account for the new binding. -/ +def Subst.liftTVar (s : Subst s1 s2) : Subst (s1,X) (s2,X) := + { tvar := fun X => match X with + | .here => .tvar .here + | .there_tvar X0 => (s.tvar X0).rename Rename.succTVar + var := fun x => match x with + | .there_tvar x0 => (s.var x0).rename Rename.succTVar } -def Subst.open_var (e : Exp s) : Subst (s,x) s := by - constructor - case var => - intro x; cases x - case here => exact e - case there_var x0 => exact .var x0 - case tvar => - intro X; cases X - case there_var X0 => exact .tvar X0 +/-- Create a substitution that replaces the outermost term variable with the given + expression, while leaving all other variables unchanged. This is used for + function application (beta reduction). -/ +def Subst.open_var (e : Exp s) : Subst (s,x) s := + { var := fun x => match x with + | .here => e + | .there_var x0 => .var x0 + tvar := fun X => match X with + | .there_var X0 => .tvar X0 } -def Subst.open_tvar (T : Ty s) : Subst (s,X) s := by - constructor - case var => - intro x; cases x - case there_tvar x0 => exact .var x0 - case tvar => - intro X; cases X - case here => exact T - case there_tvar X0 => exact .tvar X0 +/-- Create a substitution that replaces the outermost type variable with the given + type, while leaving all other variables unchanged. This is used for + type application in polymorphic functions. -/ +def Subst.open_tvar (T : Ty s) : Subst (s,X) s := + { var := fun x => match x with + | .there_tvar x0 => .var x0 + tvar := fun X => match X with + | .here => T + | .there_tvar X0 => .tvar X0 } -def Rename.asSubst (f : Rename s1 s2) : Subst s1 s2 := by - constructor - case var => intro x; exact .var (f.var x) - case tvar => intro X; exact .tvar (f.tvar X) +/-- Convert a renaming into a substitution. Every variable is mapped to the + correspondingly renamed variable. -/ +def Rename.asSubst (f : Rename s1 s2) : Subst s1 s2 := + { var := fun x => .var (f.var x) + tvar := fun X => .tvar (f.tvar X) } +/-- Functional extensionality for substitutions: two substitutions are equal + if they map all variables in the same way. -/ theorem Subst.funext {σ1 σ2 : Subst s1 s2} (var : ∀ x, σ1.var x = σ2.var x) (tvar : ∀ X, σ1.tvar X = σ2.tvar X) : σ1 = σ2 := by @@ -58,12 +88,14 @@ theorem Subst.funext {σ1 σ2 : Subst s1 s2} { funext x; aesop } { funext X; aesop } +/-- Lift a substitution to work under multiple binders specified by a signature. + This generalizes `liftVar` and `liftTVar` to arbitrary sequences of binders. -/ def Subst.lift : Subst s1 s2 -> (s : Sig) -> Subst (s1 ++ s) (s2 ++ s) | σ, .empty => σ -| σ, .cons_var s => (σ.lift s).liftVar -| σ, .cons_tvar s => (σ.lift s).liftTVar +| σ, .push_var s => (σ.lift s).liftVar +| σ, .push_tvar s => (σ.lift s).liftTVar -def Subst.id : Subst s s := by - constructor - case var => intro x; exact .var x - case tvar => intro X; exact .tvar X +/-- The identity substitution that maps each variable to itself. -/ +def Subst.id : Subst s s := + { var := fun x => .var x + tvar := fun X => .tvar X } diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean index 09ec22cc..732e458c 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean @@ -1,73 +1,79 @@ +/- +# Properties of parallel substitution for System F<: + +This module establishes the fundamental algebraic properties of parallel substitution +that are essential for the metatheory of System F<:. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Subst -def Subst.comp (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : Subst s1 s3 := by - constructor - case var => - intro x; exact (σ1.var x).subst σ2 - case tvar => - intro X; exact (σ1.tvar X).subst σ2 +/-- Composition of substitutions. If σ₁ maps s₁ to s₂ and σ₂ maps s₂ to s₃, + then their composition maps s₁ to s₃ by first applying σ₁ then σ₂. -/ +def Subst.comp (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : Subst s1 s3 := + { var := fun x => (σ1.var x).subst σ2 + tvar := fun X => (σ1.tvar X).subst σ2 } +/-- Shows that lifting a substitution for term variables preserves type variable mappings + by renaming with succVar. -/ theorem Subst.tvar_there_var_liftVar {σ : Subst s1 s2} : (σ.liftVar.tvar (.there_var X)) = (σ.tvar X).rename Rename.succVar := rfl +/-- Shows that lifting a substitution for type variables preserves older type variable mappings + by renaming with succTVar. -/ theorem Subst.tvar_there_tvar_liftTVar {σ : Subst s1 s2} : (σ.liftTVar.tvar (.there_tvar X)) = (σ.tvar X).rename Rename.succTVar := rfl +/-- Shows that lifting a substitution for type variables preserves term variable mappings + by renaming with succTVar. -/ theorem Subst.var_there_tvar_liftTVar {σ : Subst s1 s2} : (σ.liftTVar.var (.there_tvar x)) = (σ.var x).rename Rename.succTVar := rfl +/-- For type variables, substitution followed by term variable weakening equals + term variable weakening followed by substitution with a lifted substitution. -/ theorem Ty.tvar_subst_succVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) : ((tvar X).subst (σ.lift s0)).rename (Rename.succVar.lift s0) = ((tvar X).rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by induction s0 case empty => rfl - case cons_var s0 ih => + case push_var s0 ih => cases X case there_var X0 => simp [Subst.lift, Ty.subst] conv => lhs; simp [Subst.liftVar] - conv => - rhs; simp [Ty.rename, Rename.lift, Rename.liftVar] - simp [Ty.subst] - simp [Subst.tvar_there_var_liftVar] - simp [Rename.lift] - simp [<-Ty.rename_succVar_comm] - congr - exact (ih (X:=X0)) - case cons_tvar s0 ih => - cases X - case here => rfl + conv => rhs; simp [Subst.tvar_there_var_liftVar] + simp [Rename.lift, <-Ty.rename_succVar_comm] + congr; exact (ih (X:=X0)) + case push_tvar s0 ih => + cases X <;> try rfl case there_tvar X0 => conv => lhs; simp [Subst.lift, Ty.subst] conv => lhs; simp [Subst.liftTVar, Rename.lift] simp [<-Ty.rename_succTVar_comm] - congr - exact (ih (X:=X0)) + congr; exact (ih (X:=X0)) +/-- Proves that substitution commutes with type variable weakening for type variables. -/ theorem Ty.tvar_subst_succTVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) : ((tvar X).subst (σ.lift s0)).rename (Rename.succTVar.lift s0) = ((tvar X).rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by induction s0 case empty => rfl - case cons_var s0 ih => + case push_var s0 ih => cases X case there_var X0 => conv => lhs; simp [Subst.lift, Ty.subst] conv => lhs; simp [Subst.liftVar, Rename.lift] simp [<-Ty.rename_succVar_comm] - congr - exact (ih (X:=X0)) - case cons_tvar s0 ih => - cases X - case here => rfl + congr; exact (ih (X:=X0)) + case push_tvar s0 ih => + cases X <;> try rfl case there_tvar X0 => conv => lhs; simp [Subst.lift, Ty.subst] conv => lhs; simp [Subst.liftTVar, Rename.lift] simp [<-Ty.rename_succTVar_comm] - congr - exact (ih (X:=X0)) + congr; exact (ih (X:=X0)) +/-- Proves that substitution commutes with term variable weakening for types. -/ theorem Ty.subst_succVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) : (T.subst (σ.lift s0)).rename (Rename.succVar.lift s0) = (T.rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by @@ -77,15 +83,13 @@ theorem Ty.subst_succVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) : | .arrow T1 T2 => have ih1 := Ty.subst_succVar_comm (T:=T1) (σ:=σ) have ih2 := Ty.subst_succVar_comm (T:=T2) (σ:=σ) - simp [Ty.subst, Ty.rename] - simp [ih1, ih2] + grind [Ty.subst, Ty.rename] | .poly T1 T2 => have ih1 := Ty.subst_succVar_comm (T:=T1) (σ:=σ) have ih2 := Ty.subst_succVar_comm (s0:=s0,X) (T:=T2) (σ:=σ) - simp [Ty.subst, Ty.rename] - simp [ih1] - exact ih2 + simp [Ty.subst, Ty.rename, ih1]; exact ih2 +/-- Proves that substitution commutes with type variable weakening for types. -/ theorem Ty.subst_succTVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) : (T.subst (σ.lift s0)).rename (Rename.succTVar.lift s0) = (T.rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by @@ -95,80 +99,73 @@ theorem Ty.subst_succTVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) : | .arrow T1 T2 => have ih1 := Ty.subst_succTVar_comm (T:=T1) (σ:=σ) have ih2 := Ty.subst_succTVar_comm (T:=T2) (σ:=σ) - simp [Ty.subst, Ty.rename] - simp [ih1, ih2] + grind [Ty.subst, Ty.rename] | .poly T1 T2 => have ih1 := Ty.subst_succTVar_comm (T:=T1) (σ:=σ) have ih2 := Ty.subst_succTVar_comm (s0:=s0,X) (T:=T2) (σ:=σ) - simp [Ty.subst, Ty.rename] - simp [ih1] - exact ih2 + simp [Ty.subst, Ty.rename, ih1]; exact ih2 +/-- Base case of substitution commuting with term variable weakening. -/ theorem Ty.subst_succVar_comm_base {T : Ty s1} (σ : Subst s1 s2) : (T.subst σ).rename Rename.succVar = (T.rename Rename.succVar).subst (σ.liftVar) := by exact Ty.subst_succVar_comm (T:=T) (σ:=σ) (s0:=Sig.empty) +/-- Base case of substitution commuting with type variable weakening. -/ theorem Ty.subst_succTVar_comm_base {T : Ty s1} (σ : Subst s1 s2) : (T.subst σ).rename Rename.succTVar = (T.rename Rename.succTVar).subst (σ.liftTVar) := by exact Ty.subst_succTVar_comm (T:=T) (σ:=σ) (s0:=Sig.empty) +/-- Shows that renaming an expression commutes with type variable weakening. -/ theorem Exp.rename_succTVar_comm {e : Exp s1} {f : Rename s1 s2} : (e.rename f).rename Rename.succTVar = (e.rename Rename.succTVar).rename f.liftTVar := by simp [Exp.rename_comp, Rename.rename_succTVar_comm] +/-- Shows that renaming an expression commutes with term variable weakening. -/ theorem Exp.rename_succVar_comm {e : Exp s1} {f : Rename s1 s2} : (e.rename f).rename Rename.succVar = (e.rename Rename.succVar).rename f.liftVar := by simp [Exp.rename_comp, Rename.rename_succVar_comm] +/-- Proves that substitution commutes with type variable weakening for variables. -/ theorem Exp.var_subst_succTVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) : ((var x).subst (σ.lift s0)).rename (Rename.succTVar.lift s0) = ((var x).rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by - induction s0 - case empty => rfl - case cons_var s0 ih => - cases x - case here => rfl + induction s0 <;> try rfl + case push_var s0 ih => + cases x <;> try rfl case there_var x0 => conv => lhs; simp [Subst.lift, Exp.subst] conv => lhs; simp [Subst.liftVar, Rename.lift] simp [<-Exp.rename_succVar_comm] - congr - exact (ih (x:=x0)) - case cons_tvar s0 ih => + congr; exact (ih (x:=x0)) + case push_tvar s0 ih => cases x case there_tvar x0 => - conv => lhs; simp [Subst.liftTVar] conv => lhs; simp [Subst.liftVar, Subst.lift, Rename.lift] conv => lhs; simp [Exp.subst, Subst.liftTVar] simp [<-Exp.rename_succTVar_comm] - congr - exact (ih (x:=x0)) + congr; exact (ih (x:=x0)) +/-- Proves that substitution commutes with term variable weakening for variables. -/ theorem Exp.var_subst_succVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) : ((var x).subst (σ.lift s0)).rename (Rename.succVar.lift s0) = ((var x).rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by - induction s0 - case empty => rfl - case cons_var s0 ih => - cases x - case here => rfl + induction s0 <;> try rfl + case push_var s0 ih => + cases x <;> try rfl case there_var x0 => - conv => lhs; simp [Subst.lift, Exp.subst] - conv => lhs; simp [Subst.liftVar, Rename.lift] + conv => lhs; simp [Subst.lift, Exp.subst, Subst.liftVar, Rename.lift] simp [<-Exp.rename_succVar_comm] - congr - exact (ih (x:=x0)) - case cons_tvar s0 ih => + congr; exact (ih (x:=x0)) + case push_tvar s0 ih => cases x case there_tvar x0 => - conv => lhs; simp [Subst.lift, Exp.subst] - conv => lhs; simp [Subst.liftTVar, Rename.lift] + conv => lhs; simp [Subst.lift, Exp.subst, Subst.liftTVar, Rename.lift] simp [<-Exp.rename_succTVar_comm] - congr - exact (ih (x:=x0)) + congr; exact (ih (x:=x0)) +/-- Proves that substitution commutes with type variable weakening for expressions. -/ theorem Exp.subst_succTVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) : (e.subst (σ.lift s0)).rename (Rename.succTVar.lift s0) = (e.rename (Rename.succTVar.lift s0)).subst (σ.liftTVar.lift s0) := by @@ -177,24 +174,21 @@ theorem Exp.subst_succTVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) : | .abs A t => have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ) have ih2 := Exp.subst_succTVar_comm (s0:=s0,x) (e:=t) (σ:=σ) - simp [Exp.subst, Exp.rename] - simp [ih1] - congr + simp [Exp.subst, Exp.rename, ih1]; congr | .tabs A t => have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ) have ih2 := Exp.subst_succTVar_comm (s0:=s0,X) (e:=t) (σ:=σ) - simp [Exp.subst, Exp.rename, ih1] - congr + simp [Exp.subst, Exp.rename, ih1]; congr | .app t1 t2 => have ih1 := Exp.subst_succTVar_comm (e:=t1) (σ:=σ) have ih2 := Exp.subst_succTVar_comm (e:=t2) (σ:=σ) - simp [Exp.subst, Exp.rename] - simp [ih1, ih2] + simp [Exp.subst, Exp.rename, ih1, ih2] | .tapp t A => have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ) have ih2 := Exp.subst_succTVar_comm (s0:=s0) (e:=t) (σ:=σ) simp [Exp.subst, Exp.rename, ih1, ih2] +/-- Proves that substitution commutes with term variable weakening for expressions. -/ theorem Exp.subst_succVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) : (e.subst (σ.lift s0)).rename (Rename.succVar.lift s0) = (e.rename (Rename.succVar.lift s0)).subst (σ.liftVar.lift s0) := by @@ -203,14 +197,11 @@ theorem Exp.subst_succVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) : | .abs A t => have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ) have ih2 := Exp.subst_succVar_comm (s0:=s0,x) (e:=t) (σ:=σ) - simp [Exp.subst, Exp.rename] - simp [ih1] - congr + simp [Exp.subst, Exp.rename, ih1]; congr | .tabs A t => have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ) have ih2 := Exp.subst_succVar_comm (s0:=s0,X) (e:=t) (σ:=σ) - simp [Exp.subst, Exp.rename, ih1] - congr + simp [Exp.subst, Exp.rename, ih1]; congr | .app t1 t2 => have ih1 := Exp.subst_succVar_comm (e:=t1) (σ:=σ) have ih2 := Exp.subst_succVar_comm (e:=t2) (σ:=σ) @@ -220,6 +211,7 @@ theorem Exp.subst_succVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) : have ih2 := Exp.subst_succVar_comm (s0:=s0) (e:=t) (σ:=σ) simp [Exp.subst, Exp.rename, ih1, ih2] +/-- Proves that lifting a substitution for type variables commutes with composition. -/ theorem Subst.liftTVar_comp {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : (σ1.comp σ2).liftTVar = σ1.liftTVar.comp σ2.liftTVar := by apply Subst.funext @@ -230,254 +222,163 @@ theorem Subst.liftTVar_comp {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : simpa [Subst.lift, Rename.lift] using (Exp.subst_succTVar_comm (s0:=Sig.empty) (σ:=σ2)) case tvar => - intro X; cases X - case here => rfl + intro X; cases X <;> try rfl case there_tvar X0 => - simp [Subst.comp, Subst.liftTVar] simpa [Subst.lift, Rename.lift] using (Ty.subst_succTVar_comm (s0:=Sig.empty) (T:=σ1.tvar X0) (σ:=σ2)) +/-- Proves that lifting a substitution for term variables commutes with composition. -/ theorem Subst.liftVar_comp {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : (σ1.comp σ2).liftVar = σ1.liftVar.comp σ2.liftVar := by apply Subst.funext case var => - intro x; cases x + intro x; cases x <;> try rfl case there_var x0 => - simp [Subst.comp, Subst.liftVar] simpa [Subst.lift, Rename.lift] using (Exp.subst_succVar_comm (s0:=Sig.empty) (σ:=σ2)) - case here => rfl case tvar => intro X; cases X case there_var X0 => - simp [Subst.comp] simpa [Subst.lift, Rename.lift] using (Ty.subst_succVar_comm (s0:=Sig.empty) (T:=σ1.tvar X0) (σ:=σ2)) +/-- **Fundamental associativity law for substitution composition on types**: + Sequential application of substitutions equals composition. + + This states that (T[σ₁])[σ₂] = T[σ₁ ∘ σ₂], establishing that substitution + forms a category-like structure. This is essential for reasoning about + complex substitution chains in proofs. -/ theorem Ty.subst_comp {T : Ty s1} (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : (T.subst σ1).subst σ2 = T.subst (σ1.comp σ2) := by - induction T generalizing s2 s3 - case top => rfl - case tvar X => rfl - case arrow T1 T2 ih1 ih2 => - simp [Ty.subst] - simp [ih1, ih2] - case poly T1 T2 ih1 ih2 => - simp [Ty.subst] - simp [ih1] - simp [Subst.liftTVar_comp] - simp [ih2] + induction T generalizing s2 s3 <;> try (solve | rfl) + all_goals simp [Ty.subst, Subst.liftTVar_comp]; grind + +/-- **Fundamental associativity law for substitution composition on expressions**: + Sequential application of substitutions equals composition. + This extends the associativity property to expressions, ensuring that + the substitution algebra is consistent across all syntactic categories. -/ theorem Exp.subst_comp {e : Exp s1} (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : (e.subst σ1).subst σ2 = e.subst (σ1.comp σ2) := by induction e generalizing s2 s3 case var x => rfl - case abs A t ih => - simp [Exp.subst] - simp [Ty.subst_comp] - simp [Subst.liftVar_comp] - simp [ih] - case tabs A t ih => - simp [Exp.subst] - simp [Ty.subst_comp] - simp [Subst.liftTVar_comp] - simp [ih] - case app t1 t2 ih1 ih2 => - simp [Exp.subst] - simp [ih1] - simp [ih2] - case tapp t A ih => - simp [Exp.subst] - simp [Ty.subst_comp] - simp [ih] + all_goals grind [Exp.subst, Ty.subst_comp, Subst.liftVar_comp, Subst.liftTVar_comp] +/-- Shows that converting a rename to a substitution commutes with lifting for type variables. -/ theorem Rename.asSubst_liftTVar_comm {f : Rename s1 s2} : (f.asSubst).liftTVar = f.liftTVar.asSubst := by - apply Subst.funext - case var => - intro x; cases x - case there_tvar x0 => rfl - case tvar => - intro X; cases X - case here => rfl - case there_tvar X0 => rfl + apply Subst.funext <;> intro a <;> cases a <;> rfl +/-- Shows that converting a rename to a substitution commutes with lifting for term variables. -/ theorem Rename.asSubst_liftVar_comm {f : Rename s1 s2} : (f.asSubst).liftVar = f.liftVar.asSubst := by - apply Subst.funext - case var => - intro x; cases x - case here => rfl - case there_var x0 => rfl - case tvar => intro X; cases X; rfl + apply Subst.funext <;> intro a <;> cases a <;> rfl +/-- Proves that substituting with a rename-as-substitution equals renaming for types. -/ theorem Ty.subst_asSubst {T : Ty s1} {f : Rename s1 s2} : T.subst f.asSubst = T.rename f := by induction T generalizing s2 - case top => rfl - case tvar => rfl - case arrow T1 T2 ih1 ih2 => simp [Ty.subst, Ty.rename, ih1, ih2] - case poly T1 T2 ih1 ih2 => - simp [Ty.subst, Ty.rename] - simp [ih1] - simp [Rename.asSubst_liftTVar_comm] - simp [ih2] + <;> try (solve | rfl | grind [Ty.subst, Ty.rename, Rename.asSubst_liftTVar_comm]) +/-- Proves that substituting with a rename-as-substitution equals renaming for expressions. -/ theorem Exp.subst_asSubst {e : Exp s1} {f : Rename s1 s2} : e.subst f.asSubst = e.rename f := by induction e generalizing s2 case var x => rfl - case abs A t ih => - simp [Exp.subst, Exp.rename, Ty.subst_asSubst] - simp [Rename.asSubst_liftVar_comm] - simp [ih] - case tabs A t ih => - simp [Exp.subst, Exp.rename, Ty.subst_asSubst] - simp [Rename.asSubst_liftTVar_comm] - simp [ih] - case app t1 t2 ih1 ih2 => - simp [Exp.subst, Exp.rename, ih1, ih2] - case tapp t A ih => - simp [Exp.subst, Exp.rename, Ty.subst_asSubst] - simp [ih] + all_goals (simp [Exp.subst, Exp.rename, + Ty.subst_asSubst, Rename.asSubst_liftVar_comm, Rename.asSubst_liftTVar_comm]; grind) +/-- Shows that lifting the identity substitution for term variables gives the identity. -/ theorem Subst.id_liftVar : (Subst.id (s:=s)).liftVar = Subst.id := by - apply Subst.funext - case var => intro x; cases x <;> rfl - case tvar => intro X; cases X; rfl + apply Subst.funext <;> intro a <;> cases a <;> rfl +/-- Shows that lifting the identity substitution for type variables gives the identity. -/ theorem Subst.id_liftTVar : (Subst.id (s:=s)).liftTVar = Subst.id := by - apply Subst.funext - case var => intro x; cases x; rfl - case tvar => intro X; cases X <;> rfl + apply Subst.funext <;> intro a <;> cases a <;> rfl +/-- **Identity law for types**: The identity substitution acts as neutral element. + This establishes that T[id] = T, showing that substitution has the proper + categorical structure with identity morphisms. -/ theorem Ty.subst_id {T : Ty s} : T.subst Subst.id = T := by - induction T - case top => rfl - case tvar => rfl - case arrow T1 T2 ih1 ih2 => - simp [Ty.subst, ih1, ih2] - case poly T1 T2 ih1 ih2 => - simp [Ty.subst, ih1] - simp [Subst.id_liftTVar] - simp [ih2] + induction T <;> try (solve | rfl) + all_goals (simp [Ty.subst, Subst.id_liftTVar]; grind) +/-- **Identity law for expressions**: The identity substitution acts as neutral element. + This extends the identity property to expressions, completing the algebraic + structure of the substitution category. -/ theorem Exp.subst_id {e : Exp s} : e.subst Subst.id = e := by - induction e - case var x => rfl - case abs A t ih => - simp [Exp.subst, Ty.subst_id] - simp [Subst.id_liftVar] - simp [ih] - case tabs A t ih => - simp [Exp.subst, Ty.subst_id] - simp [Subst.id_liftTVar] - simp [ih] - case app t1 t2 ih1 ih2 => - simp [Exp.subst, ih1, ih2] - case tapp t A ih => - simp [Exp.subst, Ty.subst_id] - simp [ih] + induction e <;> try (solve | rfl) + all_goals (simp [Exp.subst, Ty.subst_id, Subst.id_liftVar, Subst.id_liftTVar]; grind) +/-- Proves that opening a type variable commutes with renaming for substitutions. -/ theorem Subst.open_tvar_rename_comm {T : Ty s} {f : Rename s s'} : (Subst.open_tvar T).comp (f.asSubst) = f.liftTVar.asSubst.comp (Subst.open_tvar (T.rename f)) := by apply Subst.funext - case var => - intro x - cases x - case there_tvar x0 => rfl - case tvar => - intro X - cases X - case here => - simp [Subst.comp] - conv => lhs; simp [Subst.open_tvar] - conv => - rhs; simp [Rename.asSubst, Rename.liftTVar, Ty.subst] - simp [Subst.open_tvar] - simp [Ty.subst_asSubst] - case there_tvar X0 => rfl + case var => intro x; cases x; rfl + case tvar => intro X; cases X <;> try (solve | rfl | simp [Subst.comp, Ty.subst_asSubst]; rfl) +/-- Proves that opening a type variable commutes with renaming for types. -/ theorem Ty.open_tvar_rename_comm {T : Ty (s,X)} {U : Ty s} {f : Rename s s'} : (T.open_tvar U).rename f = (T.rename f.liftTVar).open_tvar (U.rename f) := by simp [Ty.open_tvar, <-Ty.subst_asSubst] - simp [Ty.subst_comp] - simp [Subst.open_tvar_rename_comm] - simp [Ty.subst_asSubst] + grind [Ty.subst_comp, Subst.open_tvar_rename_comm, Ty.subst_asSubst] +/-- Shows that successively weakening then opening a type variable gives the identity. -/ theorem Subst.succTVar_open_tvar {T : Ty s} : - Rename.succTVar.asSubst.comp (Subst.open_tvar T) = Subst.id := by - apply Subst.funext - case var => intro x; rfl - case tvar => intro X; rfl + Rename.succTVar.asSubst.comp (Subst.open_tvar T) = Subst.id := by apply Subst.funext <;> aesop +/-- Proves that renaming with succTVar then opening cancels out for expressions. -/ theorem Exp.rename_succTVar_open_tvar {e : Exp s} : (e.rename Rename.succTVar).subst (Subst.open_tvar X) = e := by simp [<-Exp.subst_asSubst] - simp [Exp.subst_comp] - simp [Subst.succTVar_open_tvar] - simp [Exp.subst_id] + grind [Exp.subst_comp, Subst.succTVar_open_tvar, Exp.subst_id] +/-- Proves that renaming with succTVar then opening cancels out for types. -/ theorem Ty.rename_succTVar_open_tvar {T : Ty s} : (T.rename Rename.succTVar).subst (Subst.open_tvar X) = T := by simp [<-Ty.subst_asSubst] - simp [Ty.subst_comp] - simp [Subst.succTVar_open_tvar] - simp [Ty.subst_id] + grind [Ty.subst_comp, Subst.succTVar_open_tvar, Ty.subst_id] +/-- Shows that successively weakening then opening a term variable gives the identity. -/ theorem Subst.succVar_open_var {e : Exp s} : - Rename.succVar.asSubst.comp (Subst.open_var e) = Subst.id := by - apply Subst.funext - case var => intro x; rfl - case tvar => intro X; rfl + Rename.succVar.asSubst.comp (Subst.open_var e) = Subst.id := by apply Subst.funext <;> aesop +/-- Proves that renaming with succVar then opening cancels out for expressions. -/ theorem Exp.rename_succVar_open_var {e : Exp s} : (e.rename Rename.succVar).subst (Subst.open_var X) = e := by simp [<-Exp.subst_asSubst] - simp [Exp.subst_comp] - simp [Subst.succVar_open_var] - simp [Exp.subst_id] + grind [Exp.subst_comp, Subst.succVar_open_var, Exp.subst_id] +/-- Proves that renaming with succVar then opening cancels out for types. -/ theorem Ty.rename_succVar_open_var {T : Ty s} : (T.rename Rename.succVar).subst (Subst.open_var X) = T := by simp [<-Ty.subst_asSubst] - simp [Ty.subst_comp] - simp [Subst.succVar_open_var] - simp [Ty.subst_id] + grind [Ty.subst_comp, Subst.succVar_open_var, Ty.subst_id] +/-- Proves that opening a type variable commutes with substitution for substitutions. -/ theorem Subst.open_tvar_subst_comm {T : Ty s} {σ : Subst s s'} : (Subst.open_tvar T).comp σ = σ.liftTVar.comp (Subst.open_tvar (T.subst σ)) := by apply Subst.funext case var => - intro x - cases x + intro x; cases x conv => lhs; simp [Subst.comp, Subst.open_tvar] - conv => - rhs - simp [Subst.comp, Subst.liftTVar] - simp [Exp.rename_succTVar_open_tvar] - rfl + conv => rhs; simp [Subst.comp, Subst.liftTVar] + simp [Exp.rename_succTVar_open_tvar]; rfl case tvar => - intro X - cases X - case here => rfl + intro X; cases X <;> try rfl case there_tvar X0 => conv => lhs; simp [Subst.comp, Subst.open_tvar] - conv => - rhs - simp [Subst.comp, Subst.liftTVar] - simp [Ty.rename_succTVar_open_tvar] - rfl + conv => rhs; simp [Subst.comp, Subst.liftTVar] + simp [Ty.rename_succTVar_open_tvar]; rfl +/-- Proves that opening a type variable commutes with substitution for types. -/ theorem Ty.open_tvar_subst_comm {T : Ty (s,X)} {U : Ty s} {σ : Subst s s'} : (T.open_tvar U).subst σ = (T.subst σ.liftTVar).open_tvar (U.subst σ) := by - simp [Ty.open_tvar] - simp [Ty.subst_comp] - simp [Subst.open_tvar_subst_comm] + simp [Ty.open_tvar, Ty.subst_comp, Subst.open_tvar_subst_comm] diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean index 5cc6f61b..64f60e1f 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean @@ -1,3 +1,14 @@ +/- +# System F<: syntax + +This module aggregates all the syntactic components of System F<:. + +## Components: +- `Core`: Basic types and expressions with their renaming operations +- `Context`: Typing contexts and variable lookup relations +- `Subst`: Substitution operations and their lifting under binders +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Context import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Subst diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean index 221ca0d1..f92e63b4 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean @@ -1,29 +1,53 @@ +/- +# Typing contexts for System F<: + +This module defines typing contexts and variable lookup relations for System F<:. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core +/-- A typing context assigns types to term variables and upper bounds to type variables. -/ inductive Ctx : Sig -> Type where +/-- Empty context -/ | empty : Ctx {} +/-- Extend with term variable x : T -/ | cons_var : Ctx s -> Ty s -> Ctx (s,x) +/-- Extend with type variable X <: T -/ | cons_tvar : Ctx s -> Ty s -> Ctx (s,X) +/-- Convenient notation for extending context with a term variable -/ infixl:50 ",x:" => Ctx.cons_var +/-- Convenient notation for extending context with a type variable -/ infixl:50 ",X<:" => Ctx.cons_tvar +/-- Variable lookup relation. `Ctx.LookupVar Γ x T` means that term variable `x` + has type `T` in context `Γ`. -/ +@[grind] inductive Ctx.LookupVar : Ctx s -> Var s -> Ty s -> Prop where +/-- Look up the most recently bound term variable -/ | here : Ctx.LookupVar (Γ,x:T) .here (T.rename Rename.succVar) +/-- Skip over a more recent term variable binding -/ | there_var : Ctx.LookupVar Γ x T -> Ctx.LookupVar (Γ,x:U) (x.there_var) (T.rename Rename.succVar) +/-- Skip over a more recent type variable binding -/ | there_tvar : Ctx.LookupVar Γ x T -> Ctx.LookupVar (Γ,X<:S) (x.there_tvar) (T.rename Rename.succTVar) +/-- Type variable lookup relation. `Ctx.LookupTVar Γ X T` means that type variable `X` + has upper bound `T` in context `Γ`. -/ +@[grind] inductive Ctx.LookupTVar : Ctx s -> TVar s -> Ty s -> Prop where +/-- Look up the most recently bound type variable -/ | here : Ctx.LookupTVar (Γ,X<:T) .here (T.rename Rename.succTVar) +/-- Skip over a more recent term variable binding -/ | there_var : Ctx.LookupTVar Γ X T -> Ctx.LookupTVar (Γ,x:U) X.there_var (T.rename Rename.succVar) +/-- Skip over a more recent type variable binding -/ | there_tvar : Ctx.LookupTVar Γ X T -> Ctx.LookupTVar (Γ,X<:S) X.there_tvar (T.rename Rename.succTVar) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean index d4211550..2c657664 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean @@ -1,24 +1,64 @@ +/- +# Core syntax for System F<: + +This module defines the core syntactic constructs of System F<: (System F with subtyping). +The syntax uses intrinsically scoped de Bruijn indices where variables are indexed by +signatures that ensure well-scopedness by construction. + +The module defines: +- `Ty`: Types including top type, type variables, function types, and polymorphic types +- `Exp`: Expressions including variables, abstractions, applications, and type applications +- Renaming operations for both types and expressions +- Value predicate identifying syntactic values + +The syntax is intrinsically well-scoped. +Variables cannot refer to bindings that don't exist. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Debruijn +/-- Types in System F<:. The type system includes: + - `top`: The universal supertype that all types are subtypes of + - `tvar`: Type variables, intrinsically scoped by signature + - `arrow`: Function types (A -> B) + - `poly`: Polymorphic types (forall X <: A. B) where B has access to type variable X -/ inductive Ty : Sig -> Type where +/-- The top type, supertype of all types -/ | top : Ty s +/-- Type variable -/ | tvar : TVar s -> Ty s +/-- Function type A -> B -/ | arrow : Ty s -> Ty s -> Ty s +/-- Polymorphic type ∀X<:A.B -/ | poly : Ty s -> Ty (s,X) -> Ty s +/-- Rename all type variables in a type according to the given renaming. -/ def Ty.rename : Ty s1 -> Rename s1 s2 -> Ty s2 | .top, _ => .top | .tvar X, ρ => .tvar (ρ.tvar X) | .arrow A B, ρ => .arrow (A.rename ρ) (B.rename ρ) | .poly A B, ρ => .poly (A.rename ρ) (B.rename ρ.liftTVar) +/-- Expressions in System F<:. The expression language includes: + - `var`: Term variables, intrinsically scoped + - `abs`: Function abstraction (λx:T. e) where T is the parameter type + - `tabs`: Type abstraction (ΛX<:T. e) for polymorphic functions + - `app`: Function application (e₁ e₂) + - `tapp`: Type application (e T) for instantiating polymorphic functions -/ inductive Exp : Sig -> Type where +/-- Term variable -/ | var : Var s -> Exp s +/-- Function abstraction λx:T.e -/ | abs : Ty s -> Exp (s,x) -> Exp s +/-- Type abstraction ΛX<:T.e -/ | tabs : Ty s -> Exp (s,X) -> Exp s +/-- Function application e₁ e₂ -/ | app : Exp s -> Exp s -> Exp s +/-- Type application e[T] -/ | tapp : Exp s -> Ty s -> Exp s +/-- Rename all variables (both term and type variables) in an expression + according to the given renaming. -/ def Exp.rename : Exp s1 -> Rename s1 s2 -> Exp s2 | .var x, ρ => .var (ρ.var x) | .abs A e, ρ => .abs (A.rename ρ) (e.rename ρ.liftVar) @@ -26,49 +66,45 @@ def Exp.rename : Exp s1 -> Rename s1 s2 -> Exp s2 | .app e1 e2, ρ => .app (e1.rename ρ) (e2.rename ρ) | .tapp e A, ρ => .tapp (e.rename ρ) (A.rename ρ) +/-- Renaming with the identity renaming leaves a type unchanged. -/ theorem Ty.rename_id {T : Ty s} : T.rename Rename.id = T := by - induction T - case top => rfl - case tvar => rfl - case arrow A B ihA ihB => simp [Ty.rename, ihA, ihB] - case poly A B ihA ihB => simp [Ty.rename, ihA, ihB] + induction T <;> try (solve | rfl | simp [Ty.rename]; grind) +/-- Renaming with the identity renaming leaves an expression unchanged. -/ theorem Exp.rename_id {e : Exp s} : e.rename Rename.id = e := by - induction e - case var => rfl - case abs A e ih => simp [Exp.rename, ih, Ty.rename_id] - case tabs A e ih => simp [Exp.rename, ih, Ty.rename_id] - case app e1 e2 ih1 ih2 => simp [Exp.rename, ih1, ih2] - case tapp e A ih => simp [Exp.rename, ih, Ty.rename_id] + induction e <;> try (solve | rfl | simp [Exp.rename, Ty.rename_id]; grind) +/-- Composition of renamings: renaming by f₁ then f₂ equals renaming by their composition. -/ theorem Ty.rename_comp {T : Ty s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} : (T.rename f1).rename f2 = T.rename (f1.comp f2) := by - induction T generalizing s2 s3 - case top => rfl - case tvar => rfl - case arrow A B ihA ihB => simp [Ty.rename, ihA, ihB] - case poly A B ihA ihB => - simp [Ty.rename, ihA] - simp [Rename.comp_liftTVar] - simp [ihB] + induction T generalizing s2 s3 <;> + try (solve | rfl | simp [Ty.rename, Rename.comp_liftTVar]; grind) +/-- Composition of renamings: renaming by f₁ then f₂ equals renaming by their composition. -/ theorem Exp.rename_comp {e : Exp s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} : (e.rename f1).rename f2 = e.rename (f1.comp f2) := by - induction e generalizing s2 s3 - case var => rfl - case abs A e ih => simp [Exp.rename, ih, Ty.rename_comp, Rename.comp_liftVar] - case tabs A e ih => simp [Exp.rename, ih, Ty.rename_comp, Rename.comp_liftTVar] - case app e1 e2 ih1 ih2 => simp [Exp.rename, ih1, ih2] - case tapp e A ih => simp [Exp.rename, ih, Ty.rename_comp] + induction e generalizing s2 s3 <;> + try (solve | rfl) + all_goals + simp [Exp.rename, Ty.rename_comp, Rename.comp_liftVar, Rename.comp_liftTVar]; grind +/-- Commutativity law for term variable weakening and general renamings. -/ theorem Ty.rename_succVar_comm {T : Ty s} : (T.rename f).rename Rename.succVar = (T.rename Rename.succVar).rename f.liftVar := by simp [Ty.rename_comp, Rename.rename_succVar_comm] +/-- Commutativity law for type variable weakening and general renamings. -/ theorem Ty.rename_succTVar_comm {T : Ty s} : (T.rename f).rename Rename.succTVar = (T.rename Rename.succTVar).rename f.liftTVar := by simp [Ty.rename_comp, Rename.rename_succTVar_comm] +/-- The value predicate identifies expressions that are syntactic values. + In System F<:, values are function abstractions and type abstractions. + This predicate is used in the operational semantics to determine when + evaluation has reached a final result. -/ +@[grind] inductive Exp.IsVal : Exp s -> Prop where +/-- Function abstractions are values -/ | abs : IsVal (.abs T e) +/-- Type abstractions are values -/ | tabs : IsVal (.tabs T e) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean index 802ab078..7369e7f5 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean @@ -1,11 +1,19 @@ +/- +# Substitution operations for System F<: syntax + +This module defines substitution operations for types and expressions in System F<:. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core +/-- Apply a parallel substitution to a type. -/ def Ty.subst : Ty s1 -> Subst s1 s2 -> Ty s2 | .top, _ => .top | .tvar X, s => s.tvar X | .arrow A B, s => .arrow (A.subst s) (B.subst s) | .poly A B, s => .poly (A.subst s) (B.subst s.liftTVar) +/-- Apply a parallel substitution to an expression. -/ def Exp.subst : Exp s1 -> Subst s1 s2 -> Exp s2 | .var x, s => s.var x | .abs A e, s => .abs (A.subst s) (e.subst s.liftVar) @@ -13,11 +21,14 @@ def Exp.subst : Exp s1 -> Subst s1 s2 -> Exp s2 | .app e1 e2, s => .app (e1.subst s) (e2.subst s) | .tapp e A, s => .tapp (e.subst s) (A.subst s) +/-- Substitute a concrete type for the outermost type variable in a polymorphic type. -/ def Ty.open_tvar (T : Ty (s,X)) (U : Ty s) : Ty s := T.subst (Subst.open_tvar U) +/-- Substitute a concrete expression for the outermost term variable in an expression. -/ def Exp.open_var (e : Exp (s,x)) (U : Exp s) : Exp s := e.subst (Subst.open_var U) +/-- Substitute a concrete type for the outermost type variable in an expression. -/ def Exp.open_tvar (e : Exp (s,X)) (U : Ty s) : Exp s := e.subst (Subst.open_tvar U) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean index ca1b2996..c3c85433 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean @@ -1,132 +1,79 @@ +/- +# Canonical forms lemmas for System F<: +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem +/-- Predicate for empty contexts -/ inductive Ctx.IsEmpty : Ctx s -> Prop where | empty_is_empty : Ctx.IsEmpty .empty theorem HasType.app_inv (ht : HasType Γ (.app e1 e2) T) : ∃ T1 T2, - HasType Γ e1 (.arrow T1 T2) - ∧ HasType Γ e2 T1 - ∧ Subtyp Γ T2 T := by + HasType Γ e1 (.arrow T1 T2) ∧ HasType Γ e2 T1 ∧ Subtyp Γ T2 T := by generalize he0 : Exp.app e1 e2 = e at ht - induction ht <;> cases he0 - case app T1 U1 _ ht1 ht2 _ _ => - use T1, U1 - split_ands - { exact ht1 } - { exact ht2 } - { apply Subtyp.refl } - case sub hsub _ ih => - have ⟨T1, T2, ht1, ht2, hs0⟩ := ih rfl - use T1, T2 - split_ands - { exact ht1 } - { exact ht2 } - { apply Subtyp.trans hs0 hsub } + induction ht <;> cases he0 <;> grind theorem Subtyp.top_inv (hsub : Subtyp Γ .top T) : T = .top := by generalize he0 : Ty.top = T at hsub - induction hsub <;> cases he0 - case top => rfl - case refl => rfl - case trans => aesop + induction hsub <;> cases he0 <;> try (solve | rfl | aesop) theorem Subtyp.arrow_inv_left (hsub : Subtyp Γ (.arrow T1 U1) T) : (∃ T2 U2, T = .arrow T2 U2) ∨ T = .top := by generalize he0 : Ty.arrow T1 U1 = T at hsub - induction hsub <;> cases he0 - case top => right; rfl - case refl => left; aesop - case arrow => left; aesop + induction hsub <;> cases he0 <;> try (solve | rfl | aesop) case trans ih1 _ ih2 => - specialize ih2 rfl - cases ih2 - case inl ih2 => - aesop - case inr ih2 => - cases ih2 - rename_i hsub _ - have heq := Subtyp.top_inv hsub - aesop + cases (ih2 rfl) + case inl ih2 => aesop + case inr ih2 => cases ih2; grind [Subtyp.top_inv] theorem Subtyp.poly_inv_left (hsub : Subtyp Γ (.poly T1 T2) T) : (∃ T3 T4, T = .poly T3 T4) ∨ T = .top := by generalize he0 : Ty.poly T1 T2 = T at hsub - induction hsub <;> cases he0 - case top => right; rfl - case refl => left; aesop - case poly => left; aesop + induction hsub <;> cases he0 <;> try (solve | aesop) case trans ih1 _ ih2 => - specialize ih2 rfl - cases ih2 - case inl ih2 => - aesop - case inr ih2 => - cases ih2 - rename_i hsub _ - have heq := Subtyp.top_inv hsub - aesop + cases (ih2 rfl) + case inl ih2 => aesop + case inr ih2 => cases ih2; grind [Subtyp.top_inv] theorem Subtype.tvar_inv_right (hsub : Subtyp Γ T (.tvar X)) : ∃ X0, T = .tvar X0 := by generalize he0 : Ty.tvar X = T0 at hsub - induction hsub <;> cases he0 - case refl => aesop - case trans => aesop - case tvar => aesop + induction hsub <;> cases he0 <;> try (solve | aesop) theorem Subtyp.arrow_inv_right (hsub : Subtyp Γ T (.arrow T2 U2)) : (∃ T1 U1, T = .arrow T1 U1) ∨ (∃ X, T = .tvar X) := by generalize he0 : Ty.arrow T2 U2 = T0 at hsub - induction hsub <;> cases he0 - case refl => aesop - case tvar => aesop - case arrow => aesop + induction hsub <;> cases he0 <;> try (solve | aesop) case trans ih1 _ ih2 => - specialize ih2 rfl - cases ih2 + cases (ih2 rfl) case inl ih2 => have ⟨T2, U2, h⟩ := ih2 - cases h - specialize ih1 rfl - aesop + cases h; specialize ih1 rfl; grind case inr ih2 => - have ⟨X, h⟩ := ih2 - cases h - rename_i hsub _ - have := Subtype.tvar_inv_right hsub - aesop + have ⟨X, h⟩ := ih2; cases h; rename_i hsub _ _ + have := Subtype.tvar_inv_right hsub; grind theorem Subtyp.poly_inv_right (hsub : Subtyp Γ T (.poly T2 U2)) : (∃ T1 U1, T = .poly T1 U1) ∨ (∃ X, T = .tvar X) := by generalize he0 : Ty.poly T2 U2 = T0 at hsub - induction hsub <;> cases he0 - case refl => aesop - case tvar => aesop - case poly => aesop + induction hsub <;> cases he0 <;> try (solve | aesop) case trans ih1 _ ih2 => - specialize ih2 rfl - cases ih2 - case inl ih2 => - have ⟨T2, U2, h⟩ := ih2 - cases h - specialize ih1 rfl - aesop + cases (ih2 rfl) + case inl ih2 => have ⟨T2, U2, h⟩ := ih2; cases h; grind case inr ih2 => - have ⟨X, h⟩ := ih2 - cases h - rename_i hsub _ - have := Subtype.tvar_inv_right hsub - aesop + have ⟨X, h⟩ := ih2; cases h + rename_i hsub _ _ + have := Subtype.tvar_inv_right hsub; grind theorem Subtyp.arrow_inv (hsub : Subtyp Γ (.arrow T1 U1) (.arrow T2 U2)) : @@ -135,24 +82,8 @@ theorem Subtyp.arrow_inv generalize he2 : Ty.arrow T2 U2 = P2 at hsub induction hsub <;> cases he1 <;> cases he2 case refl => constructor <;> apply Subtyp.refl - case trans hs1 ih1 hs2 ih2 => - have := Subtyp.arrow_inv_left hs1 - cases this - case inr h => - cases h - have := Subtyp.top_inv hs2 - contradiction - case inl h => - have ⟨T3, U3, h⟩ := h - cases h - specialize ih1 rfl rfl - specialize ih2 rfl rfl - have ⟨ih11, ih12⟩ := ih1 - have ⟨ih21, ih22⟩ := ih2 - constructor - { apply Subtyp.trans ih21 ih11 } - { apply Subtyp.trans ih12 ih22 } case arrow => aesop + case trans hs1 ih1 hs2 ih2 => cases (Subtyp.arrow_inv_left hs1) <;> grind [Subtyp.top_inv] theorem Subtyp.poly_inv (hsub : Subtyp Γ (.poly T1 U1) (.poly T2 U2)) : @@ -163,51 +94,28 @@ theorem Subtyp.poly_inv case refl => constructor <;> apply Subtyp.refl case poly => aesop case trans hs1 ih1 hs2 ih2 => - have := Subtyp.poly_inv_left hs1 - cases this + cases (Subtyp.poly_inv_left hs1) case inl h => - have ⟨T3, T4, h⟩ := h - cases h - specialize ih1 rfl rfl - specialize ih2 rfl rfl - have ⟨ih11, ih12⟩ := ih1 - have ⟨ih21, ih22⟩ := ih2 + have ⟨T3, T4, h⟩ := h; cases h + have ⟨ih11, ih12⟩ := ih1 rfl rfl; have ⟨ih21, ih22⟩ := ih2 rfl rfl constructor - { apply Subtyp.trans ih21 ih11 } + { grind } { have ih12' := ih12.retype (Retype.narrow_tvar ih21) - simp [Ty.subst_id] at ih12' - apply Subtyp.trans ih12' ih22 } - case inr h => - cases h - have := Subtyp.top_inv hs2 - contradiction + grind [Ty.subst_id] } + case inr h => cases h; grind [Subtyp.top_inv] theorem Subtyp.non_tvar_left_inv (hsub : Subtyp Γ T1 T2) (hnt : ∀ X, T1 ≠ .tvar X) : ∀ X, T2 ≠ .tvar X := by - induction hsub - case top => aesop - case refl => aesop - case tvar => - rename_i X _ _ - specialize hnt X - contradiction - case trans ih1 ih2 => aesop - case arrow => aesop - case poly => aesop + induction hsub <;> try (solve | aesop) theorem HasType.value_typing (hv : Exp.IsVal v) (ht : HasType Γ v T) : ∀ X, T ≠ .tvar X := by - induction ht <;> try (solve | cases hv) - case sub hsub _ ih => - specialize ih hv - apply Subtyp.non_tvar_left_inv hsub - exact ih - case abs => aesop - case tabs => aesop + induction ht <;> try (solve | cases hv | aesop) + case sub hsub _ _ => apply Subtyp.non_tvar_left_inv hsub; aesop theorem HasType.abs_inv {Γ : Ctx s} (ht : HasType Γ (.abs T0 e) (.arrow T1 U1)) : @@ -218,32 +126,11 @@ theorem HasType.abs_inv {Γ : Ctx s} generalize he1 : Exp.abs T0 e = t at ht generalize he2 : Ty.arrow T1 U1 = P at ht induction ht <;> cases he1 <;> cases he2 - case abs T0 t0 U0 ht _ => - use U0 - split_ands - { exact ht } - { apply Subtyp.refl } - { apply Subtyp.refl } + case abs T0 t0 U0 ht _ => use U0; split_ands <;> grind case sub hsub => - have := Subtyp.arrow_inv_right hsub - cases this - case inl h => - have ⟨T1, U1, h⟩ := h - cases h - rename_i ih - specialize ih rfl rfl - have ⟨U0, ih1, ih2, ih3⟩ := ih - have ⟨h1, h2⟩ := Subtyp.arrow_inv hsub - use U0 - split_ands - { exact ih1 } - { apply Subtyp.trans h1 ih2 } - { apply Subtyp.trans ih3 h2 } - case inr h => - have ⟨X, h⟩ := h - rename_i hv _ _ - have := HasType.value_typing (by constructor) hv - aesop + cases (Subtyp.arrow_inv_right hsub) + case inl h => have ⟨T1, U1, h⟩ := h; cases h; grind [Subtyp.arrow_inv] + case inr h => grind [HasType.value_typing] theorem HasType.tapp_inv (ht : HasType Γ (.tapp e T) U) : @@ -251,20 +138,7 @@ theorem HasType.tapp_inv HasType Γ e (.poly T T2) ∧ Subtyp Γ (T2.open_tvar T) U := by generalize he1 : Exp.tapp e T = t0 at ht - induction ht <;> cases he1 - case tapp => - rename_i T2 ht _ - use T2 - split_ands - { exact ht } - { apply Subtyp.refl } - case sub hs _ ih => - specialize ih rfl - have ⟨T2, ih1, ih2⟩ := ih - use T2 - split_ands - { exact ih1 } - { apply Subtyp.trans ih2 hs } + induction ht <;> cases he1 <;> grind theorem HasType.tabs_inv (ht : HasType Γ (.tabs T0 e) (.poly T1 U1)) : @@ -275,78 +149,37 @@ theorem HasType.tabs_inv generalize he1 : Exp.tabs T0 e = t0 at ht generalize he2 : Ty.poly T1 U1 = P at ht induction ht <;> cases he1 <;> cases he2 - case tabs T _ U h _ => - use U - split_ands - { exact h } - { apply Subtyp.refl } - { apply Subtyp.refl } + case tabs T _ U h _ => use U; split_ands <;> grind case sub ht ih hs => - have := Subtyp.poly_inv_right hs - cases this + cases (Subtyp.poly_inv_right hs) case inl h => have ⟨T2, U2, h⟩ := h - cases h - rename_i ih - specialize ih rfl rfl - have ⟨U0, ih1, ih2, ih3⟩ := ih + cases h; rename_i ih + have ⟨U0, ih1, ih2, ih3⟩ := ih rfl rfl have ⟨h1, h2⟩ := Subtyp.poly_inv hs - use U0 - split_ands - { exact ih1 } - { apply Subtyp.trans h1 ih2 } + use U0; split_ands <;> try grind { have ih3' := ih3.retype (Retype.narrow_tvar h1) - simp [Ty.subst_id] at ih3' - apply Subtyp.trans ih3' h2 } - case inr h => - have ⟨X, h⟩ := h - cases h - rename_i ht _ - have := HasType.value_typing (by constructor) ht - aesop + grind [Ty.subst_id] } + case inr h => grind [HasType.value_typing] theorem HasType.value_typing_arrow_inv - (hv : Exp.IsVal v) - (ht : HasType Γ v (.arrow T U)) : + (hv : Exp.IsVal v) (ht : HasType Γ v (.arrow T U)) : ∃ T0 e0, v = .abs T0 e0 := by generalize he : Ty.arrow T U = P at ht - induction ht <;> try (solve | cases he | cases hv) + induction ht <;> try (solve | cases he | cases hv | aesop) case sub ih => - cases he - rename_i hs - have := Subtyp.arrow_inv_right hs - cases this - case inl h => - have ⟨T1, U1, h⟩ := h - cases h - specialize ih hv rfl - trivial - case inr h => - have ⟨X, h⟩ := h - rename_i hvt _ - have := HasType.value_typing hv hvt - aesop - case abs => aesop + cases he; rename_i hs + cases (Subtyp.arrow_inv_right hs) + case inl h => aesop + case inr h => grind [HasType.value_typing] theorem HasType.value_typing_poly_inv - (hv : Exp.IsVal v) - (ht : HasType Γ v (.poly T U)) : + (hv : Exp.IsVal v) (ht : HasType Γ v (.poly T U)) : ∃ T0 e0, v = .tabs T0 e0 := by generalize he : Ty.poly T U = P at ht - induction ht <;> try (solve | cases he | cases hv) + induction ht <;> try (solve | cases he | cases hv | aesop) case sub ih => - cases he - rename_i hs - have := Subtyp.poly_inv_right hs - cases this - case inl h => - have ⟨T1, U1, h⟩ := h - cases h - specialize ih hv rfl - trivial - case inr h => - have ⟨X, h⟩ := h - rename_i hvt _ - have := HasType.value_typing hv hvt - aesop - case tabs => aesop + cases he; rename_i hs + cases (Subtyp.poly_inv_right hs) + case inl h => aesop + case inr h => grind [HasType.value_typing] diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean index e23dbd13..12271719 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean @@ -1,9 +1,25 @@ +/- +# Preservation theorem for System F<: + +This module proves the preservation theorem for System F<:. +Preservation states that if a well-typed expression takes a reduction step, +the result is still well-typed with the same type. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Reduce import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Canonical +/-- **Preservation theorem**: Well-typed expressions remain + well-typed after taking reduction steps. + + If `∅ ⊢ e : T` and `e ⟶ e'`, then `∅ ⊢ e' : T`. + + This is the fundamental type safety theorem establishing that computation + preserves typing invariants. Together with progress, this constitutes + the complete proof of type soundness for System F<:. -/ theorem preservation (ht : HasType .empty t T) (hred : Reduce t t') : @@ -11,14 +27,12 @@ theorem preservation induction hred generalizing T case red_app_fun ih => have ⟨T1, T2, ht1, ht2, hs0⟩ := HasType.app_inv ht - have ih := ih ht1 apply HasType.sub hs0 - apply HasType.app ih ht2 + apply HasType.app (ih ht1) ht2 case red_app_arg ih => have ⟨T1, T2, ht1, ht2, hs0⟩ := HasType.app_inv ht - have ih := ih ht2 apply HasType.sub hs0 - apply HasType.app ht1 ih + apply HasType.app ht1 (ih ht2) case red_app => have ⟨T1, T2, ht1, ht2, hs0⟩ := HasType.app_inv ht have ⟨U0, h1, h2, h3⟩ := HasType.abs_inv ht1 @@ -29,14 +43,12 @@ theorem preservation apply Subtyp.trans h3 hs0 case red_tapp_fun ih => have ⟨T2, ht1, hs2⟩ := HasType.tapp_inv ht - have ih := ih ht1 apply HasType.sub hs2 - apply HasType.tapp ih + apply HasType.tapp (ih ht1) case red_tapp => have ⟨T2, ht1, hs2⟩ := HasType.tapp_inv ht have ⟨U0, h1, h2, h3⟩ := HasType.tabs_inv ht1 have h1' := h1.retype (Retype.open_tvar h2) - rename_i R have h3' := h3.retype (Retype.open_tvar Subtyp.refl) apply HasType.sub _ h1' apply Subtyp.trans h3' hs2 diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean index 282dc878..44d98bd6 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean @@ -1,50 +1,50 @@ +/- +# Progress theorem for System F<: + +This module proves the progress theorem for System F<:. +Progress states that well-typed expressions in the empty context are either values +or can take a reduction step. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Reduce import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSoundness.Canonical +/-- Progress theorem: well-typed expressions in empty contexts either are values + or can take a reduction step. -/ theorem progress (ht : HasType Γ t T) (hem : Ctx.IsEmpty Γ) : (∃ t', Reduce t t') ∨ t.IsVal := by induction ht - case var hb => - cases hem - cases hb + case var hb => cases hem; cases hb case sub ih => aesop case abs => right; constructor case tabs => right; constructor case app ih1 ih2 => - specialize ih1 hem - cases ih1 + cases (ih1 hem) case inl ih1 => have ⟨t1', ih1⟩ := ih1 - left - constructor - apply Reduce.red_app_fun - exact ih1 + left; constructor + apply Reduce.red_app_fun ih1 case inr ih1 => - rename_i hvt _ - have := HasType.value_typing_arrow_inv ih1 hvt - have ⟨T0, e0, h⟩ := this + rename_i hvt _ _ + have ⟨T0, e0, h⟩ := HasType.value_typing_arrow_inv ih1 hvt cases h - left - constructor + left; constructor apply Reduce.red_app case tapp ih => specialize ih hem cases ih case inl ih => have ⟨t1', ih⟩ := ih - left - constructor - apply Reduce.red_tapp_fun - exact ih + left; constructor + apply Reduce.red_tapp_fun ih case inr ih => rename_i hvt have := HasType.value_typing_poly_inv ih hvt have ⟨T0, e0, h⟩ := this cases h - left - constructor + left; constructor apply Reduce.red_tapp diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean index a605a2e4..0962ff7a 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean @@ -1,44 +1,95 @@ +/- +# Type system for System F<: + +This module defines the core type system for System F<: (System F with bounded quantification). + +The module defines: +- `Subtyp`: The subtyping relation Γ ⊢ A <: B +- `HasType`: The typing relation Γ ⊢ e : T + +System F<: extends System F with bounded type quantification. +The subtyping relation includes structural rules (reflexivity, transitivity), +the top type as universal supertype, contravariant function subtyping, +and covariant bounded quantifier subtyping. + +The typing system is standard for System F<: with subsumption: +if an expression has type A and A <: B, then the expression also has type B. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax +/-- The subtyping relation for System F<:. `Subtyp Γ A B` means that type `A` is a + subtype of type `B` under context `Γ`. + + The rules include: + - `top`: Every type is a subtype of the top type + - `refl`: Subtyping is reflexive + - `trans`: Subtyping is transitive + - `tvar`: Type variables are subtypes of their bounds + - `arrow`: Function types are contravariant in domain, covariant in codomain + - `poly`: Polymorphic types are covariant in both bound and body -/ +@[grind] inductive Subtyp : Ctx s -> Ty s -> Ty s -> Prop where +/-- Every type is a subtype of the top type -/ | top : Subtyp Γ T .top +/-- Subtyping is reflexive -/ | refl : Subtyp Γ T T +/-- Subtyping is transitive -/ | trans : Subtyp Γ A B -> Subtyp Γ B C -> Subtyp Γ A C +/-- Type variables are subtypes of their declared upper bounds -/ | tvar : Ctx.LookupTVar Γ X T -> Subtyp Γ (.tvar X) T +/-- Function subtyping: contravariant in domain, covariant in codomain -/ | arrow : Subtyp Γ T2 T1 -> Subtyp Γ U1 U2 -> Subtyp Γ (.arrow T1 U1) (.arrow T2 U2) +/-- Polymorphic subtyping: covariant in bound and body -/ | poly : Subtyp Γ T2 T1 -> Subtyp (Γ,X<:T2) U1 U2 -> Subtyp Γ (.poly T1 U1) (.poly T2 U2) +/-- The typing relation for System F<:. `HasType Γ e T` means that expression `e` + has type `T` under context `Γ`. + + The rules include: + - `var`: Type variables according to context lookup + - `sub`: Subsumption - if e : T₁ and T₁ <: T₂ then e : T₂ + - `abs`: Function abstraction + - `tabs`: Type abstraction (polymorphic functions) + - `app`: Function application + - `tapp`: Type application (polymorphic instantiation) -/ inductive HasType : Ctx s -> Exp s -> Ty s -> Prop where +/-- Term variables have the type assigned in the context -/ | var : Ctx.LookupVar Γ x T -> HasType Γ (.var x) T +/-- Subsumption: if e : T₁ and T₁ <: T₂, then e : T₂ -/ | sub : Subtyp Γ T1 T2 -> HasType Γ t T1 -> HasType Γ t T2 +/-- Function abstraction: λx:T.e has type T -> U if e has type U under x:T -/ | abs : HasType (Γ,x:T) t (U.rename Rename.succVar) -> HasType Γ (.abs T t) (.arrow T U) +/-- Type abstraction: ΛX<:T.e has type ∀X<:T.U if e has type U under X<:T -/ | tabs : HasType (Γ,X<:T) t U -> HasType Γ (.tabs T t) (.poly T U) +/-- Function application: if e₁ : T -> U and e₂ : T, then e₁ e₂ : U -/ | app : HasType Γ t1 (.arrow T1 U1) -> HasType Γ t2 T1 -> HasType Γ (.app t1 t2) U1 +/-- Type application: if e : ∀X<:T.U and S <: T, then e[S] : U[X := S] -/ | tapp : HasType Γ t (.poly T U) -> HasType Γ (.tapp t T) (U.open_tvar T) From 6e1ed4bc80a7019ec9af36ea2f0ad4c860674e92 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sat, 13 Sep 2025 23:47:34 +0200 Subject: [PATCH 03/13] Add copyright --- .../LambdaCalculus/WellScoped/FSub/Debruijn.lean | 6 ++++++ .../Computability/LambdaCalculus/WellScoped/FSub/Eval.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean | 6 ++++++ .../WellScoped/FSub/RebindTheory/TypeSystem.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/Reduce.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean | 6 ++++++ .../WellScoped/FSub/RetypeTheory/TypeSystem.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/Substitution.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/Substitution/Core.lean | 6 ++++++ .../WellScoped/FSub/Substitution/Properties.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/Syntax.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/Syntax/Context.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/Syntax/Core.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean | 6 ++++++ .../WellScoped/FSub/TypeSoundness/Canonical.lean | 6 ++++++ .../WellScoped/FSub/TypeSoundness/Preservation.lean | 6 ++++++ .../WellScoped/FSub/TypeSoundness/Progress.lean | 6 ++++++ .../LambdaCalculus/WellScoped/FSub/TypeSystem.lean | 6 ++++++ 18 files changed, 108 insertions(+) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean index daf1d5c1..ee57fdd2 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Intrinsically scoped de Bruijn indices diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean index cec1543a..8f018c15 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Big-step evaluator for System F<: -/ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean index f4ec250d..afedacd5 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Rebinding morphisms diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean index 4585fe2d..65352c68 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.Core import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Properties diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean index aac43dad..af2f147b 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Operational semantics for System F<: diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean index 50dd4041..14aa85d1 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Retyping morphisms diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean index e66c5d02..045a6618 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.Core /-- Context retyping preserves subtyping judgments. -/ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean index 105aec17..a99da0f2 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Parallel substitution for System F<: diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean index 0aade90a..85a9478d 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Parallel substitution for System F<: diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean index 732e458c..676a7c61 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Properties of parallel substitution for System F<: diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean index 64f60e1f..520f87af 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # System F<: syntax diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean index f92e63b4..fbf4dbad 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Typing contexts for System F<: diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean index 2c657664..f6d71320 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Core syntax for System F<: diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean index 7369e7f5..4c677dce 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Substitution operations for System F<: syntax diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean index c3c85433..b8e4086c 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Canonical forms lemmas for System F<: -/ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean index 12271719..d3823965 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Preservation theorem for System F<: diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean index 44d98bd6..20f4ded1 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Progress.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Progress theorem for System F<: diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean index 0962ff7a..84221a75 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2025 Yichen Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yichen Xu. +-/ + /- # Type system for System F<: From 909c1cc7474d5c05b36d22880cbd3daa5534aa68 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 14 Sep 2025 00:15:39 +0200 Subject: [PATCH 04/13] Use simp only for a lot of cases --- .../WellScoped/FSub/RebindTheory/Core.lean | 12 +-- .../FSub/RebindTheory/TypeSystem.lean | 4 +- .../WellScoped/FSub/RetypeTheory/Core.lean | 12 +-- .../FSub/RetypeTheory/TypeSystem.lean | 2 +- .../FSub/Substitution/Properties.lean | 75 ++++++++++--------- .../WellScoped/FSub/Syntax/Core.lean | 9 ++- .../FSub/TypeSoundness/Preservation.lean | 2 +- 7 files changed, 59 insertions(+), 57 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean index afedacd5..282b1c93 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean @@ -43,15 +43,15 @@ structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.rename f) where var := fun x P hb => by cases hb - case here => simp [<-Ty.rename_succVar_comm]; constructor + case here => simp only [<-Ty.rename_succVar_comm]; constructor case there_var hb => - simp [<-Ty.rename_succVar_comm] + simp only [<-Ty.rename_succVar_comm] constructor apply ρ.var _ _ hb tvar := fun X S hb => by cases hb case there_var hb => - simp [<-Ty.rename_succVar_comm] + simp only [<-Ty.rename_succVar_comm] constructor apply ρ.tvar _ _ hb @@ -62,14 +62,14 @@ def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.r def Rebind.liftTVar (ρ : Rebind Γ f Δ) : Rebind (Γ,X<:T) (f.liftTVar) (Δ,X<:T.rename f) where tvar := fun X S hb => by cases hb - case here => simp [<-Ty.rename_succTVar_comm]; constructor + case here => simp only [<-Ty.rename_succTVar_comm]; constructor case there_tvar hb => - simp [<-Ty.rename_succTVar_comm] + simp only [<-Ty.rename_succTVar_comm] constructor apply ρ.tvar _ _ hb var := fun x P hb => by cases hb - case there_tvar hb => simp [<-Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb + case there_tvar hb => simp only [<-Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb /-- **Term variable weakening morphism**. diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean index 65352c68..9184739f 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean @@ -37,7 +37,7 @@ theorem HasType.rebind {f : Rename s1 s2} { apply ih ρ } case abs ih => apply HasType.abs - simp [Ty.rename_succVar_comm] + simp only [Ty.rename_succVar_comm] apply ih ρ.liftVar case tabs ih => apply HasType.tabs @@ -47,6 +47,6 @@ theorem HasType.rebind {f : Rename s1 s2} { apply ih1 ρ } { apply ih2 ρ } case tapp ih => - simp [Ty.open_tvar_rename_comm] + simp only [Ty.open_tvar_rename_comm] apply tapp aesop diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean index 14aa85d1..58effe36 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean @@ -40,17 +40,17 @@ def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P cases hb case here => apply HasType.var - simp [<-Ty.subst_succVar_comm_base] + simp only [<-Ty.subst_succVar_comm_base] constructor case there_var hb0 => have h0 := ρ.var _ _ hb0 - simp [<-Ty.subst_succVar_comm_base] + simp only [<-Ty.subst_succVar_comm_base] apply h0.rebind Rebind.succVar tvar := fun X S hb => by cases hb case there_var hb0 => have h0 := ρ.tvar _ _ hb0 - simp [<-Ty.subst_succVar_comm_base] + simp only [<-Ty.subst_succVar_comm_base] apply h0.rebind Rebind.succVar /-- Extends a retyping morphism to contexts with an additional type variable. -/ @@ -59,7 +59,7 @@ def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ, cases hb case there_tvar hb0 => have h0 := ρ.var _ _ hb0 - simp [<-Ty.subst_succTVar_comm_base] + simp only [<-Ty.subst_succTVar_comm_base] apply h0.rebind Rebind.succTVar tvar := fun X S hb => by cases hb @@ -68,7 +68,7 @@ def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ, grind [Ty.subst_succTVar_comm_base] case there_tvar hb0 => have h0 := ρ.tvar _ _ hb0 - simp [<-Ty.subst_succTVar_comm_base] + simp only [<-Ty.subst_succTVar_comm_base] apply h0.rebind Rebind.succTVar /-- Creates a retyping morphism that substitutes an expression for the newest term variable. -/ @@ -93,7 +93,7 @@ def Retype.narrow_tvar case here => apply Subtyp.trans { apply Subtyp.tvar; constructor } - { simp [Ty.subst_id]; apply hs.rebind Rebind.succTVar } + { simp only [Ty.subst_id]; apply hs.rebind Rebind.succTVar } case there_tvar hb0 => apply Subtyp.tvar; grind [Ty.subst_id] /-- Creates a retyping morphism that substitutes a type for the newest type variable. -/ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean index 045a6618..12e2bbf9 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean @@ -32,4 +32,4 @@ theorem HasType.retype {σ : Subst s1 s2} case abs ih => apply HasType.abs; simpa [Ty.subst_succVar_comm_base] using ih ρ.liftVar case tabs ih => apply HasType.tabs; apply ih ρ.liftTVar case app ih1 ih2 => apply HasType.app <;> aesop - case tapp ih => simp [Ty.open_tvar_subst_comm]; apply HasType.tapp; aesop + case tapp ih => simp only [Ty.open_tvar_subst_comm]; apply HasType.tapp; aesop diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean index 676a7c61..62796c6f 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean @@ -45,17 +45,17 @@ theorem Ty.tvar_subst_succVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) : case push_var s0 ih => cases X case there_var X0 => - simp [Subst.lift, Ty.subst] - conv => lhs; simp [Subst.liftVar] - conv => rhs; simp [Subst.tvar_there_var_liftVar] - simp [Rename.lift, <-Ty.rename_succVar_comm] + simp only [Subst.lift, Ty.subst] + conv => lhs; simp only [Subst.liftVar] + conv => rhs; simp only [Subst.tvar_there_var_liftVar] + simp only [Rename.lift, <-Ty.rename_succVar_comm] congr; exact (ih (X:=X0)) case push_tvar s0 ih => cases X <;> try rfl case there_tvar X0 => - conv => lhs; simp [Subst.lift, Ty.subst] - conv => lhs; simp [Subst.liftTVar, Rename.lift] - simp [<-Ty.rename_succTVar_comm] + conv => lhs; simp only [Subst.lift, Ty.subst] + conv => lhs; simp only [Subst.liftTVar, Rename.lift] + simp only [<-Ty.rename_succTVar_comm] congr; exact (ih (X:=X0)) /-- Proves that substitution commutes with type variable weakening for type variables. -/ @@ -67,16 +67,16 @@ theorem Ty.tvar_subst_succTVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) : case push_var s0 ih => cases X case there_var X0 => - conv => lhs; simp [Subst.lift, Ty.subst] - conv => lhs; simp [Subst.liftVar, Rename.lift] - simp [<-Ty.rename_succVar_comm] + conv => lhs; simp only [Subst.lift, Ty.subst] + conv => lhs; simp only [Subst.liftVar, Rename.lift] + simp only [<-Ty.rename_succVar_comm] congr; exact (ih (X:=X0)) case push_tvar s0 ih => cases X <;> try rfl case there_tvar X0 => - conv => lhs; simp [Subst.lift, Ty.subst] - conv => lhs; simp [Subst.liftTVar, Rename.lift] - simp [<-Ty.rename_succTVar_comm] + conv => lhs; simp only [Subst.lift, Ty.subst] + conv => lhs; simp only [Subst.liftTVar, Rename.lift] + simp only [<-Ty.rename_succTVar_comm] congr; exact (ih (X:=X0)) /-- Proves that substitution commutes with term variable weakening for types. -/ @@ -141,16 +141,16 @@ theorem Exp.var_subst_succTVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) : case push_var s0 ih => cases x <;> try rfl case there_var x0 => - conv => lhs; simp [Subst.lift, Exp.subst] - conv => lhs; simp [Subst.liftVar, Rename.lift] - simp [<-Exp.rename_succVar_comm] + conv => lhs; simp only [Subst.lift, Exp.subst] + conv => lhs; simp only [Subst.liftVar, Rename.lift] + simp only [<-Exp.rename_succVar_comm] congr; exact (ih (x:=x0)) case push_tvar s0 ih => cases x case there_tvar x0 => - conv => lhs; simp [Subst.liftVar, Subst.lift, Rename.lift] - conv => lhs; simp [Exp.subst, Subst.liftTVar] - simp [<-Exp.rename_succTVar_comm] + conv => lhs; simp only [Subst.liftVar, Subst.lift, Rename.lift] + conv => lhs; simp only [Exp.subst, Subst.liftTVar] + simp only [<-Exp.rename_succTVar_comm] congr; exact (ih (x:=x0)) /-- Proves that substitution commutes with term variable weakening for variables. -/ @@ -161,14 +161,14 @@ theorem Exp.var_subst_succVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) : case push_var s0 ih => cases x <;> try rfl case there_var x0 => - conv => lhs; simp [Subst.lift, Exp.subst, Subst.liftVar, Rename.lift] - simp [<-Exp.rename_succVar_comm] + conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftVar, Rename.lift] + simp only [<-Exp.rename_succVar_comm] congr; exact (ih (x:=x0)) case push_tvar s0 ih => cases x case there_tvar x0 => - conv => lhs; simp [Subst.lift, Exp.subst, Subst.liftTVar, Rename.lift] - simp [<-Exp.rename_succTVar_comm] + conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftTVar, Rename.lift] + simp only [<-Exp.rename_succTVar_comm] congr; exact (ih (x:=x0)) /-- Proves that substitution commutes with type variable weakening for expressions. -/ @@ -180,11 +180,11 @@ theorem Exp.subst_succTVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) : | .abs A t => have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ) have ih2 := Exp.subst_succTVar_comm (s0:=s0,x) (e:=t) (σ:=σ) - simp [Exp.subst, Exp.rename, ih1]; congr + simp only [Exp.subst, Exp.rename, ih1]; congr | .tabs A t => have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ) have ih2 := Exp.subst_succTVar_comm (s0:=s0,X) (e:=t) (σ:=σ) - simp [Exp.subst, Exp.rename, ih1]; congr + simp only [Exp.subst, Exp.rename, ih1]; congr | .app t1 t2 => have ih1 := Exp.subst_succTVar_comm (e:=t1) (σ:=σ) have ih2 := Exp.subst_succTVar_comm (e:=t2) (σ:=σ) @@ -203,11 +203,11 @@ theorem Exp.subst_succVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) : | .abs A t => have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ) have ih2 := Exp.subst_succVar_comm (s0:=s0,x) (e:=t) (σ:=σ) - simp [Exp.subst, Exp.rename, ih1]; congr + simp only [Exp.subst, Exp.rename, ih1]; congr | .tabs A t => have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ) have ih2 := Exp.subst_succVar_comm (s0:=s0,X) (e:=t) (σ:=σ) - simp [Exp.subst, Exp.rename, ih1]; congr + simp only [Exp.subst, Exp.rename, ih1]; congr | .app t1 t2 => have ih1 := Exp.subst_succVar_comm (e:=t1) (σ:=σ) have ih2 := Exp.subst_succVar_comm (e:=t2) (σ:=σ) @@ -257,7 +257,7 @@ theorem Subst.liftVar_comp {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : theorem Ty.subst_comp {T : Ty s1} (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : (T.subst σ1).subst σ2 = T.subst (σ1.comp σ2) := by induction T generalizing s2 s3 <;> try (solve | rfl) - all_goals simp [Ty.subst, Subst.liftTVar_comp]; grind + all_goals simp only [Ty.subst, Subst.liftTVar_comp]; grind /-- **Fundamental associativity law for substitution composition on expressions**: Sequential application of substitutions equals composition. @@ -309,14 +309,14 @@ theorem Subst.id_liftTVar : categorical structure with identity morphisms. -/ theorem Ty.subst_id {T : Ty s} : T.subst Subst.id = T := by induction T <;> try (solve | rfl) - all_goals (simp [Ty.subst, Subst.id_liftTVar]; grind) + all_goals (simp only [Ty.subst, Subst.id_liftTVar]; grind) /-- **Identity law for expressions**: The identity substitution acts as neutral element. This extends the identity property to expressions, completing the algebraic structure of the substitution category. -/ theorem Exp.subst_id {e : Exp s} : e.subst Subst.id = e := by induction e <;> try (solve | rfl) - all_goals (simp [Exp.subst, Ty.subst_id, Subst.id_liftVar, Subst.id_liftTVar]; grind) + all_goals (simp only [Exp.subst, Ty.subst_id, Subst.id_liftVar, Subst.id_liftTVar]; grind) /-- Proves that opening a type variable commutes with renaming for substitutions. -/ theorem Subst.open_tvar_rename_comm {T : Ty s} {f : Rename s s'} : @@ -324,7 +324,8 @@ theorem Subst.open_tvar_rename_comm {T : Ty s} {f : Rename s s'} : = f.liftTVar.asSubst.comp (Subst.open_tvar (T.rename f)) := by apply Subst.funext case var => intro x; cases x; rfl - case tvar => intro X; cases X <;> try (solve | rfl | simp [Subst.comp, Ty.subst_asSubst]; rfl) + case tvar => + intro X; cases X <;> try (solve | rfl | simp only [Subst.comp, Ty.subst_asSubst]; rfl) /-- Proves that opening a type variable commutes with renaming for types. -/ theorem Ty.open_tvar_rename_comm {T : Ty (s,X)} {U : Ty s} {f : Rename s s'} : @@ -374,15 +375,15 @@ theorem Subst.open_tvar_subst_comm {T : Ty s} {σ : Subst s s'} : apply Subst.funext case var => intro x; cases x - conv => lhs; simp [Subst.comp, Subst.open_tvar] - conv => rhs; simp [Subst.comp, Subst.liftTVar] - simp [Exp.rename_succTVar_open_tvar]; rfl + conv => lhs; simp only [Subst.comp, Subst.open_tvar] + conv => rhs; simp only [Subst.comp, Subst.liftTVar] + simp only [Exp.rename_succTVar_open_tvar]; rfl case tvar => intro X; cases X <;> try rfl case there_tvar X0 => - conv => lhs; simp [Subst.comp, Subst.open_tvar] - conv => rhs; simp [Subst.comp, Subst.liftTVar] - simp [Ty.rename_succTVar_open_tvar]; rfl + conv => lhs; simp only [Subst.comp, Subst.open_tvar] + conv => rhs; simp only [Subst.comp, Subst.liftTVar] + simp only [Ty.rename_succTVar_open_tvar]; rfl /-- Proves that opening a type variable commutes with substitution for types. -/ theorem Ty.open_tvar_subst_comm {T : Ty (s,X)} {U : Ty s} {σ : Subst s s'} : diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean index f6d71320..c18524c3 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean @@ -74,17 +74,18 @@ def Exp.rename : Exp s1 -> Rename s1 s2 -> Exp s2 /-- Renaming with the identity renaming leaves a type unchanged. -/ theorem Ty.rename_id {T : Ty s} : T.rename Rename.id = T := by - induction T <;> try (solve | rfl | simp [Ty.rename]; grind) + induction T <;> try (solve | rfl | simp only [Ty.rename, Rename.id_liftTVar_eq_id]; grind) /-- Renaming with the identity renaming leaves an expression unchanged. -/ theorem Exp.rename_id {e : Exp s} : e.rename Rename.id = e := by - induction e <;> try (solve | rfl | simp [Exp.rename, Ty.rename_id]; grind) + induction e <;> try (solve | rfl | + simp only [Exp.rename, Ty.rename_id, Rename.id_liftVar_eq_id, Rename.id_liftTVar_eq_id]; grind) /-- Composition of renamings: renaming by f₁ then f₂ equals renaming by their composition. -/ theorem Ty.rename_comp {T : Ty s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} : (T.rename f1).rename f2 = T.rename (f1.comp f2) := by induction T generalizing s2 s3 <;> - try (solve | rfl | simp [Ty.rename, Rename.comp_liftTVar]; grind) + try (solve | rfl | simp only [Ty.rename, Rename.comp_liftTVar]; grind) /-- Composition of renamings: renaming by f₁ then f₂ equals renaming by their composition. -/ theorem Exp.rename_comp {e : Exp s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} : @@ -92,7 +93,7 @@ theorem Exp.rename_comp {e : Exp s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} : induction e generalizing s2 s3 <;> try (solve | rfl) all_goals - simp [Exp.rename, Ty.rename_comp, Rename.comp_liftVar, Rename.comp_liftTVar]; grind + simp only [Exp.rename, Ty.rename_comp, Rename.comp_liftVar, Rename.comp_liftTVar]; grind /-- Commutativity law for term variable weakening and general renamings. -/ theorem Ty.rename_succVar_comm {T : Ty s} : diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean index d3823965..1baa2450 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean @@ -44,7 +44,7 @@ theorem preservation have ⟨U0, h1, h2, h3⟩ := HasType.abs_inv ht1 have ht2' := HasType.sub h2 ht2 have h1' := h1.retype (Retype.open_var ht2') - simp [Ty.rename_succVar_open_var] at h1' + simp only [Ty.rename_succVar_open_var] at h1' apply HasType.sub _ h1' apply Subtyp.trans h3 hs0 case red_tapp_fun ih => From e7fa44f6015f40d601b6d2ee3d0a457832df393d Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 14 Sep 2025 00:18:11 +0200 Subject: [PATCH 05/13] replace all `<-` with unicode `\lto` --- .../WellScoped/FSub/RebindTheory/Core.lean | 12 ++++----- .../WellScoped/FSub/RetypeTheory/Core.lean | 10 +++---- .../FSub/Substitution/Properties.lean | 26 +++++++++---------- 3 files changed, 24 insertions(+), 24 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean index 282b1c93..84a22d61 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean @@ -43,15 +43,15 @@ structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.rename f) where var := fun x P hb => by cases hb - case here => simp only [<-Ty.rename_succVar_comm]; constructor + case here => simp only [←Ty.rename_succVar_comm]; constructor case there_var hb => - simp only [<-Ty.rename_succVar_comm] + simp only [←Ty.rename_succVar_comm] constructor apply ρ.var _ _ hb tvar := fun X S hb => by cases hb case there_var hb => - simp only [<-Ty.rename_succVar_comm] + simp only [←Ty.rename_succVar_comm] constructor apply ρ.tvar _ _ hb @@ -62,14 +62,14 @@ def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.r def Rebind.liftTVar (ρ : Rebind Γ f Δ) : Rebind (Γ,X<:T) (f.liftTVar) (Δ,X<:T.rename f) where tvar := fun X S hb => by cases hb - case here => simp only [<-Ty.rename_succTVar_comm]; constructor + case here => simp only [←Ty.rename_succTVar_comm]; constructor case there_tvar hb => - simp only [<-Ty.rename_succTVar_comm] + simp only [←Ty.rename_succTVar_comm] constructor apply ρ.tvar _ _ hb var := fun x P hb => by cases hb - case there_tvar hb => simp only [<-Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb + case there_tvar hb => simp only [←Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb /-- **Term variable weakening morphism**. diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean index 58effe36..348e2762 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean @@ -40,17 +40,17 @@ def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P cases hb case here => apply HasType.var - simp only [<-Ty.subst_succVar_comm_base] + simp only [←Ty.subst_succVar_comm_base] constructor case there_var hb0 => have h0 := ρ.var _ _ hb0 - simp only [<-Ty.subst_succVar_comm_base] + simp only [←Ty.subst_succVar_comm_base] apply h0.rebind Rebind.succVar tvar := fun X S hb => by cases hb case there_var hb0 => have h0 := ρ.tvar _ _ hb0 - simp only [<-Ty.subst_succVar_comm_base] + simp only [←Ty.subst_succVar_comm_base] apply h0.rebind Rebind.succVar /-- Extends a retyping morphism to contexts with an additional type variable. -/ @@ -59,7 +59,7 @@ def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ, cases hb case there_tvar hb0 => have h0 := ρ.var _ _ hb0 - simp only [<-Ty.subst_succTVar_comm_base] + simp only [←Ty.subst_succTVar_comm_base] apply h0.rebind Rebind.succTVar tvar := fun X S hb => by cases hb @@ -68,7 +68,7 @@ def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ, grind [Ty.subst_succTVar_comm_base] case there_tvar hb0 => have h0 := ρ.tvar _ _ hb0 - simp only [<-Ty.subst_succTVar_comm_base] + simp only [←Ty.subst_succTVar_comm_base] apply h0.rebind Rebind.succTVar /-- Creates a retyping morphism that substitutes an expression for the newest term variable. -/ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean index 62796c6f..7dc15cae 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean @@ -48,14 +48,14 @@ theorem Ty.tvar_subst_succVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) : simp only [Subst.lift, Ty.subst] conv => lhs; simp only [Subst.liftVar] conv => rhs; simp only [Subst.tvar_there_var_liftVar] - simp only [Rename.lift, <-Ty.rename_succVar_comm] + simp only [Rename.lift, ←Ty.rename_succVar_comm] congr; exact (ih (X:=X0)) case push_tvar s0 ih => cases X <;> try rfl case there_tvar X0 => conv => lhs; simp only [Subst.lift, Ty.subst] conv => lhs; simp only [Subst.liftTVar, Rename.lift] - simp only [<-Ty.rename_succTVar_comm] + simp only [←Ty.rename_succTVar_comm] congr; exact (ih (X:=X0)) /-- Proves that substitution commutes with type variable weakening for type variables. -/ @@ -69,14 +69,14 @@ theorem Ty.tvar_subst_succTVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) : case there_var X0 => conv => lhs; simp only [Subst.lift, Ty.subst] conv => lhs; simp only [Subst.liftVar, Rename.lift] - simp only [<-Ty.rename_succVar_comm] + simp only [←Ty.rename_succVar_comm] congr; exact (ih (X:=X0)) case push_tvar s0 ih => cases X <;> try rfl case there_tvar X0 => conv => lhs; simp only [Subst.lift, Ty.subst] conv => lhs; simp only [Subst.liftTVar, Rename.lift] - simp only [<-Ty.rename_succTVar_comm] + simp only [←Ty.rename_succTVar_comm] congr; exact (ih (X:=X0)) /-- Proves that substitution commutes with term variable weakening for types. -/ @@ -143,14 +143,14 @@ theorem Exp.var_subst_succTVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) : case there_var x0 => conv => lhs; simp only [Subst.lift, Exp.subst] conv => lhs; simp only [Subst.liftVar, Rename.lift] - simp only [<-Exp.rename_succVar_comm] + simp only [←Exp.rename_succVar_comm] congr; exact (ih (x:=x0)) case push_tvar s0 ih => cases x case there_tvar x0 => conv => lhs; simp only [Subst.liftVar, Subst.lift, Rename.lift] conv => lhs; simp only [Exp.subst, Subst.liftTVar] - simp only [<-Exp.rename_succTVar_comm] + simp only [←Exp.rename_succTVar_comm] congr; exact (ih (x:=x0)) /-- Proves that substitution commutes with term variable weakening for variables. -/ @@ -162,13 +162,13 @@ theorem Exp.var_subst_succVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) : cases x <;> try rfl case there_var x0 => conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftVar, Rename.lift] - simp only [<-Exp.rename_succVar_comm] + simp only [←Exp.rename_succVar_comm] congr; exact (ih (x:=x0)) case push_tvar s0 ih => cases x case there_tvar x0 => conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftTVar, Rename.lift] - simp only [<-Exp.rename_succTVar_comm] + simp only [←Exp.rename_succTVar_comm] congr; exact (ih (x:=x0)) /-- Proves that substitution commutes with type variable weakening for expressions. -/ @@ -330,7 +330,7 @@ theorem Subst.open_tvar_rename_comm {T : Ty s} {f : Rename s s'} : /-- Proves that opening a type variable commutes with renaming for types. -/ theorem Ty.open_tvar_rename_comm {T : Ty (s,X)} {U : Ty s} {f : Rename s s'} : (T.open_tvar U).rename f = (T.rename f.liftTVar).open_tvar (U.rename f) := by - simp [Ty.open_tvar, <-Ty.subst_asSubst] + simp [Ty.open_tvar, ←Ty.subst_asSubst] grind [Ty.subst_comp, Subst.open_tvar_rename_comm, Ty.subst_asSubst] /-- Shows that successively weakening then opening a type variable gives the identity. -/ @@ -341,14 +341,14 @@ theorem Subst.succTVar_open_tvar {T : Ty s} : theorem Exp.rename_succTVar_open_tvar {e : Exp s} : (e.rename Rename.succTVar).subst (Subst.open_tvar X) = e := by - simp [<-Exp.subst_asSubst] + simp [←Exp.subst_asSubst] grind [Exp.subst_comp, Subst.succTVar_open_tvar, Exp.subst_id] /-- Proves that renaming with succTVar then opening cancels out for types. -/ theorem Ty.rename_succTVar_open_tvar {T : Ty s} : (T.rename Rename.succTVar).subst (Subst.open_tvar X) = T := by - simp [<-Ty.subst_asSubst] + simp [←Ty.subst_asSubst] grind [Ty.subst_comp, Subst.succTVar_open_tvar, Ty.subst_id] /-- Shows that successively weakening then opening a term variable gives the identity. -/ @@ -359,14 +359,14 @@ theorem Subst.succVar_open_var {e : Exp s} : theorem Exp.rename_succVar_open_var {e : Exp s} : (e.rename Rename.succVar).subst (Subst.open_var X) = e := by - simp [<-Exp.subst_asSubst] + simp [←Exp.subst_asSubst] grind [Exp.subst_comp, Subst.succVar_open_var, Exp.subst_id] /-- Proves that renaming with succVar then opening cancels out for types. -/ theorem Ty.rename_succVar_open_var {T : Ty s} : (T.rename Rename.succVar).subst (Subst.open_var X) = T := by - simp [<-Ty.subst_asSubst] + simp [←Ty.subst_asSubst] grind [Ty.subst_comp, Subst.succVar_open_var, Ty.subst_id] /-- Proves that opening a type variable commutes with substitution for substitutions. -/ From 103bd2d05eedc85d44a089d0de88b8ba47b92803 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 14 Sep 2025 00:24:35 +0200 Subject: [PATCH 06/13] use `where` for structures --- .../WellScoped/FSub/Debruijn.lean | 44 +++++++------- .../WellScoped/FSub/Substitution/Core.lean | 60 +++++++++---------- .../FSub/Substitution/Properties.lean | 6 +- 3 files changed, 57 insertions(+), 53 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean index ee57fdd2..7d6a9399 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean @@ -76,40 +76,44 @@ structure Rename (s1 s2 : Sig) where /-- Lift a renaming to work under a new term variable binder. The new term variable is mapped to itself, while existing variables are renamed and shifted. -/ -def Rename.liftVar (f : Rename s1 s2) : Rename (s1,x) (s2,x) := - { var := fun x => match x with - | .here => .here - | .there_var x0 => .there_var (f.var x0) - tvar := fun X => match X with - | .there_var X0 => .there_var (f.tvar X0) } +def Rename.liftVar (f : Rename s1 s2) : Rename (s1,x) (s2,x) where + var := fun x => match x with + | .here => .here + | .there_var x0 => .there_var (f.var x0) + tvar := fun X => match X with + | .there_var X0 => .there_var (f.tvar X0) /-- Lift a renaming to work under a new type variable binder. The new type variable is mapped to itself, while existing variables are renamed and shifted. -/ -def Rename.liftTVar (f : Rename s1 s2) : Rename (s1,X) (s2,X) := - { tvar := fun X => match X with - | .here => .here - | .there_tvar X0 => .there_tvar (f.tvar X0) - var := fun x => match x with - | .there_tvar x0 => .there_tvar (f.var x0) } +def Rename.liftTVar (f : Rename s1 s2) : Rename (s1,X) (s2,X) where + tvar := fun X => match X with + | .here => .here + | .there_tvar X0 => .there_tvar (f.tvar X0) + var := fun x => match x with + | .there_tvar x0 => .there_tvar (f.var x0) /-- Weakening renaming that adds a new term variable to the context. All existing variables are shifted to account for the new binding. -/ -def Rename.succVar : Rename s1 (s1,x) := - { var := fun x => x.there_var, tvar := fun X => X.there_var } +def Rename.succVar : Rename s1 (s1,x) where + var := fun x => x.there_var + tvar := fun X => X.there_var /-- Weakening renaming that adds a new type variable to the context. All existing variables are shifted to account for the new binding. -/ -def Rename.succTVar : Rename s1 (s1,X) := - { var := fun x => x.there_tvar, tvar := fun X => X.there_tvar } +def Rename.succTVar : Rename s1 (s1,X) where + var := fun x => x.there_tvar + tvar := fun X => X.there_tvar /-- The identity renaming that maps each variable to itself. -/ -def Rename.id : Rename s s := - { var := fun x => x, tvar := fun X => X } +def Rename.id : Rename s s where + var := fun x => x + tvar := fun X => X /-- Composition of renamings. If `f1` renames from `s1` to `s2` and `f2` renames from `s2` to `s3`, then their composition renames from `s1` to `s3`. -/ -def Rename.comp (f1 : Rename s1 s2) (f2 : Rename s2 s3) : Rename s1 s3 := - { var := fun x => f2.var (f1.var x), tvar := fun X => f2.tvar (f1.tvar X) } +def Rename.comp (f1 : Rename s1 s2) (f2 : Rename s2 s3) : Rename s1 s3 where + var := fun x => f2.var (f1.var x) + tvar := fun X => f2.tvar (f1.tvar X) /-- Two renamings are equal if they map variables in the same way. -/ theorem Rename.funext {f g : Rename s1 s2} diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean index 85a9478d..ae0c834c 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean @@ -40,48 +40,48 @@ structure Subst (s1 s2 : Sig) where /-- Lift a substitution to work under a term variable binder. The newly bound variable is mapped to itself, while existing variables are substituted and then weakened to account for the new binding. -/ -def Subst.liftVar (s : Subst s1 s2) : Subst (s1,x) (s2,x) := - { var := fun x => match x with - | .here => .var .here - | .there_var x0 => (s.var x0).rename Rename.succVar - tvar := fun X => match X with - | .there_var X0 => (s.tvar X0).rename Rename.succVar } +def Subst.liftVar (s : Subst s1 s2) : Subst (s1,x) (s2,x) where + var := fun x => match x with + | .here => .var .here + | .there_var x0 => (s.var x0).rename Rename.succVar + tvar := fun X => match X with + | .there_var X0 => (s.tvar X0).rename Rename.succVar /-- Lift a substitution to work under a type variable binder. The newly bound type variable is mapped to itself, while existing variables are substituted and then weakened to account for the new binding. -/ -def Subst.liftTVar (s : Subst s1 s2) : Subst (s1,X) (s2,X) := - { tvar := fun X => match X with - | .here => .tvar .here - | .there_tvar X0 => (s.tvar X0).rename Rename.succTVar - var := fun x => match x with - | .there_tvar x0 => (s.var x0).rename Rename.succTVar } +def Subst.liftTVar (s : Subst s1 s2) : Subst (s1,X) (s2,X) where + tvar := fun X => match X with + | .here => .tvar .here + | .there_tvar X0 => (s.tvar X0).rename Rename.succTVar + var := fun x => match x with + | .there_tvar x0 => (s.var x0).rename Rename.succTVar /-- Create a substitution that replaces the outermost term variable with the given expression, while leaving all other variables unchanged. This is used for function application (beta reduction). -/ -def Subst.open_var (e : Exp s) : Subst (s,x) s := - { var := fun x => match x with - | .here => e - | .there_var x0 => .var x0 - tvar := fun X => match X with - | .there_var X0 => .tvar X0 } +def Subst.open_var (e : Exp s) : Subst (s,x) s where + var := fun x => match x with + | .here => e + | .there_var x0 => .var x0 + tvar := fun X => match X with + | .there_var X0 => .tvar X0 /-- Create a substitution that replaces the outermost type variable with the given type, while leaving all other variables unchanged. This is used for type application in polymorphic functions. -/ -def Subst.open_tvar (T : Ty s) : Subst (s,X) s := - { var := fun x => match x with - | .there_tvar x0 => .var x0 - tvar := fun X => match X with - | .here => T - | .there_tvar X0 => .tvar X0 } +def Subst.open_tvar (T : Ty s) : Subst (s,X) s where + var := fun x => match x with + | .there_tvar x0 => .var x0 + tvar := fun X => match X with + | .here => T + | .there_tvar X0 => .tvar X0 /-- Convert a renaming into a substitution. Every variable is mapped to the correspondingly renamed variable. -/ -def Rename.asSubst (f : Rename s1 s2) : Subst s1 s2 := - { var := fun x => .var (f.var x) - tvar := fun X => .tvar (f.tvar X) } +def Rename.asSubst (f : Rename s1 s2) : Subst s1 s2 where + var := fun x => .var (f.var x) + tvar := fun X => .tvar (f.tvar X) /-- Functional extensionality for substitutions: two substitutions are equal if they map all variables in the same way. -/ @@ -102,6 +102,6 @@ def Subst.lift : Subst s1 s2 -> (s : Sig) -> Subst (s1 ++ s) (s2 ++ s) | σ, .push_tvar s => (σ.lift s).liftTVar /-- The identity substitution that maps each variable to itself. -/ -def Subst.id : Subst s s := - { var := fun x => .var x - tvar := fun X => .tvar X } +def Subst.id : Subst s s where + var := fun x => .var x + tvar := fun X => .tvar X diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean index 7dc15cae..de3ee8c1 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean @@ -16,9 +16,9 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Subst /-- Composition of substitutions. If σ₁ maps s₁ to s₂ and σ₂ maps s₂ to s₃, then their composition maps s₁ to s₃ by first applying σ₁ then σ₂. -/ -def Subst.comp (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : Subst s1 s3 := - { var := fun x => (σ1.var x).subst σ2 - tvar := fun X => (σ1.tvar X).subst σ2 } +def Subst.comp (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : Subst s1 s3 where + var := fun x => (σ1.var x).subst σ2 + tvar := fun X => (σ1.tvar X).subst σ2 /-- Shows that lifting a substitution for term variables preserves type variable mappings by renaming with succVar. -/ From 3158681ae4879b217c0682d385d9c2558086a503 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 14 Sep 2025 00:30:28 +0200 Subject: [PATCH 07/13] Use `\to`, not `->` --- .../WellScoped/FSub/Debruijn.lean | 24 ++++++------ .../LambdaCalculus/WellScoped/FSub/Eval.lean | 4 +- .../WellScoped/FSub/RebindTheory/Core.lean | 4 +- .../WellScoped/FSub/Reduce.lean | 10 ++--- .../WellScoped/FSub/RetypeTheory/Core.lean | 4 +- .../WellScoped/FSub/Substitution/Core.lean | 6 +-- .../WellScoped/FSub/Syntax/Context.lean | 18 ++++----- .../WellScoped/FSub/Syntax/Core.lean | 30 +++++++-------- .../WellScoped/FSub/Syntax/Subst.lean | 4 +- .../FSub/TypeSoundness/Canonical.lean | 2 +- .../WellScoped/FSub/TypeSystem.lean | 38 +++++++++---------- 11 files changed, 72 insertions(+), 72 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean index 7d6a9399..a2f1d960 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean @@ -30,9 +30,9 @@ import Mathlib.Tactic inductive Sig : Type where | empty : Sig /-- Extend signature with a term variable -/ -| push_var : Sig -> Sig +| push_var : Sig → Sig /-- Extend signature with a type variable -/ -| push_tvar : Sig -> Sig +| push_tvar : Sig → Sig @[simp] instance : EmptyCollection Sig := ⟨Sig.empty⟩ @@ -47,32 +47,32 @@ postfix:50 ",X" => Sig.push_tvar /-- Term variables indexed by signatures. A `Var s` represents a term variable that is valid in signature `s`. The constructors correspond to different ways a variable can be accessed from the current context. -/ -inductive Var : Sig -> Type where +inductive Var : Sig → Type where /-- The most recently bound term variable -/ | here : Var (s,x) /-- Skip over the most recent term variable -/ -| there_var : Var s -> Var (s,x) +| there_var : Var s → Var (s,x) /-- Skip over the most recent type variable -/ -| there_tvar : Var s -> Var (s,X) +| there_tvar : Var s → Var (s,X) /-- Type variables indexed by signatures. A `TVar s` represents a type variable that is valid in signature `s`. -/ -inductive TVar : Sig -> Type where +inductive TVar : Sig → Type where /-- The most recently bound type variable -/ | here : TVar (s,X) /-- Skip over the most recent term variable -/ -| there_var : TVar s -> TVar (s,x) +| there_var : TVar s → TVar (s,x) /-- Skip over the most recent type variable -/ -| there_tvar : TVar s -> TVar (s,X) +| there_tvar : TVar s → TVar (s,X) /-- A renaming between signatures `s1` and `s2` specifies how to map variables from `s1` to variables in `s2`. This is the foundation for all variable renamings in the mechanization. -/ structure Rename (s1 s2 : Sig) where /-- How to rename term variables -/ - var : Var s1 -> Var s2 + var : Var s1 → Var s2 /-- How to rename type variables -/ - tvar : TVar s1 -> TVar s2 + tvar : TVar s1 → TVar s2 /-- Lift a renaming to work under a new term variable binder. The new term variable is mapped to itself, while existing variables are renamed and shifted. -/ @@ -165,7 +165,7 @@ theorem Rename.rename_succTVar_comm {f : Rename s1 s2} : case tvar => intro X; rfl /-- Append two signatures, concatenating their binder sequences. -/ -def Sig.append : Sig -> Sig -> Sig +def Sig.append : Sig → Sig → Sig | s1, .empty => s1 | s1, .push_var s2 => .push_var (s1.append s2) | s1, .push_tvar s2 => .push_tvar (s1.append s2) @@ -175,7 +175,7 @@ instance : Append Sig := ⟨Sig.append⟩ /-- Lift a renaming to work under multiple binders specified by a signature. This is the generalization of `liftVar` and `liftTVar` to arbitrary sequences of binders. -/ -def Rename.lift : Rename s1 s2 -> (s : Sig) -> Rename (s1 ++ s) (s2 ++ s) +def Rename.lift : Rename s1 s2 → (s : Sig) → Rename (s1 ++ s) (s2 ++ s) | f, .empty => f | f, .push_var s => (f.lift s).liftVar | f, .push_tvar s => (f.lift s).liftTVar diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean index 8f018c15..264b8742 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Eval.lean @@ -14,14 +14,14 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax fail with an error, or exhaust its fuel allocation. -/ inductive Result (s : Sig) where /-- Successful evaluation to a value -/ -| ok : Exp s -> Result s +| ok : Exp s → Result s /-- Runtime error (e.g., free variable, type mismatch) -/ | err : Result s /-- Evaluation did not terminate within fuel limit -/ | nonterm : Result s /-- Big-step evaluator with fuel-based termination. -/ -def eval : Nat -> Exp s -> Result s +def eval : Nat → Exp s → Result s | 0, _ => .nonterm | _, .var _ => .err | _, .abs A e => .ok (.abs A e) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean index 84a22d61..055d2eed 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean @@ -32,9 +32,9 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax must preserve the variable and type bindings in the context. -/ structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where /-- Term variable preservation: x:T in Γ implies f(x):f(T) in Δ -/ - var : ∀ x T, Ctx.LookupVar Γ x T -> Ctx.LookupVar Δ (f.var x) (T.rename f) + var : ∀ x T, Ctx.LookupVar Γ x T → Ctx.LookupVar Δ (f.var x) (T.rename f) /-- Type variable preservation: X<:T in Γ implies f(X)<:f(T) in Δ -/ - tvar : ∀ X T, Ctx.LookupTVar Γ X T -> Ctx.LookupTVar Δ (f.tvar X) (T.rename f) + tvar : ∀ X T, Ctx.LookupTVar Γ X T → Ctx.LookupTVar Δ (f.tvar X) (T.rename f) /-- **Lifting rebinding morphisms over term variable binders**. diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean index af2f147b..e3ce35b1 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Reduce.lean @@ -14,22 +14,22 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax /-- The small-step reduction relation for System F<:. `Reduce e₁ e₂` means that expression `e₁` can take a single computational step to become `e₂`. -/ -inductive Reduce : Exp s -> Exp s -> Prop where +inductive Reduce : Exp s → Exp s → Prop where /-- Evaluate function position: if e₁ ⟶ e₁', then (e₁ e₂) ⟶ (e₁' e₂) -/ | red_app_fun : - Reduce e1 e1' -> + Reduce e1 e1' → Reduce (.app e1 e2) (.app e1' e2) /-- Evaluate argument position: if v₁ is a value and e₂ ⟶ e₂', then (v₁ e₂) ⟶ (v₁ e₂') -/ | red_app_arg : - Exp.IsVal v1 -> - Reduce e2 e2' -> + Exp.IsVal v1 → + Reduce e2 e2' → Reduce (.app v1 e2) (.app v1 e2') /-- Beta reduction: (λx:T.e₁) e₂ ⟶ e₁[x := e₂] -/ | red_app : Reduce (.app (.abs T e1) e2) (e1.open_var e2) /-- Evaluate polymorphic expression: if e ⟶ e', then (e [T]) ⟶ (e' [T]) -/ | red_tapp_fun : - Reduce e e' -> + Reduce e e' → Reduce (.tapp e T) (.tapp e' T) /-- Type application: (ΛX<:T'.e) [T] ⟶ e[X := T] -/ | red_tapp : diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean index 348e2762..799e95a0 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean @@ -31,8 +31,8 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.TypeSyste Unlike rebinding morphisms, retyping morphisms map variables to typing derivations. -/ structure Retype (Γ : Ctx s1) (σ : Subst s1 s2) (Δ : Ctx s2) where - var : ∀ x T, Γ.LookupVar x T -> HasType Δ (σ.var x) (T.subst σ) - tvar : ∀ X S, Γ.LookupTVar X S -> Subtyp Δ (σ.tvar X) (S.subst σ) + var : ∀ x T, Γ.LookupVar x T → HasType Δ (σ.var x) (T.subst σ) + tvar : ∀ X S, Γ.LookupTVar X S → Subtyp Δ (σ.tvar X) (S.subst σ) /-- Extends a retyping morphism to contexts with an additional term variable. -/ def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P.subst σ) where diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean index ae0c834c..4822e9c8 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean @@ -33,9 +33,9 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core preserving well-scopedness. -/ structure Subst (s1 s2 : Sig) where /-- How to substitute term variables -/ - var : Var s1 -> Exp s2 + var : Var s1 → Exp s2 /-- How to substitute type variables -/ - tvar : TVar s1 -> Ty s2 + tvar : TVar s1 → Ty s2 /-- Lift a substitution to work under a term variable binder. The newly bound variable is mapped to itself, while existing variables are substituted and @@ -96,7 +96,7 @@ theorem Subst.funext {σ1 σ2 : Subst s1 s2} /-- Lift a substitution to work under multiple binders specified by a signature. This generalizes `liftVar` and `liftTVar` to arbitrary sequences of binders. -/ -def Subst.lift : Subst s1 s2 -> (s : Sig) -> Subst (s1 ++ s) (s2 ++ s) +def Subst.lift : Subst s1 s2 → (s : Sig) → Subst (s1 ++ s) (s2 ++ s) | σ, .empty => σ | σ, .push_var s => (σ.lift s).liftVar | σ, .push_tvar s => (σ.lift s).liftTVar diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean index fbf4dbad..577a7717 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Context.lean @@ -13,13 +13,13 @@ This module defines typing contexts and variable lookup relations for System F<: import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax.Core /-- A typing context assigns types to term variables and upper bounds to type variables. -/ -inductive Ctx : Sig -> Type where +inductive Ctx : Sig → Type where /-- Empty context -/ | empty : Ctx {} /-- Extend with term variable x : T -/ -| cons_var : Ctx s -> Ty s -> Ctx (s,x) +| cons_var : Ctx s → Ty s → Ctx (s,x) /-- Extend with type variable X <: T -/ -| cons_tvar : Ctx s -> Ty s -> Ctx (s,X) +| cons_tvar : Ctx s → Ty s → Ctx (s,X) /-- Convenient notation for extending context with a term variable -/ infixl:50 ",x:" => Ctx.cons_var @@ -29,33 +29,33 @@ infixl:50 ",X<:" => Ctx.cons_tvar /-- Variable lookup relation. `Ctx.LookupVar Γ x T` means that term variable `x` has type `T` in context `Γ`. -/ @[grind] -inductive Ctx.LookupVar : Ctx s -> Var s -> Ty s -> Prop where +inductive Ctx.LookupVar : Ctx s → Var s → Ty s → Prop where /-- Look up the most recently bound term variable -/ | here : Ctx.LookupVar (Γ,x:T) .here (T.rename Rename.succVar) /-- Skip over a more recent term variable binding -/ | there_var : - Ctx.LookupVar Γ x T -> + Ctx.LookupVar Γ x T → Ctx.LookupVar (Γ,x:U) (x.there_var) (T.rename Rename.succVar) /-- Skip over a more recent type variable binding -/ | there_tvar : - Ctx.LookupVar Γ x T -> + Ctx.LookupVar Γ x T → Ctx.LookupVar (Γ,X<:S) (x.there_tvar) (T.rename Rename.succTVar) /-- Type variable lookup relation. `Ctx.LookupTVar Γ X T` means that type variable `X` has upper bound `T` in context `Γ`. -/ @[grind] -inductive Ctx.LookupTVar : Ctx s -> TVar s -> Ty s -> Prop where +inductive Ctx.LookupTVar : Ctx s → TVar s → Ty s → Prop where /-- Look up the most recently bound type variable -/ | here : Ctx.LookupTVar (Γ,X<:T) .here (T.rename Rename.succTVar) /-- Skip over a more recent term variable binding -/ | there_var : - Ctx.LookupTVar Γ X T -> + Ctx.LookupTVar Γ X T → Ctx.LookupTVar (Γ,x:U) X.there_var (T.rename Rename.succVar) /-- Skip over a more recent type variable binding -/ | there_tvar : - Ctx.LookupTVar Γ X T -> + Ctx.LookupTVar Γ X T → Ctx.LookupTVar (Γ,X<:S) X.there_tvar (T.rename Rename.succTVar) @[simp] diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean index c18524c3..40c7e7cb 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean @@ -26,20 +26,20 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Debruijn /-- Types in System F<:. The type system includes: - `top`: The universal supertype that all types are subtypes of - `tvar`: Type variables, intrinsically scoped by signature - - `arrow`: Function types (A -> B) + - `arrow`: Function types (A → B) - `poly`: Polymorphic types (forall X <: A. B) where B has access to type variable X -/ -inductive Ty : Sig -> Type where +inductive Ty : Sig → Type where /-- The top type, supertype of all types -/ | top : Ty s /-- Type variable -/ -| tvar : TVar s -> Ty s -/-- Function type A -> B -/ -| arrow : Ty s -> Ty s -> Ty s +| tvar : TVar s → Ty s +/-- Function type A → B -/ +| arrow : Ty s → Ty s → Ty s /-- Polymorphic type ∀X<:A.B -/ -| poly : Ty s -> Ty (s,X) -> Ty s +| poly : Ty s → Ty (s,X) → Ty s /-- Rename all type variables in a type according to the given renaming. -/ -def Ty.rename : Ty s1 -> Rename s1 s2 -> Ty s2 +def Ty.rename : Ty s1 → Rename s1 s2 → Ty s2 | .top, _ => .top | .tvar X, ρ => .tvar (ρ.tvar X) | .arrow A B, ρ => .arrow (A.rename ρ) (B.rename ρ) @@ -51,21 +51,21 @@ def Ty.rename : Ty s1 -> Rename s1 s2 -> Ty s2 - `tabs`: Type abstraction (ΛX<:T. e) for polymorphic functions - `app`: Function application (e₁ e₂) - `tapp`: Type application (e T) for instantiating polymorphic functions -/ -inductive Exp : Sig -> Type where +inductive Exp : Sig → Type where /-- Term variable -/ -| var : Var s -> Exp s +| var : Var s → Exp s /-- Function abstraction λx:T.e -/ -| abs : Ty s -> Exp (s,x) -> Exp s +| abs : Ty s → Exp (s,x) → Exp s /-- Type abstraction ΛX<:T.e -/ -| tabs : Ty s -> Exp (s,X) -> Exp s +| tabs : Ty s → Exp (s,X) → Exp s /-- Function application e₁ e₂ -/ -| app : Exp s -> Exp s -> Exp s +| app : Exp s → Exp s → Exp s /-- Type application e[T] -/ -| tapp : Exp s -> Ty s -> Exp s +| tapp : Exp s → Ty s → Exp s /-- Rename all variables (both term and type variables) in an expression according to the given renaming. -/ -def Exp.rename : Exp s1 -> Rename s1 s2 -> Exp s2 +def Exp.rename : Exp s1 → Rename s1 s2 → Exp s2 | .var x, ρ => .var (ρ.var x) | .abs A e, ρ => .abs (A.rename ρ) (e.rename ρ.liftVar) | .tabs A e, ρ => .tabs (A.rename ρ) (e.rename ρ.liftTVar) @@ -110,7 +110,7 @@ theorem Ty.rename_succTVar_comm {T : Ty s} : This predicate is used in the operational semantics to determine when evaluation has reached a final result. -/ @[grind] -inductive Exp.IsVal : Exp s -> Prop where +inductive Exp.IsVal : Exp s → Prop where /-- Function abstractions are values -/ | abs : IsVal (.abs T e) /-- Type abstractions are values -/ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean index 4c677dce..0c4bcfb3 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Subst.lean @@ -13,14 +13,14 @@ This module defines substitution operations for types and expressions in System import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Substitution.Core /-- Apply a parallel substitution to a type. -/ -def Ty.subst : Ty s1 -> Subst s1 s2 -> Ty s2 +def Ty.subst : Ty s1 → Subst s1 s2 → Ty s2 | .top, _ => .top | .tvar X, s => s.tvar X | .arrow A B, s => .arrow (A.subst s) (B.subst s) | .poly A B, s => .poly (A.subst s) (B.subst s.liftTVar) /-- Apply a parallel substitution to an expression. -/ -def Exp.subst : Exp s1 -> Subst s1 s2 -> Exp s2 +def Exp.subst : Exp s1 → Subst s1 s2 → Exp s2 | .var x, s => s.var x | .abs A e, s => .abs (A.subst s) (e.subst s.liftVar) | .tabs A e, s => .tabs (A.subst s) (e.subst s.liftTVar) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean index b8e4086c..0797e39d 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean @@ -12,7 +12,7 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.TypeSystem import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RetypeTheory.TypeSystem /-- Predicate for empty contexts -/ -inductive Ctx.IsEmpty : Ctx s -> Prop where +inductive Ctx.IsEmpty : Ctx s → Prop where | empty_is_empty : Ctx.IsEmpty .empty theorem HasType.app_inv diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean index 84221a75..60a91853 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSystem.lean @@ -35,7 +35,7 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax - `arrow`: Function types are contravariant in domain, covariant in codomain - `poly`: Polymorphic types are covariant in both bound and body -/ @[grind] -inductive Subtyp : Ctx s -> Ty s -> Ty s -> Prop where +inductive Subtyp : Ctx s → Ty s → Ty s → Prop where /-- Every type is a subtype of the top type -/ | top : Subtyp Γ T .top @@ -44,22 +44,22 @@ inductive Subtyp : Ctx s -> Ty s -> Ty s -> Prop where Subtyp Γ T T /-- Subtyping is transitive -/ | trans : - Subtyp Γ A B -> - Subtyp Γ B C -> + Subtyp Γ A B → + Subtyp Γ B C → Subtyp Γ A C /-- Type variables are subtypes of their declared upper bounds -/ | tvar : - Ctx.LookupTVar Γ X T -> + Ctx.LookupTVar Γ X T → Subtyp Γ (.tvar X) T /-- Function subtyping: contravariant in domain, covariant in codomain -/ | arrow : - Subtyp Γ T2 T1 -> - Subtyp Γ U1 U2 -> + Subtyp Γ T2 T1 → + Subtyp Γ U1 U2 → Subtyp Γ (.arrow T1 U1) (.arrow T2 U2) /-- Polymorphic subtyping: covariant in bound and body -/ | poly : - Subtyp Γ T2 T1 -> - Subtyp (Γ,X<:T2) U1 U2 -> + Subtyp Γ T2 T1 → + Subtyp (Γ,X<:T2) U1 U2 → Subtyp Γ (.poly T1 U1) (.poly T2 U2) /-- The typing relation for System F<:. `HasType Γ e T` means that expression `e` @@ -72,30 +72,30 @@ inductive Subtyp : Ctx s -> Ty s -> Ty s -> Prop where - `tabs`: Type abstraction (polymorphic functions) - `app`: Function application - `tapp`: Type application (polymorphic instantiation) -/ -inductive HasType : Ctx s -> Exp s -> Ty s -> Prop where +inductive HasType : Ctx s → Exp s → Ty s → Prop where /-- Term variables have the type assigned in the context -/ | var : - Ctx.LookupVar Γ x T -> + Ctx.LookupVar Γ x T → HasType Γ (.var x) T /-- Subsumption: if e : T₁ and T₁ <: T₂, then e : T₂ -/ | sub : - Subtyp Γ T1 T2 -> - HasType Γ t T1 -> + Subtyp Γ T1 T2 → + HasType Γ t T1 → HasType Γ t T2 -/-- Function abstraction: λx:T.e has type T -> U if e has type U under x:T -/ +/-- Function abstraction: λx:T.e has type T → U if e has type U under x:T -/ | abs : - HasType (Γ,x:T) t (U.rename Rename.succVar) -> + HasType (Γ,x:T) t (U.rename Rename.succVar) → HasType Γ (.abs T t) (.arrow T U) /-- Type abstraction: ΛX<:T.e has type ∀X<:T.U if e has type U under X<:T -/ | tabs : - HasType (Γ,X<:T) t U -> + HasType (Γ,X<:T) t U → HasType Γ (.tabs T t) (.poly T U) -/-- Function application: if e₁ : T -> U and e₂ : T, then e₁ e₂ : U -/ +/-- Function application: if e₁ : T → U and e₂ : T, then e₁ e₂ : U -/ | app : - HasType Γ t1 (.arrow T1 U1) -> - HasType Γ t2 T1 -> + HasType Γ t1 (.arrow T1 U1) → + HasType Γ t2 T1 → HasType Γ (.app t1 t2) U1 /-- Type application: if e : ∀X<:T.U and S <: T, then e[S] : U[X := S] -/ | tapp : - HasType Γ t (.poly T U) -> + HasType Γ t (.poly T U) → HasType Γ (.tapp t T) (U.open_tvar T) From 29bb3065d996a28b99c22f5eaa8b148ee46ecb8f Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 14 Sep 2025 00:32:36 +0200 Subject: [PATCH 08/13] Drop unnecessary `.`s --- .../WellScoped/FSub/Syntax/Core.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean index 40c7e7cb..652c6971 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean @@ -40,10 +40,10 @@ inductive Ty : Sig → Type where /-- Rename all type variables in a type according to the given renaming. -/ def Ty.rename : Ty s1 → Rename s1 s2 → Ty s2 -| .top, _ => .top -| .tvar X, ρ => .tvar (ρ.tvar X) -| .arrow A B, ρ => .arrow (A.rename ρ) (B.rename ρ) -| .poly A B, ρ => .poly (A.rename ρ) (B.rename ρ.liftTVar) +| top, _ => top +| tvar X, ρ => tvar (ρ.tvar X) +| arrow A B, ρ => arrow (A.rename ρ) (B.rename ρ) +| poly A B, ρ => poly (A.rename ρ) (B.rename ρ.liftTVar) /-- Expressions in System F<:. The expression language includes: - `var`: Term variables, intrinsically scoped @@ -66,11 +66,11 @@ inductive Exp : Sig → Type where /-- Rename all variables (both term and type variables) in an expression according to the given renaming. -/ def Exp.rename : Exp s1 → Rename s1 s2 → Exp s2 -| .var x, ρ => .var (ρ.var x) -| .abs A e, ρ => .abs (A.rename ρ) (e.rename ρ.liftVar) -| .tabs A e, ρ => .tabs (A.rename ρ) (e.rename ρ.liftTVar) -| .app e1 e2, ρ => .app (e1.rename ρ) (e2.rename ρ) -| .tapp e A, ρ => .tapp (e.rename ρ) (A.rename ρ) +| var x, ρ => var (ρ.var x) +| abs A e, ρ => abs (A.rename ρ) (e.rename ρ.liftVar) +| tabs A e, ρ => tabs (A.rename ρ) (e.rename ρ.liftTVar) +| app e1 e2, ρ => app (e1.rename ρ) (e2.rename ρ) +| tapp e A, ρ => tapp (e.rename ρ) (A.rename ρ) /-- Renaming with the identity renaming leaves a type unchanged. -/ theorem Ty.rename_id {T : Ty s} : T.rename Rename.id = T := by From 4083de0c31b6dfe8ea98e3db7b96d28ad3bfe413 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 14 Sep 2025 14:03:13 +0200 Subject: [PATCH 09/13] Simplify proofs --- .../WellScoped/FSub/Debruijn.lean | 24 +++++-------------- 1 file changed, 6 insertions(+), 18 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean index a2f1d960..2b38aec6 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean @@ -125,44 +125,32 @@ theorem Rename.funext {f g : Rename s1 s2} /-- Lifting the identity renaming gives the identity renaming. -/ @[simp] theorem Rename.id_liftVar_eq_id : Rename.id.liftVar = (Rename.id (s:=(s,x))) := by - apply Rename.funext - case var => intro x; cases x <;> rfl - case tvar => intro X; cases X; rfl + apply Rename.funext <;> intro x <;> cases x <;> rfl /-- Lifting the identity renaming gives the identity renaming. -/ @[simp] theorem Rename.id_liftTVar_eq_id : Rename.id.liftTVar = (Rename.id (s:=(s,X))) := by - apply Rename.funext - case var => intro x; cases x; rfl - case tvar => intro X; cases X <;> rfl + apply Rename.funext <;> intro X <;> cases X <;> rfl /-- Composition commutes with lifting over type variables. -/ theorem Rename.comp_liftTVar {f1 : Rename s1 s2} {f2 : Rename s2 s3} : (f1.comp f2).liftTVar = f1.liftTVar.comp f2.liftTVar := by - apply Rename.funext - case var => intro x; cases x; rfl - case tvar => intro X; cases X <;> rfl + apply Rename.funext <;> intro X <;> cases X <;> rfl /-- Composition commutes with lifting over term variables. -/ theorem Rename.comp_liftVar {f1 : Rename s1 s2} {f2 : Rename s2 s3} : (f1.comp f2).liftVar = f1.liftVar.comp f2.liftVar := by - apply Rename.funext - case var => intro x; cases x <;> rfl - case tvar => intro X; cases X; rfl + apply Rename.funext <;> intro x <;> cases x <;> rfl /-- Composing with variable weakening commutes with lifting. -/ theorem Rename.rename_succVar_comm {f : Rename s1 s2} : (f.comp Rename.succVar) = Rename.succVar.comp f.liftVar := by - apply Rename.funext - case var => intro x; rfl - case tvar => intro X; rfl + apply Rename.funext <;> aesop /-- Composing with type variable weakening commutes with lifting. -/ theorem Rename.rename_succTVar_comm {f : Rename s1 s2} : (f.comp Rename.succTVar) = Rename.succTVar.comp f.liftTVar := by - apply Rename.funext - case var => intro x; rfl - case tvar => intro X; rfl + apply Rename.funext <;> aesop /-- Append two signatures, concatenating their binder sequences. -/ def Sig.append : Sig → Sig → Sig From 2528b1b2bc1beb71a632c5f169724ee9732790f5 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 14 Sep 2025 14:05:11 +0200 Subject: [PATCH 10/13] Use wildcards for ununsed names --- .../FSub/TypeSoundness/Preservation.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean index 1baa2450..10ae07c7 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean @@ -32,28 +32,28 @@ theorem preservation HasType .empty t' T := by induction hred generalizing T case red_app_fun ih => - have ⟨T1, T2, ht1, ht2, hs0⟩ := HasType.app_inv ht + have ⟨_, _, ht1, ht2, hs0⟩ := HasType.app_inv ht apply HasType.sub hs0 apply HasType.app (ih ht1) ht2 case red_app_arg ih => - have ⟨T1, T2, ht1, ht2, hs0⟩ := HasType.app_inv ht + have ⟨_, _, ht1, ht2, hs0⟩ := HasType.app_inv ht apply HasType.sub hs0 apply HasType.app ht1 (ih ht2) case red_app => - have ⟨T1, T2, ht1, ht2, hs0⟩ := HasType.app_inv ht - have ⟨U0, h1, h2, h3⟩ := HasType.abs_inv ht1 + have ⟨_, _, ht1, ht2, hs0⟩ := HasType.app_inv ht + have ⟨_, h1, h2, h3⟩ := HasType.abs_inv ht1 have ht2' := HasType.sub h2 ht2 have h1' := h1.retype (Retype.open_var ht2') simp only [Ty.rename_succVar_open_var] at h1' apply HasType.sub _ h1' apply Subtyp.trans h3 hs0 case red_tapp_fun ih => - have ⟨T2, ht1, hs2⟩ := HasType.tapp_inv ht + have ⟨_, ht1, hs2⟩ := HasType.tapp_inv ht apply HasType.sub hs2 apply HasType.tapp (ih ht1) case red_tapp => - have ⟨T2, ht1, hs2⟩ := HasType.tapp_inv ht - have ⟨U0, h1, h2, h3⟩ := HasType.tabs_inv ht1 + have ⟨_, ht1, hs2⟩ := HasType.tapp_inv ht + have ⟨_, h1, h2, h3⟩ := HasType.tabs_inv ht1 have h1' := h1.retype (Retype.open_tvar h2) have h3' := h3.retype (Retype.open_tvar Subtyp.refl) apply HasType.sub _ h1' From 1ba8c9d802d7f7299e8622f1ba760cdae39e2c98 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 14 Sep 2025 14:12:54 +0200 Subject: [PATCH 11/13] Use `\cdot` for subgoals --- .../WellScoped/FSub/RebindTheory/TypeSystem.lean | 10 +++++----- .../WellScoped/FSub/RetypeTheory/Core.lean | 4 ++-- .../WellScoped/FSub/RetypeTheory/TypeSystem.lean | 2 +- .../WellScoped/FSub/Substitution/Core.lean | 4 ++-- .../WellScoped/FSub/TypeSoundness/Canonical.lean | 10 +++++----- 5 files changed, 15 insertions(+), 15 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean index 9184739f..cd317a68 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean @@ -21,7 +21,7 @@ theorem Subtyp.rebind {f : Rename s1 s2} apply Subtyp.arrow <;> grind case poly ih1 ih2 => apply Subtyp.poly <;> try grind - { apply ih2 ρ.liftTVar } + · apply ih2 ρ.liftTVar theorem HasType.rebind {f : Rename s1 s2} (ht : HasType Γ t T) @@ -33,8 +33,8 @@ theorem HasType.rebind {f : Rename s1 s2} apply ρ.var _ _ hb case sub hsub _ ih => apply sub - { apply hsub.rebind ρ } - { apply ih ρ } + · apply hsub.rebind ρ + · apply ih ρ case abs ih => apply HasType.abs simp only [Ty.rename_succVar_comm] @@ -44,8 +44,8 @@ theorem HasType.rebind {f : Rename s1 s2} apply ih ρ.liftTVar case app ih1 ih2 => apply HasType.app - { apply ih1 ρ } - { apply ih2 ρ } + · apply ih1 ρ + · apply ih2 ρ case tapp ih => simp only [Ty.open_tvar_rename_comm] apply tapp diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean index 799e95a0..acf9a8bf 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean @@ -92,8 +92,8 @@ def Retype.narrow_tvar cases hb case here => apply Subtyp.trans - { apply Subtyp.tvar; constructor } - { simp only [Ty.subst_id]; apply hs.rebind Rebind.succTVar } + · apply Subtyp.tvar; constructor + · simp only [Ty.subst_id]; apply hs.rebind Rebind.succTVar case there_tvar hb0 => apply Subtyp.tvar; grind [Ty.subst_id] /-- Creates a retyping morphism that substitutes a type for the newest type variable. -/ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean index 12e2bbf9..f5266c5c 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean @@ -17,7 +17,7 @@ def Subtyp.retype {σ : Subst s1 s2} case arrow => apply arrow <;> aesop case poly ih1 ih2 => apply poly <;> try grind - { apply ih2 ρ.liftTVar } + · apply ih2 ρ.liftTVar /-- Context retyping preserves typing judgments. -/ theorem HasType.retype {σ : Subst s1 s2} diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean index 4822e9c8..9b462a82 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean @@ -91,8 +91,8 @@ theorem Subst.funext {σ1 σ2 : Subst s1 s2} cases σ1; cases σ2 simp constructor - { funext x; aesop } - { funext X; aesop } + · funext x; aesop + · funext X; aesop /-- Lift a substitution to work under multiple binders specified by a signature. This generalizes `liftVar` and `liftTVar` to arbitrary sequences of binders. -/ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean index 0797e39d..d10351c1 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Canonical.lean @@ -105,9 +105,9 @@ theorem Subtyp.poly_inv have ⟨T3, T4, h⟩ := h; cases h have ⟨ih11, ih12⟩ := ih1 rfl rfl; have ⟨ih21, ih22⟩ := ih2 rfl rfl constructor - { grind } - { have ih12' := ih12.retype (Retype.narrow_tvar ih21) - grind [Ty.subst_id] } + · grind + · have ih12' := ih12.retype (Retype.narrow_tvar ih21) + grind [Ty.subst_id] case inr h => cases h; grind [Subtyp.top_inv] theorem Subtyp.non_tvar_left_inv @@ -164,8 +164,8 @@ theorem HasType.tabs_inv have ⟨U0, ih1, ih2, ih3⟩ := ih rfl rfl have ⟨h1, h2⟩ := Subtyp.poly_inv hs use U0; split_ands <;> try grind - { have ih3' := ih3.retype (Retype.narrow_tvar h1) - grind [Ty.subst_id] } + · have ih3' := ih3.retype (Retype.narrow_tvar h1) + grind [Ty.subst_id] case inr h => grind [HasType.value_typing] theorem HasType.value_typing_arrow_inv From 98740bd8480a5249eb4e614d1514560beb67c0ec Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Sun, 14 Sep 2025 14:17:17 +0200 Subject: [PATCH 12/13] Use named hypothesis --- .../LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean | 8 ++++++-- .../LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean | 8 ++++++-- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean index 055d2eed..1b87b1b2 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean @@ -32,9 +32,13 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.Syntax must preserve the variable and type bindings in the context. -/ structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where /-- Term variable preservation: x:T in Γ implies f(x):f(T) in Δ -/ - var : ∀ x T, Ctx.LookupVar Γ x T → Ctx.LookupVar Δ (f.var x) (T.rename f) + var : ∀ x T, + (hb : Ctx.LookupVar Γ x T) → + Ctx.LookupVar Δ (f.var x) (T.rename f) /-- Type variable preservation: X<:T in Γ implies f(X)<:f(T) in Δ -/ - tvar : ∀ X T, Ctx.LookupTVar Γ X T → Ctx.LookupTVar Δ (f.tvar X) (T.rename f) + tvar : ∀ X T, + (hb : Ctx.LookupTVar Γ X T) → + Ctx.LookupTVar Δ (f.tvar X) (T.rename f) /-- **Lifting rebinding morphisms over term variable binders**. diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean index acf9a8bf..3158b65a 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean @@ -31,8 +31,12 @@ import Cslib.Computability.LambdaCalculus.WellScoped.FSub.RebindTheory.TypeSyste Unlike rebinding morphisms, retyping morphisms map variables to typing derivations. -/ structure Retype (Γ : Ctx s1) (σ : Subst s1 s2) (Δ : Ctx s2) where - var : ∀ x T, Γ.LookupVar x T → HasType Δ (σ.var x) (T.subst σ) - tvar : ∀ X S, Γ.LookupTVar X S → Subtyp Δ (σ.tvar X) (S.subst σ) + var : ∀ x T, + (hb : Γ.LookupVar x T) → + HasType Δ (σ.var x) (T.subst σ) + tvar : ∀ X S, + (hb : Γ.LookupTVar X S) → + Subtyp Δ (σ.tvar X) (S.subst σ) /-- Extends a retyping morphism to contexts with an additional term variable. -/ def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P.subst σ) where From 418afd111989ca6659ffcf87081a099e596dd1e0 Mon Sep 17 00:00:00 2001 From: Yichen Xu Date: Mon, 15 Sep 2025 13:27:13 +0200 Subject: [PATCH 13/13] Rebase & fix all warnings Lean linter is doing more and more things, no? --- .../LambdaCalculus/WellScoped/FSub/Debruijn.lean | 4 ++-- .../WellScoped/FSub/Substitution/Core.lean | 5 +---- .../WellScoped/FSub/Substitution/Properties.lean | 16 ++++++++-------- 3 files changed, 11 insertions(+), 14 deletions(-) diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean index 2b38aec6..88c1ddd3 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Debruijn.lean @@ -119,8 +119,8 @@ def Rename.comp (f1 : Rename s1 s2) (f2 : Rename s2 s3) : Rename s1 s3 where theorem Rename.funext {f g : Rename s1 s2} (var : ∀ x, f.var x = g.var x) (tvar : ∀ X, f.tvar X = g.tvar X) : f = g := by - cases f; cases g; simp - split_ands <;> aesop + cases f; cases g + aesop /-- Lifting the identity renaming gives the identity renaming. -/ @[simp] diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean index 9b462a82..938b66e2 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Core.lean @@ -89,10 +89,7 @@ theorem Subst.funext {σ1 σ2 : Subst s1 s2} (var : ∀ x, σ1.var x = σ2.var x) (tvar : ∀ X, σ1.tvar X = σ2.tvar X) : σ1 = σ2 := by cases σ1; cases σ2 - simp - constructor - · funext x; aesop - · funext X; aesop + aesop /-- Lift a substitution to work under multiple binders specified by a signature. This generalizes `liftVar` and `liftTVar` to arbitrary sequences of binders. -/ diff --git a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean index de3ee8c1..5a4aca5b 100644 --- a/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean +++ b/Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean @@ -93,7 +93,7 @@ theorem Ty.subst_succVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) : | .poly T1 T2 => have ih1 := Ty.subst_succVar_comm (T:=T1) (σ:=σ) have ih2 := Ty.subst_succVar_comm (s0:=s0,X) (T:=T2) (σ:=σ) - simp [Ty.subst, Ty.rename, ih1]; exact ih2 + simpa [Ty.subst, Ty.rename, ih1] /-- Proves that substitution commutes with type variable weakening for types. -/ theorem Ty.subst_succTVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) : @@ -109,7 +109,7 @@ theorem Ty.subst_succTVar_comm {T : Ty (s1 ++ s0)} (σ : Subst s1 s2) : | .poly T1 T2 => have ih1 := Ty.subst_succTVar_comm (T:=T1) (σ:=σ) have ih2 := Ty.subst_succTVar_comm (s0:=s0,X) (T:=T2) (σ:=σ) - simp [Ty.subst, Ty.rename, ih1]; exact ih2 + simpa [Ty.subst, Ty.rename, ih1] /-- Base case of substitution commuting with term variable weakening. -/ theorem Ty.subst_succVar_comm_base {T : Ty s1} (σ : Subst s1 s2) : @@ -291,7 +291,7 @@ theorem Exp.subst_asSubst {e : Exp s1} {f : Rename s1 s2} : e.subst f.asSubst = e.rename f := by induction e generalizing s2 case var x => rfl - all_goals (simp [Exp.subst, Exp.rename, + all_goals (simp only [Exp.subst, Exp.rename, Ty.subst_asSubst, Rename.asSubst_liftVar_comm, Rename.asSubst_liftTVar_comm]; grind) /-- Shows that lifting the identity substitution for term variables gives the identity. -/ @@ -330,7 +330,7 @@ theorem Subst.open_tvar_rename_comm {T : Ty s} {f : Rename s s'} : /-- Proves that opening a type variable commutes with renaming for types. -/ theorem Ty.open_tvar_rename_comm {T : Ty (s,X)} {U : Ty s} {f : Rename s s'} : (T.open_tvar U).rename f = (T.rename f.liftTVar).open_tvar (U.rename f) := by - simp [Ty.open_tvar, ←Ty.subst_asSubst] + simp only [Ty.open_tvar, ←Ty.subst_asSubst] grind [Ty.subst_comp, Subst.open_tvar_rename_comm, Ty.subst_asSubst] /-- Shows that successively weakening then opening a type variable gives the identity. -/ @@ -341,14 +341,14 @@ theorem Subst.succTVar_open_tvar {T : Ty s} : theorem Exp.rename_succTVar_open_tvar {e : Exp s} : (e.rename Rename.succTVar).subst (Subst.open_tvar X) = e := by - simp [←Exp.subst_asSubst] + simp only [←Exp.subst_asSubst] grind [Exp.subst_comp, Subst.succTVar_open_tvar, Exp.subst_id] /-- Proves that renaming with succTVar then opening cancels out for types. -/ theorem Ty.rename_succTVar_open_tvar {T : Ty s} : (T.rename Rename.succTVar).subst (Subst.open_tvar X) = T := by - simp [←Ty.subst_asSubst] + simp only [←Ty.subst_asSubst] grind [Ty.subst_comp, Subst.succTVar_open_tvar, Ty.subst_id] /-- Shows that successively weakening then opening a term variable gives the identity. -/ @@ -359,14 +359,14 @@ theorem Subst.succVar_open_var {e : Exp s} : theorem Exp.rename_succVar_open_var {e : Exp s} : (e.rename Rename.succVar).subst (Subst.open_var X) = e := by - simp [←Exp.subst_asSubst] + simp only [←Exp.subst_asSubst] grind [Exp.subst_comp, Subst.succVar_open_var, Exp.subst_id] /-- Proves that renaming with succVar then opening cancels out for types. -/ theorem Ty.rename_succVar_open_var {T : Ty s} : (T.rename Rename.succVar).subst (Subst.open_var X) = T := by - simp [←Ty.subst_asSubst] + simp only [←Ty.subst_asSubst] grind [Ty.subst_comp, Subst.succVar_open_var, Ty.subst_id] /-- Proves that opening a type variable commutes with substitution for substitutions. -/