Skip to content

Commit 2ff3359

Browse files
WegmannDavidWegmannDavid
committed
split over multiple files, without forgetting MultiSubst.lean
1 parent 0602c7e commit 2ff3359

2 files changed

Lines changed: 142 additions & 137 deletions

File tree

‎Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean‎

Lines changed: 11 additions & 137 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
55
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
66
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
77
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
8+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
89

910
namespace Cslib
1011

@@ -21,114 +22,6 @@ open scoped Term
2122

2223

2324

24-
abbrev Environment (Var : Type u) := Context Var (Term Var)
25-
26-
def multiSubst (σ : Environment Var) (M : Term Var) : Term Var :=
27-
match σ with
28-
| [] => M
29-
| ⟨ i, sub ⟩ :: σ' => (multiSubst σ' M) [ i := sub ]
30-
31-
def fv (Ns : Environment Var) : Finset Var :=
32-
match Ns with
33-
| [] => {}
34-
| ⟨ _, sub ⟩ :: Ns' => sub.fv ∪ fv Ns'
35-
36-
@[simp]
37-
def context_LC (Γ : Environment Var) : Prop :=
38-
∀ {x M}, ⟨ x, M ⟩ ∈ Γ → LC M
39-
40-
lemma context_LC_cons {Γ : Environment Var} {x : Var} {sub : Term Var} :
41-
LC sub → context_LC Γ → context_LC (⟨ x, sub ⟩ :: Γ) := by
42-
intro lc_sub lc_Γ y σ h_mem
43-
cases h_mem
44-
· assumption
45-
· apply lc_Γ
46-
assumption
47-
48-
49-
50-
def multiSubst_fvar_fresh (Ns : Environment Var) :
51-
∀ x ∉ Ns.dom, multiSubst Ns (Term.fvar x) = Term.fvar x := by
52-
induction Ns <;> intro x h_fresh
53-
· case nil =>
54-
simp [multiSubst]
55-
· case cons N Ns ih =>
56-
simp only [multiSubst]
57-
simp only [Context.dom] at h_fresh
58-
rw[ih]
59-
· rw[subst_fvar]
60-
by_cases h : N.1 = x <;> simp_all
61-
· simp_all
62-
63-
lemma multiSubst_preserves_not_fvar {x : Var}
64-
(M : Term Var)
65-
(Ns : Environment Var)
66-
(nmem : x ∉ M.fv ∪ fv Ns) :
67-
x ∉ (multiSubst Ns M).fv := by
68-
induction Ns
69-
· case nil =>
70-
rw[multiSubst]
71-
simp_all
72-
· case cons N Ns ih =>
73-
rw[multiSubst]
74-
apply subst_preserve_not_fvar
75-
rw[fv] at nmem
76-
simp_all
77-
78-
79-
80-
def multiSubst_app (M N : Term Var) (Ps : Environment Var) :
81-
multiSubst Ps (Term.app M N) = Term.app (multiSubst Ps M) (multiSubst Ps N) := by
82-
induction Ps
83-
· rfl
84-
· case cons N Ns ih => rw[multiSubst,multiSubst,ih]; rfl
85-
86-
def multiSubst_abs (M : Term Var) (Ns : Environment Var) :
87-
multiSubst Ns (Term.abs M) =
88-
Term.abs (multiSubst Ns M) := by
89-
induction Ns
90-
· rfl
91-
· case cons N Ns ih => rw[multiSubst, ih]; rfl
92-
93-
lemma open'_fvar_subst (M N : Term Var) (x : Var) (H : x ∉ Term.fv M) :
94-
(i : Nat) → (M ⟦ i ↝ Term.fvar x ⟧) [x := N] = M ⟦ i ↝ N ⟧ := by
95-
induction M <;> intro i
96-
· case bvar j =>
97-
rw[Term.openRec_bvar, Term.openRec_bvar]
98-
by_cases h : i = j <;> simp[h, Term.subst_fvar, Term.subst_bvar]
99-
· case fvar y =>
100-
rw[Term.openRec_fvar, Term.openRec_fvar]
101-
simp only [Term.fv, Finset.mem_singleton] at H
102-
simp only [subst_fvar, ite_eq_right_iff]
103-
intro H
104-
contradiction
105-
· case abs M ih =>
106-
rw[Term.openRec_abs, Term.openRec_abs]
107-
rw[Term.subst_abs]
108-
rw[ih H]
109-
· case app l r ih_l ih_r =>
110-
rw[Term.openRec_app, Term.openRec_app]
111-
rw[Term.subst_app]
112-
simp only [Term.fv, Finset.mem_union, not_or] at H
113-
rw[ih_l H.1]
114-
rw[ih_r H.2]
115-
116-
117-
lemma multiSubst_open_var (M : Term Var) (Ns : Environment Var) (x : Var) :
118-
x ∉ Ns.dom →
119-
context_LC Ns →
120-
(multiSubst Ns (M ^ (Term.fvar x))) =
121-
(multiSubst Ns M) ^ (Term.fvar x) := by
122-
intro h_ndom h_lc
123-
induction Ns with
124-
| nil => rfl
125-
| cons N Ns ih =>
126-
rw[multiSubst, multiSubst]
127-
rw[ih]
128-
· rw[subst_open_var] <;> aesop
129-
· simp_all
130-
aesop
131-
13225
inductive saturated (S : Set (Term Var)) : Prop :=
13326
| intro : (∀ M ∈ S, LC M) →
13427
(∀ M ∈ S, SN M) →
@@ -144,17 +37,6 @@ def semanticMap (τ : Ty Base) : Set (Term Var) :=
14437
| Ty.arrow τ₁ τ₂ =>
14538
{ t : Term Var | ∀ s : Term Var, s ∈ semanticMap τ₁ → (Term.app t s) ∈ semanticMap τ₂ }
14639

147-
lemma multiApp_lc : ∀ {M P : Term Var} {Ns : List (Term Var)},
148-
LC (multiApp M Ns) → (LC M → LC P) → LC (multiApp P Ns) := by
149-
intro N P Ns
150-
induction Ns <;> intro lc_Ns lc_P
151-
· simp_all[multiApp]
152-
· case cons a l ih =>
153-
rw[multiApp]
154-
rw[multiApp] at lc_Ns
155-
cases lc_Ns
156-
grind
157-
15840

15941

16042
def semanticMap_saturated (τ : Ty Base) :
@@ -168,13 +50,9 @@ def semanticMap_saturated (τ : Ty Base) :
16850
· intro M N P lc_N sn_N h_app
16951
constructor
17052
· simp_all[multiApp_sn]
171-
· apply multiApp_lc
172-
· apply h_app.2
173-
· intro Hlc
174-
constructor
175-
· apply open_abs_lc
176-
assumption
177-
· assumption
53+
· have H := h_app.2
54+
rw[multiApp_lc] at *
55+
grind[open_abs_lc]
17856
· case arrow τ₁ τ₂ ih₁ ih₂ =>
17957
constructor
18058
· intro M hM
@@ -210,7 +88,7 @@ def semanticMap_saturated (τ : Ty Base) :
21088

21189

21290

213-
def entails_context (Ns : Context Var (Term Var)) (Γ : Context Var (Ty Base)) :=
91+
def entails_context (Ns : Term.Environment Var) (Γ : Context Var (Ty Base)) :=
21492
∀ {x τ}, ⟨ x, τ ⟩ ∈ Γ → (multiSubst Ns (Term.fvar x)) ∈ semanticMap τ
21593

21694
lemma entails_context_empty {Γ : Context Var (Ty Base)} :
@@ -220,9 +98,9 @@ lemma entails_context_empty {Γ : Context Var (Ty Base)} :
22098
apply (semanticMap_saturated τ).3 <;> constructor
22199

222100

223-
lemma entails_context_cons (Ns : Context Var (Term Var)) (Γ : Context Var (Ty Base))
101+
lemma entails_context_cons (Ns : Term.Environment Var) (Γ : Context Var (Ty Base))
224102
(x : Var) (τ : Ty Base) (sub : Term Var) :
225-
x ∉ Ns.dom ∪ fv Ns ∪ Γ.dom →
103+
x ∉ Ns.dom ∪ Ns.fv ∪ Γ.dom →
226104
sub ∈ semanticMap τ →
227105
entails_context Ns Γ → entails_context (⟨ x, sub ⟩ :: Ns) (⟨ x, τ ⟩ :: Γ) := by
228106
intro h_fresh h_mem h_entails y σ h_mem
@@ -243,12 +121,8 @@ lemma entails_context_cons (Ns : Context Var (Term Var)) (Γ : Context Var (Ty B
243121
aesop
244122

245123

246-
247-
248124
def entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) :=
249-
∀ Ns, context_LC Ns → (entails_context Ns Γ) → (multiSubst Ns t) ∈ semanticMap τ
250-
251-
125+
∀ Ns, env_LC Ns → (entails_context Ns Γ) → (multiSubst Ns t) ∈ semanticMap τ
252126

253127

254128
theorem soundness {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} :
@@ -267,15 +141,15 @@ theorem soundness {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} :
267141
· apply (semanticMap_saturated _).2
268142
assumption
269143
· rw[multiApp]
270-
set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ ∪ (multiSubst Ns t).fv)
271-
have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ fv Ns ∪ Context.dom Γ ∪ (multiSubst Ns t).fv := by apply fresh_notMem
144+
set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ Ns.fv ∪ Context.dom Γ ∪ (multiSubst Ns t).fv)
145+
have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ Ns.fv ∪ Context.dom Γ ∪ (multiSubst Ns t).fv := by apply fresh_notMem
272146
have hfreshL : x ∉ L := by simp_all
273147
have H1 := derivation_t x hfreshL
274148
rw[entails] at H1
275149
specialize H1 (⟨x,s⟩ :: Ns)
276150
rw [multiSubst, multiSubst_open_var, ←subst_intro] at H1
277151
· apply H1
278-
· apply context_LC_cons
152+
· apply env_LC_cons
279153
· apply (semanticMap_saturated _).1
280154
assumption
281155
· assumption

‎Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean‎

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
module
2+
3+
public import Cslib.Foundations.Data.Relation
4+
public import Cslib.Foundations.Data.HasFresh
5+
public import Cslib.Foundations.Syntax.HasSubstitution
6+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
7+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
8+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
9+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
10+
11+
@[expose] public section
12+
13+
namespace Cslib
14+
15+
universe u v
16+
17+
18+
namespace LambdaCalculus.LocallyNameless.Untyped.Term
19+
20+
variable {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var]
21+
22+
23+
abbrev Environment (Var : Type u) := Context Var (Term Var)
24+
25+
def multiSubst (σ : Environment Var) (M : Term Var) : Term Var :=
26+
match σ with
27+
| [] => M
28+
| ⟨ i, sub ⟩ :: σ' => (multiSubst σ' M) [ i := sub ]
29+
30+
def Environment.fv (Ns : Environment Var) : Finset Var :=
31+
match Ns with
32+
| [] => {}
33+
| ⟨ _, sub ⟩ :: Ns' => sub.fv ∪ fv Ns'
34+
35+
36+
@[simp]
37+
def env_LC (Γ : Environment Var) : Prop :=
38+
∀ {x M}, ⟨ x, M ⟩ ∈ Γ → LC M
39+
40+
lemma env_LC_cons {Γ : Environment Var} {x : Var} {sub : Term Var} :
41+
LC sub → env_LC Γ → env_LC (⟨ x, sub ⟩ :: Γ) := by
42+
intro lc_sub lc_Γ y σ h_mem
43+
cases h_mem
44+
· assumption
45+
· apply lc_Γ
46+
assumption
47+
48+
49+
50+
def multiSubst_fvar_fresh (Ns : Environment Var) :
51+
∀ x ∉ Ns.dom, multiSubst Ns (Term.fvar x) = Term.fvar x := by
52+
induction Ns <;> intro x h_fresh
53+
· case nil =>
54+
simp [multiSubst]
55+
· case cons N Ns ih =>
56+
simp only [multiSubst]
57+
simp only [Context.dom] at h_fresh
58+
rw[ih]
59+
· rw[subst_fvar]
60+
by_cases h : N.1 = x <;> simp_all
61+
· simp_all
62+
63+
lemma multiSubst_preserves_not_fvar {x : Var}
64+
(M : Term Var)
65+
(Ns : Environment Var)
66+
(nmem : x ∉ M.fv ∪ Ns.fv) :
67+
x ∉ (multiSubst Ns M).fv := by
68+
induction Ns
69+
· case nil =>
70+
rw[multiSubst]
71+
simp_all
72+
· case cons N Ns ih =>
73+
rw[multiSubst]
74+
apply subst_preserve_not_fvar
75+
rw[Environment.fv] at nmem
76+
simp_all
77+
78+
def multiSubst_app (M N : Term Var) (Ps : Environment Var) :
79+
multiSubst Ps (Term.app M N) = Term.app (multiSubst Ps M) (multiSubst Ps N) := by
80+
induction Ps
81+
· rfl
82+
· case cons N Ns ih => rw[multiSubst, multiSubst, ih]; rfl
83+
84+
def multiSubst_abs (M : Term Var) (Ns : Environment Var) :
85+
multiSubst Ns (Term.abs M) =
86+
Term.abs (multiSubst Ns M) := by
87+
induction Ns
88+
· rfl
89+
· case cons N Ns ih => rw[multiSubst, ih]; rfl
90+
91+
lemma open'_fvar_subst (M N : Term Var) (x : Var) (H : x ∉ Term.fv M) :
92+
(i : Nat) → (M ⟦ i ↝ Term.fvar x ⟧) [x := N] = M ⟦ i ↝ N ⟧ := by
93+
induction M <;> intro i
94+
· case bvar j =>
95+
rw[Term.openRec_bvar, Term.openRec_bvar]
96+
by_cases h : i = j <;> simp[h, Term.subst_fvar, Term.subst_bvar]
97+
· case fvar y =>
98+
rw[Term.openRec_fvar, Term.openRec_fvar]
99+
simp only [Term.fv, Finset.mem_singleton] at H
100+
simp only [subst_fvar, ite_eq_right_iff]
101+
intro H
102+
contradiction
103+
· case abs M ih =>
104+
rw[Term.openRec_abs, Term.openRec_abs]
105+
rw[Term.subst_abs]
106+
rw[ih H]
107+
· case app l r ih_l ih_r =>
108+
rw[Term.openRec_app, Term.openRec_app]
109+
rw[Term.subst_app]
110+
simp only [Term.fv, Finset.mem_union, not_or] at H
111+
rw[ih_l H.1]
112+
rw[ih_r H.2]
113+
114+
lemma multiSubst_open_var (M : Term Var) (Ns : Environment Var) (x : Var) :
115+
x ∉ Ns.dom →
116+
env_LC Ns →
117+
(multiSubst Ns (M ^ (Term.fvar x))) =
118+
(multiSubst Ns M) ^ (Term.fvar x) := by
119+
intro h_ndom h_lc
120+
induction Ns with
121+
| nil => rfl
122+
| cons N Ns ih =>
123+
rw[multiSubst, multiSubst]
124+
rw[ih]
125+
· rw[subst_open_var] <;> aesop
126+
· simp_all
127+
aesop
128+
129+
end LambdaCalculus.LocallyNameless.Untyped.Term
130+
131+
end Cslib

0 commit comments

Comments
 (0)