From 3136dd1170cd82a0ee60bde59e0832b4d75251eb Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 03:20:59 -0400 Subject: [PATCH 01/25] cleaning, docs --- .../LocallyNameless/Context.lean | 124 ++++- .../LocallyNameless/Fsub/Basic.lean | 108 +++++ .../LocallyNameless/Fsub/Opening.lean | 422 ++++++++++++++++++ .../LocallyNameless/Fsub/WellFormed.lean | 175 ++++++++ 4 files changed, 817 insertions(+), 12 deletions(-) create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index c1c20a96..17f01ec6 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -17,43 +17,143 @@ Contexts as pairs of free variables and types. universe u v -variable {Var : Type u} {Ty : Type v} [DecidableEq Var] +variable {α : Type u} {β : Type v} [DecidableEq α] + +-- TODO: These are pieces of API that cannot be directly automated by adding `grind` attributes to +-- `Mathlib.Data.List.Sigma`. We should consider upstreaming them to Mathlib. +namespace List + +variable {β : α → Type v} {Γ Δ : List (Sigma β)} + +omit [DecidableEq α] in +/-- Keys distribute with appending. -/ +theorem keys_append : (Δ ++ Γ).keys = Δ.keys ++ Γ.keys := by + induction Δ <;> simp_all + +/-- Sublists without duplicate keys preserve lookups. -/ +theorem sublist_dlookup (l₁ l₂ : List (Sigma β)) (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) + (s : l₁ <+ l₂) (mem : b ∈ l₁.dlookup a) : b ∈ l₂.dlookup a := by + induction s generalizing a b + case slnil => exact mem + case cons p' _ ih => + obtain ⟨a', b'⟩ := p' + have := ih nd₁ (by grind [nodupKeys_cons]) mem |> of_mem_dlookup |> mem_keys_of_mem + have : a ≠ a' := by grind [nodupKeys_cons] + simp_all + case cons₂ p' _ ih => + obtain ⟨a', b'⟩ := p' + by_cases h : a = a' + · subst h + rw [List.dlookup_cons_eq] at * + exact mem + · simp_all + +/-- A lookup in appended lists must appear in one of the lists. -/ +theorem dlookup_append_mem (l₁ l₂ : List (Sigma β)) (mem : b ∈ (l₁ ++ l₂).dlookup a) : + b ∈ l₁.dlookup a ∨ b ∈ l₂.dlookup a := by + rw [List.dlookup_append l₁ l₂ a] at mem + simp at mem + grind + +/-- List permutation preserves keys. -/ +theorem perm_keys (h : Γ.Perm Δ) : x ∈ Γ.keys ↔ x ∈ Δ.keys := by + induction h <;> grind [keys_cons] + +/-- A key not appearing in an appending of list must appear in either list. -/ +theorem nmem_append_keys (l₁ l₂ : List (Sigma β)) : + a ∉ (l₁ ++ l₂).keys ↔ a ∉ l₁.keys ∧ a ∉ l₂.keys := by + constructor <;> ( + intro h + induction l₂ + case nil => simp_all + case cons hd tl ih => + have perm : (l₁ ++ hd :: tl).Perm (hd :: (l₁ ++ tl)) := by simp + grind [keys_cons, => perm_keys] + ) + +end List namespace LambdaCalculus.LocallyNameless /-- A typing context is a list of free variables and corresponding types. -/ -abbrev Context (Var : Type u) (Ty : Type v) := List ((_ : Var) × Ty) +abbrev Context (α : Type u) (β : Type v) := List ((_ : α) × β) namespace Context open List +-- we would like grind to see through certain notations +attribute [scoped grind =] Option.mem_def +attribute [scoped grind _=_] List.append_eq +attribute [scoped grind =] List.Nodup +attribute [scoped grind =] List.NodupKeys +attribute [scoped grind _=_] List.singleton_append + +-- a few grinds on Option: +attribute [scoped grind =] Option.or_eq_some_iff +attribute [scoped grind =] Option.or_eq_none_iff + +-- we would like grind to treat list and finset membership the same +attribute [scoped grind _=_] List.mem_toFinset + +-- otherwise, we mostly reuse existing API in `Mathlib.Data.List.Sigma` +attribute [scoped grind =] List.keys_cons +attribute [scoped grind =] List.dlookup_cons_eq +attribute [scoped grind =] List.dlookup_cons_ne +attribute [scoped grind =] List.dlookup_nil +attribute [scoped grind _=_] List.dlookup_isSome + /-- The domain of a context is the finite set of free variables it uses. -/ @[simp, grind =] -def dom : Context Var Ty → Finset Var := toFinset ∘ keys +def dom (Γ : Context α β) : Finset α := Γ.keys.toFinset -/-- A well-formed context. -/ -abbrev Ok : Context Var Ty → Prop := NodupKeys +instance : HasWellFormed (Context α β) := + ⟨NodupKeys⟩ -instance : HasWellFormed (Context Var Ty) := - ⟨Ok⟩ +omit [DecidableEq α] in +@[scoped grind _=_] +theorem haswellformed_def (Γ : Context α β) : Γ✓ = Γ.NodupKeys := by rfl -variable {Γ Δ : Context Var Ty} +variable {Γ Δ : Context α β} /-- Context membership is preserved on permuting a context. -/ -theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} : x ∈ Γ.dom ↔ x ∈ Δ.dom := by - induction h <;> simp_all only [dom, Function.comp_apply, mem_toFinset, keys_cons, mem_cons] +theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : α} : x ∈ Γ.dom ↔ x ∈ Δ.dom := by + induction h <;> simp_all only [dom, mem_toFinset, keys_cons, mem_cons] grind -omit [DecidableEq Var] in +omit [DecidableEq α] in /-- Context well-formedness is preserved on permuting a context. -/ @[scoped grind →] theorem wf_perm (h : Γ.Perm Δ) : Γ✓ → Δ✓ := (List.perm_nodupKeys h).mp -omit [DecidableEq Var] in +omit [DecidableEq α] in /-- Context well-formedness is preserved on removing an element. -/ @[scoped grind →] theorem wf_strengthen (ok : (Δ ++ ⟨x, σ⟩ :: Γ)✓) : (Δ ++ Γ)✓ := by exact List.NodupKeys.sublist (by simp) ok +/-- A mapping of values within a context. -/ +@[simp, scoped grind] +def map_val (f : β → β) (Γ : Context α β) : Context α β := + Γ.map (fun ⟨var,ty⟩ => ⟨var,f ty⟩) + +omit [DecidableEq α] in +/-- A mapping of values preserves keys. -/ +@[scoped grind] +lemma map_val_keys (f) : Γ.keys = (Γ.map_val f).keys := by + induction Γ <;> simp_all + +omit [DecidableEq α] in +/-- A mapping of values preserves non-duplication of keys. -/ +theorem map_val_ok (f : β → β) : Γ✓ ↔ (Γ.map_val f)✓ := by + grind + +/-- A mapping of values maps lookups. -/ +lemma map_val_mem (mem : σ ∈ Γ.dlookup x) (f) : f σ ∈ (Γ.map_val f).dlookup x := by + induction Γ <;> grind + +/-- A mapping of values preserves non-lookups. -/ +lemma map_val_nmem (nmem : Γ.dlookup x = none) (f) : (Γ.map_val f).dlookup x = none := by + grind [List.dlookup_eq_none] + end LambdaCalculus.LocallyNameless.Context diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean new file mode 100644 index 00000000..8aaa6755 --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2025 Chris Henson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Henson +-/ + +import Cslib.Foundations.Data.HasFresh +import Cslib.Foundations.Syntax.HasSubstitution +import Cslib.Languages.LambdaCalculus.LocallyNameless.Context + +/-! # λ-calculus + +The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. + +## References + +* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012] +* See also , from which + this is adapted + +-/ + +variable {Var : Type u} [HasFresh Var] [DecidableEq Var] + +namespace LambdaCalculus.LocallyNameless.Fsub + +/-- Types of the polymorphic lambda calculus. -/ +inductive Ty (Var : Type u) + /-- The type ⊤, with a single inhabitant. -/ + | top : Ty Var + /-- Bound variables that appear in a type, using a de-Bruijn index. -/ + | bvar : ℕ → Ty Var + /-- Free type variables. -/ + | fvar : Var → Ty Var + /-- A function type. -/ + | arrow : Ty Var → Ty Var → Ty Var + /-- A universal quantification. -/ + | all : Ty Var → Ty Var → Ty Var + /-- A sum type. -/ + | sum : Ty Var → Ty Var → Ty Var + deriving Inhabited + +/-- Syntax of locally nameless lambda terms, with free variables over `Var`. -/ +inductive Term (Var : Type u) + /-- Bound term variables that appear under a lambda abstraction, using a de-Bruijn index. -/ + | bvar : ℕ → Term Var + /-- Free term variables. -/ + | fvar : Var → Term Var + /-- Lambda abstraction, introducing a new bound term variable. -/ + | abs : Ty Var → Term Var → Term Var + /-- Function application. -/ + | app : Term Var → Term Var → Term Var + /-- Type abstraction, introducing a new bound type variable. -/ + | tabs : Ty Var → Term Var → Term Var + /-- Type application. -/ + -- TODO: match this match tabs + | tapp : Term Var → Ty Var → Term Var + /-- Binding of a term. -/ + | let' : Term Var → Term Var → Term Var + /-- Left constructor of a sum. -/ + | inl : Term Var → Term Var + /-- Right constructor of a sum. -/ + | inr : Term Var → Term Var + /-- Case matching on a sum. -/ + | case : Term Var → Term Var → Term Var → Term Var + +/-- A context binding. -/ +inductive Binding (Var : Type u) + /-- Subtype binding. -/ + | sub : Ty Var → Binding Var + /-- Type binding. -/ + | ty : Ty Var → Binding Var + deriving Inhabited + +/-- Free variables of a type. -/ +@[scoped grind =] +def Ty.fv : Ty Var → Finset Var +| top | bvar _ => {} +| fvar X => {X} +| arrow σ τ | all σ τ | sum σ τ => σ.fv ∪ τ.fv + +/-- Free variables of a binding. -/ +@[scoped grind =] +def Binding.fv : Binding Var → Finset Var +| sub σ | ty σ => σ.fv + +/-- Free type variables of a term. -/ +@[scoped grind =] +def Term.fv_ty : Term Var → Finset Var +| bvar _ | fvar _ => {} +| abs σ t₁ | tabs σ t₁ | tapp t₁ σ => σ.fv ∪ t₁.fv_ty +| inl t₁ | inr t₁ => t₁.fv_ty +| app t₁ t₂ | let' t₁ t₂ => t₁.fv_ty ∪ t₂.fv_ty +| case t₁ t₂ t₃ => t₁.fv_ty ∪ t₂.fv_ty ∪ t₃.fv_ty + +/-- Free term variables of a term. -/ +@[scoped grind =] +def Term.fv_tm : Term Var → Finset Var +| bvar _ => {} +| fvar x => {x} +| abs _ t₁ | tabs _ t₁ | tapp t₁ _ | inl t₁ | inr t₁ => t₁.fv_tm +| app t₁ t₂ | let' t₁ t₂ => t₁.fv_tm ∪ t₂.fv_tm +| case t₁ t₂ t₃ => t₁.fv_tm ∪ t₂.fv_tm ∪ t₃.fv_tm + +/-- A context of bindings. -/ +abbrev Env (Var : Type u) := Context Var (Binding Var) + +end LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean new file mode 100644 index 00000000..89b787da --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean @@ -0,0 +1,422 @@ +/- +Copyright (c) 2025 Chris Henson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Henson +-/ + +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic + + +/-! # λ-calculus + +The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. +This file defines opening, local closure, and substitution. + +## References + +* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012] +* See also , from which + this is adapted + +-/ + +universe u + +variable {Var : Type u} [HasFresh Var] [DecidableEq Var] + +namespace LambdaCalculus.LocallyNameless.Fsub + +namespace Ty + +/-- Variable opening (type opening to type) of the ith bound variable. -/ +@[scoped grind =] +def openRec (X : ℕ) (δ : Ty Var) : Ty Var → Ty Var +| top => top +| bvar Y => if X = Y then δ else bvar Y +| fvar X => fvar X +| arrow σ τ => arrow (openRec X δ σ) (openRec X δ τ) +| all σ τ => all (openRec X δ σ) (openRec (X + 1) δ τ) +| sum σ τ => sum (openRec X δ σ) (openRec X δ τ) + +scoped notation:68 γ "⟦" X " ↝ " δ "⟧ᵞ"=> openRec X δ γ + +/-- Variable opening (type opening to type) of the closest binding. -/ +@[scoped grind =] +def open' (γ δ : Ty Var) := openRec 0 δ γ + +scoped infixr:80 " ^ᵞ " => open' + +/-- Locally closed types. -/ +inductive LC : Ty Var → Prop + | top : LC top + | var : LC (fvar X) + | arrow : LC σ → LC τ → LC (arrow σ τ) + | all (L : Finset Var) : LC σ → (∀ X ∉ L, LC (τ ^ᵞ fvar X)) → LC (all σ τ) + | sum : LC σ → LC τ → LC (sum σ τ) + +-- TODO: correct grind? +attribute [scoped grind <=] LC.top LC.var LC.arrow LC.sum + +/-- Type substitution. -/ +@[scoped grind =] +def subst (X : Var) (δ : Ty Var) : Ty Var → Ty Var +| top => top +| bvar J => bvar J +| fvar Y => if Y = X then δ else fvar Y +| arrow σ τ => arrow (subst X δ σ) (subst X δ τ) +| all σ τ => all (subst X δ σ) (subst X δ τ) +| sum σ τ => sum (subst X δ σ) (subst X δ τ) + +instance : HasSubstitution (Ty Var) Var (Ty Var) where + subst γ X δ := Ty.subst X δ γ + +variable {σ τ δ γ : Ty Var} + +omit [HasFresh Var] [DecidableEq Var] in +/-- An opening appearing in both sides of an equality of types can be removed. -/ +lemma openRec_neq_eq {σ τ γ : Ty Var} (neq : X ≠ Y) (h : σ⟦Y ↝ τ⟧ᵞ = σ⟦Y ↝ τ⟧ᵞ⟦X ↝ γ⟧ᵞ) : + σ = σ⟦X ↝ γ⟧ᵞ := by induction σ generalizing Y X <;> grind + +/-- A locally closed type is unchanged by opening. -/ +lemma openRec_lc {σ τ : Ty Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ᵞ := by + induction lc generalizing X <;> (have := fresh_exists <| free_union Var; grind [openRec_neq_eq]) + +omit [HasFresh Var] in +@[scoped grind _=_] +lemma subst_def : Ty.subst (X : Var) (δ : Ty Var) (γ : Ty Var) = γ[X := δ] := by rfl + +omit [HasFresh Var] in +/-- Substitution of a free variable not present in a type leaves it unchanged. -/ +lemma subst_fresh (nmem : X ∉ γ.fv) (δ : Ty Var) : γ = γ[X := δ] := by + induction γ <;> grind + +/-- Substitution of a locally closed type distributes with opening. -/ +lemma openRec_subst (Y : ℕ) (σ τ : Ty Var) (lc : δ.LC) (X : Var) : + (σ⟦Y ↝ τ⟧ᵞ)[X := δ] = σ[X := δ]⟦Y ↝ τ[X := δ]⟧ᵞ := by + induction σ generalizing Y + all_goals grind [openRec_lc] + +/-- Specialize `Ty.openRec_subst` to the first opening. -/ +lemma open_subst (σ τ : Ty Var) (lc : δ.LC) (X : Var) : (σ ^ᵞ τ)[X := δ] = σ[X := δ] ^ᵞ τ[X := δ] + := openRec_subst 0 σ τ lc X + +/-- Specialize `Ty.subst_open` to free variables. -/ +lemma open_subst_var (σ : Ty Var) (neq : Y ≠ X) (lc : δ.LC) : + (σ ^ᵞ fvar Y)[X := δ] = (σ[X := δ]) ^ᵞ fvar Y := by grind [open_subst] + +omit [HasFresh Var] in +/-- Opening to a type is equivalent to opening to a free variable and substituting. -/ +lemma openRec_subst_intro (Y : ℕ) (δ : Ty Var) (nmem : X ∉ γ.fv) : + γ⟦Y ↝ δ⟧ᵞ = (γ⟦Y ↝ fvar X⟧ᵞ)[X := δ] := by + induction γ generalizing δ Y <;> grind + +omit [HasFresh Var] in +/-- Specialize `Ty.openRec_subst_intro` to the first opening. -/ +lemma open_subst_intro (δ : Ty Var) (nmem : X ∉ γ.fv) : γ ^ᵞ δ = (γ ^ᵞ fvar X)[X := δ] := + openRec_subst_intro _ _ nmem + +lemma subst_lc (σ_lc : σ.LC) (τ_lc : τ.LC) (X : Var) : σ[X := τ].LC := by + induction σ_lc + case all => apply LC.all (free_union Var) <;> grind [openRec_subst] + all_goals grind [openRec_subst] + +omit [HasFresh Var] in +lemma nmem_fv_openRec (nmem : X ∉ (σ⟦k ↝ γ⟧ᵞ).fv) : X ∉ σ.fv := by + induction σ generalizing k <;> grind + +omit [HasFresh Var] in +lemma nmem_fv_open (nmem : X ∉ (σ ^ᵞ γ).fv) : X ∉ σ.fv := + Ty.nmem_fv_openRec (k := 0) nmem + +end Ty + +namespace Term + +open scoped Ty + +/-- Variable opening (term opening to type) of the ith bound variable. -/ +@[scoped grind =] +def openRec_ty (X : ℕ) (δ : Ty Var) : Term Var → Term Var +| bvar x => bvar x +| fvar x => fvar x +| abs σ t₁ => abs (σ⟦X ↝ δ⟧ᵞ) (openRec_ty X δ t₁) +| app t₁ t₂ => app (openRec_ty X δ t₁) (openRec_ty X δ t₂) +| tabs σ t₁ => tabs (σ⟦X ↝ δ⟧ᵞ) (openRec_ty (X + 1) δ t₁) +| tapp t₁ σ => tapp (openRec_ty X δ t₁) (σ⟦X ↝ δ⟧ᵞ) +| let' t₁ t₂ => let' (openRec_ty X δ t₁) (openRec_ty X δ t₂) +| inl t₁ => inl (openRec_ty X δ t₁) +| inr t₂ => inr (openRec_ty X δ t₂) +| case t₁ t₂ t₃ => case (openRec_ty X δ t₁) (openRec_ty X δ t₂) (openRec_ty X δ t₃) + +scoped notation:68 t "⟦" X " ↝ " δ "⟧ᵗᵞ"=> openRec_ty X δ t + +/-- Variable opening (term opening to type) of the closest binding. -/ +@[scoped grind =] +def open_ty (t : Term Var) (δ : Ty Var) := openRec_ty 0 δ t + +scoped infixr:80 " ^ᵗᵞ " => open_ty + +/-- Variable opening (term opening to term) of the ith bound variable. -/ +@[scoped grind =] +def openRec_tm (x : ℕ) (s : Term Var) : Term Var → Term Var +| bvar y => if x = y then s else (bvar y) +| fvar x => fvar x +| abs σ t₁ => abs σ (openRec_tm (x + 1) s t₁) +| app t₁ t₂ => app (openRec_tm x s t₁) (openRec_tm x s t₂) +| tabs σ t₁ => tabs σ (openRec_tm x s t₁) +| tapp t₁ σ => tapp (openRec_tm x s t₁) σ +| let' t₁ t₂ => let' (openRec_tm x s t₁) (openRec_tm (x + 1) s t₂) +| inl t₁ => inl (openRec_tm x s t₁) +| inr t₂ => inr (openRec_tm x s t₂) +| case t₁ t₂ t₃ => case (openRec_tm x s t₁) (openRec_tm (x + 1) s t₂) (openRec_tm (x + 1) s t₃) + +scoped notation:68 t "⟦" x " ↝ " s "⟧ᵗᵗ"=> openRec_tm x s t + +/-- Variable opening (term opening to term) of the closest binding. -/ +@[scoped grind =] +def open_tm (t₁ t₂ : Term Var) := openRec_tm 0 t₂ t₁ + +scoped infixr:80 " ^ᵗᵗ " => open_tm + +/-- Locally closed terms. -/ +inductive LC : Term Var → Prop + | var : LC (fvar x) + | abs (L : Finset Var) : σ.LC → (∀ x ∉ L, LC (t₁ ^ᵗᵗ fvar x)) → LC (abs σ t₁) + | app : LC t₁ → LC t₂ → LC (app t₁ t₂) + | tabs (L : Finset Var) : σ.LC → (∀ X ∉ L, LC (t₁ ^ᵗᵞ .fvar X)) → LC (tabs σ t₁) + | tapp : LC t₁ → σ.LC → LC (tapp t₁ σ) + | let' (L : Finset Var) : LC t₁ → (∀ x ∉ L, LC (t₂ ^ᵗᵗ fvar x)) → LC (let' t₁ t₂) + | inl : LC t₁ → LC (inl t₁) + | inr : LC t₁ → LC (inr t₁) + | case (L : Finset Var) : + LC t₁ → + (∀ x ∉ L, LC (t₂ ^ᵗᵗ fvar x)) → + (∀ x ∉ L, LC (t₃ ^ᵗᵗ fvar x)) → + LC (case t₁ t₂ t₃) + +-- TODO: correct grind? +attribute [scoped grind <=] LC.var LC.app LC.inl LC.inr LC.tapp + +variable {t : Term Var} {δ : Ty Var} + +omit [HasFresh Var] [DecidableEq Var] in +/-- An opening (term to type) appearing in both sides of an equality of terms can be removed. -/ +lemma openRec_ty_neq_eq (neq : X ≠ Y) (eq : t⟦Y ↝ σ⟧ᵗᵞ = t⟦Y ↝ σ⟧ᵗᵞ⟦X ↝ τ⟧ᵗᵞ) : + t = t⟦X ↝ τ⟧ᵗᵞ := by + induction t generalizing X Y <;> grind [Ty.openRec_neq_eq] + +omit [HasFresh Var] [DecidableEq Var] in +/-- Elimination of mixed term and type opening. -/ +@[scoped grind] +lemma openRec_tm_ty_eq (eq : t⟦x ↝ s⟧ᵗᵗ = t⟦x ↝ s⟧ᵗᵗ⟦y ↝ δ⟧ᵗᵞ) : t = t⟦y ↝ δ⟧ᵗᵞ + := by induction t generalizing x y <;> grind + +/-- A locally closed term is unchanged by type opening. -/ +@[scoped grind] +lemma openRec_ty_lc {t : Term Var} (lc : t.LC) : t = t⟦X ↝ σ⟧ᵗᵞ := by + induction lc generalizing X + case let' | case | tabs | abs => + have := fresh_exists <| free_union Var + congr <;> grind [Ty.openRec_lc, openRec_ty_neq_eq] + all_goals grind [Ty.openRec_lc] + +/-- Substitution of a type within a term. -/ +@[scoped grind =] +def subst_ty (X : Var) (δ : Ty Var) : Term Var → Term Var +| bvar x => bvar x +| fvar x => fvar x +| abs σ t₁ => abs (σ [X := δ]) (subst_ty X δ t₁) +| app t₁ t₂ => app (subst_ty X δ t₁) (subst_ty X δ t₂) +| tabs σ t₁ => tabs (σ [X := δ]) (subst_ty X δ t₁) +| tapp t₁ σ => tapp (subst_ty X δ t₁) (σ[X := δ]) +| let' t₁ t₂ => let' (subst_ty X δ t₁) (subst_ty X δ t₂) +| inl t₁ => inl (subst_ty X δ t₁) +| inr t₁ => inr (subst_ty X δ t₁) +| case t₁ t₂ t₃ => case (subst_ty X δ t₁) (subst_ty X δ t₂) (subst_ty X δ t₃) + +instance : HasSubstitution (Term Var) Var (Ty Var) where + subst t X δ := Term.subst_ty X δ t + +omit [HasFresh Var] in +@[scoped grind _=_] +lemma subst_ty_def : subst_ty (X : Var) (δ : Ty Var) (t : Term Var) = t[X := δ] := by rfl + +omit [HasFresh Var] in +/-- Substitution of a free type variable not present in a term leaves it unchanged. -/ +lemma subst_ty_fresh (nmem : X ∉ t.fv_ty) (δ : Ty Var) : t = t [X := δ] := + by induction t <;> grind [Ty.subst_fresh] + +/-- Substitution of a locally closed type distributes with term opening to a type . -/ +lemma openRec_ty_subst_ty (Y : ℕ) (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : + (t⟦Y ↝ σ⟧ᵗᵞ)[X := δ] = (t[X := δ])⟦Y ↝ σ[X := δ]⟧ᵗᵞ := by + induction t generalizing Y <;> grind [Ty.openRec_subst] + +/-- Specialize `Term.openRec_ty_subst` to the first opening. -/ +lemma open_ty_subst_ty (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : + (t ^ᵗᵞ σ)[X := δ] = t[X := δ] ^ᵗᵞ σ[X := δ] := openRec_ty_subst_ty 0 t σ lc X + +/-- Specialize `Term.open_ty_subst` to free type variables. -/ +lemma open_ty_subst_ty_var (t : Term Var) (neq : Y ≠ X) (lc : δ.LC) : + (t ^ᵗᵞ .fvar Y)[X := δ] = t[X := δ] ^ᵗᵞ .fvar Y := by grind [open_ty_subst_ty] + +omit [HasFresh Var] + +/-- Opening a term to a type is equivalent to opening to a free variable and substituting. -/ +lemma openRec_ty_subst_ty_intro (Y : ℕ) (t : Term Var) (nmem : X ∉ t.fv_ty) : + t⟦Y ↝ δ⟧ᵗᵞ = (t⟦Y ↝ Ty.fvar X⟧ᵗᵞ)[X := δ] := by + induction t generalizing X δ Y <;> grind [Ty.openRec_subst_intro] + +/-- Specialize `Term.openRec_ty_subst_ty_intro` to the first opening. -/ +lemma open_ty_subst_ty_intro (t : Term Var) (δ : Ty Var) (nmem : X ∉ t.fv_ty) : + t ^ᵗᵞ δ = (t ^ᵗᵞ Ty.fvar X)[X := δ] := openRec_ty_subst_ty_intro _ _ nmem + +/-- Substitution of a term within a term. -/ +@[scoped grind =] +def subst_tm (x : Var) (s : Term Var) : Term Var → Term Var +| bvar x => bvar x +| fvar y => if y = x then s else fvar y +| abs σ t₁ => abs σ (subst_tm x s t₁) +| app t₁ t₂ => app (subst_tm x s t₁) (subst_tm x s t₂) +| tabs σ t₁ => tabs σ (subst_tm x s t₁) +| tapp t₁ σ => tapp (subst_tm x s t₁) σ +| let' t₁ t₂ => let' (subst_tm x s t₁) (subst_tm x s t₂) +| inl t₁ => inl (subst_tm x s t₁) +| inr t₁ => inr (subst_tm x s t₁) +| case t₁ t₂ t₃ => case (subst_tm x s t₁) (subst_tm x s t₂) (subst_tm x s t₃) + +instance : HasSubstitution (Term Var) Var (Term Var) where + subst t x s := Term.subst_tm x s t + +@[scoped grind _=_] +lemma subst_tm_def : subst_tm (x : Var) (s : Term Var) (t : Term Var) = t[x := s] := by rfl + +omit [DecidableEq Var] in +/-- An opening (term to term) appearing in both sides of an equality of terms can be removed. -/ +lemma openRec_tm_neq_eq (neq : x ≠ y) (eq : t⟦y ↝ s₁⟧ᵗᵗ = t⟦y ↝ s₁⟧ᵗᵗ⟦x ↝ s₂⟧ᵗᵗ) : + t = t⟦x ↝ s₂⟧ᵗᵗ := by + induction t generalizing x y <;> grind + +omit [DecidableEq Var] in +/-- Elimination of mixed term and type opening. -/ +lemma openRec_ty_tm_eq (eq : t⟦Y ↝ σ⟧ᵗᵞ = t⟦Y ↝ σ⟧ᵗᵞ⟦x ↝ s⟧ᵗᵗ) : t = t⟦x ↝ s⟧ᵗᵗ := by + induction t generalizing x Y <;> grind + +variable [HasFresh Var] + +/-- A locally closed term is unchanged by term opening. -/ +@[scoped grind] +lemma openRec_tm_lc (lc : t.LC) : t = t⟦x ↝ s⟧ᵗᵗ := by + induction lc generalizing x + case let' | case | tabs | abs => + have := fresh_exists <| free_union Var + congr <;> grind [openRec_tm_neq_eq, openRec_ty_tm_eq] + all_goals grind + +variable {t s : Term Var} {δ : Ty Var} {x : Var} + +omit [HasFresh Var] in +/-- Substitution of a free term variable not present in a term leaves it unchanged. -/ +lemma subst_tm_fresh (nmem : x ∉ t.fv_tm) (s : Term Var) : t = t[x := s] := by + induction t <;> grind + +/-- Substitution of a locally closed term distributes with term opening to a term. -/ +lemma openRec_tm_subst_tm (y : ℕ) (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : + (t₁⟦y ↝ t₂⟧ᵗᵗ)[x := s] = (t₁[x := s])⟦y ↝ t₂[x := s]⟧ᵗᵗ := by + induction t₁ generalizing y <;> grind + +/-- Specialize `Term.openRec_tm_subst_tm` to the first opening. -/ +lemma open_tm_subst_tm (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : + (t₁ ^ᵗᵗ t₂)[x := s] = (t₁[x := s]) ^ᵗᵗ t₂[x := s] := openRec_tm_subst_tm 0 t₁ t₂ lc x + +/-- Specialize `Term.openRec_tm_subst_tm` to free term variables. -/ +lemma open_tm_subst_tm_var (t : Term Var) (neq : y ≠ x) (lc : s.LC) : + (t ^ᵗᵗ fvar y)[x := s] = (t[x := s]) ^ᵗᵗ fvar y := by grind [open_tm_subst_tm] + +/-- Substitution of a locally closed type distributes with term opening to a term. -/ +lemma openRec_tm_subst_ty (y : ℕ) (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) : + (t₁⟦y ↝ t₂⟧ᵗᵗ)[X := δ] = (t₁[X := δ])⟦y ↝ t₂[X := δ]⟧ᵗᵗ := by + induction t₁ generalizing y <;> grind + +/-- Specialize `Term.openRec_tm_subst_ty` to the first opening -/ +lemma open_tm_subst_ty (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) : + (t₁ ^ᵗᵗ t₂)[X := δ] = (t₁[X := δ]) ^ᵗᵗ t₂[X := δ] := openRec_tm_subst_ty 0 t₁ t₂ δ X + +/-- Specialize `Term.open_tm_subst_ty` to free term variables -/ +lemma open_tm_subst_ty_var (t₁ : Term Var) (δ : Ty Var) (X y : Var) : + (t₁ ^ᵗᵗ fvar y)[X := δ] = (t₁[X := δ]) ^ᵗᵗ fvar y := by grind [open_tm_subst_ty] + +/-- Substitution of a locally closed term distributes with term opening to a type. -/ +lemma openRec_ty_subst_tm (Y : ℕ) (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) : + (t⟦Y ↝ δ⟧ᵗᵞ)[x := s] = t[x := s]⟦Y ↝ δ⟧ᵗᵞ := by + induction t generalizing Y <;> grind + +/-- Specialize `Term.openRec_ty_subst_tm` to the first opening. -/ +lemma open_ty_subst_tm (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) : + (t ^ᵗᵞ δ)[x := s] = t[x := s] ^ᵗᵞ δ := openRec_ty_subst_tm 0 t δ lc x + +/-- Specialize `Term.open_ty_subst_tm` to free type variables. -/ +lemma open_ty_subst_tm_var (t : Term Var) (lc : s.LC) (x Y : Var) : + (t ^ᵗᵞ .fvar Y)[x := s] = t[x := s] ^ᵗᵞ .fvar Y := open_ty_subst_tm _ _ lc _ + +omit [HasFresh Var] + +/-- Opening a term to a term is equivalent to opening to a free variable and substituting. -/ +lemma openRec_tm_subst_tm_intro (y : ℕ) (t s : Term Var) (nmem : x ∉ t.fv_tm) : + t⟦y ↝ s⟧ᵗᵗ = (t⟦y ↝ fvar x⟧ᵗᵗ)[x := s] := by + induction t generalizing y <;> grind + +/-- Specialize `Term.openRec_tm_subst_tm_intro` to the first opening. -/ +lemma open_tm_subst_tm_intro (t s : Term Var) (nmem : x ∉ t.fv_tm) : + t ^ᵗᵗs = (t ^ᵗᵗ fvar x)[x := s] := openRec_tm_subst_tm_intro _ _ _ nmem + +variable [HasFresh Var] + +lemma subst_ty_lc (t_lc : t.LC) (δ_lc : δ.LC) (X : Var) : t[X := δ].LC := by + induction t_lc + -- TODO: find a way to incorporate this into a tactic... + case abs => apply LC.abs (free_union Var) <;> grind [Ty.subst_lc, open_tm_subst_ty_var] + case tabs => apply LC.tabs (free_union Var) <;> grind [Ty.subst_lc, openRec_ty_subst_ty] + case let' => apply LC.let' (free_union Var) <;> grind [Ty.subst_lc, open_tm_subst_ty_var] + case case => apply LC.case (free_union Var) <;> grind [Ty.subst_lc, open_tm_subst_ty_var] + all_goals grind [Ty.subst_lc, open_tm_subst_ty_var] + +lemma subst_tm_lc (t_lc : t.LC) (s_lc : s.LC) (x : Var) : t[x := s].LC := by + induction t_lc + -- TODO: find a way to incorporate this into a tactic... + case abs => apply LC.abs (free_union Var) <;> grind [open_tm_subst_tm_var] + case let' => apply LC.let' (free_union Var) <;> grind [open_tm_subst_tm_var] + case case => apply LC.case (free_union Var) <;> grind [open_tm_subst_tm_var] + case tabs => apply LC.tabs (free_union Var) <;> grind [open_ty_subst_tm_var] + all_goals grind + +end Term + +namespace Binding + +omit [HasFresh Var] + +/-- Binding substitution of types. -/ +@[scoped grind =] +def subst (X : Var) (δ : Ty Var) : Binding Var → Binding Var +| sub γ => sub <| γ[X := δ] +| ty γ => ty <| γ[X := δ] + +instance : HasSubstitution (Binding Var) Var (Ty Var) where + subst γ X δ := Binding.subst X δ γ + +variable {δ γ : Ty Var} {X : Var} + +@[scoped grind _=_] +lemma subst_sub : (sub γ)[X := δ] = sub (γ[X := δ]) := by rfl + +@[scoped grind _=_] +lemma subst_ty : (ty γ)[X := δ] = ty (γ[X := δ]) := by rfl + +open scoped Ty in +/-- Substitution of a free variable not present in a binding leaves it unchanged. -/ +lemma subst_fresh {γ : Binding Var} (nmem : X ∉ γ.fv) (δ : Ty Var) : γ = γ[X := δ] := by + induction γ <;> grind [Ty.subst_fresh] + +end Binding + +end LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean new file mode 100644 index 00000000..a5ac317b --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -0,0 +1,175 @@ +/- +Copyright (c) 2025 Chris Henson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Henson +-/ + +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening + +/-! # λ-calculus + +The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. +This file defines the well-formedness condition for types and contexts. + +## References + +* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012] +* See also , from which + this is adapted + +-/ + +universe u + +variable {Var : Type u} [DecidableEq Var] + +namespace LambdaCalculus.LocallyNameless.Fsub + +open scoped Ty in +/-- A type is well-formed when it is locally closed and all free variables appear in a context. -/ +inductive Ty.Wf : Env Var → Ty Var → Prop + | top : Ty.Wf Γ top + | var : Binding.sub σ ∈ Γ.dlookup X → Ty.Wf Γ (fvar X) + | arrow : Ty.Wf Γ σ → Ty.Wf Γ τ → Ty.Wf Γ (arrow σ τ) + | all (L : Finset Var) : + Ty.Wf Γ σ → + (∀ X ∉ L, Ty.Wf (⟨X,Binding.sub σ⟩ :: Γ) (τ ^ᵞ fvar X)) → + Ty.Wf Γ (all σ τ) + | sum : Ty.Wf Γ σ → Ty.Wf Γ τ → Ty.Wf Γ (sum σ τ) + +attribute [scoped grind] Ty.Wf.top Ty.Wf.var Ty.Wf.arrow Ty.Wf.sum + +/-- An environment is well-formed if it binds each variable exactly once to a well-formed type. -/ +inductive Env.Wf : Env Var → Prop + | empty : Wf [] + | sub : Wf Γ → τ.Wf Γ → X ∉ Γ.dom → Wf (⟨X, Binding.sub τ⟩ :: Γ) + | ty : Wf Γ → τ.Wf Γ → x ∉ Γ.dom → Wf (⟨x, Binding.ty τ⟩ :: Γ) + +attribute [scoped grind] Env.Wf.sub Env.Wf.ty + +variable {Γ Δ Θ : Env Var} {σ τ τ' γ δ : Ty Var} + +open scoped Context in +/-- A well-formed context contains no duplicate keys. -/ +lemma Env.Wf.to_ok {Γ : Env Var} (wf : Γ.Wf) : Γ✓ := by + induction wf <;> constructor <;> first | assumption | grind [List.mem_keys_of_mem] + +namespace Ty.Wf + +open Context List + +/-- A well-formed type is locally closed. -/ +@[grind →] +theorem lc (wf : σ.Wf Γ) : σ.LC := by + induction wf with + | all => apply LC.all (free_union Var) <;> grind + | _ => grind + +/-- A type remains well-formed under context permutation. -/ +theorem perm_env (wf : σ.Wf Γ) (perm : Γ ~ Δ) (ok_Γ : Γ✓) (ok_Δ : Δ✓) : σ.Wf Δ := by + induction wf generalizing Δ with + | all => apply all (free_union [dom] Var) <;> grind [Perm.cons, nodupKeys_cons] + | _ => grind [perm_dlookup] + +-- TODO: move the simp_all into grind? +/-- A type remains well-formed under context weakening (in the middle). -/ +theorem weaken (wf_ΓΘ : σ.Wf (Γ ++ Θ)) (ok_ΓΔΘ : (Γ ++ Δ ++ Θ)✓) : σ.Wf (Γ ++ Δ ++ Θ) := by + generalize eq : Γ ++ Θ = ΓΔ at wf_ΓΘ + induction wf_ΓΘ generalizing Γ + case all σ _ _ _ _ _ ih => + apply all (free_union [Context.dom] Var) (by grind) + intro X _ + apply ih (Γ := ⟨X, Binding.sub σ⟩ :: Γ) + · grind + · simp_all [haswellformed_def, keys] + · grind + all_goals grind [NodupKeys.sublist, sublist_dlookup] + +-- TODO: remove this? +/-- A type remains well-formed under context weakening (at the front). -/ +theorem weaken_head (wf : σ.Wf Δ) (ok : (Γ ++ Δ)✓) : σ.Wf (Γ ++ Δ) := by + have : Γ ++ Δ = [] ++ Γ ++ Δ := by rfl + grind [weaken] + +/-- A type remains well-formed under context narrowing. -/ +lemma narrow (wf : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (ok : (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ)✓) : + σ.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by + generalize eq : (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ) = Θ at wf + induction wf generalizing Γ with + | all => apply all (free_union [dom] Var) <;> grind [nodupKeys_cons, nmem_append_keys] + | _ => grind [sublist_dlookup, dlookup_append] + +/-- A type remains well-formed under context strengthening. -/ +lemma strengthen (wf : σ.Wf (Γ ++ ⟨X, Binding.ty τ⟩ :: Δ)) : σ.Wf (Γ ++ Δ) := by + generalize eq : Γ ++ ⟨X, Binding.ty τ⟩ :: Δ = Θ at wf + induction wf generalizing Γ with + | all => apply all (free_union [Context.dom] Var) <;> grind + | _ => grind [dlookup_append] + +/-- A type remains well-formed under context substitution (of a well-formed type). -/ +lemma map_subst (wf_σ : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) + (ok : (Γ.map_val (·[X:=τ']) ++ Δ)✓) : σ[X:=τ'].Wf <| Γ.map_val (·[X:=τ']) ++ Δ := sorry + +variable [HasFresh Var] in +/-- A type remains well-formed under opening (to a well-formed type). -/ +lemma open_lc (ok_Γ : Γ✓) (wf_all : (Ty.all σ τ).Wf Γ) (wf_δ : δ.Wf Γ) : (τ ^ᵞ δ).Wf Γ := by + cases wf_all with | all => + let ⟨X, _⟩ := fresh_exists <| free_union [fv, Context.dom] Var + have : Γ = Context.map_val (·[X:=δ]) [] ++ Γ := by grind + grind [open_subst_intro, map_subst] + +/-- A type bound in a context is well formed. -/ +lemma from_bind_ty (wf : Γ.Wf) (bind : Binding.ty σ ∈ Γ.dlookup X) : σ.Wf Γ := by + induction wf <;> grind [Env.Wf.to_ok, weaken_head] + +/-- A type at the head of a well-formed context is well-formed. -/ +lemma from_env_bind_ty (wf : Env.Wf (⟨X, Binding.ty σ⟩ :: Γ)) : σ.Wf Γ := by + cases wf + assumption + +/-- A subtype at the head of a well-formed context is well-formed. -/ +lemma from_env_bind_sub (wf : Env.Wf (⟨X, Binding.sub σ⟩ :: Γ)) : σ.Wf Γ := by + cases wf + assumption + +variable [HasFresh Var] in +/-- A variable not appearing in a context does not appear in its well-formed types. -/ +lemma nmem_fv {σ : Ty Var} (wf : σ.Wf Γ) (nmem : X ∉ Γ.dom) : X ∉ σ.fv := by + induction wf with + | all => have := fresh_exists <| free_union [dom] Var; grind [keys_cons, nmem_fv_open, openRec_lc] + | _ => grind + +end Ty.Wf + +namespace Env.Wf + +open Context List Binding + +/-- A context remains well-formed under narrowing (of a well-formed subtype). -/ +lemma narrow (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) : + Env.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by + induction Γ <;> cases wf_env <;> + grind [to_ok, Ty.Wf.narrow, nmem_append_keys, eq_nil_of_append_eq_nil, cases Env.Wf] + +/-- A context remains well-formed under strengthening. -/ +lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| Γ ++ Δ := by + induction Γ <;> cases wf <;> grind [Ty.Wf.strengthen, List.nmem_append_keys] + +/-- A context remains well-formed under substitution (of a well-formed type). -/ +lemma map_subst (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) : + Env.Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by + induction Γ generalizing wf_τ' Δ τ' <;> cases wf_env + case nil => grind + case cons.sub | cons.ty => constructor <;> grind [Ty.Wf.map_subst, Env.Wf.to_ok, keys_append] + +variable [HasFresh Var] + +/-- A well-formed context is unchaged by substituting for a free key. -/ +lemma map_subst_nmem (Γ : Env Var) (X : Var) (σ : Ty Var) (wf : Γ.Wf) (nmem : X ∉ Γ.dom) : + Γ = Γ.map_val (·[X:=σ]) := by + induction wf <;> grind [Ty.Wf.nmem_fv, Binding.subst_fresh] + +end Env.Wf + +end LambdaCalculus.LocallyNameless.Fsub From 2f94b9369c26e3008fa46e9f36caca733f4a7006 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 04:27:31 -0400 Subject: [PATCH 02/25] map_subst --- .../LocallyNameless/Fsub/WellFormed.lean | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index a5ac317b..55e37b59 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -57,7 +57,7 @@ lemma Env.Wf.to_ok {Γ : Env Var} (wf : Γ.Wf) : Γ✓ := by namespace Ty.Wf -open Context List +open Context List Binding /-- A well-formed type is locally closed. -/ @[grind →] @@ -107,9 +107,21 @@ lemma strengthen (wf : σ.Wf (Γ ++ ⟨X, Binding.ty τ⟩ :: Δ)) : σ.Wf (Γ + | all => apply all (free_union [Context.dom] Var) <;> grind | _ => grind [dlookup_append] +variable [HasFresh Var] in /-- A type remains well-formed under context substitution (of a well-formed type). -/ lemma map_subst (wf_σ : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) - (ok : (Γ.map_val (·[X:=τ']) ++ Δ)✓) : σ[X:=τ'].Wf <| Γ.map_val (·[X:=τ']) ++ Δ := sorry + (ok : (Γ.map_val (·[X:=τ']) ++ Δ)✓) : σ[X:=τ'].Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by + have := @map_val_mem Var (Binding Var) + generalize eq : Γ ++ ⟨X, Binding.sub τ⟩ :: Δ = Θ at wf_σ + induction wf_σ generalizing Γ τ' + case all γ _ _ _ _ _ _ => + subst eq + apply all (free_union [dom] Var) + · grind + · intro X' _ + have : (map_val (·[X:=τ']) (⟨X', Binding.sub γ⟩ :: Γ) ++ Δ)✓ := by grind [keys_append] + grind [open_subst_var] + all_goals grind [weaken_head, dlookup_append, map_val_nmem] variable [HasFresh Var] in /-- A type remains well-formed under opening (to a well-formed type). -/ @@ -137,7 +149,7 @@ variable [HasFresh Var] in /-- A variable not appearing in a context does not appear in its well-formed types. -/ lemma nmem_fv {σ : Ty Var} (wf : σ.Wf Γ) (nmem : X ∉ Γ.dom) : X ∉ σ.fv := by induction wf with - | all => have := fresh_exists <| free_union [dom] Var; grind [keys_cons, nmem_fv_open, openRec_lc] + | all => have := fresh_exists <| free_union [dom] Var; grind [nmem_fv_open, openRec_lc] | _ => grind end Ty.Wf @@ -156,6 +168,7 @@ lemma narrow (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| Γ ++ Δ := by induction Γ <;> cases wf <;> grind [Ty.Wf.strengthen, List.nmem_append_keys] +variable [HasFresh Var] in /-- A context remains well-formed under substitution (of a well-formed type). -/ lemma map_subst (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) : Env.Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by From df3bf9e049d9edc3905e3cda50762baadfd0b9bd Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 07:58:20 -0400 Subject: [PATCH 03/25] rest of porting --- .../LocallyNameless/Fsub/Opening.lean | 6 +- .../LocallyNameless/Fsub/Reduction.lean | 126 +++++++++++++ .../LocallyNameless/Fsub/Safety.lean | 118 +++++++++++++ .../LocallyNameless/Fsub/Subtype.lean | 143 +++++++++++++++ .../LocallyNameless/Fsub/Typing.lean | 166 ++++++++++++++++++ .../LocallyNameless/Fsub/WellFormed.lean | 8 + 6 files changed, 563 insertions(+), 4 deletions(-) create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean index 89b787da..e5f6d329 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean @@ -54,8 +54,7 @@ inductive LC : Ty Var → Prop | all (L : Finset Var) : LC σ → (∀ X ∉ L, LC (τ ^ᵞ fvar X)) → LC (all σ τ) | sum : LC σ → LC τ → LC (sum σ τ) --- TODO: correct grind? -attribute [scoped grind <=] LC.top LC.var LC.arrow LC.sum +attribute [scoped grind] LC.top LC.var LC.arrow LC.sum /-- Type substitution. -/ @[scoped grind =] @@ -194,8 +193,7 @@ inductive LC : Term Var → Prop (∀ x ∉ L, LC (t₃ ^ᵗᵗ fvar x)) → LC (case t₁ t₂ t₃) --- TODO: correct grind? -attribute [scoped grind <=] LC.var LC.app LC.inl LC.inr LC.tapp +attribute [scoped grind] LC.var LC.app LC.inl LC.inr LC.tapp variable {t : Term Var} {δ : Ty Var} diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean new file mode 100644 index 00000000..9ed84695 --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2025 Chris Henson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Henson +-/ + +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening +import Cslib.Foundations.Semantics.ReductionSystem.Basic + +/-! # λ-calculus + +The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. +This file defines a call-by-value reduction. + +## References + +* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012] +* See also , from which + this is adapted + +-/ + +universe u + +variable {Var : Type u} + + +namespace LambdaCalculus.LocallyNameless.Fsub + +namespace Term + +/-- Existential predicate for being a locally closed body of an abstraction. -/ +@[scoped grind =] +def body (t : Term Var) := ∃ L : Finset Var, ∀ x ∉ L, LC (t ^ᵗᵗ fvar x) + +section + +variable {t₁ t₂ t₃ : Term Var} + +variable [DecidableEq Var] + +/-- Locally closed let bindings have a locally closed body. -/ +@[scoped grind _=_] +lemma body_let : (let' t₁ t₂).LC ↔ t₁.LC ∧ t₂.body := by + constructor <;> intro h <;> cases h + case mp.let' L _ _ => + split_ands + · grind + · exists L + case mpr.intro body => + obtain ⟨_, _⟩ := body + apply LC.let' (free_union Var) <;> grind + +/-- Locally closed case bindings have a locally closed bodies. -/ +@[scoped grind _=_] +lemma body_case : (case t₁ t₂ t₃).LC ↔ t₁.LC ∧ t₂.body ∧ t₃.body := by + constructor <;> intro h + case mp => + cases h with | case L => + split_ands + · grind + · exists L + · exists L + case mpr => + obtain ⟨_, ⟨_, _⟩, ⟨_, _⟩⟩ := h + apply LC.case (free_union Var) <;> grind + +variable [HasFresh Var] + +/-- Opening a body preserves local closure. -/ +@[scoped grind <=] +lemma open_tm_body (body : t₁.body) (lc : t₂.LC) : (t₁ ^ᵗᵗ t₂).LC := by + cases body + have := fresh_exists <| free_union [fv_tm] Var + grind [subst_tm_lc, open_tm_subst_tm_intro] + +end + +/-- Values are irreducible terms. -/ +@[grind] +inductive Value : Term Var → Prop + | abs : LC (abs σ t₁) → Value (abs σ t₁) + | tabs : LC (tabs σ t₁) → Value (tabs σ t₁) + | inl : Value t₁ → Value (inl t₁) + | inr : Value t₁ → Value (inr t₁) + +@[grind →] +lemma Value.lc {t : Term Var} (val : t.Value) : t.LC := by + induction val <;> grind + +/-- The call-by-value reduction relation. -/ +@[grind, reduction_sys rs "βᵛ"] +inductive Red : Term Var → Term Var → Prop + | appₗ : LC t₂ → Red t₁ t₁' → Red (app t₁ t₂) (app t₁' t₂) + | appᵣ : Value t₁ → Red t₂ t₂' → Red (app t₁ t₂) (app t₁ t₂') + | tapp : σ.LC → Red t₁ t₁' → Red (tapp t₁ σ) (tapp t₁' σ) + | abs : LC (abs σ t₁) → Value t₂ → Red (app (abs σ t₁) t₂) (t₁ ^ᵗᵗ t₂) + | tabs : LC (tabs σ t₁) → τ.LC → Red (tapp (tabs σ t₁) τ) (t₁ ^ᵗᵞ τ) + | let_bind : Red t₁ t₁' → t₂.body → Red (let' t₁ t₂) (let' t₁' t₂) + | let_body : Value t₁ → t₂.body → Red (let' t₁ t₂) (t₂ ^ᵗᵗ t₁) + | inl : Red t₁ t₁' → Red (inl t₁) (inl t₁') + | inr : Red t₁ t₁' → Red (inr t₁) (inr t₁') + | case : Red t₁ t₁' → t₂.body → t₃.body → Red (case t₁ t₂ t₃) (case t₁' t₂ t₃) + | case_inl : Value t₁ → t₂.body → t₃.body → Red (case (inl t₁) t₂ t₃) (t₂ ^ᵗᵗ t₁) + | case_inr : Value t₁ → t₂.body → t₃.body → Red (case (inr t₁) t₂ t₃) (t₃ ^ᵗᵗ t₁) + +@[grind _=_] +private lemma rs_eq {t t' : Term Var} : t ⭢βᵛ t' ↔ Red t t' := by + have : (@rs Var).Red = Red := by rfl + simp_all + +variable [HasFresh Var] [DecidableEq Var] in +/-- Terms of a reduction are locally closed. -/ +lemma Red.lc {t t' : Term Var} (red : t ⭢βᵛ t') : t.LC ∧ t'.LC := by + induction red + case abs lc _ | tabs lc _ => + split_ands + · grind + · cases lc + have := fresh_exists <| free_union [fv_tm, fv_ty] Var + grind [subst_tm_lc, subst_ty_lc, open_tm_subst_tm_intro, open_ty_subst_ty_intro] + all_goals grind + +end Term + +end LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean new file mode 100644 index 00000000..7aa96c8a --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean @@ -0,0 +1,118 @@ +/- +Copyright (c) 2025 Chris Henson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Henson +-/ + +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction + +/-! # λ-calculus + +The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. +This file proves type safety. + +## References + +* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012] +* See also , from which + this is adapted + +-/ + +universe u + +variable {Var : Type u} [HasFresh Var] [DecidableEq Var] + +namespace LambdaCalculus.LocallyNameless.Fsub + +open Context List Env.Wf Term + +variable {t : Term Var} + +/-- Any reduction step preserves typing. -/ +lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing Γ t' τ := + sorry + +/-- Any typable term either has a reduction step or is a value. -/ +lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t' := by + generalize eq : [] = Γ at der + have der' : Typing Γ t τ := by assumption + induction der <;> subst eq <;> simp only [forall_const] at * + case var mem => grind + case app t₁ _ _ t₂ l r ih_l ih_r => + right + cases ih_l l with + | inl val_l => + cases ih_r r with + | inl val_r => + have ⟨σ, t₁, eq⟩ := Typing.canonical_form_abs val_l l + exists t₁ ^ᵗᵗ t₂ + grind + | inr red_r => + obtain ⟨t₂', _⟩ := red_r + exists t₁.app t₂' + grind + | inr red_l => + obtain ⟨t₁', _⟩ := red_l + exists t₁'.app t₂ + grind + case tapp σ' der _ ih => + right + specialize ih der + cases ih with + | inl val => + obtain ⟨_, t, _⟩ := Typing.canonical_form_tabs val der + exists t ^ᵗᵞ σ' + grind + | inr red => + obtain ⟨t', _⟩ := red + exists .tapp t' σ' + grind + case let' t₁ σ t₂ τ L der _ _ ih => + right + cases ih der with + | inl _ => + exists t₂ ^ᵗᵗ t₁ + grind + | inr red => + obtain ⟨t₁', _⟩ := red + exists t₁'.let' t₂ + grind + case inl der _ ih => + cases (ih der) with + | inl val => grind + | inr red => + right + obtain ⟨t', _⟩ := red + exists .inl t' + grind + case inr der _ ih => + cases (ih der) with + | inl val => grind + | inr red => + right + obtain ⟨t', _⟩ := red + exists .inr t' + grind + case case t₁ _ _ t₂ _ t₃ _ der _ _ _ _ ih => + right + cases ih der with + | inl val => + have ⟨t₁, lr⟩ := Typing.canonical_form_sum val der + cases lr <;> [exists t₂ ^ᵗᵗ t₁; exists t₃ ^ᵗᵗ t₁] <;> grind + | inr red => + obtain ⟨t₁', _⟩ := red + exists t₁'.case t₂ t₃ + grind + case sub => grind + case abs σ _ τ L _ _=> + left + constructor + apply LC.abs L <;> grind [cases Env.Wf, cases Term.LC] + case tabs L _ _=> + left + constructor + apply LC.tabs L <;> grind [cases Env.Wf, cases Term.LC] + +end LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean new file mode 100644 index 00000000..f7b9d9d5 --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean @@ -0,0 +1,143 @@ +/- +Copyright (c) 2025 Chris Henson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Henson +-/ + +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed + +/-! # λ-calculus + +The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. +This file defines the subtyping relation. + +## References + +* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012] +* See also , from which + this is adapted + +-/ + +universe u + +variable {Var : Type u} [DecidableEq Var] + +namespace LambdaCalculus.LocallyNameless.Fsub + +open Ty + +/-- The subtyping relation. -/ +inductive Sub : Env Var → Ty Var → Ty Var → Prop + | top : Γ.Wf → σ.Wf Γ → Sub Γ σ top + | refl_tvar : Γ.Wf → (fvar X).Wf Γ → Sub Γ (fvar X) (fvar X) + | trans_tvar : Binding.sub σ ∈ Γ.dlookup X → Sub Γ σ σ' → Sub Γ (fvar X) σ' + | arrow : Sub Γ σ σ' → Sub Γ τ' τ → Sub Γ (arrow σ' τ') (arrow σ τ) + | all (L : Finset Var) : + Sub Γ σ σ' → + (∀ X ∉ L, Sub (⟨X, Binding.sub σ⟩ :: Γ) (τ' ^ᵞ fvar X) (τ ^ᵞ fvar X)) → + Sub Γ (all σ' τ') (all σ τ) + | sum : Sub Γ σ' σ → Sub Γ τ' τ → Sub Γ (sum σ' τ') (sum σ τ) + +namespace Sub + +open Context List Ty.Wf Env.Wf + +attribute [scoped grind] Sub.top Sub.refl_tvar Sub.trans_tvar Sub.arrow Sub.sum + +variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var} + +-- TODO: rename this +/-- Subtypes have well-formed contexts and types. -/ +@[grind →] +lemma lc (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ σ.Wf Γ ∧ σ'.Wf Γ := by + induction sub with + | all => + refine ⟨by grind, ?_, ?_⟩ <;> + apply Wf.all (free_union Var) <;> grind [Env.Wf.to_ok, Wf.narrow_cons, cases Env.Wf, cases LC] + | _ => grind + +/-- Subtypes are reflexive when well-formed. -/ +lemma refl (wf_Γ : Γ.Wf) (wf_σ : σ.Wf Γ) : Sub Γ σ σ := by + induction wf_σ with + | all => apply all (free_union [Context.dom] Var) <;> grind + | _ => grind + +/-- Weakening of subtypes. -/ +lemma weaken (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ ++ Δ ++ Θ) σ σ' := by + generalize eq : Γ ++ Θ = ΓΘ at sub + induction sub generalizing Γ + case all => + subst eq + apply all (free_union [Context.dom] Var) <;> grind [keys_append] + all_goals grind [Ty.Wf.weaken_head, Env.Wf.to_ok, Ty.Wf.weaken, sublist_dlookup] + +lemma narrow_aux + (trans : ∀ Γ σ τ, Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ) + (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) σ τ) (sub₂ : Sub Δ δ' δ) : + Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ := by + generalize eq : Γ ++ ⟨X, Binding.sub δ⟩ :: Δ = Θ at sub₁ + induction sub₁ generalizing Γ δ + case trans_tvar σ _ σ' X' mem sub ih => + have p : ∀ δ, Γ ++ ⟨X, Binding.sub δ⟩ :: Δ ~ ⟨X, Binding.sub δ⟩ :: (Γ ++ Δ) := + by grind [perm_middle] + have := perm_dlookup (p := p δ') + have := perm_dlookup (p := p δ) + grind [Sub.weaken, Env.Wf.to_ok, sublist_append_of_sublist_right] + case all => apply Sub.all (free_union Var) <;> grind + all_goals grind [Ty.Wf.weaken_head, Env.Wf.narrow, Env.Wf.to_ok, Ty.Wf.narrow] + +@[grind →] +lemma trans : Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ := by + intro sub₁ sub₂ + have δ_lc : δ.LC := by grind + induction δ_lc generalizing Γ σ τ + case top => cases sub₁ <;> cases sub₂ <;> grind + case var X => + generalize eq : fvar X = γ at sub₁ + induction sub₁ <;> grind [cases Sub] + case arrow σ' τ' _ _ _ _ => + generalize eq : σ'.arrow τ' = γ at sub₁ + induction sub₁ <;> grind [cases Sub] + case sum σ' τ' _ _ _ _ => + generalize eq : σ'.sum τ' = γ at sub₁ + induction sub₁ <;> grind [cases Sub] + case all σ' τ' _ _ _ _ _ => + generalize eq : σ'.all τ' = γ at sub₁ + induction sub₁ + case all => + cases eq + cases sub₂ + case refl.top Γ σ'' τ'' _ _ _ _ _ _ _ => + have : Sub Γ (σ''.all τ'') (σ'.all τ') := by apply all (free_union Var) <;> grind + grind + case refl.all Γ _ _ _ _ _ σ _ _ _ _ _ _ => + apply all (free_union Var) + · grind + · intro X nmem + have eq : ∀ σ, ⟨X, Binding.sub σ⟩ :: Γ = [] ++ ⟨X, Binding.sub σ⟩ :: Γ := by grind + grind [Sub.narrow_aux] + all_goals grind + +instance (Γ : Env Var) : Trans (Sub Γ) (Sub Γ) (Sub Γ) := + ⟨Sub.trans⟩ + +/-- Narrowing of subtypes. -/ +lemma narrow (sub_δ : Sub Δ δ δ') (sub_narrow : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) : + Sub (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) σ τ := by + apply narrow_aux (δ := δ') <;> grind + +/-- Subtyping of substitutions. -/ +lemma map_subst (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub₂ : Sub Δ δ δ') : + Sub (Γ.map_val (·[X:=δ]) ++ Δ) (σ[X:=δ]) (τ[X:=δ]) := sorry + +/-- Strengthening of subtypes. -/ +lemma strengthen (sub : Sub (Γ ++ ⟨X, Binding.ty δ⟩ :: Δ) σ τ) : Sub (Γ ++ Δ) σ τ := by + generalize eq : Γ ++ ⟨X, Binding.ty δ⟩ :: Δ = Θ at sub + induction sub generalizing Γ + case all => apply Sub.all (free_union Var) <;> grind + all_goals grind [weaken_head, to_ok, Wf.strengthen, Env.Wf.strengthen, dlookup_append] + +end Sub + +end LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean new file mode 100644 index 00000000..cfd93d6a --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -0,0 +1,166 @@ +/- +Copyright (c) 2025 Chris Henson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Henson +-/ + +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype +import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction + +/-! # λ-calculus + +The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. +This file defines the typing relation. + +## References + +* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012] +* See also , from which + this is adapted + +-/ + +universe u + +variable {Var : Type u} [DecidableEq Var] [HasFresh Var] + +namespace LambdaCalculus.LocallyNameless.Fsub + +open Term Ty Ty.Wf Env.Wf Sub Context List + +/-- The typing relation. -/ +inductive Typing : Env Var → Term Var → Ty Var → Prop + | var : Γ.Wf → Binding.ty σ ∈ Γ.dlookup x → Typing Γ (fvar x) σ + | abs (L : Finset Var) : + (∀ x ∉ L, Typing (⟨x, Binding.ty σ⟩ :: Γ) (t₁ ^ᵗᵗ fvar x) τ) → + Typing Γ (abs σ t₁) (arrow σ τ) + | app : Typing Γ t₁ (arrow σ τ) → Typing Γ t₂ σ → Typing Γ (app t₁ t₂) τ + | tabs (L : Finset Var) : + (∀ X ∉ L, Typing (⟨X, Binding.sub σ⟩ :: Γ) (t₁ ^ᵗᵞ fvar X) (τ ^ᵞ fvar X)) → + Typing Γ (tabs σ t₁) (all σ τ) + | tapp : Typing Γ t₁ (all σ τ) → Sub Γ σ' σ → Typing Γ (tapp t₁ σ') (τ ^ᵞ σ') + | sub : Typing Γ t τ → Sub Γ τ τ' → Typing Γ t τ' + | let' (L : Finset Var) : + Typing Γ t₁ σ → + (∀ x ∉ L, Typing (⟨x, Binding.ty σ⟩ :: Γ) (t₂ ^ᵗᵗ fvar x) τ) → + Typing Γ (let' t₁ t₂) τ + | inl : Typing Γ t₁ σ → τ.Wf Γ → Typing Γ (inl t₁) (sum σ τ) + | inr : Typing Γ t₁ τ → σ.Wf Γ → Typing Γ (inr t₁) (sum σ τ) + | case (L : Finset Var) : + Typing Γ t₁ (sum σ τ) → + (∀ x ∉ L, Typing (⟨x, Binding.ty σ⟩ :: Γ) (t₂ ^ᵗᵗ fvar x) δ) → + (∀ x ∉ L, Typing (⟨x, Binding.ty τ⟩ :: Γ) (t₃ ^ᵗᵗ fvar x) δ) → + Typing Γ (case t₁ t₂ t₃) δ + +namespace Typing + +variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var} + +attribute [grind] Typing.var Typing.app Typing.tapp Typing.sub Typing.inl Typing.inr + +-- TODO: better name +@[grind →] +lemma lc {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : + Γ.Wf ∧ t.LC ∧ τ.Wf Γ := by + induction der + case tabs => + let ⟨X,mem⟩ := fresh_exists <| free_union Var + split_ands + · grind [cases Env.Wf] + · apply LC.tabs (free_union Var) <;> grind [cases Env.Wf] + · apply Ty.Wf.all (free_union Var) <;> grind [cases Env.Wf] + case abs σ Γ _ _ _ _ _ => + let ⟨X,_⟩ := fresh_exists <| free_union Var + split_ands + · grind [cases Env.Wf] + · apply LC.abs (free_union Var) <;> grind [cases Env.Wf] + · have eq : ⟨X, Binding.ty σ⟩ :: Γ = [] ++ [⟨X, Binding.ty σ⟩] ++ Γ := by rfl + grind [Ty.Wf.strengthen, cases Env.Wf] + case let' Γ _ σ _ _ _ _ _ _ _ => + let ⟨X,_⟩ := fresh_exists <| free_union Var + split_ands + · grind + · apply LC.let' (free_union Var) <;> grind + · have eq : ⟨X, Binding.ty σ⟩ :: Γ = [] ++ [⟨X, Binding.ty σ⟩] ++ Γ := by rfl + grind [Ty.Wf.strengthen] + case case Γ _ σ _ _ _ _ _ _ _ _ _ _ _ => + let ⟨X,_⟩ := fresh_exists <| free_union Var + split_ands + · grind + · apply LC.case (free_union Var) <;> grind + · have eq : ⟨X, Binding.ty σ⟩ :: Γ = [] ++ [⟨X, Binding.ty σ⟩] ++ Γ := by rfl + grind [Ty.Wf.strengthen] + all_goals grind [from_bind_ty, to_ok, open_lc, cases Env.Wf, cases Ty.Wf] + +lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : + Typing (Γ ++ Θ ++ Δ) t τ := sorry + +lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) : + Typing (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) t τ := sorry + +lemma subst_tm (der : Typing (Γ ++ ⟨X, Binding.ty σ⟩ :: Δ) t τ) (der_sub : Typing Δ s σ) : + Typing (Γ ++ Δ) (t[X := s]) τ := sorry + +lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub : Sub Γ δ δ') : + Typing (Γ.map_val (·[X := δ]) ++ Δ) (t[X := δ]) (τ[X := δ]) := sorry + +open Term Ty + +omit [HasFresh Var] + +lemma abs_inv (der : Typing Γ (.abs γ' t) τ) (sub : Sub Γ τ (arrow γ δ)) : + Sub Γ γ γ' + ∧ ∃ δ' L, ∀ x ∉ (L : Finset Var), + Typing ([⟨x, Binding.ty γ'⟩] ++ Γ) (t ^ᵗᵗ .fvar x) δ' ∧ Sub Γ δ' δ := by + generalize eq : Term.abs γ' t = e at der + induction der generalizing t γ' γ δ + case abs τ L _ _ => + cases eq + cases sub + split_ands + · assumption + · exists τ, L + grind + case sub Γ _ τ τ' _ _ ih => + subst eq + have sub' : Sub Γ τ (γ.arrow δ) := by grind + obtain ⟨_, δ', L, _⟩ := ih sub' (by rfl) + split_ands + · assumption + · exists δ', L + all_goals grind + +lemma inl_inv (der : Typing Γ (.inl t) τ) (sub : Sub Γ τ (sum γ δ)) : + ∃ γ', Typing Γ t γ' ∧ Sub Γ γ' γ := by + generalize eq : t.inl =t at der + induction der generalizing γ δ <;> grind [cases Sub] + +lemma inr_inv (der : Typing Γ (.inr t) T) (sub : Sub Γ T (sum γ δ)) : + ∃ δ', Typing Γ t δ' ∧ Sub Γ δ' δ := by + generalize eq : t.inr =t at der + induction der generalizing γ δ <;> grind [cases Sub] + +lemma canonical_form_abs (val : Value t) (der : Typing [] t (arrow σ τ)) : + ∃ δ t', t = .abs δ t' := by + generalize eq : σ.arrow τ = γ at der + generalize eq' : [] = Γ at der + induction der generalizing σ τ <;> grind [cases Sub, cases Value] + +omit [HasFresh Var] in +lemma canonical_form_tabs (val : Value t) (der : Typing [] t (all σ τ)) : + ∃ δ t', t = .tabs δ t' := by + generalize eq : σ.all τ = γ at der + generalize eq' : [] = Γ at der + induction der generalizing σ τ <;> grind [cases Sub, cases Value] + +omit [HasFresh Var] in +lemma canonical_form_sum (val : Value t) (der : Typing [] t (sum σ τ)) : + ∃ t', t = .inl t' ∨ t = .inr t' := by + generalize eq : σ.sum τ = γ at der + generalize eq' : [] = Γ at der + induction der generalizing σ τ <;> grind [cases Sub, cases Value] + +end Typing + +end LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index 55e37b59..89317ae9 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -92,6 +92,9 @@ theorem weaken_head (wf : σ.Wf Δ) (ok : (Γ ++ Δ)✓) : σ.Wf (Γ ++ Δ) := b have : Γ ++ Δ = [] ++ Γ ++ Δ := by rfl grind [weaken] +theorem weaken_cons (wf : σ.Wf Δ) (ok : (⟨X, b⟩ :: Δ)✓) : σ.Wf (⟨X, b⟩:: Δ) := by + grind [weaken_head] + /-- A type remains well-formed under context narrowing. -/ lemma narrow (wf : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (ok : (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ)✓) : σ.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by @@ -100,6 +103,11 @@ lemma narrow (wf : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (ok : (Γ ++ ⟨ | all => apply all (free_union [dom] Var) <;> grind [nodupKeys_cons, nmem_append_keys] | _ => grind [sublist_dlookup, dlookup_append] +lemma narrow_cons (wf : σ.Wf (⟨X, Binding.sub τ⟩ :: Δ)) (ok : (⟨X, Binding.sub τ'⟩ :: Δ)✓) : + σ.Wf (⟨X, Binding.sub τ'⟩ :: Δ) := by + rw [←List.nil_append (⟨X, sub τ'⟩ :: Δ)] + grind [narrow] + /-- A type remains well-formed under context strengthening. -/ lemma strengthen (wf : σ.Wf (Γ ++ ⟨X, Binding.ty τ⟩ :: Δ)) : σ.Wf (Γ ++ Δ) := by generalize eq : Γ ++ ⟨X, Binding.ty τ⟩ :: Δ = Θ at wf From aa32892d1373584f69e3f407a394d0f218668f0d Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 08:03:13 -0400 Subject: [PATCH 04/25] rm weaken_head TODO --- .../LambdaCalculus/LocallyNameless/Fsub/Subtype.lean | 9 ++++----- .../LambdaCalculus/LocallyNameless/Fsub/Typing.lean | 3 +-- .../LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean | 1 - 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean index f7b9d9d5..742dd3f7 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean @@ -47,10 +47,9 @@ attribute [scoped grind] Sub.top Sub.refl_tvar Sub.trans_tvar Sub.arrow Sub.sum variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var} --- TODO: rename this /-- Subtypes have well-formed contexts and types. -/ @[grind →] -lemma lc (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ σ.Wf Γ ∧ σ'.Wf Γ := by +lemma wf (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ σ.Wf Γ ∧ σ'.Wf Γ := by induction sub with | all => refine ⟨by grind, ?_, ?_⟩ <;> @@ -70,7 +69,7 @@ lemma weaken (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ case all => subst eq apply all (free_union [Context.dom] Var) <;> grind [keys_append] - all_goals grind [Ty.Wf.weaken_head, Env.Wf.to_ok, Ty.Wf.weaken, sublist_dlookup] + all_goals grind [Env.Wf.to_ok, Ty.Wf.weaken, sublist_dlookup] lemma narrow_aux (trans : ∀ Γ σ τ, Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ) @@ -85,7 +84,7 @@ lemma narrow_aux have := perm_dlookup (p := p δ) grind [Sub.weaken, Env.Wf.to_ok, sublist_append_of_sublist_right] case all => apply Sub.all (free_union Var) <;> grind - all_goals grind [Ty.Wf.weaken_head, Env.Wf.narrow, Env.Wf.to_ok, Ty.Wf.narrow] + all_goals grind [Env.Wf.narrow, Env.Wf.to_ok, Ty.Wf.narrow] @[grind →] lemma trans : Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ := by @@ -136,7 +135,7 @@ lemma strengthen (sub : Sub (Γ ++ ⟨X, Binding.ty δ⟩ :: Δ) σ τ) : Sub ( generalize eq : Γ ++ ⟨X, Binding.ty δ⟩ :: Δ = Θ at sub induction sub generalizing Γ case all => apply Sub.all (free_union Var) <;> grind - all_goals grind [weaken_head, to_ok, Wf.strengthen, Env.Wf.strengthen, dlookup_append] + all_goals grind [to_ok, Wf.strengthen, Env.Wf.strengthen, dlookup_append] end Sub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index cfd93d6a..9f9e736a 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -59,9 +59,8 @@ variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var} attribute [grind] Typing.var Typing.app Typing.tapp Typing.sub Typing.inl Typing.inr --- TODO: better name @[grind →] -lemma lc {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : +lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : Γ.Wf ∧ t.LC ∧ τ.Wf Γ := by induction der case tabs => diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index 89317ae9..befda3cc 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -86,7 +86,6 @@ theorem weaken (wf_ΓΘ : σ.Wf (Γ ++ Θ)) (ok_ΓΔΘ : (Γ ++ Δ ++ Θ)✓) : · grind all_goals grind [NodupKeys.sublist, sublist_dlookup] --- TODO: remove this? /-- A type remains well-formed under context weakening (at the front). -/ theorem weaken_head (wf : σ.Wf Δ) (ok : (Γ ++ Δ)✓) : σ.Wf (Γ ++ Δ) := by have : Γ ++ Δ = [] ++ Γ ++ Δ := by rfl From 0feec1d0d18eb1ef6c448ecdff0047fa271ce875 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 08:45:53 -0400 Subject: [PATCH 05/25] easy parts of preservation --- .../LocallyNameless/Fsub/Safety.lean | 23 +++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean index 7aa96c8a..56ee66da 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean @@ -31,8 +31,27 @@ open Context List Env.Wf Term variable {t : Term Var} /-- Any reduction step preserves typing. -/ -lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing Γ t' τ := - sorry +lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing Γ t' τ := by + induction der generalizing t' + case app => + cases step with + | appₗ => grind + | appᵣ => grind + | abs => sorry + case tapp => + cases step with + | tapp => grind + | tabs => sorry + case let' L der _ _ ih => + cases step with + | let_bind => sorry + | let_body => sorry + case case => + cases step with + | «case» => sorry + | case_inl => sorry + | case_inr => sorry + all_goals grind [cases Red] /-- Any typable term either has a reduction step or is a value. -/ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t' := by From 5fad2feadc420e7b846315b99e843b77c2bc4707 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 08:51:21 -0400 Subject: [PATCH 06/25] some docs --- .../LambdaCalculus/LocallyNameless/Fsub/Typing.lean | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index 9f9e736a..523817e1 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -59,6 +59,7 @@ variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var} attribute [grind] Typing.var Typing.app Typing.tapp Typing.sub Typing.inl Typing.inr +/-- Typings have well-formed contexts and types. -/ @[grind →] lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : Γ.Wf ∧ t.LC ∧ τ.Wf Γ := by @@ -92,15 +93,19 @@ lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : grind [Ty.Wf.strengthen] all_goals grind [from_bind_ty, to_ok, open_lc, cases Env.Wf, cases Ty.Wf] +/-- Weakening of typings. -/ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : Typing (Γ ++ Θ ++ Δ) t τ := sorry +/-- Narrowing of typings. -/ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) : Typing (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) t τ := sorry +/-- Term substitution within a typing. -/ lemma subst_tm (der : Typing (Γ ++ ⟨X, Binding.ty σ⟩ :: Δ) t τ) (der_sub : Typing Δ s σ) : Typing (Γ ++ Δ) (t[X := s]) τ := sorry +/-- Type substitution within a typing. -/ lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub : Sub Γ δ δ') : Typing (Γ.map_val (·[X := δ]) ++ Δ) (t[X := δ]) (τ[X := δ]) := sorry @@ -108,6 +113,7 @@ open Term Ty omit [HasFresh Var] +/-- Invert the typing of an abstraction. -/ lemma abs_inv (der : Typing Γ (.abs γ' t) τ) (sub : Sub Γ τ (arrow γ δ)) : Sub Γ γ γ' ∧ ∃ δ' L, ∀ x ∉ (L : Finset Var), @@ -130,30 +136,33 @@ lemma abs_inv (der : Typing Γ (.abs γ' t) τ) (sub : Sub Γ τ (arrow γ δ)) · exists δ', L all_goals grind +/-- Invert the typing of a left case. -/ lemma inl_inv (der : Typing Γ (.inl t) τ) (sub : Sub Γ τ (sum γ δ)) : ∃ γ', Typing Γ t γ' ∧ Sub Γ γ' γ := by generalize eq : t.inl =t at der induction der generalizing γ δ <;> grind [cases Sub] +/-- Invert the typing of a right case. -/ lemma inr_inv (der : Typing Γ (.inr t) T) (sub : Sub Γ T (sum γ δ)) : ∃ δ', Typing Γ t δ' ∧ Sub Γ δ' δ := by generalize eq : t.inr =t at der induction der generalizing γ δ <;> grind [cases Sub] +/-- A value that types as a function is an abstraction. -/ lemma canonical_form_abs (val : Value t) (der : Typing [] t (arrow σ τ)) : ∃ δ t', t = .abs δ t' := by generalize eq : σ.arrow τ = γ at der generalize eq' : [] = Γ at der induction der generalizing σ τ <;> grind [cases Sub, cases Value] -omit [HasFresh Var] in +/-- A value that types as a quantifier is a type abstraction. -/ lemma canonical_form_tabs (val : Value t) (der : Typing [] t (all σ τ)) : ∃ δ t', t = .tabs δ t' := by generalize eq : σ.all τ = γ at der generalize eq' : [] = Γ at der induction der generalizing σ τ <;> grind [cases Sub, cases Value] -omit [HasFresh Var] in +/-- A value that types as a sum is a left or right case. -/ lemma canonical_form_sum (val : Value t) (der : Typing [] t (sum σ τ)) : ∃ t', t = .inl t' ∨ t = .inr t' := by generalize eq : σ.sum τ = γ at der From 258c8bf029879b785ed301c6e9a36835bffe833a Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 13:22:13 -0400 Subject: [PATCH 07/25] more preservation --- .../LambdaCalculus/LocallyNameless/Fsub/Safety.lean | 13 ++++++++----- .../LambdaCalculus/LocallyNameless/Fsub/Typing.lean | 2 +- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean index 56ee66da..297a9385 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean @@ -33,11 +33,14 @@ variable {t : Term Var} /-- Any reduction step preserves typing. -/ lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing Γ t' τ := by induction der generalizing t' - case app => - cases step with - | appₗ => grind - | appᵣ => grind - | abs => sorry + case app Γ _ σ τ _ _ _ _ _ => + cases step + case appₗ | appᵣ => grind + case abs der _ _ => + have sub : Sub Γ (σ.arrow τ) (σ.arrow τ) := by grind [Sub.refl] + have ⟨_, _, ⟨_, _⟩⟩ := der.abs_inv sub + have ⟨_, _⟩ := fresh_exists <| free_union [fv_tm] Var + grind [open_tm_subst_tm_intro, subst_tm, Sub.weaken] case tapp => cases step with | tapp => grind diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index 523817e1..3d52b190 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -117,7 +117,7 @@ omit [HasFresh Var] lemma abs_inv (der : Typing Γ (.abs γ' t) τ) (sub : Sub Γ τ (arrow γ δ)) : Sub Γ γ γ' ∧ ∃ δ' L, ∀ x ∉ (L : Finset Var), - Typing ([⟨x, Binding.ty γ'⟩] ++ Γ) (t ^ᵗᵗ .fvar x) δ' ∧ Sub Γ δ' δ := by + Typing (⟨x, Binding.ty γ'⟩ :: Γ) (t ^ᵗᵗ .fvar x) δ' ∧ Sub Γ δ' δ := by generalize eq : Term.abs γ' t = e at der induction der generalizing t γ' γ δ case abs τ L _ _ => From f03f2c02237ab3680684648a02a9cbdbdf694549 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 20:05:55 -0400 Subject: [PATCH 08/25] finish preservation --- .../LocallyNameless/Fsub/Safety.lean | 49 ++++++++++++------- .../LocallyNameless/Fsub/Typing.lean | 28 ++++++++++- 2 files changed, 59 insertions(+), 18 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean index 297a9385..6302d667 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean @@ -26,7 +26,7 @@ variable {Var : Type u} [HasFresh Var] [DecidableEq Var] namespace LambdaCalculus.LocallyNameless.Fsub -open Context List Env.Wf Term +open Context List Env.Wf Term Ty variable {t : Term Var} @@ -41,19 +41,34 @@ lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing have ⟨_, _, ⟨_, _⟩⟩ := der.abs_inv sub have ⟨_, _⟩ := fresh_exists <| free_union [fv_tm] Var grind [open_tm_subst_tm_intro, subst_tm, Sub.weaken] - case tapp => - cases step with - | tapp => grind - | tabs => sorry - case let' L der _ _ ih => - cases step with - | let_bind => sorry - | let_body => sorry - case case => - cases step with - | «case» => sorry - | case_inl => sorry - | case_inr => sorry + case tapp Γ _ σ τ σ' _ _ _ => + cases step + case tabs der _ _ => + have sub : Sub Γ (σ.all τ) (σ.all τ) := by grind [Sub.refl] + have ⟨_, _, ⟨_, _⟩⟩ := der.tabs_inv sub + have ⟨X, _⟩ := fresh_exists <| free_union [Ty.fv, fv_ty] Var + have : Γ = (Context.map_val (·[X:=σ']) []) ++ Γ := by simp + rw [open_ty_subst_ty_intro (X := X), open_subst_intro (X := X)] <;> grind [subst_ty] + case tapp => grind + case let' Γ _ _ _ _ L der _ ih₁ _ => + cases step + case let_bind red₁ _ => apply Typing.let' L (ih₁ red₁); grind + case let_body => + have ⟨x, _⟩ := fresh_exists <| free_union [fv_tm] Var + grind [open_tm_subst_tm_intro, subst_tm] + case case Γ _ σ τ _ _ _ L _ _ _ ih₁ _ _ => + have sub : Sub Γ (σ.sum τ) (σ.sum τ) := by grind [Sub.refl] + have : Γ = [] ++ Γ := by rfl + cases step + case «case» red₁ _ _ => apply Typing.case L (ih₁ red₁) <;> grind + case case_inl der _ _ => + have ⟨_, ⟨_, _⟩⟩ := der.inl_inv sub + have ⟨x, _⟩ := fresh_exists <| free_union [fv_tm] Var + grind [open_tm_subst_tm_intro, subst_tm] + case case_inr der _ _ => + have ⟨_, ⟨_, _⟩⟩ := der.inr_inv sub + have ⟨x, _⟩ := fresh_exists <| free_union [fv_tm] Var + grind [open_tm_subst_tm_intro, subst_tm] all_goals grind [cases Red] /-- Any typable term either has a reduction step or is a value. -/ @@ -68,7 +83,7 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t' | inl val_l => cases ih_r r with | inl val_r => - have ⟨σ, t₁, eq⟩ := Typing.canonical_form_abs val_l l + have ⟨σ, t₁, eq⟩ := l.canonical_form_abs val_l exists t₁ ^ᵗᵗ t₂ grind | inr red_r => @@ -84,7 +99,7 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t' specialize ih der cases ih with | inl val => - obtain ⟨_, t, _⟩ := Typing.canonical_form_tabs val der + obtain ⟨_, t, _⟩ := der.canonical_form_tabs val exists t ^ᵗᵞ σ' grind | inr red => @@ -121,7 +136,7 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t' right cases ih der with | inl val => - have ⟨t₁, lr⟩ := Typing.canonical_form_sum val der + have ⟨t₁, lr⟩ := der.canonical_form_sum val cases lr <;> [exists t₂ ^ᵗᵗ t₁; exists t₃ ^ᵗᵗ t₁] <;> grind | inr red => obtain ⟨t₁', _⟩ := red diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index 3d52b190..dbfaec33 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -106,7 +106,7 @@ lemma subst_tm (der : Typing (Γ ++ ⟨X, Binding.ty σ⟩ :: Δ) t τ) (der_sub Typing (Γ ++ Δ) (t[X := s]) τ := sorry /-- Type substitution within a typing. -/ -lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub : Sub Γ δ δ') : +lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub : Sub Δ δ δ') : Typing (Γ.map_val (·[X := δ]) ++ Δ) (t[X := δ]) (τ[X := δ]) := sorry open Term Ty @@ -136,6 +136,32 @@ lemma abs_inv (der : Typing Γ (.abs γ' t) τ) (sub : Sub Γ τ (arrow γ δ)) · exists δ', L all_goals grind +variable [HasFresh Var] in +/-- Invert the typing of a type abstraction. -/ +lemma tabs_inv (der : Typing Γ (.tabs γ' t) τ) (sub : Sub Γ τ (all γ δ)) : + Sub Γ γ γ' + ∧ ∃ δ' L, ∀ X ∉ (L : Finset Var), + Typing (⟨X, Binding.sub γ⟩ :: Γ) (t ^ᵗᵞ fvar X) (δ' ^ᵞ fvar X) + ∧ Sub (⟨X, Binding.sub γ⟩ :: Γ) (δ' ^ᵞ fvar X) (δ ^ᵞ fvar X) := by + generalize eq : Term.tabs γ' t = e at der + induction der generalizing γ δ t γ' + case tabs σ Γ _ τ L der _ => + cases sub with | all L' sub => + split_ands + · grind + · exists τ, L ∪ L' + intro X _ + have eq : ⟨X, Binding.sub γ⟩ :: Γ = [] ++ ⟨X, Binding.sub γ⟩ :: Γ := by rfl + grind [Typing.narrow] + case sub Γ _ τ τ' _ _ ih => + subst eq + have sub' : Sub Γ τ (γ.all δ) := by trans τ' <;> grind + obtain ⟨_, δ', L, _⟩ := ih sub' (by rfl) + split_ands + · assumption + · exists δ', L + all_goals grind + /-- Invert the typing of a left case. -/ lemma inl_inv (der : Typing Γ (.inl t) τ) (sub : Sub Γ τ (sum γ δ)) : ∃ γ', Typing Γ t γ' ∧ Sub Γ γ' γ := by From b201322492d8b0d0135db8c93fe9fdc8a14fd3e6 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 21:52:55 -0400 Subject: [PATCH 09/25] all but trans case of map_subst --- .../LambdaCalculus/LocallyNameless/Context.lean | 10 ++++++++++ .../LocallyNameless/Fsub/Subtype.lean | 13 ++++++++++++- 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index 17f01ec6..20daeeba 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -156,4 +156,14 @@ lemma map_val_mem (mem : σ ∈ Γ.dlookup x) (f) : f σ ∈ (Γ.map_val f).dloo lemma map_val_nmem (nmem : Γ.dlookup x = none) (f) : (Γ.map_val f).dlookup x = none := by grind [List.dlookup_eq_none] +/-- A mapping of part of an appending of lists preseves non-duplicate keys. -/ +lemma map_val_append_left (f) (ok : (Γ ++ Δ)✓) : (Γ.map_val f ++ Δ)✓ := by + induction Δ + case nil => grind + case cons hd tl ih => + have perm : hd :: (map_val f Γ ++ tl) ~ map_val f Γ ++ hd :: tl := Perm.symm perm_middle + have perm' : hd :: (Γ ++ tl) ~ Γ ++ hd :: tl := Perm.symm perm_middle + have ok' : (hd :: (Γ ++ tl))✓ := wf_perm (id (Perm.symm perm')) ok + grind [List.nodupKeys_cons, nmem_append_keys] + end LambdaCalculus.LocallyNameless.Context diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean index 742dd3f7..2bcfc0e6 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean @@ -126,9 +126,20 @@ lemma narrow (sub_δ : Sub Δ δ δ') (sub_narrow : Sub (Γ ++ ⟨X, Binding.sub Sub (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) σ τ := by apply narrow_aux (δ := δ') <;> grind +variable [HasFresh Var] in /-- Subtyping of substitutions. -/ lemma map_subst (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub₂ : Sub Δ δ δ') : - Sub (Γ.map_val (·[X:=δ]) ++ Δ) (σ[X:=δ]) (τ[X:=δ]) := sorry + Sub (Γ.map_val (·[X:=δ]) ++ Δ) (σ[X:=δ]) (τ[X:=δ]) := by + generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at sub₁ + induction sub₁ generalizing Γ + case all => apply Sub.all (free_union Var) <;> grind [Ty.open_subst_var, Binding.subst_sub] + case trans_tvar X' _ _ _ => + subst eq + by_cases eq : X = X' + · sorry + · sorry + all_goals + grind [Env.Wf.to_ok, map_val_append_left, Sub.refl, Env.Wf.map_subst, Ty.Wf.map_subst] /-- Strengthening of subtypes. -/ lemma strengthen (sub : Sub (Γ ++ ⟨X, Binding.ty δ⟩ :: Δ) σ τ) : Sub (Γ ++ Δ) σ τ := by From 0ce79351e19171cd5c5d6c7c6e761d854f487c48 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 22 Sep 2025 22:09:23 -0400 Subject: [PATCH 10/25] easy weaken cases --- .../LambdaCalculus/LocallyNameless/Fsub/Typing.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index dbfaec33..ef5114f0 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -95,7 +95,16 @@ lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : /-- Weakening of typings. -/ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : - Typing (Γ ++ Θ ++ Δ) t τ := sorry + Typing (Γ ++ Θ ++ Δ) t τ := by + generalize eq : Γ ++ Δ = ΓΔ at der + induction der generalizing Γ wf + case var => sorry + case abs => sorry + case tabs => sorry + case let' => sorry + case case => sorry + case sub | app | tapp | inr | inl => + grind [Sub.weaken, Wf.from_env_bind_ty, Wf.from_env_bind_sub, Sub.refl] /-- Narrowing of typings. -/ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) : From d8c790556772eadd3cc35766e97d753517e14a4e Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Tue, 23 Sep 2025 15:45:37 -0400 Subject: [PATCH 11/25] half of the trans case --- .../LocallyNameless/Context.lean | 6 ++++++ .../LocallyNameless/Fsub/Subtype.lean | 21 +++++++++++-------- .../LocallyNameless/Fsub/Typing.lean | 2 +- .../LocallyNameless/Fsub/WellFormed.lean | 8 ++++--- 4 files changed, 24 insertions(+), 13 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index 20daeeba..72ec78cb 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -71,6 +71,12 @@ theorem nmem_append_keys (l₁ l₂ : List (Sigma β)) : grind [keys_cons, => perm_keys] ) +@[grind →] +theorem nodupKeys_of_nodupKeys_middle (l₁ l₂ : List (Sigma β)) (h : (l₁ ++ s :: l₂).NodupKeys) : + s.fst ∉ l₁.keys ∧ s.fst ∉ l₂.keys:= by + have : (s :: (l₁ ++ l₂)).NodupKeys := by grind [perm_middle, perm_nodupKeys] + grind [→ notMem_keys_of_nodupKeys_cons, nmem_append_keys] + end List namespace LambdaCalculus.LocallyNameless diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean index 2bcfc0e6..f9ff9bef 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean @@ -41,7 +41,7 @@ inductive Sub : Env Var → Ty Var → Ty Var → Prop namespace Sub -open Context List Ty.Wf Env.Wf +open Context List Ty.Wf Env.Wf Binding attribute [scoped grind] Sub.top Sub.refl_tvar Sub.trans_tvar Sub.arrow Sub.sum @@ -53,7 +53,7 @@ lemma wf (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ σ.W induction sub with | all => refine ⟨by grind, ?_, ?_⟩ <;> - apply Wf.all (free_union Var) <;> grind [Env.Wf.to_ok, Wf.narrow_cons, cases Env.Wf, cases LC] + apply Wf.all (free_union Var) <;> grind [Wf.narrow_cons, cases Env.Wf, cases LC] | _ => grind /-- Subtypes are reflexive when well-formed. -/ @@ -69,7 +69,11 @@ lemma weaken (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ case all => subst eq apply all (free_union [Context.dom] Var) <;> grind [keys_append] - all_goals grind [Env.Wf.to_ok, Ty.Wf.weaken, sublist_dlookup] + all_goals grind [Ty.Wf.weaken, sublist_dlookup] + +lemma weaken_head (sub : Sub Δ σ σ') (wf : (Γ ++ Δ).Wf) : Sub (Γ ++ Δ) σ σ' := by + have eq : Γ ++ Δ = [] ++ Γ ++ Δ := by grind + grind [weaken] lemma narrow_aux (trans : ∀ Γ σ τ, Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ) @@ -82,9 +86,9 @@ lemma narrow_aux by grind [perm_middle] have := perm_dlookup (p := p δ') have := perm_dlookup (p := p δ) - grind [Sub.weaken, Env.Wf.to_ok, sublist_append_of_sublist_right] + grind [Sub.weaken, sublist_append_of_sublist_right] case all => apply Sub.all (free_union Var) <;> grind - all_goals grind [Env.Wf.narrow, Env.Wf.to_ok, Ty.Wf.narrow] + all_goals grind [Env.Wf.narrow, Ty.Wf.narrow] @[grind →] lemma trans : Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ := by @@ -132,11 +136,10 @@ lemma map_subst (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub Sub (Γ.map_val (·[X:=δ]) ++ Δ) (σ[X:=δ]) (τ[X:=δ]) := by generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at sub₁ induction sub₁ generalizing Γ - case all => apply Sub.all (free_union Var) <;> grind [Ty.open_subst_var, Binding.subst_sub] - case trans_tvar X' _ _ _ => - subst eq + case all => apply Sub.all (free_union Var) <;> grind [open_subst_var] + case trans_tvar σ _ τ X' mem sub ih => by_cases eq : X = X' - · sorry + · trans δ' <;> grind [→ mem_dlookup, Ty.subst_fresh, Ty.Wf.nmem_fv, weaken_head] · sorry all_goals grind [Env.Wf.to_ok, map_val_append_left, Sub.refl, Env.Wf.map_subst, Ty.Wf.map_subst] diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index ef5114f0..b8d2590b 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -91,7 +91,7 @@ lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : · apply LC.case (free_union Var) <;> grind · have eq : ⟨X, Binding.ty σ⟩ :: Γ = [] ++ [⟨X, Binding.ty σ⟩] ++ Γ := by rfl grind [Ty.Wf.strengthen] - all_goals grind [from_bind_ty, to_ok, open_lc, cases Env.Wf, cases Ty.Wf] + all_goals grind [from_bind_ty, open_lc, cases Env.Wf, cases Ty.Wf] /-- Weakening of typings. -/ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index befda3cc..fa8f998e 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -52,12 +52,14 @@ variable {Γ Δ Θ : Env Var} {σ τ τ' γ δ : Ty Var} open scoped Context in /-- A well-formed context contains no duplicate keys. -/ +@[scoped grind →] lemma Env.Wf.to_ok {Γ : Env Var} (wf : Γ.Wf) : Γ✓ := by induction wf <;> constructor <;> first | assumption | grind [List.mem_keys_of_mem] namespace Ty.Wf open Context List Binding +open scoped Env.Wf /-- A well-formed type is locally closed. -/ @[grind →] @@ -140,7 +142,7 @@ lemma open_lc (ok_Γ : Γ✓) (wf_all : (Ty.all σ τ).Wf Γ) (wf_δ : δ.Wf Γ) /-- A type bound in a context is well formed. -/ lemma from_bind_ty (wf : Γ.Wf) (bind : Binding.ty σ ∈ Γ.dlookup X) : σ.Wf Γ := by - induction wf <;> grind [Env.Wf.to_ok, weaken_head] + induction wf <;> grind [weaken_head] /-- A type at the head of a well-formed context is well-formed. -/ lemma from_env_bind_ty (wf : Env.Wf (⟨X, Binding.ty σ⟩ :: Γ)) : σ.Wf Γ := by @@ -169,7 +171,7 @@ open Context List Binding lemma narrow (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) : Env.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by induction Γ <;> cases wf_env <;> - grind [to_ok, Ty.Wf.narrow, nmem_append_keys, eq_nil_of_append_eq_nil, cases Env.Wf] + grind [Ty.Wf.narrow, nmem_append_keys, eq_nil_of_append_eq_nil, cases Env.Wf] /-- A context remains well-formed under strengthening. -/ lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| Γ ++ Δ := by @@ -181,7 +183,7 @@ lemma map_subst (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' Env.Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by induction Γ generalizing wf_τ' Δ τ' <;> cases wf_env case nil => grind - case cons.sub | cons.ty => constructor <;> grind [Ty.Wf.map_subst, Env.Wf.to_ok, keys_append] + case cons.sub | cons.ty => constructor <;> grind [Ty.Wf.map_subst, keys_append] variable [HasFresh Var] From 9a433f3fa81f01567e629093952f8336e8b4a22c Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Tue, 23 Sep 2025 18:18:09 -0400 Subject: [PATCH 12/25] complete map_subst --- .../LambdaCalculus/LocallyNameless/Fsub/Subtype.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean index f9ff9bef..3a76fc09 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean @@ -137,10 +137,14 @@ lemma map_subst (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at sub₁ induction sub₁ generalizing Γ case all => apply Sub.all (free_union Var) <;> grind [open_subst_var] - case trans_tvar σ _ τ X' mem sub ih => - by_cases eq : X = X' + case trans_tvar σ _ _ X' _ _ _ => + have := map_subst_nmem Δ X δ + have : Γ ++ ⟨X, .sub δ'⟩ :: Δ ~ ⟨X, .sub δ'⟩ :: (Γ ++ Δ) := perm_middle + have : .sub σ ∈ dlookup X' (⟨X, .sub δ'⟩ :: (Γ ++ Δ)) := by grind [perm_dlookup] + have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var)) + by_cases X = X' · trans δ' <;> grind [→ mem_dlookup, Ty.subst_fresh, Ty.Wf.nmem_fv, weaken_head] - · sorry + · grind all_goals grind [Env.Wf.to_ok, map_val_append_left, Sub.refl, Env.Wf.map_subst, Ty.Wf.map_subst] From 7b77d47d976748c1456842405d0cd7ccede85b41 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Tue, 23 Sep 2025 23:53:34 -0400 Subject: [PATCH 13/25] type weakening --- .../LocallyNameless/Fsub/Typing.lean | 17 ++++++++--------- .../LocallyNameless/Fsub/WellFormed.lean | 6 +++--- 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index b8d2590b..8a50c447 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -91,20 +91,19 @@ lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : · apply LC.case (free_union Var) <;> grind · have eq : ⟨X, Binding.ty σ⟩ :: Γ = [] ++ [⟨X, Binding.ty σ⟩] ++ Γ := by rfl grind [Ty.Wf.strengthen] - all_goals grind [from_bind_ty, open_lc, cases Env.Wf, cases Ty.Wf] + all_goals grind [of_bind_ty, open_lc, cases Env.Wf, cases Ty.Wf] /-- Weakening of typings. -/ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : Typing (Γ ++ Θ ++ Δ) t τ := by generalize eq : Γ ++ Δ = ΓΔ at der - induction der generalizing Γ wf - case var => sorry - case abs => sorry - case tabs => sorry - case let' => sorry - case case => sorry - case sub | app | tapp | inr | inl => - grind [Sub.weaken, Wf.from_env_bind_ty, Wf.from_env_bind_sub, Sub.refl] + induction der generalizing Γ + case' abs => apply Typing.abs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) + case' tabs => apply Typing.tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) + case' let' der _ => apply Typing.let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) + case' case der _ _ => apply Typing.case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) + all_goals + grind [Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, Sub.refl, sublist_dlookup] /-- Narrowing of typings. -/ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) : diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index fa8f998e..cd344de0 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -141,16 +141,16 @@ lemma open_lc (ok_Γ : Γ✓) (wf_all : (Ty.all σ τ).Wf Γ) (wf_δ : δ.Wf Γ) grind [open_subst_intro, map_subst] /-- A type bound in a context is well formed. -/ -lemma from_bind_ty (wf : Γ.Wf) (bind : Binding.ty σ ∈ Γ.dlookup X) : σ.Wf Γ := by +lemma of_bind_ty (wf : Γ.Wf) (bind : Binding.ty σ ∈ Γ.dlookup X) : σ.Wf Γ := by induction wf <;> grind [weaken_head] /-- A type at the head of a well-formed context is well-formed. -/ -lemma from_env_bind_ty (wf : Env.Wf (⟨X, Binding.ty σ⟩ :: Γ)) : σ.Wf Γ := by +lemma of_env_ty (wf : Env.Wf (⟨X, Binding.ty σ⟩ :: Γ)) : σ.Wf Γ := by cases wf assumption /-- A subtype at the head of a well-formed context is well-formed. -/ -lemma from_env_bind_sub (wf : Env.Wf (⟨X, Binding.sub σ⟩ :: Γ)) : σ.Wf Γ := by +lemma of_env_sub (wf : Env.Wf (⟨X, Binding.sub σ⟩ :: Γ)) : σ.Wf Γ := by cases wf assumption From 9c7b236e72df83796d37d0ba1a3a9e4755d16ded Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 24 Sep 2025 00:45:17 -0400 Subject: [PATCH 14/25] narrow --- .../LocallyNameless/Fsub/Typing.lean | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index 8a50c447..c4f2fef6 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -98,7 +98,7 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : Typing (Γ ++ Θ ++ Δ) t τ := by generalize eq : Γ ++ Δ = ΓΔ at der induction der generalizing Γ - case' abs => apply Typing.abs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) + case' abs => apply Typing.abs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) case' tabs => apply Typing.tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) case' let' der _ => apply Typing.let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) case' case der _ _ => apply Typing.case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) @@ -107,7 +107,18 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : /-- Narrowing of typings. -/ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) : - Typing (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) t τ := sorry + Typing (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) t τ := by + generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at der + induction der generalizing Γ + case var X' _ _ => + have : X ≠ X' := by grind [→ List.mem_dlookup] + have p (δ) : Γ ++ ⟨X, Binding.sub δ⟩ :: Δ ~ ⟨X, Binding.sub δ⟩ :: (Γ ++ Δ) := perm_middle + grind [Env.Wf.narrow, List.perm_nodupKeys, => List.perm_dlookup] + case' abs => apply Typing.abs (free_union Var) + case' tabs => apply Typing.tabs (free_union Var) + case' let' der _ => apply Typing.let' (free_union Var) (der eq) + case' case der _ _ => apply Typing.case (free_union Var) (der eq) + all_goals grind [Ty.Wf.narrow, Env.Wf.narrow, Sub.narrow] /-- Term substitution within a typing. -/ lemma subst_tm (der : Typing (Γ ++ ⟨X, Binding.ty σ⟩ :: Δ) t τ) (der_sub : Typing Δ s σ) : From 7ebca76c0d13a367c17d548ac867250243fb658b Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 24 Sep 2025 00:51:07 -0400 Subject: [PATCH 15/25] style --- .../LocallyNameless/Fsub/Typing.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index c4f2fef6..83099b30 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -98,10 +98,10 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : Typing (Γ ++ Θ ++ Δ) t τ := by generalize eq : Γ ++ Δ = ΓΔ at der induction der generalizing Γ - case' abs => apply Typing.abs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) - case' tabs => apply Typing.tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) - case' let' der _ => apply Typing.let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) - case' case der _ _ => apply Typing.case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) + case' abs => apply abs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) + case' tabs => apply tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) + case' let' der _ => apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) + case' case der _ _ => apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) all_goals grind [Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, Sub.refl, sublist_dlookup] @@ -114,10 +114,10 @@ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ have : X ≠ X' := by grind [→ List.mem_dlookup] have p (δ) : Γ ++ ⟨X, Binding.sub δ⟩ :: Δ ~ ⟨X, Binding.sub δ⟩ :: (Γ ++ Δ) := perm_middle grind [Env.Wf.narrow, List.perm_nodupKeys, => List.perm_dlookup] - case' abs => apply Typing.abs (free_union Var) - case' tabs => apply Typing.tabs (free_union Var) - case' let' der _ => apply Typing.let' (free_union Var) (der eq) - case' case der _ _ => apply Typing.case (free_union Var) (der eq) + case' abs => apply abs (free_union Var) + case' tabs => apply tabs (free_union Var) + case' let' der _ => apply let' (free_union Var) (der eq) + case' case der _ _ => apply case (free_union Var) (der eq) all_goals grind [Ty.Wf.narrow, Env.Wf.narrow, Sub.narrow] /-- Term substitution within a typing. -/ @@ -171,7 +171,7 @@ lemma tabs_inv (der : Typing Γ (.tabs γ' t) τ) (sub : Sub Γ τ (all γ δ)) · exists τ, L ∪ L' intro X _ have eq : ⟨X, Binding.sub γ⟩ :: Γ = [] ++ ⟨X, Binding.sub γ⟩ :: Γ := by rfl - grind [Typing.narrow] + grind [narrow] case sub Γ _ τ τ' _ _ ih => subst eq have sub' : Sub Γ τ (γ.all δ) := by trans τ' <;> grind From b8d8f28c8b1c4289fcd843e0f17639eb83c9ebea Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 24 Sep 2025 04:03:43 -0400 Subject: [PATCH 16/25] donegit st! --- .../LocallyNameless/Fsub/Typing.lean | 58 +++++++++++++++++-- 1 file changed, 53 insertions(+), 5 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index 83099b30..dbd33400 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -27,7 +27,7 @@ variable {Var : Type u} [DecidableEq Var] [HasFresh Var] namespace LambdaCalculus.LocallyNameless.Fsub -open Term Ty Ty.Wf Env.Wf Sub Context List +open Term Ty Ty.Wf Env.Wf Sub Context List Binding /-- The typing relation. -/ inductive Typing : Env Var → Term Var → Ty Var → Prop @@ -105,6 +105,14 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : all_goals grind [Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, Sub.refl, sublist_dlookup] +/-- Weakening of typings (at the front). -/ +lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) : + Typing (Γ ++ Δ) t τ := by + have eq : Δ = [] ++ Δ := by rfl + rw [eq] at der + have := Typing.weaken der wf + grind + /-- Narrowing of typings. -/ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) : Typing (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) t τ := by @@ -112,7 +120,7 @@ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ induction der generalizing Γ case var X' _ _ => have : X ≠ X' := by grind [→ List.mem_dlookup] - have p (δ) : Γ ++ ⟨X, Binding.sub δ⟩ :: Δ ~ ⟨X, Binding.sub δ⟩ :: (Γ ++ Δ) := perm_middle + have p (δ) : Γ ++ ⟨X, .sub δ⟩ :: Δ ~ ⟨X, .sub δ⟩ :: (Γ ++ Δ) := perm_middle grind [Env.Wf.narrow, List.perm_nodupKeys, => List.perm_dlookup] case' abs => apply abs (free_union Var) case' tabs => apply tabs (free_union Var) @@ -121,12 +129,52 @@ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ all_goals grind [Ty.Wf.narrow, Env.Wf.narrow, Sub.narrow] /-- Term substitution within a typing. -/ -lemma subst_tm (der : Typing (Γ ++ ⟨X, Binding.ty σ⟩ :: Δ) t τ) (der_sub : Typing Δ s σ) : - Typing (Γ ++ Δ) (t[X := s]) τ := sorry +lemma subst_tm (der : Typing (Γ ++ ⟨X, .ty σ⟩ :: Δ) t τ) (der_sub : Typing Δ s σ) : + Typing (Γ ++ Δ) (t[X := s]) τ := by + generalize eq : Γ ++ ⟨X, .ty σ⟩ :: Δ = Θ at der + induction der generalizing Γ X + case var σ' _ X' _ _ => + have : Γ ++ ⟨X, .ty σ⟩ :: Δ ~ ⟨X, .ty σ⟩ :: (Γ ++ Δ) := perm_middle + by_cases eq : X = X' + · grind [→ List.mem_dlookup, weaken_head, Env.Wf.strengthen] + · grind [Env.Wf.strengthen, => List.perm_dlookup] + case abs => + apply abs (free_union Var) + grind [open_tm_subst_tm_var] + case tabs => + apply tabs (free_union Var) + grind [open_ty_subst_tm_var] + case let' der _ => + apply let' (free_union Var) (der eq) + grind [open_tm_subst_tm_var] + case case der _ _ => + apply case (free_union Var) (der eq) <;> grind [open_tm_subst_tm_var] + all_goals grind [Env.Wf.strengthen, Ty.Wf.strengthen, Sub.strengthen] /-- Type substitution within a typing. -/ lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub : Sub Δ δ δ') : - Typing (Γ.map_val (·[X := δ]) ++ Δ) (t[X := δ]) (τ[X := δ]) := sorry + Typing (Γ.map_val (·[X := δ]) ++ Δ) (t[X := δ]) (τ[X := δ]) := by + generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at der + induction der generalizing Γ X + case var σ _ X' _ mem => + have := map_subst_nmem Δ X δ + have : Γ ++ ⟨X, .sub δ'⟩ :: Δ ~ ⟨X, .sub δ'⟩ :: (Γ ++ Δ) := perm_middle + have : .ty σ ∈ dlookup X' (⟨X, .sub δ'⟩ :: (Γ ++ Δ)) := by grind [perm_dlookup] + have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var)) + grind [Env.Wf.map_subst] + case abs => + apply abs (free_union [Ty.fv] Var) + grind [Ty.subst_fresh, open_tm_subst_ty_var] + case tabs => + apply tabs (free_union Var) + grind [open_ty_subst_ty_var, open_subst_var] + case let' der _ => + apply let' (free_union Var) (der eq) + grind [open_tm_subst_ty_var] + case case der _ _ => + apply case (free_union Var) (der eq) <;> grind [open_tm_subst_ty_var] + case tapp => grind [Ty.open_subst, Env.Wf.map_subst, Ty.Wf.map_subst, Sub.map_subst] + all_goals grind [Env.Wf.map_subst, Ty.Wf.map_subst, Sub.map_subst] open Term Ty From 94052f54b55f52d3dc2b38edcc3109a0f2cd3609 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 24 Sep 2025 04:19:05 -0400 Subject: [PATCH 17/25] rm duplicated API --- .../LambdaCalculus/LocallyNameless/Context.lean | 14 +++----------- .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean | 4 ++-- 2 files changed, 5 insertions(+), 13 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index 72ec78cb..ab348c3a 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -71,6 +71,7 @@ theorem nmem_append_keys (l₁ l₂ : List (Sigma β)) : grind [keys_cons, => perm_keys] ) +/-- An element between two appended lists without duplicate keys appears in neither list. -/ @[grind →] theorem nodupKeys_of_nodupKeys_middle (l₁ l₂ : List (Sigma β)) (h : (l₁ ++ s :: l₂).NodupKeys) : s.fst ∉ l₁.keys ∧ s.fst ∉ l₂.keys:= by @@ -108,6 +109,7 @@ attribute [scoped grind =] List.dlookup_cons_eq attribute [scoped grind =] List.dlookup_cons_ne attribute [scoped grind =] List.dlookup_nil attribute [scoped grind _=_] List.dlookup_isSome +attribute [scoped grind →] List.perm_nodupKeys /-- The domain of a context is the finite set of free variables it uses. -/ @[simp, grind =] @@ -122,16 +124,6 @@ theorem haswellformed_def (Γ : Context α β) : Γ✓ = Γ.NodupKeys := by rfl variable {Γ Δ : Context α β} -/-- Context membership is preserved on permuting a context. -/ -theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : α} : x ∈ Γ.dom ↔ x ∈ Δ.dom := by - induction h <;> simp_all only [dom, mem_toFinset, keys_cons, mem_cons] - grind - -omit [DecidableEq α] in -/-- Context well-formedness is preserved on permuting a context. -/ -@[scoped grind →] -theorem wf_perm (h : Γ.Perm Δ) : Γ✓ → Δ✓ := (List.perm_nodupKeys h).mp - omit [DecidableEq α] in /-- Context well-formedness is preserved on removing an element. -/ @[scoped grind →] @@ -169,7 +161,7 @@ lemma map_val_append_left (f) (ok : (Γ ++ Δ)✓) : (Γ.map_val f ++ Δ)✓ := case cons hd tl ih => have perm : hd :: (map_val f Γ ++ tl) ~ map_val f Γ ++ hd :: tl := Perm.symm perm_middle have perm' : hd :: (Γ ++ tl) ~ Γ ++ hd :: tl := Perm.symm perm_middle - have ok' : (hd :: (Γ ++ tl))✓ := wf_perm (id (Perm.symm perm')) ok + have ok' : (hd :: (Γ ++ tl))✓ := by grind grind [List.nodupKeys_cons, nmem_append_keys] end LambdaCalculus.LocallyNameless.Context diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean index 5e28a18f..016f5e02 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean @@ -102,7 +102,7 @@ lemma subst_aux (h : Δ ++ ⟨x, σ⟩ :: Γ ⊢ t ∶ τ) (der : Γ ⊢ s ∶ case var x' τ ok mem => simp only [subst_fvar] subst eq - cases (Context.wf_perm (by simp) ok : (⟨x, σ⟩ :: Δ ++ Γ)✓) + cases ((List.perm_nodupKeys (by simp)).mp ok : (⟨x, σ⟩ :: Δ ++ Γ)✓) case cons ok_weak _ => observe perm : (Γ ++ Δ).Perm (Δ ++ Γ) by_cases h : x = x' <;> simp only [h] @@ -120,7 +120,7 @@ lemma subst_aux (h : Δ ++ ⟨x, σ⟩ :: Γ ⊢ t ∶ τ) (der : Γ ⊢ s ∶ match mem with | _ => simp_all rw [eq'] refine (weaken der ?_).perm perm - exact Context.wf_perm (id (List.Perm.symm perm)) ok_weak + grind case abs σ Γ' t T2 xs ih' ih => apply Typing.abs (free_union Var) intros From edf2ba27a10edba6dff66a3953e9d388a19cea7d Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 24 Sep 2025 04:21:19 -0400 Subject: [PATCH 18/25] redundant lemma --- .../Languages/LambdaCalculus/LocallyNameless/Context.lean | 7 ------- 1 file changed, 7 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index ab348c3a..a024cfc4 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -48,13 +48,6 @@ theorem sublist_dlookup (l₁ l₂ : List (Sigma β)) (nd₁ : l₁.NodupKeys) ( exact mem · simp_all -/-- A lookup in appended lists must appear in one of the lists. -/ -theorem dlookup_append_mem (l₁ l₂ : List (Sigma β)) (mem : b ∈ (l₁ ++ l₂).dlookup a) : - b ∈ l₁.dlookup a ∨ b ∈ l₂.dlookup a := by - rw [List.dlookup_append l₁ l₂ a] at mem - simp at mem - grind - /-- List permutation preserves keys. -/ theorem perm_keys (h : Γ.Perm Δ) : x ∈ Γ.keys ↔ x ∈ Δ.keys := by induction h <;> grind [keys_cons] From 9a3b092dadfa192f951f9a6b1b55d9eeb0ee6cdf Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 24 Sep 2025 04:53:09 -0400 Subject: [PATCH 19/25] large union trouble --- .../LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index cd344de0..c41be4c9 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -74,18 +74,11 @@ theorem perm_env (wf : σ.Wf Γ) (perm : Γ ~ Δ) (ok_Γ : Γ✓) (ok_Δ : Δ✓ | all => apply all (free_union [dom] Var) <;> grind [Perm.cons, nodupKeys_cons] | _ => grind [perm_dlookup] --- TODO: move the simp_all into grind? /-- A type remains well-formed under context weakening (in the middle). -/ theorem weaken (wf_ΓΘ : σ.Wf (Γ ++ Θ)) (ok_ΓΔΘ : (Γ ++ Δ ++ Θ)✓) : σ.Wf (Γ ++ Δ ++ Θ) := by generalize eq : Γ ++ Θ = ΓΔ at wf_ΓΘ induction wf_ΓΘ generalizing Γ - case all σ _ _ _ _ _ ih => - apply all (free_union [Context.dom] Var) (by grind) - intro X _ - apply ih (Γ := ⟨X, Binding.sub σ⟩ :: Γ) - · grind - · simp_all [haswellformed_def, keys] - · grind + case all => apply all ((Γ ++ Δ ++ Θ).dom ∪ free_union Var) <;> grind all_goals grind [NodupKeys.sublist, sublist_dlookup] /-- A type remains well-formed under context weakening (at the front). -/ From a4946a4df9b200739f686744d93123877b75ac33 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 24 Sep 2025 04:55:31 -0400 Subject: [PATCH 20/25] old TODOs --- .../LocallyNameless/Fsub/Basic.lean | 1 - .../LocallyNameless/Fsub/Opening.lean | 22 +++++++++---------- 2 files changed, 10 insertions(+), 13 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean index 8aaa6755..60b0c523 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean @@ -53,7 +53,6 @@ inductive Term (Var : Type u) /-- Type abstraction, introducing a new bound type variable. -/ | tabs : Ty Var → Term Var → Term Var /-- Type application. -/ - -- TODO: match this match tabs | tapp : Term Var → Ty Var → Term Var /-- Binding of a term. -/ | let' : Term Var → Term Var → Term Var diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean index e5f6d329..a09411c6 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean @@ -371,21 +371,19 @@ variable [HasFresh Var] lemma subst_ty_lc (t_lc : t.LC) (δ_lc : δ.LC) (X : Var) : t[X := δ].LC := by induction t_lc - -- TODO: find a way to incorporate this into a tactic... - case abs => apply LC.abs (free_union Var) <;> grind [Ty.subst_lc, open_tm_subst_ty_var] - case tabs => apply LC.tabs (free_union Var) <;> grind [Ty.subst_lc, openRec_ty_subst_ty] - case let' => apply LC.let' (free_union Var) <;> grind [Ty.subst_lc, open_tm_subst_ty_var] - case case => apply LC.case (free_union Var) <;> grind [Ty.subst_lc, open_tm_subst_ty_var] - all_goals grind [Ty.subst_lc, open_tm_subst_ty_var] + case' abs => apply LC.abs (free_union Var) + case' tabs => apply LC.tabs (free_union Var) + case' let' => apply LC.let' (free_union Var) + case' case => apply LC.case (free_union Var) + all_goals grind [Ty.subst_lc, open_tm_subst_ty_var, openRec_ty_subst_ty] lemma subst_tm_lc (t_lc : t.LC) (s_lc : s.LC) (x : Var) : t[x := s].LC := by induction t_lc - -- TODO: find a way to incorporate this into a tactic... - case abs => apply LC.abs (free_union Var) <;> grind [open_tm_subst_tm_var] - case let' => apply LC.let' (free_union Var) <;> grind [open_tm_subst_tm_var] - case case => apply LC.case (free_union Var) <;> grind [open_tm_subst_tm_var] - case tabs => apply LC.tabs (free_union Var) <;> grind [open_ty_subst_tm_var] - all_goals grind + case' abs => apply LC.abs (free_union Var) + case' let' => apply LC.let' (free_union Var) + case' case => apply LC.case (free_union Var) + case' tabs => apply LC.tabs (free_union Var) + all_goals grind [open_tm_subst_tm_var, open_ty_subst_tm_var] end Term From 8e8f38e3c713ae41d6014ea4c4e745a6bc7ef2cd Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 24 Sep 2025 05:29:03 -0400 Subject: [PATCH 21/25] style --- .../LocallyNameless/Fsub/Reduction.lean | 1 - .../LocallyNameless/Fsub/Typing.lean | 36 ++++--------------- 2 files changed, 6 insertions(+), 31 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean index 9ed84695..7e955632 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean @@ -24,7 +24,6 @@ universe u variable {Var : Type u} - namespace LambdaCalculus.LocallyNameless.Fsub namespace Term diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index dbd33400..2271974f 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -61,36 +61,12 @@ attribute [grind] Typing.var Typing.app Typing.tapp Typing.sub Typing.inl Typing /-- Typings have well-formed contexts and types. -/ @[grind →] -lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : - Γ.Wf ∧ t.LC ∧ τ.Wf Γ := by - induction der - case tabs => - let ⟨X,mem⟩ := fresh_exists <| free_union Var - split_ands - · grind [cases Env.Wf] - · apply LC.tabs (free_union Var) <;> grind [cases Env.Wf] - · apply Ty.Wf.all (free_union Var) <;> grind [cases Env.Wf] - case abs σ Γ _ _ _ _ _ => - let ⟨X,_⟩ := fresh_exists <| free_union Var - split_ands - · grind [cases Env.Wf] - · apply LC.abs (free_union Var) <;> grind [cases Env.Wf] - · have eq : ⟨X, Binding.ty σ⟩ :: Γ = [] ++ [⟨X, Binding.ty σ⟩] ++ Γ := by rfl - grind [Ty.Wf.strengthen, cases Env.Wf] - case let' Γ _ σ _ _ _ _ _ _ _ => - let ⟨X,_⟩ := fresh_exists <| free_union Var - split_ands - · grind - · apply LC.let' (free_union Var) <;> grind - · have eq : ⟨X, Binding.ty σ⟩ :: Γ = [] ++ [⟨X, Binding.ty σ⟩] ++ Γ := by rfl - grind [Ty.Wf.strengthen] - case case Γ _ σ _ _ _ _ _ _ _ _ _ _ _ => - let ⟨X,_⟩ := fresh_exists <| free_union Var - split_ands - · grind - · apply LC.case (free_union Var) <;> grind - · have eq : ⟨X, Binding.ty σ⟩ :: Γ = [] ++ [⟨X, Binding.ty σ⟩] ++ Γ := by rfl - grind [Ty.Wf.strengthen] +lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : Γ.Wf ∧ t.LC ∧ τ.Wf Γ := by + induction der <;> let L := free_union Var <;> have := fresh_exists L + case tabs => refine ⟨?_, LC.tabs L ?_ ?_, Ty.Wf.all L ?_ ?_⟩ <;> grind [cases Env.Wf] + case abs => refine ⟨?_, LC.abs L ?_ ?_, ?_⟩ <;> grind [Wf.strengthen, cases Env.Wf] + case let' => refine ⟨?_, LC.let' L ?_ ?_, ?_⟩ <;> grind [Ty.Wf.strengthen] + case case => refine ⟨?_, LC.case L ?_ ?_ ?_, ?_⟩ <;> grind [Ty.Wf.strengthen] all_goals grind [of_bind_ty, open_lc, cases Env.Wf, cases Ty.Wf] /-- Weakening of typings. -/ From 7830a431d77e0c8feb0ecf3a55fefcbe703c2864 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Wed, 24 Sep 2025 05:33:32 -0400 Subject: [PATCH 22/25] prefer Type* --- .../LambdaCalculus/LocallyNameless/Fsub/Basic.lean | 10 +++++----- .../LambdaCalculus/LocallyNameless/Fsub/Opening.lean | 4 +--- .../LambdaCalculus/LocallyNameless/Fsub/Reduction.lean | 4 +--- .../LambdaCalculus/LocallyNameless/Fsub/Safety.lean | 4 +--- .../LambdaCalculus/LocallyNameless/Fsub/Subtype.lean | 4 +--- .../LambdaCalculus/LocallyNameless/Fsub/Typing.lean | 4 +--- .../LocallyNameless/Fsub/WellFormed.lean | 4 +--- 7 files changed, 11 insertions(+), 23 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean index 60b0c523..ce0770cb 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean @@ -20,12 +20,12 @@ The λ-calculus with polymorphism and subtyping, with a locally nameless represe -/ -variable {Var : Type u} [HasFresh Var] [DecidableEq Var] +variable {Var : Type*} [HasFresh Var] [DecidableEq Var] namespace LambdaCalculus.LocallyNameless.Fsub /-- Types of the polymorphic lambda calculus. -/ -inductive Ty (Var : Type u) +inductive Ty (Var : Type*) /-- The type ⊤, with a single inhabitant. -/ | top : Ty Var /-- Bound variables that appear in a type, using a de-Bruijn index. -/ @@ -41,7 +41,7 @@ inductive Ty (Var : Type u) deriving Inhabited /-- Syntax of locally nameless lambda terms, with free variables over `Var`. -/ -inductive Term (Var : Type u) +inductive Term (Var : Type*) /-- Bound term variables that appear under a lambda abstraction, using a de-Bruijn index. -/ | bvar : ℕ → Term Var /-- Free term variables. -/ @@ -64,7 +64,7 @@ inductive Term (Var : Type u) | case : Term Var → Term Var → Term Var → Term Var /-- A context binding. -/ -inductive Binding (Var : Type u) +inductive Binding (Var : Type*) /-- Subtype binding. -/ | sub : Ty Var → Binding Var /-- Type binding. -/ @@ -102,6 +102,6 @@ def Term.fv_tm : Term Var → Finset Var | case t₁ t₂ t₃ => t₁.fv_tm ∪ t₂.fv_tm ∪ t₃.fv_tm /-- A context of bindings. -/ -abbrev Env (Var : Type u) := Context Var (Binding Var) +abbrev Env (Var : Type*) := Context Var (Binding Var) end LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean index a09411c6..68bc3b69 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean @@ -20,9 +20,7 @@ This file defines opening, local closure, and substitution. -/ -universe u - -variable {Var : Type u} [HasFresh Var] [DecidableEq Var] +variable {Var : Type*} [HasFresh Var] [DecidableEq Var] namespace LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean index 7e955632..87e7a2ec 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean @@ -20,9 +20,7 @@ This file defines a call-by-value reduction. -/ -universe u - -variable {Var : Type u} +variable {Var : Type*} namespace LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean index 6302d667..27153349 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean @@ -20,9 +20,7 @@ This file proves type safety. -/ -universe u - -variable {Var : Type u} [HasFresh Var] [DecidableEq Var] +variable {Var : Type*} [HasFresh Var] [DecidableEq Var] namespace LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean index 3a76fc09..c52f39f7 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean @@ -19,9 +19,7 @@ This file defines the subtyping relation. -/ -universe u - -variable {Var : Type u} [DecidableEq Var] +variable {Var : Type*} [DecidableEq Var] namespace LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index 2271974f..408f29ae 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -21,9 +21,7 @@ This file defines the typing relation. -/ -universe u - -variable {Var : Type u} [DecidableEq Var] [HasFresh Var] +variable {Var : Type*} [DecidableEq Var] [HasFresh Var] namespace LambdaCalculus.LocallyNameless.Fsub diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index c41be4c9..1d435b8b 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -20,9 +20,7 @@ This file defines the well-formedness condition for types and contexts. -/ -universe u - -variable {Var : Type u} [DecidableEq Var] +variable {Var : Type*} [DecidableEq Var] namespace LambdaCalculus.LocallyNameless.Fsub From 2cd0e811fc2f463f5eb496819b6a9babe5ff5102 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Thu, 25 Sep 2025 06:09:42 -0400 Subject: [PATCH 23/25] docs typo --- Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index a024cfc4..a51d21a3 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -52,7 +52,7 @@ theorem sublist_dlookup (l₁ l₂ : List (Sigma β)) (nd₁ : l₁.NodupKeys) ( theorem perm_keys (h : Γ.Perm Δ) : x ∈ Γ.keys ↔ x ∈ Δ.keys := by induction h <;> grind [keys_cons] -/-- A key not appearing in an appending of list must appear in either list. -/ +/-- A key not appearing in an appending of list must not appear in either list. -/ theorem nmem_append_keys (l₁ l₂ : List (Sigma β)) : a ∉ (l₁ ++ l₂).keys ↔ a ∉ l₁.keys ∧ a ∉ l₂.keys := by constructor <;> ( From 8ad87b411cb9ba6efad309ad6191048114581fcc Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Thu, 25 Sep 2025 06:45:34 -0400 Subject: [PATCH 24/25] golfing --- .../LocallyNameless/Context.lean | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index a51d21a3..02a35c03 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -33,20 +33,11 @@ theorem keys_append : (Δ ++ Γ).keys = Δ.keys ++ Γ.keys := by /-- Sublists without duplicate keys preserve lookups. -/ theorem sublist_dlookup (l₁ l₂ : List (Sigma β)) (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) (s : l₁ <+ l₂) (mem : b ∈ l₁.dlookup a) : b ∈ l₂.dlookup a := by - induction s generalizing a b - case slnil => exact mem - case cons p' _ ih => - obtain ⟨a', b'⟩ := p' - have := ih nd₁ (by grind [nodupKeys_cons]) mem |> of_mem_dlookup |> mem_keys_of_mem - have : a ≠ a' := by grind [nodupKeys_cons] - simp_all - case cons₂ p' _ ih => - obtain ⟨a', b'⟩ := p' - by_cases h : a = a' - · subst h - rw [List.dlookup_cons_eq] at * - exact mem - · simp_all + induction s generalizing a b with + | slnil => exact mem + | cons p' | cons₂ p' => + by_cases a = p'.fst <;> + grind [dlookup_cons_eq, nodupKeys_cons, dlookup_cons_ne, → of_mem_dlookup, → mem_keys_of_mem] /-- List permutation preserves keys. -/ theorem perm_keys (h : Γ.Perm Δ) : x ∈ Γ.keys ↔ x ∈ Δ.keys := by From f5b426ea7c5ac582ac95c426f0155f6971513822 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Fri, 26 Sep 2025 13:20:51 -0400 Subject: [PATCH 25/25] naming convention, unused hypothesis --- .../LambdaCalculus/LocallyNameless/Context.lean | 12 ++++++------ .../LambdaCalculus/LocallyNameless/Fsub/Subtype.lean | 2 +- .../LambdaCalculus/LocallyNameless/Fsub/Typing.lean | 2 +- .../LocallyNameless/Fsub/WellFormed.lean | 2 +- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean index 02a35c03..921f4601 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean @@ -23,16 +23,16 @@ variable {α : Type u} {β : Type v} [DecidableEq α] -- `Mathlib.Data.List.Sigma`. We should consider upstreaming them to Mathlib. namespace List -variable {β : α → Type v} {Γ Δ : List (Sigma β)} +variable {β : α → Type v} {l₁ l₂ : List (Sigma β)} omit [DecidableEq α] in /-- Keys distribute with appending. -/ -theorem keys_append : (Δ ++ Γ).keys = Δ.keys ++ Γ.keys := by - induction Δ <;> simp_all +theorem keys_append : (l₁ ++ l₂).keys = l₁.keys ++ l₂.keys := by + induction l₁ <;> simp_all /-- Sublists without duplicate keys preserve lookups. -/ -theorem sublist_dlookup (l₁ l₂ : List (Sigma β)) (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) - (s : l₁ <+ l₂) (mem : b ∈ l₁.dlookup a) : b ∈ l₂.dlookup a := by +theorem sublist_dlookup (nd₂ : l₂.NodupKeys) (s : l₁ <+ l₂) (mem : b ∈ l₁.dlookup a) : + b ∈ l₂.dlookup a := by induction s generalizing a b with | slnil => exact mem | cons p' | cons₂ p' => @@ -40,7 +40,7 @@ theorem sublist_dlookup (l₁ l₂ : List (Sigma β)) (nd₁ : l₁.NodupKeys) ( grind [dlookup_cons_eq, nodupKeys_cons, dlookup_cons_ne, → of_mem_dlookup, → mem_keys_of_mem] /-- List permutation preserves keys. -/ -theorem perm_keys (h : Γ.Perm Δ) : x ∈ Γ.keys ↔ x ∈ Δ.keys := by +theorem perm_keys (h : l₁.Perm l₂) : x ∈ l₁.keys ↔ x ∈ l₂.keys := by induction h <;> grind [keys_cons] /-- A key not appearing in an appending of list must not appear in either list. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean index c52f39f7..ee85c728 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean @@ -67,7 +67,7 @@ lemma weaken (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ case all => subst eq apply all (free_union [Context.dom] Var) <;> grind [keys_append] - all_goals grind [Ty.Wf.weaken, sublist_dlookup] + all_goals grind [Ty.Wf.weaken, <= sublist_dlookup] lemma weaken_head (sub : Sub Δ σ σ') (wf : (Γ ++ Δ).Wf) : Sub (Γ ++ Δ) σ σ' := by have eq : Γ ++ Δ = [] ++ Γ ++ Δ := by grind diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean index 408f29ae..540c48ef 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean @@ -77,7 +77,7 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : case' let' der _ => apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) case' case der _ _ => apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq) all_goals - grind [Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, Sub.refl, sublist_dlookup] + grind [Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, Sub.refl, <= sublist_dlookup] /-- Weakening of typings (at the front). -/ lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) : diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean index 1d435b8b..841beee8 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean @@ -77,7 +77,7 @@ theorem weaken (wf_ΓΘ : σ.Wf (Γ ++ Θ)) (ok_ΓΔΘ : (Γ ++ Δ ++ Θ)✓) : generalize eq : Γ ++ Θ = ΓΔ at wf_ΓΘ induction wf_ΓΘ generalizing Γ case all => apply all ((Γ ++ Δ ++ Θ).dom ∪ free_union Var) <;> grind - all_goals grind [NodupKeys.sublist, sublist_dlookup] + all_goals grind [NodupKeys.sublist, <= sublist_dlookup] /-- A type remains well-formed under context weakening (at the front). -/ theorem weaken_head (wf : σ.Wf Δ) (ok : (Γ ++ Δ)✓) : σ.Wf (Γ ++ Δ) := by