Skip to content

Commit f5be8a8

Browse files
chenson2018chenson2018
authored
feat(Languages/LambdaCalculus/LocallyNameless): Fsub (#68)
* cleaning, docs * map_subst * rest of porting * rm weaken_head TODO * easy parts of preservation * some docs * more preservation * finish preservation * all but trans case of map_subst * easy weaken cases * half of the trans case * complete map_subst * type weakening * narrow * style * donegit st! * rm duplicated API * redundant lemma * large union trouble * old TODOs * style * prefer Type* * docs typo * golfing * naming convention, unused hypothesis * better proof of keys_append * redundant keys lemma * a few more unused context lemmas * style * better sublist_dlookup proof * better generality for nodupKeys_middle
1 parent 7e8f5f0 commit f5be8a8

File tree

9 files changed

+1461
-22
lines changed

9 files changed

+1461
-22
lines changed

‎Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean‎

Lines changed: 73 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -17,43 +17,96 @@ Contexts as pairs of free variables and types.
1717

1818
universe u v
1919

20-
variable {Var : Type u} {Ty : Type v} [DecidableEq Var]
20+
variable {α : Type u} {β : Type v}
21+
22+
-- TODO: These are pieces of API that cannot be directly automated by adding `grind` attributes to
23+
-- `Mathlib.Data.List.Sigma`. We should consider upstreaming them to Mathlib.
24+
namespace List
25+
26+
variable {β : α → Type v} {l₁ l₂ : List (Sigma β)}
27+
28+
/-- Keys distribute with appending. -/
29+
theorem keys_append : (l₁ ++ l₂).keys = l₁.keys ++ l₂.keys := by
30+
simp [keys]
31+
32+
variable [DecidableEq α] in
33+
/-- Sublists without duplicate keys preserve lookups. -/
34+
theorem sublist_dlookup (nd₂ : l₂.NodupKeys) (s : l₁ <+ l₂) (mem : b ∈ l₁.dlookup a) :
35+
b ∈ l₂.dlookup a := by
36+
grind [Option.mem_def, → perm_nodupKeys, dlookup_append, => perm_dlookup,
37+
→ Sublist.exists_perm_append]
38+
39+
@[grind =]
40+
lemma nodupKeys_middle : (l₁ ++ s :: l₂).NodupKeys ↔ (s :: (l₁ ++ l₂)).NodupKeys := by
41+
simp_all [NodupKeys, keys, nodup_middle]
42+
43+
end List
2144

2245
namespace LambdaCalculus.LocallyNameless
2346

47+
variable [DecidableEq α]
48+
2449
/-- A typing context is a list of free variables and corresponding types. -/
25-
abbrev Context (Var : Type u) (Ty : Type v) := List ((_ : Var) × Ty)
50+
abbrev Context (α : Type u) (β : Type v) := List ((_ : α) × β)
2651

2752
namespace Context
2853

2954
open List
3055

31-
/-- The domain of a context is the finite set of free variables it uses. -/
32-
@[simp, grind =]
33-
def dom : Context Var Ty → Finset Var := toFinset ∘ keys
56+
-- we would like grind to see through certain notations
57+
attribute [scoped grind =] Option.mem_def
58+
attribute [scoped grind _=_] List.append_eq
59+
attribute [scoped grind =] List.Nodup
60+
attribute [scoped grind =] List.NodupKeys
61+
attribute [scoped grind _=_] List.singleton_append
3462

35-
/-- A well-formed context. -/
36-
abbrev Ok : Context Var Ty → Prop := NodupKeys
63+
-- a few grinds on Option:
64+
attribute [scoped grind =] Option.or_eq_some_iff
65+
attribute [scoped grind =] Option.or_eq_none_iff
3766

38-
instance : HasWellFormed (Context Var Ty) :=
39-
⟨Ok⟩
67+
-- we would like grind to treat list and finset membership the same
68+
attribute [scoped grind _=_] List.mem_toFinset
4069

41-
variable {Γ Δ : Context Var Ty}
70+
-- otherwise, we mostly reuse existing API in `Mathlib.Data.List.Sigma`
71+
attribute [scoped grind =] List.keys_cons
72+
attribute [scoped grind =] List.dlookup_cons_eq
73+
attribute [scoped grind =] List.dlookup_cons_ne
74+
attribute [scoped grind =] List.dlookup_nil
75+
attribute [scoped grind _=_] List.dlookup_isSome
76+
attribute [scoped grind →] List.perm_nodupKeys
4277

43-
/-- Context membership is preserved on permuting a context. -/
44-
theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} : x ∈ Γ.dom ↔ x ∈ Δ.dom := by
45-
induction h <;> simp_all only [dom, Function.comp_apply, mem_toFinset, keys_cons, mem_cons]
46-
grind
78+
/-- The domain of a context is the finite set of free variables it uses. -/
79+
@[simp, grind =]
80+
def dom (Γ : Context α β) : Finset α := Γ.keys.toFinset
4781

48-
omit [DecidableEq Var] in
49-
/-- Context well-formedness is preserved on permuting a context. -/
50-
@[scoped grind →]
51-
theorem wf_perm (h : Γ.Perm Δ) : Γ✓ → Δ✓ := (List.perm_nodupKeys h).mp
82+
instance : HasWellFormed (Context α β) :=
83+
⟨NodupKeys⟩
84+
85+
omit [DecidableEq α] in
86+
@[scoped grind _=_]
87+
theorem haswellformed_def (Γ : Context α β) : Γ✓ = Γ.NodupKeys := by rfl
88+
89+
variable {Γ Δ : Context α β}
5290

53-
omit [DecidableEq Var] in
91+
omit [DecidableEq α] in
5492
/-- Context well-formedness is preserved on removing an element. -/
5593
@[scoped grind →]
5694
theorem wf_strengthen (ok : (Δ ++ ⟨x, σ⟩ :: Γ)✓) : (Δ ++ Γ)✓ := by
57-
exact List.NodupKeys.sublist (by simp) ok
95+
grind [keys_append]
96+
97+
/-- A mapping of values within a context. -/
98+
@[simp, scoped grind]
99+
def map_val (f : β → β) (Γ : Context α β) : Context α β :=
100+
Γ.map (fun ⟨var,ty⟩ => ⟨var,f ty⟩)
101+
102+
omit [DecidableEq α] in
103+
/-- A mapping of values preserves keys. -/
104+
@[scoped grind]
105+
lemma map_val_keys (f) : Γ.keys = (Γ.map_val f).keys := by
106+
induction Γ <;> grind
107+
108+
/-- A mapping of values maps lookups. -/
109+
lemma map_val_mem (mem : σ ∈ Γ.dlookup x) (f) : f σ ∈ (Γ.map_val f).dlookup x := by
110+
induction Γ <;> grind
58111

59112
end LambdaCalculus.LocallyNameless.Context

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

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
/-
2+
Copyright (c) 2025 Chris Henson. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Chris Henson
5+
-/
6+
7+
import Cslib.Foundations.Data.HasFresh
8+
import Cslib.Foundations.Syntax.HasSubstitution
9+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
10+
11+
/-! # λ-calculus
12+
13+
The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.
14+
15+
## References
16+
17+
* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
18+
* See also <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
19+
this is adapted
20+
21+
-/
22+
23+
variable {Var : Type*} [HasFresh Var] [DecidableEq Var]
24+
25+
namespace LambdaCalculus.LocallyNameless.Fsub
26+
27+
/-- Types of the polymorphic lambda calculus. -/
28+
inductive Ty (Var : Type*)
29+
/-- The type ⊤, with a single inhabitant. -/
30+
| top : Ty Var
31+
/-- Bound variables that appear in a type, using a de-Bruijn index. -/
32+
| bvar : ℕ → Ty Var
33+
/-- Free type variables. -/
34+
| fvar : Var → Ty Var
35+
/-- A function type. -/
36+
| arrow : Ty Var → Ty Var → Ty Var
37+
/-- A universal quantification. -/
38+
| all : Ty Var → Ty Var → Ty Var
39+
/-- A sum type. -/
40+
| sum : Ty Var → Ty Var → Ty Var
41+
deriving Inhabited
42+
43+
/-- Syntax of locally nameless lambda terms, with free variables over `Var`. -/
44+
inductive Term (Var : Type*)
45+
/-- Bound term variables that appear under a lambda abstraction, using a de-Bruijn index. -/
46+
| bvar : ℕ → Term Var
47+
/-- Free term variables. -/
48+
| fvar : Var → Term Var
49+
/-- Lambda abstraction, introducing a new bound term variable. -/
50+
| abs : Ty Var → Term Var → Term Var
51+
/-- Function application. -/
52+
| app : Term Var → Term Var → Term Var
53+
/-- Type abstraction, introducing a new bound type variable. -/
54+
| tabs : Ty Var → Term Var → Term Var
55+
/-- Type application. -/
56+
| tapp : Term Var → Ty Var → Term Var
57+
/-- Binding of a term. -/
58+
| let' : Term Var → Term Var → Term Var
59+
/-- Left constructor of a sum. -/
60+
| inl : Term Var → Term Var
61+
/-- Right constructor of a sum. -/
62+
| inr : Term Var → Term Var
63+
/-- Case matching on a sum. -/
64+
| case : Term Var → Term Var → Term Var → Term Var
65+
66+
/-- A context binding. -/
67+
inductive Binding (Var : Type*)
68+
/-- Subtype binding. -/
69+
| sub : Ty Var → Binding Var
70+
/-- Type binding. -/
71+
| ty : Ty Var → Binding Var
72+
deriving Inhabited
73+
74+
/-- Free variables of a type. -/
75+
@[scoped grind =]
76+
def Ty.fv : Ty Var → Finset Var
77+
| top | bvar _ => {}
78+
| fvar X => {X}
79+
| arrow σ τ | all σ τ | sum σ τ => σ.fv ∪ τ.fv
80+
81+
/-- Free variables of a binding. -/
82+
@[scoped grind =]
83+
def Binding.fv : Binding Var → Finset Var
84+
| sub σ | ty σ => σ.fv
85+
86+
/-- Free type variables of a term. -/
87+
@[scoped grind =]
88+
def Term.fv_ty : Term Var → Finset Var
89+
| bvar _ | fvar _ => {}
90+
| abs σ t₁ | tabs σ t₁ | tapp t₁ σ => σ.fv ∪ t₁.fv_ty
91+
| inl t₁ | inr t₁ => t₁.fv_ty
92+
| app t₁ t₂ | let' t₁ t₂ => t₁.fv_ty ∪ t₂.fv_ty
93+
| case t₁ t₂ t₃ => t₁.fv_ty ∪ t₂.fv_ty ∪ t₃.fv_ty
94+
95+
/-- Free term variables of a term. -/
96+
@[scoped grind =]
97+
def Term.fv_tm : Term Var → Finset Var
98+
| bvar _ => {}
99+
| fvar x => {x}
100+
| abs _ t₁ | tabs _ t₁ | tapp t₁ _ | inl t₁ | inr t₁ => t₁.fv_tm
101+
| app t₁ t₂ | let' t₁ t₂ => t₁.fv_tm ∪ t₂.fv_tm
102+
| case t₁ t₂ t₃ => t₁.fv_tm ∪ t₂.fv_tm ∪ t₃.fv_tm
103+
104+
/-- A context of bindings. -/
105+
abbrev Env (Var : Type*) := Context Var (Binding Var)
106+
107+
end LambdaCalculus.LocallyNameless.Fsub

0 commit comments

Comments
 (0)