Skip to content

Commit 9f2a9bd

Browse files
amarmadukeamarmaduke
committed
system f with basic metatheory
1 parent 9809178 commit 9f2a9bd

16 files changed

Lines changed: 939 additions & 537 deletions

‎LeanSysF/CtxWf.lean‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
2+
import LeanSubst
3+
import LeanSysF.Term
4+
import LeanSysF.Kinding
5+
6+
open LeanSubst
7+
8+
inductive CtxWf : Ctx Term -> Prop where
9+
| nil : CtxWf []
10+
| cons :
11+
Γ ⊢ A type ->
12+
CtxWf Γ ->
13+
CtxWf (A::Γ)
14+
15+
notation:170 "⊢ " Γ:170 => CtxWf Γ

‎LeanSysF/FreeVar.lean‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
2+
import LeanSubst
3+
import LeanSysF.Utility
4+
import LeanSysF.Term
5+
6+
open LeanSubst
7+
8+
inductive FV : Term -> Nat -> Prop
9+
| var : FV #x x
10+
| ctor {i : Fin v.arity} {ts : Fin v.arity -> Term} : FV (ts i) x -> FV (.ctor v ts) x
11+
| bind1 {i : Fin v.arity} {ts : Fin v.arity -> Term} : FV (ts i) x -> FV (.bind v ts t) x
12+
| bind2 : FV t (x + 1) -> FV (.bind v ts t) x
13+
14+
instance : Membership Nat Term where
15+
mem := FV
16+
17+
theorem FV.found : x ∈ #x := by simp [Membership.mem]; apply FV.var
18+
19+
@[simp]
20+
theorem FV.ctor_inj : x ∈ (Term.ctor v ts) <-> ∃ i, x ∈ (ts i) := by
21+
apply Iff.intro
22+
case _ =>
23+
intro h; simp [Membership.mem] at *
24+
cases h; case _ i h =>
25+
exists i
26+
case _ =>
27+
intro h; simp [Membership.mem] at *
28+
cases h; case _ i h =>
29+
apply FV.ctor h
30+
31+
@[simp]
32+
theorem FV.bind_inj : x ∈ (Term.bind v ts t) <-> (∃ i, x ∈ (ts i)) ∨ x + 1 ∈ t := by
33+
apply Iff.intro
34+
case _ =>
35+
intro h; cases h
36+
case _ i h => apply Or.inl; exists i
37+
case _ h => apply Or.inr; apply h
38+
case _ =>
39+
intro h; cases h
40+
case _ h =>
41+
cases h; case _ i h =>
42+
apply FV.bind1 h
43+
case _ h => apply FV.bind2 h
44+
45+
theorem lift_iterated_succ_is_re
46+
: ((Subst.lift (T := Term))^[n]) +1 y = z -> ∃ i, z = re i
47+
:= by
48+
intro h
49+
induction n generalizing y z
50+
case zero =>
51+
simp at h; cases z
52+
case _ i =>
53+
injection h with e; subst e
54+
exists (y + 1)
55+
case _ t => injection h
56+
case succ n ih =>
57+
simp at h
58+
cases y <;> simp at h
59+
case zero => exists 0; subst h; rfl
60+
case succ y =>
61+
unfold Subst.compose at h; simp at h
62+
generalize udef : ((Subst.lift (T := Term))^[n]) +1 y = u at *
63+
cases u <;> simp at *
64+
case _ i => exists (i + 1); subst h; rfl
65+
case _ t =>
66+
replace ih := @ih y; cases ih; case _ i ih =>
67+
rw [ih] at udef; injection udef
68+
69+
theorem FV.var_not_in_one_more {t : Term} : ¬ (x ∈ t[((Subst.lift)^[x]) +1]) := by
70+
intro h
71+
induction t generalizing x <;> simp at *
72+
case var y =>
73+
induction x generalizing y <;> simp at *
74+
case _ => cases h
75+
case _ n ih =>
76+
cases y <;> simp at *
77+
case _ => cases h
78+
case _ y =>
79+
unfold Subst.compose at h; simp at h
80+
generalize zdef : (((Subst.lift (T := Term))^[n]) +1 y) = z at *
81+
cases z <;> simp at *
82+
case _ z =>
83+
replace ih := ih y
84+
cases h; rw [zdef] at ih; simp at ih
85+
apply ih; apply FV.var
86+
case _ t =>
87+
have lem := lift_iterated_succ_is_re zdef
88+
cases lem; case _ i lem =>
89+
injection lem
90+
case bind v ts t ih1 ih2 =>
91+
cases h
92+
case _ h =>
93+
cases h; case _ i h =>
94+
replace ih1 := @ih1 i x
95+
apply ih1 h
96+
case _ h =>
97+
replace ih2 := @ih2 (x + 1); simp at ih2
98+
apply ih2 h
99+
case ctor v ts ih =>
100+
cases h; case _ i h =>
101+
apply ih i h
102+
103+
theorem FV.zero_not_in_succ {t : Term} : ¬ (0 ∈ t[+1]) := by
104+
intro j
105+
have lem := @var_not_in_one_more 0 t; simp at lem
106+
apply lem j

‎LeanSysF/Kinding.lean‎

Lines changed: 187 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
1+
2+
import LeanSubst
3+
import LeanSysF.Term
4+
import LeanSysF.FreeVar
5+
6+
open LeanSubst
7+
8+
inductive Kinding : Ctx Term -> Term -> Prop where
9+
| var {Γ : Ctx Term} {x} :
10+
Γ[x] = ★ ->
11+
Kinding Γ #x
12+
| arr {Γ A B} :
13+
Kinding Γ A ->
14+
Kinding Γ B ->
15+
Kinding Γ (A -:> B)
16+
| all {Γ P} :
17+
Kinding (★::Γ) P ->
18+
Kinding Γ (:∀ P)
19+
20+
notation:170 Γ:170 " ⊢ " A:170 " type" => Kinding Γ A
21+
22+
theorem Ctx.strong_rename_lift {A : Term} {Δ Γ : Ctx Term} {r : Ren} B :
23+
(∀ x T, x + 1 ∈ A -> Γ[x] = T -> Δ[r x] = T[r]) ->
24+
∀ x T, x ∈ A -> (B::Γ)[x] = T -> (B[r]::Δ)[r.lift x] = T[r.lift]
25+
:= by
26+
intro h1 x T h2 h3
27+
cases x <;> simp at *
28+
case zero =>
29+
subst h3; simp [Ren.lift]
30+
rw [Ren.to_lift]; simp
31+
case succ x =>
32+
replace h1 := h1 x h2
33+
subst h3; simp [Ren.lift]
34+
rw [Ren.to_lift]; rw [h1]; simp
35+
36+
theorem Ctx.rename_lift {Δ Γ : Ctx Term} {r : Ren} B :
37+
(∀ x T, Γ[x] = T -> Δ[r x] = T[r]) ->
38+
∀ x T, (B::Γ)[x] = T -> (B[r]::Δ)[r.lift x] = T[r.lift]
39+
:= by
40+
intro h1 x T h3
41+
cases x <;> simp at *
42+
case zero =>
43+
subst h3; simp [Ren.lift]
44+
rw [Ren.to_lift]; simp
45+
case succ x =>
46+
replace h1 := h1 x
47+
subst h3; simp [Ren.lift]
48+
rw [Ren.to_lift]; rw [h1]; simp
49+
50+
theorem Ctx.subst_re_lift {Γ Δ : Ctx Term} A {σ : Subst Term} :
51+
(∀ x T y, Γ[x] = T -> σ x = re y -> Δ[y] = T[σ]) ->
52+
∀ x T y, (A::Γ)[x] = T -> σ.lift x = re y -> (A[σ]::Δ)[y] = T[σ.lift]
53+
:= by
54+
intro h1 x T y h2 h3
55+
cases x <;> simp at *
56+
case zero => subst h2; subst h3; simp
57+
case succ x =>
58+
simp [Subst.compose] at h3
59+
generalize zdef : σ x = z at *
60+
cases z <;> simp at h3
61+
case _ z =>
62+
subst h3
63+
replace h1 := h1 x Γ[x] z rfl zdef
64+
subst h2; simp; rw [h1]; simp
65+
66+
theorem Kinding.strong_rename {Γ A} (Δ : Ctx Term) (r : Ren) :
67+
Γ ⊢ A type ->
68+
(∀ x T, x ∈ A -> Γ[x] = T -> Δ[r x] = T[r]) ->
69+
Δ ⊢ A[r] type
70+
:= by
71+
intro j h
72+
induction j generalizing Δ r
73+
case var Γ x j =>
74+
replace h := h x ★ FV.found j; simp at h
75+
simp; apply Kinding.var h
76+
case arr Γ A B j1 j2 ih1 ih2 =>
77+
have h1 := λ x T (e : x ∈ A) => h x T (by simp; apply Or.inl e)
78+
have h2 := λ x T (e : x ∈ B) => h x T (by simp; apply Or.inr e)
79+
simp; apply Kinding.arr
80+
apply ih1 Δ r h1
81+
apply ih2 Δ r h2
82+
case all Γ P j ih =>
83+
have h2 : ∀ x T, x + 1 ∈ P -> Γ[x] = T -> Δ[r x] = T[r] := by
84+
intro x T q1 q2; simp at h
85+
replace h := h x q1; subst q2
86+
apply h
87+
simp; apply Kinding.all
88+
have lem1 := Ctx.strong_rename_lift ★ h2; simp at lem1
89+
have lem2 := ih (★::Δ) r.lift; simp at lem2
90+
replace lem2 := lem2 lem1
91+
rw [Ren.to_lift] at lem2; simp at lem2; exact lem2
92+
93+
theorem Kinding.rename {Γ A} (Δ : Ctx Term) (r : Ren) :
94+
Γ ⊢ A type ->
95+
(∀ x T, Γ[x] = T -> Δ[r x] = T[r]) ->
96+
Δ ⊢ A[r] type
97+
:= by
98+
intro j h
99+
apply strong_rename _ _ j _
100+
intro x T h1 h2
101+
apply h x T h2
102+
103+
theorem Kinding.weaken : Γ ⊢ A type -> (P::Γ) ⊢ A[+1] type := by
104+
intro j
105+
have lem := rename (P::Γ) (· + 1) j
106+
simp at lem; exact lem
107+
108+
theorem Kinding.strengthen : (P::Γ) ⊢ A[+1] type -> Γ ⊢ A type := by
109+
intro j
110+
have lem := strong_rename Γ (· - 1) j (by {
111+
intro x T h1 h2
112+
cases x <;> simp at *
113+
case zero => exfalso; apply FV.zero_not_in_succ h1
114+
case succ x => subst h2; simp
115+
})
116+
simp at lem; apply lem
117+
118+
theorem Kinding.subst_lift {Γ Δ : Ctx Term} A {σ : Subst Term} :
119+
(∀ x t, Γ[x] = ★ -> σ x = su t -> Δ ⊢ t type) ->
120+
∀ x t, (A::Γ)[x] = ★ -> σ.lift x = su t -> (A[σ]::Δ) ⊢ t type
121+
:= by
122+
intro h1 x t h2 h3
123+
cases x <;> simp at *
124+
case _ x =>
125+
replace h2 := Term.ren_eq_star h2
126+
simp [Subst.compose] at h3
127+
generalize zdef : σ x = z at *
128+
cases z <;> simp at *
129+
case _ s =>
130+
subst h3
131+
replace h1 := h1 x s h2 zdef
132+
have lem := rename (A[σ]::Δ) (· + 1) h1
133+
simp at lem; exact lem
134+
135+
theorem Kinding.subst {Γ A} (Δ : Ctx Term) (σ : Subst Term) :
136+
Γ ⊢ A type ->
137+
(∀ x T y, Γ[x] = T -> σ x = re y -> Δ[y] = T[σ]) ->
138+
(∀ x t, Γ[x] = ★ -> σ x = su t -> Δ ⊢ t type) ->
139+
Δ ⊢ A[σ] type
140+
:= by
141+
intro j h1 h2
142+
induction j generalizing Δ σ
143+
case var Γ x j =>
144+
simp; generalize zdef : σ x = z at *
145+
cases z <;> simp at *
146+
case _ y =>
147+
apply Kinding.var
148+
have lem := h1 x ★ y j zdef; simp at lem
149+
exact lem
150+
case _ t => apply h2 x t j zdef
151+
case arr Γ A B j1 j2 ih1 ih2 =>
152+
simp; apply Kinding.arr
153+
apply ih1 Δ σ h1 h2
154+
apply ih2 Δ σ h1 h2
155+
case all Γ P j ih =>
156+
-- TODO: Why does Lean unfold Subst.lift?
157+
have lem0 : ★[σ] = ★ := by simp
158+
have lem1 := Ctx.subst_re_lift ★ h1; rw [lem0] at lem1
159+
have lem2 := Kinding.subst_lift ★ h2; rw [lem0] at lem2
160+
simp; apply Kinding.all
161+
have lem3 := ih (★::Δ) σ.lift lem1 lem2; simp at lem3
162+
exact lem3
163+
164+
theorem Kinding.beta : (A::Γ) ⊢ P type -> Γ ⊢ B type -> Γ ⊢ P[su B::+0] type := by
165+
intro j1 j2
166+
apply subst Γ (su B::+0) j1
167+
case _ =>
168+
intro x T y h1 h2
169+
cases x <;> simp at *
170+
case _ n => subst h1; subst h2; simp
171+
case _ =>
172+
intro x t h1 h2
173+
cases x <;> simp at *
174+
case zero =>
175+
replace h1 := Term.ren_eq_star h1
176+
subst h1; subst h2; apply j2
177+
178+
theorem Kinding.injection_arrow : Γ ⊢ (A -:> B) type -> Γ ⊢ A type ∧ Γ ⊢ B type := by
179+
intro j; generalize zdef : A -:> B = z at *
180+
cases j; all_goals injection zdef
181+
case arr A' B' j1 j2 e1 e2 =>
182+
have lem1 : ∀ x, (λ i => mk2 A B i) x = (λ i => mk2 A' B' i) x := by
183+
intro x; rw [e2]
184+
have lem2 := lem1 0; simp [mk2] at lem2
185+
have lem3 := lem1 1; simp [mk2] at lem3
186+
subst lem2; subst lem3
187+
apply And.intro j1 j2

0 commit comments

Comments
 (0)