Skip to content

Commit fc7a8df

Browse files
amarmadukeamarmaduke
committed
fill in some SNi proofs
1 parent 7dae6dc commit fc7a8df

1 file changed

Lines changed: 86 additions & 181 deletions

File tree

‎LeanStlc/SNi.lean‎

Lines changed: 86 additions & 181 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,8 @@ namespace SN
9494
subst zdef
9595
apply ih (:λ[A] y) (Red.lam r) rfl
9696

97+
theorem succ : SN Red t <-> SN Red t.succ := by sorry
98+
9799
theorem neutral_app {f a} : Neutral f -> SN Red f -> SN Red a -> SN Red (f :@ a) := by
98100
intro h1 h2 h3
99101
induction h2 generalizing a
@@ -110,6 +112,27 @@ namespace SN
110112
case _ a' r =>
111113
apply ih3 a' r
112114

115+
theorem neutral_nrec :
116+
Neutral n ->
117+
SN Red z ->
118+
SN Red s ->
119+
SN Red n ->
120+
SN Red (Term.nrec A z s n)
121+
:= by
122+
intro nh j1 j2 j3
123+
induction j3 generalizing z s; case _ n h1 ih1 =>
124+
induction j2 generalizing z; case _ s h2 ih2 =>
125+
induction j1; case _ z h3 ih3 =>
126+
apply SN.sn; case _ =>
127+
intro y r; cases r
128+
case nrec_zero => cases nh
129+
case nrec_succ => cases nh
130+
case nrec1 z' r => apply ih3 _ r
131+
case nrec2 s' r => apply ih2 _ r (.sn h3)
132+
case nrec3 n' r =>
133+
apply ih1 _ r _ (.sn h3) (.sn h2)
134+
apply Red.preservation_of_neutral_step nh r
135+
113136
theorem weak_head_expansion {t b A}
114137
: SN Red t -> SN Red (b[.su t::+0]) -> SN Red ((:λ[A] b) :@ t)
115138
:= by
@@ -195,54 +218,6 @@ mutual
195218
| step_nrec : SnRed n n' -> SnRed (.nrec A z s n) (.nrec A z s n')
196219
end
197220

198-
inductive SnVariant where
199-
| neu | nor | red
200-
201-
@[simp]
202-
abbrev SnIndices : SnVariant -> Type
203-
| .neu => Term
204-
| .nor => Term
205-
| .red => (Term) × (Term)
206-
207-
inductive SNi : (v : SnVariant) -> SnIndices v -> Prop where
208-
| var {x} : SNi .neu (.var x)
209-
| app {s t} :
210-
SNi .neu s ->
211-
SNi .nor t ->
212-
SNi .neu (s :@ t)
213-
| lam {t A} :
214-
SNi .nor t ->
215-
SNi .nor (:λ[A] t)
216-
| zero : SNi .nor .zero
217-
| succ :
218-
SNi .nor t ->
219-
SNi .nor t.succ
220-
| nrec :
221-
SNi .neu t ->
222-
SNi .nor z ->
223-
SNi .nor s ->
224-
SNi .neu (.nrec A z s t)
225-
| neu {t} :
226-
SNi .neu t ->
227-
SNi .nor t
228-
| red {t t'} :
229-
SNi .red (t, t') ->
230-
SNi .nor t' ->
231-
SNi .nor t
232-
| beta {t A b} :
233-
SNi .nor t ->
234-
SNi .red ((:λ[A] b) :@ t, b[.su t :: +0])
235-
| nrec_zero :
236-
SNi .red (.nrec A z s .zero, z)
237-
| nrec_succ :
238-
SNi .red (.nrec A z s t.succ, s :@ (.nrec A z s t))
239-
| step_nrec :
240-
SNi .red (t, t') ->
241-
SNi .red (.nrec A z s t, .nrec A z s t')
242-
| step_app {s s' t} :
243-
SNi .red (s, s') ->
244-
SNi .red (s :@ t, s' :@ t)
245-
246221
mutual
247222
def SnNor.rename (r : Ren) : SnNor t -> SnNor t[r]
248223
| @SnNor.lam t _ th =>
@@ -279,33 +254,71 @@ mutual
279254
def SnRed.antirename (r : Ren) : SnRed t t' -> ∀ z, t = z[r] -> ∃ z', t' = z'[r] ∧ SnRed z z' := sorry
280255
end
281256

282-
mutual
283-
def SnNor.beta_var : SnNor s -> ∀ t x, s = t :@ .var x -> SnNor t := sorry
284-
285-
def SnNeu.beta_var : SnNeu s -> ∀ t x, s = t :@ .var x -> SnNeu t := sorry
286-
end
287-
288-
mutual
289-
def SnNeu.weaken : SnNeu t -> Neutral t := sorry
290-
291-
def SnRed.weaken : SnRed t t' -> t ~> t' := sorry
292-
end
257+
def SnNeu.beta_var : SnNeu s -> s = t :@ .var x -> SnNeu t
258+
| .app f a, e => by grind
259+
260+
theorem SnNor.beta_var : ∀ {s}, SnNor s -> ∀ {t x}, s = t :@ .var x -> SnNor t := by
261+
intro s sn
262+
apply SnNor.brecOn
263+
(motive_1 := λ s sn => ∀ {t x}, s = t :@ .var x -> SnNor t)
264+
(motive_2 := λ _ _ => True)
265+
(motive_3 := λ _ _ _ => True)
266+
sn
267+
case _ =>
268+
intro s sn ih t x e
269+
cases ih; all_goals try solve | injection e
270+
case neu sn _ =>
271+
apply SnNor.neu
272+
apply SnNeu.beta_var sn e
273+
case red t' t'n _ t'nb ih r rb =>
274+
subst e; cases rb
275+
case beta b _ _ ih2 =>
276+
apply SnNor.lam
277+
let r : Ren := x :: id
278+
have lem : b[.su #x :: +0] = b[r] := by
279+
subst r; rw [ren_subst_apply_eq]
280+
intro i y h
281+
cases i <;> simp at *
282+
case zero => exact h
283+
case _ z => exact h
284+
rw [lem] at t'n
285+
apply SnNor.antirename r t'n b rfl
286+
case step_app s' _ r rb =>
287+
apply SnNor.red r
288+
apply ih rfl
289+
all_goals simp
290+
291+
def SnNeu.weaken : SnNeu t -> Neutral t
292+
| .var => .var
293+
| .app f a => .app f.weaken
294+
| .nrec _ _ n => .nrec n.weaken
295+
296+
def SnRed.weaken : SnRed t t' -> t ~> t'
297+
| .beta t => .beta
298+
| .zero => .nrec_zero
299+
| .succ => .nrec_succ
300+
| .step_app r => .app1 r.weaken
301+
| .step_nrec r => .nrec3 r.weaken
293302

294303
mutual
295-
def SnNor.sound : SnNor t -> SN Red t := sorry
296-
297-
def SnNeu.sound : SnNeu t -> SN Red t := sorry
298-
299-
def SnRed.sound : SnRed t t' -> t ~>sn t' := sorry
300-
end
301-
302-
mutual
303-
def SnRed.expansion (j : Γ ⊢ t' : A) : SnRed t t' -> Γ ⊢ t : A
304-
| .beta t => sorry
305-
| .zero => sorry
306-
| .succ => sorry
307-
| .step_app r => sorry
308-
| .step_nrec r => sorry
304+
def SnNor.sound : SnNor t -> SN Red t
305+
| .lam h => SN.lam.1 h.sound
306+
| .zero => SN.sn (by grind)
307+
| .succ h => SN.succ.1 h.sound
308+
| .neu h => h.sound
309+
| .red r h => SN.backward_closure h.sound r.sound
310+
311+
def SnNeu.sound : SnNeu t -> SN Red t
312+
| .var => SN.sn (by grind)
313+
| .app s t => SN.neutral_app s.weaken s.sound t.sound
314+
| .nrec z s n => SN.neutral_nrec n.weaken z.sound s.sound n.sound
315+
316+
def SnRed.sound : SnRed t t' -> t ~>sn t'
317+
| .beta h => .beta h.sound
318+
| .zero => .zero
319+
| .succ => .succ
320+
| .step_app h => .app _ h.sound
321+
| .step_nrec h => .nrec h.sound
309322
end
310323

311324
namespace SNi
@@ -382,112 +395,4 @@ namespace SNi
382395
-- exists (z' :@ v); simp [*]
383396
-- apply SNi.step (h'.2)
384397

385-
-- @[simp]
386-
-- abbrev SnBetaVarLemmaType : (v : SnVariant) -> (i : SnIndices v) -> Prop
387-
-- | .neu, s => ∀ t x, s = t :@ .var x -> SNi .neu t
388-
-- | .nor, s => ∀ t x, s = t :@ .var x -> SNi .nor t
389-
-- | .red, _ => True
390-
391-
-- theorem beta_var {v i} : SNi v i -> SnBetaVarLemmaType v i := by
392-
-- intro j; induction j <;> simp at *
393-
-- case app s t j1 j2 ih1 ih2 =>
394-
-- intro u x e1 e2; subst e1; subst e2
395-
-- apply j1
396-
-- case neu t j ih =>
397-
-- intro u x e
398-
-- cases t <;> simp at e
399-
-- case _ v w =>
400-
-- cases e; case _ e1 e2 =>
401-
-- subst e1; subst e2
402-
-- cases j; case _ j1 j2 =>
403-
-- apply SNi.neu j1
404-
-- case red t t' j1 j2 ih1 ih2 =>
405-
-- intro u x e
406-
-- cases t <;> simp at e
407-
-- case _ v w =>
408-
-- cases e; case _ e1 e2 =>
409-
-- subst e1; subst e2
410-
-- cases j1
411-
-- case beta A b j1 =>
412-
-- let r : Ren := x :: id
413-
-- have lem : b[.su (.var x) :: +0] = b[r] := by
414-
-- subst r; rw [ren_subst_apply_eq]
415-
-- intro i y h
416-
-- cases i <;> simp at *
417-
-- case zero => exact h
418-
-- case _ z => exact h
419-
-- rw [lem] at j2
420-
-- apply SNi.lam
421-
-- apply @antirename .nor (b[r]) r j2
422-
-- rfl
423-
-- case step s' j1 =>
424-
-- replace ih2 := ih2 s' x rfl
425-
-- apply SNi.red j1 ih2
426-
427-
-- @[simp]
428-
-- abbrev SnPropertyWeakenLemmaType : (v : SnVariant) -> (i : SnIndices v) -> Prop
429-
-- | .neu, s => Neutral s
430-
-- | .nor, _ => True
431-
-- | .red, (s, t) => s ~> t
432-
433-
-- theorem property_weaken {v i} : SNi v i -> SnPropertyWeakenLemmaType v i := by
434-
-- intro h
435-
-- induction h <;> simp at *
436-
-- case _ => apply Neutral.var
437-
-- case _ ih _ => apply Neutral.app ih
438-
-- case _ => apply Red.beta
439-
-- case _ ih => apply Red.app1 ih
440-
441-
-- @[simp]
442-
-- abbrev SnSoundLemmaType : (v : SnVariant) -> (i : SnIndices v) -> Prop
443-
-- | .neu, s => SN Red s
444-
-- | .nor, s => SN Red s
445-
-- | .red, (s, t) => s ~>sn t
446-
447-
-- theorem sound {v i} : SNi v i -> SnSoundLemmaType v i := by
448-
-- intro h; induction h <;> simp at *
449-
-- case _ => apply SN.sn; intro y r; cases r
450-
-- case _ s t j1 j2 ih1 ih2 =>
451-
-- have lem := property_weaken j1; simp at lem
452-
-- apply SN.neutral_app lem ih1 ih2
453-
-- case _ t A j ih => apply SN.lam.1 ih
454-
-- case _ t j ih => apply ih
455-
-- case _ ih1 ih2 => apply SN.backward_closure ih2 ih1
456-
-- case _ ih => apply SnHeadRed.beta ih
457-
-- case _ ih => apply SnHeadRed.app _ ih
458-
459-
-- -- TODO: prove completeness
460-
-- theorem complete {t} : (SN Red t -> SNi .nor t) ∧ (∀ t', t ~>sn t' -> SNi .red (t, t')) := by
461-
-- induction t
462-
-- case _ x =>
463-
-- apply And.intro
464-
-- intro h; apply SNi.neu (SNi.var)
465-
-- intro t' h; cases h
466-
-- case _ f a ih1 ih2 =>
467-
-- apply And.intro
468-
-- case _ =>
469-
-- intro h
470-
-- have lem1 := sn_subterm_app h
471-
-- have lem2 := ih1.1 lem1.1
472-
-- cases lem2
473-
-- case _ j =>
474-
-- sorry
475-
-- case _ h => apply SNi.neu (SNi.app h (ih2.1 lem1.2))
476-
-- case _ t' j1 j2 =>
477-
-- have lem : SNi .red (f :@ a, t' :@ a) := by sorry
478-
-- apply SNi.red lem
479-
-- sorry
480-
-- case _ =>
481-
-- intro t' r; cases r
482-
-- case _ A b h =>
483-
-- apply SNi.beta
484-
-- apply ih2.1 h
485-
-- case _ f' r =>
486-
-- apply SNi.step
487-
-- apply ih1.2 f' r
488-
-- case _ A t ih =>
489-
-- apply And.intro
490-
-- intro h; apply SNi.lam
491-
-- apply ih.1 (sn_lam.2 h)
492-
-- intro t' r; cases r
493398
end SNi

0 commit comments

Comments
 (0)