Skip to content

Commit 6e127b2

Browse files
amarmadukeamarmaduke
committed
refactor proofs to agda-style
1 parent 284bc73 commit 6e127b2

5 files changed

Lines changed: 451 additions & 416 deletions

File tree

‎LeanStlc/Reduction.lean‎

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -524,16 +524,12 @@ namespace Red
524524
instance : HasConfluence Red where
525525
confluence := confluence
526526

527-
theorem preservation_of_neutral_step : Neutral t -> t ~> t' -> Neutral t' := by
528-
sorry
529-
-- intro h r
530-
-- induction h generalizing t'
531-
-- case _ => cases r
532-
-- case _ f a h ih =>
533-
-- cases r
534-
-- case _ => cases h
535-
-- case _ f' r => apply Neutral.app (ih r)
536-
-- case _ a' r => apply Neutral.app h
527+
theorem preservation_of_neutral_step : Neutral t -> t ~> t' -> Neutral t'
528+
| .app fn, .app1 r => .app (preservation_of_neutral_step fn r)
529+
| .app fn, .app2 r => .app fn
530+
| .nrec nn, .nrec1 r => .nrec nn
531+
| .nrec nn, .nrec2 r => .nrec nn
532+
| .nrec nn, .nrec3 r => .nrec (preservation_of_neutral_step nn r)
537533

538534
theorem preservation_of_neutral : Neutral t -> t ~>* t' -> Neutral t' := by
539535
intro h r

‎LeanStlc/SN.lean‎

Lines changed: 306 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,306 @@
1+
import LeanSubst
2+
import LeanStlc.Reduction
3+
4+
open LeanSubst
5+
6+
inductive SnHeadRed : Term -> Term -> Prop where
7+
| beta {t A b} : SN Red t -> SnHeadRed ((:λ[A] b) :@ t) (b[.su t::+0])
8+
| zero : SN Red s -> SnHeadRed (.nrec A z s .zero) z
9+
| succ : SnHeadRed (.nrec A z s (.succ n)) (s :@ (.nrec A z s n))
10+
| nrec : SnHeadRed n n' -> SnHeadRed (.nrec A z s n) (.nrec A z s n')
11+
| app {f f'} a : SnHeadRed f f' -> SnHeadRed (f :@ a) (f' :@ a)
12+
13+
infix:80 " ~>sn " => SnHeadRed
14+
15+
def SnHeadRed.red_compatible {t a b} : t ~>sn a -> t ~> b -> a = b ∨ ∃ z, b ~>sn z ∧ a ~>* z
16+
| .beta t, .beta => .inl rfl
17+
| .beta tn, .app1 (.lam r) => .inr ⟨_, .beta tn, .subst _ (.step .refl r)⟩
18+
| .beta (t := t) tn, .app2 (a' := a) r =>
19+
let h : ∀ (x : Nat), ActionRed Red ((su t :: +0) x) ((su a :: +0) x)
20+
| 0 => .su r
21+
| x + 1 => .re
22+
.inr ⟨_, .beta (.preservation_step tn r), Red.subst_arg h⟩
23+
| .zero _, .nrec_zero => .inl rfl
24+
| .zero sn, .nrec1 r => .inr ⟨_, .zero sn, .step .refl r⟩
25+
| .zero sn, .nrec2 r => .inr ⟨_, .zero (sn.preservation_step r), .refl⟩
26+
| .succ, .nrec_succ => .inl rfl
27+
| .succ, .nrec1 r => .inr ⟨_, .succ, .step .refl (.app2 $ .nrec1 r)⟩
28+
| .succ, .nrec2 r =>
29+
let r1 := Star.step .refl r
30+
let r2 := Star.step .refl (.nrec2 r)
31+
.inr ⟨_, .succ, .congr2 Term.app .app1 .app2 r1 r2⟩
32+
| .succ, .nrec3 (.succ r) => .inr ⟨_, .succ, .step .refl (.app2 $ .nrec3 r)⟩
33+
| .nrec r, .nrec1 r2 => .inr ⟨_, .nrec r, .step .refl $ .nrec1 r2⟩
34+
| .nrec r, .nrec2 r2 => .inr ⟨_, .nrec r, .step .refl $ .nrec2 r2⟩
35+
| .nrec r, .nrec3 r2 =>
36+
match red_compatible r r2 with
37+
| .inl ih => .inl (by grind)
38+
| .inr ⟨z, ih1, ih2⟩ => .inr ⟨_, .nrec ih1, .congr3_3 _ _ (.nrec _) .nrec3 ih2⟩
39+
| .app a r, .app1 r2 =>
40+
match red_compatible r r2 with
41+
| .inl ih => .inl (by grind)
42+
| .inr ⟨z, ih1, ih2⟩ =>
43+
.inr ⟨z :@ a, .app a ih1, .congr2_1 a .app .app1 ih2⟩
44+
| .app (f' := f') a r, .app2 (a' := a') r2 =>
45+
.inr ⟨f' :@ a', .app a' r, .congr2_2 f' .app .app2 (.step .refl r2)⟩
46+
47+
namespace SN
48+
theorem subterm_app {f a} : SN Red (f :@ a) -> SN Red f ∧ SN Red a := by
49+
intro h
50+
generalize zdef : f :@ a = z at *
51+
induction h generalizing f a
52+
case _ x h ih =>
53+
apply And.intro
54+
case _ =>
55+
apply SN.sn; intro y r
56+
subst zdef
57+
replace ih := ih (y :@ a) (Red.app1 r) rfl
58+
apply ih.1
59+
case _ =>
60+
apply SN.sn; intro y r
61+
subst zdef
62+
replace ih := ih (f :@ y) (Red.app2 r) rfl
63+
apply ih.2
64+
65+
theorem subterm_nrec : SN Red (.nrec A z s n) -> SN Red z ∧ SN Red s ∧ SN Red n := by
66+
intro j; generalize wdef : Term.nrec A z s n = w at j
67+
induction j generalizing z s n; case _ w h ih =>
68+
subst wdef; apply And.intro _; apply And.intro
69+
case _ =>
70+
apply SN.sn; intro s' r
71+
replace ih := ih (.nrec A z s' n) (Red.nrec2 r) rfl
72+
apply ih.2.1
73+
case _ =>
74+
apply SN.sn; intro n' r
75+
replace ih := ih (.nrec A z s n') (Red.nrec3 r) rfl
76+
apply ih.2.2
77+
case _ =>
78+
apply SN.sn; intro z' r
79+
replace ih := ih (.nrec A z' s n) (Red.nrec1 r) rfl
80+
apply ih.1
81+
82+
theorem lam {t A} : SN Red t <-> SN Red (:λ[A] t) := by
83+
apply Iff.intro
84+
case _ =>
85+
intro h; induction h
86+
case _ t h ih =>
87+
apply SN.sn; intro y r
88+
cases r; case _ t' r =>
89+
apply ih _ r
90+
case _ =>
91+
intro h
92+
generalize zdef : (:λ[A] t) = z at *
93+
induction h generalizing t
94+
case _ x h ih =>
95+
apply SN.sn; intro y r
96+
subst zdef
97+
apply ih (:λ[A] y) (Red.lam r) rfl
98+
99+
theorem succ : SN Red t <-> SN Red t.succ := by
100+
apply Iff.intro
101+
case _ =>
102+
intro h; induction h
103+
case _ t h ih =>
104+
apply SN.sn; intro y r
105+
cases r; case _ t' r =>
106+
apply ih _ r
107+
case _ =>
108+
intro h
109+
generalize zdef : t.succ = z at *
110+
induction h generalizing t
111+
case _ x h ih =>
112+
apply SN.sn; intro y r
113+
subst zdef
114+
apply ih y.succ (Red.succ r) rfl
115+
116+
theorem neutral_app {f a} : Neutral f -> SN Red f -> SN Red a -> SN Red (f :@ a) := by
117+
intro h1 h2 h3
118+
induction h2 generalizing a
119+
case _ f h2 ih2 =>
120+
induction h3
121+
case _ a h3 ih3 =>
122+
apply SN.sn; intro y r
123+
cases r
124+
case _ => cases h1
125+
case _ f' r =>
126+
have lem1 := Red.preservation_of_neutral_step h1 r
127+
have lem2 : SN Red a := SN.sn h3
128+
apply ih2 f' r lem1 lem2
129+
case _ a' r =>
130+
apply ih3 a' r
131+
132+
theorem neutral_nrec :
133+
Neutral n ->
134+
SN Red z ->
135+
SN Red s ->
136+
SN Red n ->
137+
SN Red (Term.nrec A z s n)
138+
:= by
139+
intro nh j1 j2 j3
140+
induction j3 generalizing z s; case _ n h1 ih1 =>
141+
induction j2 generalizing z; case _ s h2 ih2 =>
142+
induction j1; case _ z h3 ih3 =>
143+
apply SN.sn; case _ =>
144+
intro y r; cases r
145+
case nrec_zero => cases nh
146+
case nrec_succ => cases nh
147+
case nrec1 z' r => apply ih3 _ r
148+
case nrec2 s' r => apply ih2 _ r (.sn h3)
149+
case nrec3 n' r =>
150+
apply ih1 _ r _ (.sn h3) (.sn h2)
151+
apply Red.preservation_of_neutral_step nh r
152+
153+
theorem weak_head_expansion {t b A} :
154+
SN Red t ->
155+
SN Red (b[.su t::+0]) ->
156+
SN Red ((:λ[A] b) :@ t)
157+
:= by
158+
intro h1; induction h1 generalizing b
159+
case _ t h1 ih1 =>
160+
intro h2
161+
generalize zdef : b[.su t :: +0] = z at *
162+
induction h2 generalizing b
163+
case _ w h2 ih2 =>
164+
apply SN.sn; intro y r
165+
cases r
166+
case _ => rw [zdef]; apply SN.sn h2
167+
case _ q r =>
168+
cases r; case _ b' r =>
169+
have lem : b[.su t::+0] ~> b'[.su t::+0] := by
170+
apply Red.subst (.su t::+0) r
171+
apply ih2 (b'[.su t::+0]) (by rw [<-zdef]; apply lem) rfl
172+
case _ t' r =>
173+
have lem1 : SN Red w := SN.sn h2; rw [<-zdef] at lem1
174+
have lem2 : b[.su t::+0] ~>* b[.su t'::+0] := by
175+
apply Red.subst_arg; intro x
176+
cases x <;> simp at *
177+
apply ActionRed.su r
178+
apply ActionRed.re
179+
have lem3 := SN.preservation lem1 lem2
180+
apply ih1 t' r lem3
181+
182+
theorem zero_expansion : SN Red s -> SN Red z -> SN Red (.nrec A z s .zero) := by
183+
intro h1 h2
184+
induction h2 generalizing s; case _ z hz ihz =>
185+
induction h1; case _ s hs ihs =>
186+
apply SN.sn; case _ =>
187+
intro y r; cases r
188+
case nrec_zero => apply SN.sn hz
189+
case nrec1 z' r =>
190+
apply ihz _ r
191+
apply SN.sn hs
192+
case nrec2 s' r => apply ihs _ r
193+
case nrec3 n' r => cases r
194+
195+
theorem succ_expansion :
196+
SN Red (s :@ .nrec A z s n) ->
197+
SN Red z ->
198+
SN Red s ->
199+
SN Red n ->
200+
SN Red (.nrec A z s n.succ)
201+
:= by
202+
intro h j1 j2 j3
203+
induction j3 generalizing z s; case _ n j3 ih3 =>
204+
induction j2 generalizing z; case _ s j2 ih2 =>
205+
induction j1; case _ z j1 ih1 =>
206+
apply SN.sn; case _ =>
207+
intro y r; cases r
208+
case nrec_succ n => exact h
209+
case nrec1 z' r =>
210+
apply ih1 _ r
211+
apply SN.preservation_step h
212+
apply Red.app2
213+
apply Red.nrec1 r
214+
case nrec2 s' r =>
215+
apply ih2 _ r
216+
apply SN.preservation h
217+
apply Star.congr2 Term.app Red.app1 Red.app2
218+
apply Star.step .refl r
219+
apply Star.step .refl
220+
apply Red.nrec2 r
221+
apply SN.sn j1
222+
case nrec3 n' r =>
223+
cases r; case _ n' r =>
224+
apply ih3 _ r _ (SN.sn j1) (SN.sn j2)
225+
apply SN.preservation_step h
226+
apply Red.app2
227+
apply Red.nrec3 r
228+
229+
theorem backward_closure_app :
230+
f ~>sn f' ->
231+
SN Red f ->
232+
SN Red a ->
233+
SN Red (f' :@ a) ->
234+
SN Red (f :@ a)
235+
:= by
236+
intro r1 h1 h2 h3
237+
induction h1 generalizing f' a
238+
case _ f h1 ih1 =>
239+
induction h2
240+
case _ a h2 ih2 =>
241+
apply SN.sn; intro y r2
242+
cases r2
243+
case _ => cases r1
244+
case _ f'' r =>
245+
have lem1 := SnHeadRed.red_compatible r1 r
246+
cases lem1
247+
case _ lem1 => subst lem1; apply h3
248+
case _ lem1 =>
249+
cases lem1; case _ z lem1 =>
250+
apply ih1 f'' r lem1.1 (SN.sn h2)
251+
apply SN.preservation h3
252+
apply Star.congr2_1 a Term.app Red.app1 lem1.2
253+
case _ a'' r =>
254+
apply ih2 a'' r
255+
apply SN.preservation h3
256+
apply Star.congr2_2 f' Term.app Red.app2 (Star.step Star.refl r)
257+
258+
theorem backward_closure_nrec :
259+
n ~>sn n' ->
260+
SN Red z ->
261+
SN Red s ->
262+
SN Red n ->
263+
SN Red (.nrec A z s n') ->
264+
SN Red (.nrec A z s n)
265+
:= by
266+
intro r1 h1 h2 h3 h4
267+
induction h3 generalizing z s n'; case _ n hn ihn =>
268+
induction h2 generalizing z; case _ s hs ihs =>
269+
induction h1; case _ z hz ihz =>
270+
apply SN.sn; intro y r2; case _ =>
271+
cases r2
272+
case nrec_zero => cases r1
273+
case nrec_succ => cases r1
274+
case nrec1 z' r =>
275+
apply ihz z' r
276+
apply SN.preservation_step h4
277+
apply Red.nrec1 r
278+
case nrec2 s' r =>
279+
apply ihs s' r (SN.sn hz)
280+
apply SN.preservation_step h4
281+
apply Red.nrec2 r
282+
case nrec3 n'' r =>
283+
have lem1 := SnHeadRed.red_compatible r1 r
284+
cases lem1
285+
case _ lem1 => subst lem1; exact h4
286+
case _ lem1 =>
287+
obtain ⟨w, lem1, lem2⟩ := lem1
288+
apply ihn n'' r lem1 (SN.sn hz) (SN.sn hs)
289+
apply SN.preservation h4
290+
apply Star.congr3_3 _ _ (Term.nrec _) Red.nrec3 lem2
291+
292+
theorem backward_closure {t' t} : SN Red t' -> t ~>sn t' -> SN Red t := by
293+
intro h r; induction r
294+
case beta h2 => apply weak_head_expansion h2 h
295+
case app r ih =>
296+
have lem := subterm_app h
297+
apply backward_closure_app r (ih lem.1) lem.2 h
298+
case zero h2 => apply zero_expansion h2 h
299+
case succ =>
300+
obtain ⟨h1, h2⟩ := subterm_app h
301+
obtain ⟨h3, h4, h5⟩ := subterm_nrec h2
302+
apply succ_expansion h h3 h4 h5
303+
case nrec r ih =>
304+
obtain ⟨h1, h2, h3⟩ := subterm_nrec h
305+
apply backward_closure_nrec r h1 h2 (ih h3) h
306+
end SN

0 commit comments

Comments
 (0)