Locally nameless Fsub

Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean

@@ -17,43 +17,135 @@ 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} {l₁ l₂ : List (Sigma β)}
+
+omit [DecidableEq α] in
+/-- Keys distribute with appending. -/
+theorem keys_append : (l₁ ++ l₂).keys = l₁.keys ++ l₂.keys := by
+  induction l₁ <;> simp_all
+
+/-- Sublists without duplicate keys preserve lookups. -/
+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' =>
+    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 : 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. -/
+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]
+  )
+
+/-- 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
+  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
 
 /-- 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
 
-/-- 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
+-- 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 well-formed context. -/
-abbrev Ok : Context Var Ty → Prop := NodupKeys
+-- a few grinds on Option:
+attribute [scoped grind =] Option.or_eq_some_iff
+attribute [scoped grind =] Option.or_eq_none_iff
 
-instance : HasWellFormed (Context Var Ty) :=
-  ⟨Ok⟩
+-- we would like grind to treat list and finset membership the same
+attribute [scoped grind _=_] List.mem_toFinset
 
-variable {Γ Δ : Context Var Ty}
+-- 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
+attribute [scoped grind →] List.perm_nodupKeys
 
-/-- 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] 
-  grind
+/-- The domain of a context is the finite set of free variables it uses. -/
+@[simp, grind =]
+def dom (Γ : Context α β) : Finset α := Γ.keys.toFinset
 
-omit [DecidableEq Var] in
-/-- Context well-formedness is preserved on permuting a context. -/
-@[scoped grind →]
-theorem wf_perm (h : Γ.Perm Δ) : Γ✓ → Δ✓ := (List.perm_nodupKeys h).mp
+instance : HasWellFormed (Context α β) :=
+  ⟨NodupKeys⟩
+
+omit [DecidableEq α] in
+@[scoped grind _=_]
+theorem haswellformed_def (Γ : Context α β) : Γ✓ = Γ.NodupKeys := by rfl
 
-omit [DecidableEq Var] in
+variable {Γ Δ : Context α β}
+
+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]
+
+/-- 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))✓ := by grind
+    grind [List.nodupKeys_cons, nmem_append_keys]
+
 end LambdaCalculus.LocallyNameless.Context

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean

@@ -0,0 +1,107 @@
+/-
+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 <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
+  this is adapted
+
+-/
+
+variable {Var : Type*} [HasFresh Var] [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Fsub
+
+/-- Types of the polymorphic lambda calculus. -/
+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. -/
+  | 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*)
+  /-- 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. -/
+  | 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*)
+  /-- 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*) := Context Var (Binding Var)
+
+end LambdaCalculus.LocallyNameless.Fsub