OAI/Computability/TypeSystem/Reduction.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.PureTypeSystem.Parallel line 10

   Source documentation

   Parallel reduction is used only to establish the beta metatheory.

   inductive Parallel {S : Type u} : Expr S → Expr S → Prop
     | var (n) : Parallel (.var n) (.var n)
     | sort (s) : Parallel (.sort s) (.sort s)
     | app {f f' a a'} : Parallel f f' → Parallel a a' →
         Parallel (.app f a) (.app f' a')
     | lam {A A' b b'} : Parallel A A' → Parallel b b' →
         Parallel (.lam A b) (.lam A' b')
     | pi {A A' B B'} : Parallel A A' → Parallel B B' →
         Parallel (.pi A B) (.pi A' B')
     | head {b b' a a'} (A) : Parallel b b' → Parallel a a' →
         Parallel (.app (.lam A b) a) (b'.instantiate a')
   …

   Mentions: OAI.PureTypeSystem.Expr

2. theorem OAI.PureTypeSystem.Parallel.refl line 26
3. theorem OAI.PureTypeSystem.Parallel.of_beta line 34
4. theorem OAI.PureTypeSystem.Parallel.rename line 44
5. theorem OAI.PureTypeSystem.Parallel.subst line 56
6. theorem OAI.PureTypeSystem.Parallel.instantiate line 74
7. def OAI.PureTypeSystem.Expr.develop line 89

   Source documentation

   Takahashi's complete development, including type annotations.

   def develop : Expr S → Expr S
     | var n => var n
     | sort s => sort s
     | app (lam _ b) a => (develop b).instantiate (develop a)
     | app f a => app (develop f) (develop a)
     | lam A b => lam (develop A) (develop b)
     | pi A B => pi (develop A) (develop B)
   
   end Expr
   
   namespace Parallel
   …

   Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Expr.instantiate, OAI.PureTypeSystem.Parallel

8. theorem OAI.PureTypeSystem.Parallel.triangle line 103
9. theorem OAI.PureTypeSystem.Parallel.diamond line 122
10. abbrev OAI.PureTypeSystem.Reduces line 127
11. theorem OAI.PureTypeSystem.Reduces.app line 133
12. theorem OAI.PureTypeSystem.Reduces.lam line 138
13. theorem OAI.PureTypeSystem.Reduces.pi line 143
14. theorem OAI.PureTypeSystem.Reduces.rename line 148
15. theorem OAI.PureTypeSystem.Reduces.subst line 151
16. theorem OAI.PureTypeSystem.Parallel.reduces line 160
17. theorem OAI.PureTypeSystem.Parallel.rtc_reduces line 170
18. theorem OAI.PureTypeSystem.Reduces.parallel line 179
19. theorem OAI.PureTypeSystem.Reduces.confluent line 182
20. theorem OAI.PureTypeSystem.Converts.join line 198
21. theorem OAI.PureTypeSystem.Normal.reduces_eq line 217
22. theorem OAI.PureTypeSystem.Normal.eq_of_converts line 222
23. theorem OAI.PureTypeSystem.Reduces.pi_inv line 232
24. theorem OAI.PureTypeSystem.Reduces.converts line 242
25. theorem OAI.PureTypeSystem.Converts.product_compatibility line 251
26. theorem OAI.PureTypeSystem.Normal.var line 267
27. theorem OAI.PureTypeSystem.Normal.sort line 271
28. theorem OAI.PureTypeSystem.Normal.stronglyNormalizing line 275
29. theorem OAI.PureTypeSystem.StronglyNormalizing.step line 284
30. theorem OAI.PureTypeSystem.StronglyNormalizing.reduces line 287
31. theorem OAI.PureTypeSystem.StronglyNormalizing.of_map line 293

    Source documentation

    SN of an image reflects along any map preserving individual reduction steps.

    theorem of_map {f : Expr S → Expr S}
        (hf : ∀ {M N}, Beta M N → Beta (f M) (f N)) {M : Expr S}
        (h : StronglyNormalizing (f M)) : StronglyNormalizing M := by
    …

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Beta, OAI.PureTypeSystem.StronglyNormalizing

32. theorem OAI.PureTypeSystem.StronglyNormalizing.app_left line 306
33. theorem OAI.PureTypeSystem.StronglyNormalizing.app_right line 309
34. theorem OAI.PureTypeSystem.StronglyNormalizing.lam_domain line 312
35. theorem OAI.PureTypeSystem.StronglyNormalizing.lam_body line 315
36. theorem OAI.PureTypeSystem.StronglyNormalizing.pi_domain line 318
37. theorem OAI.PureTypeSystem.StronglyNormalizing.pi_body line 321
38. theorem OAI.PureTypeSystem.StronglyNormalizing.of_subst line 324
39. theorem OAI.PureTypeSystem.StronglyNormalizing.of_rename line 327
40. theorem OAI.PureTypeSystem.StronglyNormalizing.lam line 330
41. theorem OAI.PureTypeSystem.StronglyNormalizing.pi line 342
42. def OAI.PureTypeSystem.Expr.apps line 360
43. theorem OAI.PureTypeSystem.Expr.apps_nil line 364
44. theorem OAI.PureTypeSystem.Expr.apps_cons line 365
45. theorem OAI.PureTypeSystem.Expr.apps_append line 368
46. inductive OAI.PureTypeSystem.ArgsStep line 377

    Source documentation

    Exactly one reduction step in one term of an argument list.

    inductive ArgsStep {S : Type u} : List (Expr S) → List (Expr S) → Prop
      | head {a a' as} : Beta a a' → ArgsStep (a :: as) (a' :: as)
      | tail {a as as'} : ArgsStep as as' → ArgsStep (a :: as) (a :: as')

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Beta

47. def OAI.PureTypeSystem.StronglyNormalizingArgs line 381
48. theorem OAI.PureTypeSystem.Beta.apps line 388
49. theorem OAI.PureTypeSystem.Beta.apps_inv line 395

    Source documentation

    If the head is not a lambda, a spine step comes from its head or an argument.

    theorem apps_inv {as : List (Expr S)} {N : Expr S}
        (hf : ∀ A b, f ≠ .lam A b) (h : Beta (f.apps as) N) :
        (∃ f', Beta f f' ∧ N = f'.apps as) ∨
        (∃ as', ArgsStep as as' ∧ N = f.apps as') := by
    …

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Beta, OAI.PureTypeSystem.ArgsStep

50. theorem OAI.PureTypeSystem.ArgsStep.apps line 416
51. theorem OAI.PureTypeSystem.Reduces.apps line 427
52. theorem OAI.PureTypeSystem.StronglyNormalizingArgs.nil line 436
53. theorem OAI.PureTypeSystem.StronglyNormalizingArgs.cons line 441
54. theorem OAI.PureTypeSystem.StronglyNormalizingArgs.of_forall line 453
55. theorem OAI.PureTypeSystem.StronglyNormalizingArgs.head line 460
56. theorem OAI.PureTypeSystem.StronglyNormalizingArgs.tail line 465
57. theorem OAI.PureTypeSystem.StronglyNormalizingArgs.of_mem line 470
58. theorem OAI.PureTypeSystem.StronglyNormalizing.apps_head line 485
59. theorem OAI.PureTypeSystem.StronglyNormalizing.var_apps line 489
60. theorem OAI.PureTypeSystem.StronglyNormalizing.head_expansion line 503

    Source documentation

    The source's head-expansion lemma, with any finite argument spine. The proof uses nested accessibility induction, not a raised recursion budget or an assumed maximal reduction height.

    theorem head_expansion {A b a : Expr S} {as : List (Expr S)}
        (hA : StronglyNormalizing A) (hb : StronglyNormalizing b)
        (ha : StronglyNormalizing a) (has : StronglyNormalizingArgs as)
        (hc : StronglyNormalizing ((b.instantiate a).apps as)) :
        StronglyNormalizing ((Expr.app (.lam A b) a).apps as) := by
    …

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.StronglyNormalizing, OAI.PureTypeSystem.StronglyNormalizingArgs, OAI.PureTypeSystem.StronglyNormalizing.lam

61. inductive OAI.PureTypeSystem.Expr.Child line 541

    Source documentation

    Only literal syntax descent, including both annotations.

    inductive Child : Expr S → Expr S → Prop
      | app_left (f a) : Child f (.app f a)
      | app_right (f a) : Child a (.app f a)
      | lam_domain (D m) : Child D (.lam D m)
      | lam_body (D m) : Child m (.lam D m)
      | pi_domain (D E) : Child D (.pi D E)
      | pi_body (D E) : Child E (.pi D E)

    Mentions: OAI.PureTypeSystem.Expr

62. inductive OAI.PureTypeSystem.Expr.Subterm line 549
63. theorem OAI.PureTypeSystem.Expr.Child.beta_lift line 555
64. theorem OAI.PureTypeSystem.Expr.Child.sn line 565
65. theorem OAI.PureTypeSystem.Expr.Subterm.trans line 577
66. theorem OAI.PureTypeSystem.Expr.Subterm.of_child line 582
67. theorem OAI.PureTypeSystem.Expr.Subterm.beta_lift line 584
68. theorem OAI.PureTypeSystem.Expr.Subterm.sn line 593
69. theorem OAI.PureTypeSystem.StronglyNormalizing.induction_subterms line 604

    Source documentation

    The manuscript's simultaneous reduction-height/syntax-size induction, proved directly from accessibility, without choosing a height or raising limits.

    theorem induction_subterms {Q : Expr S → Prop}
        (step : ∀ M, StronglyNormalizing M → (∀ N, Beta M N → Q N) →
          (∀ N, Expr.Child N M → Q N) → Q M)
        {M : Expr S} (hs : StronglyNormalizing M) : Q M := by
    …

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.StronglyNormalizing.step, OAI.PureTypeSystem.StronglyNormalizing, OAI.PureTypeSystem.Beta, OAI.PureTypeSystem.Expr.Child

70. theorem OAI.PureTypeSystem.StronglyNormalizing.induction_descendants line 647

    Source documentation

    The child hypothesis can equivalently cover every proper syntactic part.

    theorem induction_descendants {Q : Expr S → Prop}
        (step : ∀ M, StronglyNormalizing M → (∀ N, Beta M N → Q N) →
          (∀ N, (∃ K, Expr.Child K M ∧ Expr.Subterm N K) → Q N) → Q M)
        {M : Expr S} (hs : StronglyNormalizing M) : Q M := by
    …

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.StronglyNormalizing.step, OAI.PureTypeSystem.StronglyNormalizing, OAI.PureTypeSystem.Beta, OAI.PureTypeSystem.Expr.Child, OAI.PureTypeSystem.Expr.Subterm