OAI/Computability/TypeSystem/Labelled.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.PureTypeSystem.Labelled.Mode line 11
2. inductive OAI.PureTypeSystem.Labelled.Label line 16
3. def OAI.PureTypeSystem.Labelled.Label.domain line 22
4. def OAI.PureTypeSystem.Labelled.Label.result line 26
5. inductive OAI.PureTypeSystem.Labelled.Expr line 30
6. abbrev OAI.PureTypeSystem.Labelled.Expr.liftRen line 41
7. def OAI.PureTypeSystem.Labelled.Expr.rename line 43
8. def OAI.PureTypeSystem.Labelled.Expr.liftSub line 50
9. def OAI.PureTypeSystem.Labelled.Expr.subst line 54
10. def OAI.PureTypeSystem.Labelled.Expr.single line 61
11. def OAI.PureTypeSystem.Labelled.Expr.instantiate line 65
12. def OAI.PureTypeSystem.Labelled.Expr.erase line 67
13. theorem OAI.PureTypeSystem.Labelled.Expr.rename_id line 74
14. theorem OAI.PureTypeSystem.Labelled.Expr.rename_comp line 77
15. theorem OAI.PureTypeSystem.Labelled.Expr.subst_var line 82
16. theorem OAI.PureTypeSystem.Labelled.Expr.subst_rename line 86
17. theorem OAI.PureTypeSystem.Labelled.Expr.rename_subst line 93
18. theorem OAI.PureTypeSystem.Labelled.Expr.subst_subst line 102
19. theorem OAI.PureTypeSystem.Labelled.Expr.instantiate_rename line 111
20. theorem OAI.PureTypeSystem.Labelled.Expr.instantiate_subst line 116
21. theorem OAI.PureTypeSystem.Labelled.Expr.erase_rename line 123
22. theorem OAI.PureTypeSystem.Labelled.Expr.erase_liftSub line 127
23. theorem OAI.PureTypeSystem.Labelled.Expr.erase_subst line 131
24. theorem OAI.PureTypeSystem.Labelled.Expr.erase_instantiate line 135
25. inductive OAI.PureTypeSystem.Labelled.Beta line 142
26. def OAI.PureTypeSystem.Labelled.Converts line 151
27. abbrev OAI.PureTypeSystem.Labelled.Reduces line 152
28. theorem OAI.PureTypeSystem.Labelled.Beta.rename line 157
29. theorem OAI.PureTypeSystem.Labelled.Beta.subst line 169
30. theorem OAI.PureTypeSystem.Labelled.Beta.erase line 181
31. inductive OAI.PureTypeSystem.Labelled.Parallel line 194
32. theorem OAI.PureTypeSystem.Labelled.Parallel.refl line 210
33. theorem OAI.PureTypeSystem.Labelled.Parallel.of_beta line 218
34. theorem OAI.PureTypeSystem.Labelled.Parallel.rename line 228
35. theorem OAI.PureTypeSystem.Labelled.Parallel.subst line 240
36. theorem OAI.PureTypeSystem.Labelled.Parallel.instantiate line 258
37. def OAI.PureTypeSystem.Labelled.Expr.develop line 273

    Source documentation

    Complete development contracts only matching-labelled redexes.

    def develop : Expr S → Expr S
      | var n => var n
      | sort s => sort s
      | app l (lam k A b) a =>
          if l = k then (develop b).instantiate (develop a)
          else app l (lam k (develop A) (develop b)) (develop a)
      | app l f a => app l (develop f) (develop a)
      | lam l A b => lam l (develop A) (develop b)
      | pi l A B => pi l (develop A) (develop B)
    
    end Expr
    …

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

38. theorem OAI.PureTypeSystem.Labelled.Parallel.triangle line 289
39. theorem OAI.PureTypeSystem.Labelled.Parallel.diamond line 313
40. theorem OAI.PureTypeSystem.Labelled.Reduces.app line 322
41. theorem OAI.PureTypeSystem.Labelled.Reduces.lam line 327
42. theorem OAI.PureTypeSystem.Labelled.Reduces.pi line 332
43. theorem OAI.PureTypeSystem.Labelled.Reduces.rename line 337
44. theorem OAI.PureTypeSystem.Labelled.Reduces.subst line 340
45. theorem OAI.PureTypeSystem.Labelled.Parallel.reduces line 349
46. theorem OAI.PureTypeSystem.Labelled.Parallel.rtc_reduces line 359
47. theorem OAI.PureTypeSystem.Labelled.Reduces.parallel line 368
48. theorem OAI.PureTypeSystem.Labelled.Reduces.confluent line 371
49. theorem OAI.PureTypeSystem.Labelled.Converts.join line 387
50. theorem OAI.PureTypeSystem.Labelled.Reduces.pi_inv line 406
51. theorem OAI.PureTypeSystem.Labelled.Reduces.converts line 416
52. theorem OAI.PureTypeSystem.Labelled.Converts.product_compatibility line 425
53. inductive OAI.PureTypeSystem.Labelled.HasType line 437
54. inductive OAI.PureTypeSystem.Labelled.ValidContext line 455
55. theorem OAI.PureTypeSystem.Labelled.HasType.valid line 464
56. theorem OAI.PureTypeSystem.Labelled.Expr.liftSub_zero line 478
57. theorem OAI.PureTypeSystem.Labelled.Expr.liftSub_succ line 479
58. inductive OAI.PureTypeSystem.Labelled.Lookup line 483
59. theorem OAI.PureTypeSystem.Labelled.HasType.sort_of_valid line 491
60. theorem OAI.PureTypeSystem.Labelled.HasType.product_domain line 499

    Source documentation

    Domain generation alone precedes substitution and does not need any exchange or context-substitution theorem.

    theorem product_domain {Γ : List (Expr S)} {M T : Expr S} (h : HasType P Γ M T) :
        ∀ l A B, M = .pi l A B → ∃ s, HasType P Γ A (.sort s) := by
    …

    Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.HasType

61. theorem OAI.PureTypeSystem.Labelled.Converts.subst line 529
62. theorem OAI.PureTypeSystem.Labelled.Converts.rename line 537
63. def OAI.PureTypeSystem.Labelled.TypedSubstitution line 549

    Source documentation

    A simultaneous substitution respects each declared variable's exact type. This is a premise only of the substitution metatheorem, not of the main target.

    def TypedSubstitution {S : Type u} (P : Specification S)
        (Γ Δ : List (Expr S)) (σ : Nat → Expr S) : Prop :=
    …

    Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.Labelled.Expr

64. theorem OAI.PureTypeSystem.Labelled.TypedSubstitution.tail line 558
65. theorem OAI.PureTypeSystem.Labelled.TypedSubstitution.lift line 564
66. theorem OAI.PureTypeSystem.Labelled.HasType.subst line 584
67. theorem OAI.PureTypeSystem.Labelled.Expr.subst_var_rename line 611
68. theorem OAI.PureTypeSystem.Labelled.Expr.subst_lift_single line 615
69. theorem OAI.PureTypeSystem.Labelled.HasType.lookup line 626
70. theorem OAI.PureTypeSystem.Labelled.TypedSubstitution.identity line 641
71. theorem OAI.PureTypeSystem.Labelled.TypedSubstitution.weaken line 646
72. theorem OAI.PureTypeSystem.Labelled.TypedSubstitution.single line 653
73. theorem OAI.PureTypeSystem.Labelled.HasType.rename line 667
74. theorem OAI.PureTypeSystem.Labelled.HasType.instantiate line 676
75. theorem OAI.PureTypeSystem.Labelled.HasType.weaken_under line 681
76. theorem OAI.PureTypeSystem.Labelled.HasType.context_head_conversion line 696
77. def OAI.PureTypeSystem.Labelled.Normal line 712
78. theorem OAI.PureTypeSystem.Labelled.Normal.reduces_eq line 720
79. theorem OAI.PureTypeSystem.Labelled.Normal.eq_of_converts line 725
80. theorem OAI.PureTypeSystem.Labelled.Normal.var line 732
81. theorem OAI.PureTypeSystem.Labelled.Normal.sort line 733
82. def OAI.PureTypeSystem.Labelled.HasType.Generation line 741

    Source documentation

    Generation is stated up to conversion, without any functionality premise.

    def Generation (P : Specification S) (Γ : List (Expr S))
        (M T : Expr S) : Prop :=
    …

    Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.Labelled.Expr

83. theorem OAI.PureTypeSystem.Labelled.HasType.generation line 754
84. theorem OAI.PureTypeSystem.Labelled.HasType.generation_pi line 801
85. theorem OAI.PureTypeSystem.Labelled.HasType.generation_lam line 807
86. theorem OAI.PureTypeSystem.Labelled.HasType.generation_app line 812
87. theorem OAI.PureTypeSystem.Labelled.HasType.regularity line 818

    Source documentation

    Correctness of types, including the unsorted literal-sort alternative.

    theorem regularity {Γ : List (Expr S)} {M A : Expr S} (h : HasType P Γ M A) :
        (∃ s, A = .sort s) ∨ (∃ s, HasType P Γ A (.sort s)) := by
    …

    Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.HasType

88. theorem OAI.PureTypeSystem.Labelled.HasType.product_type_sorted line 836
89. theorem OAI.PureTypeSystem.Labelled.Converts.pi line 848
90. theorem OAI.PureTypeSystem.Labelled.Converts.pi_not_sort line 854
91. theorem OAI.PureTypeSystem.Labelled.Converts.sort_inj line 861
92. theorem OAI.PureTypeSystem.Labelled.Converts.instantiate_right line 864
93. theorem OAI.PureTypeSystem.Labelled.HasType.application_type_sorted_aux line 879
94. theorem OAI.PureTypeSystem.Labelled.HasType.application_type_sorted line 904
95. theorem OAI.PureTypeSystem.Labelled.HasType.abstraction_type_sorted line 908
96. theorem OAI.PureTypeSystem.Labelled.HasType.conversion_from_sort line 918

    Source documentation

    Reconstructing a sorted expression at its original expected type does not require a sorting of a terminal (unsorted) sort.

    theorem conversion_from_sort {Γ : List (Expr S)} {M T : Expr S} {s : S}
        (h : HasType P Γ M (.sort s))
        (hT : (∃ t, T = .sort t) ∨ ∃ t, HasType P Γ T (.sort t))
        (hc : Converts T (.sort s)) : HasType P Γ M T := by
    …

    Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.Converts

97. theorem OAI.PureTypeSystem.Labelled.HasType.subject_reduction line 929

    Source documentation

    Subject reduction at the exact original type, including binder annotations.

    theorem subject_reduction {Γ : List (Expr S)} {M N T : Expr S}
        (h : HasType P Γ M T) (hr : Beta M N) : HasType P Γ N T := by
    …

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

98. theorem OAI.PureTypeSystem.Labelled.HasType.subject_reduces line 975
99. theorem OAI.PureTypeSystem.Labelled.Converts.erase line 985
100. theorem OAI.PureTypeSystem.Labelled.HasType.erase line 995
101. def OAI.PureTypeSystem.Labelled.modeCons line 1012

     Source documentation

     Modes are a separate syntax discipline on the labelled PTS. This keeps metatheory independent of mode well-formedness and proves preservation below.

     def modeCons (m : Mode) (γ : Nat → Mode) : Nat → Mode
       | 0 => m
       | n+1 => γ n

     Mentions: OAI.PureTypeSystem.Labelled.Mode

102. inductive OAI.PureTypeSystem.Labelled.WellModed line 1016
103. theorem OAI.PureTypeSystem.Labelled.WellModed.rename line 1028
104. theorem OAI.PureTypeSystem.Labelled.WellModed.subst line 1042
105. theorem OAI.PureTypeSystem.Labelled.WellModed.instantiate line 1058
106. theorem OAI.PureTypeSystem.Labelled.WellModed.beta line 1067
107. theorem OAI.PureTypeSystem.Labelled.WellModed.reduces line 1080
108. theorem OAI.PureTypeSystem.Labelled.Expr.erase_lam_inv line 1088
109. theorem OAI.PureTypeSystem.Labelled.erased_app_step line 1101
110. theorem OAI.PureTypeSystem.Labelled.HasType.lift_erased_step line 1116

     Source documentation

     Every erased redex of a typable labelled term has matching labels, even inside its annotations. No weak or strong normalization is assumed.

     theorem lift_erased_step (h : HasType P Γ M T) {N : PureTypeSystem.Expr S}
         (hr : PureTypeSystem.Beta M.erase N) :
         ∃ M', Beta M M' ∧ M'.erase = N := by
     …

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

111. theorem OAI.PureTypeSystem.Labelled.HasType.lift_erased_reduces line 1155
112. theorem OAI.PureTypeSystem.Labelled.HasType.normal_erasure_reduct line 1166

     Source documentation

     The exact final interface of the labelled-metatheory lemma.

     theorem normal_erasure_reduct (h : HasType P Γ M T) {γ : Nat → Mode} {m : Mode}
         (hm : WellModed γ M m) (hw : PureTypeSystem.WeaklyNormalizing M.erase) :
         ∃ M', Reduces M M' ∧ HasType P Γ M' T ∧ WellModed γ M' m ∧
           PureTypeSystem.Normal M'.erase := by
     …

     Mentions: OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.Mode, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.WeaklyNormalizing, OAI.PureTypeSystem.Labelled.Reduces, OAI.PureTypeSystem.Normal

113. def OAI.PureTypeSystem.Labelled.Expr.weight line 1177
114. inductive OAI.PureTypeSystem.Labelled.Expr.AllData line 1184

     Source documentation

     A terminal contains data/data labels only.

     inductive AllData : Expr S → Prop
       | var (n) : AllData (.var n)
       | sort (s) : AllData (.sort s)
       | app {f a} : AllData f → AllData a → AllData (.app .dd f a)
       | lam {A b} : AllData A → AllData b → AllData (.lam .dd A b)
       | pi {A B} : AllData A → AllData B → AllData (.pi .dd A B)
     
     namespace AllData

     Mentions: OAI.PureTypeSystem.Labelled.Expr

115. theorem OAI.PureTypeSystem.Labelled.Expr.AllData.rename line 1192
116. inductive OAI.PureTypeSystem.Labelled.Expr.Positive line 1203

     Source documentation

     A positive telescope ending in an all-data terminal. The source uses constant telescopes; the no-normal-proof argument also permits dependency.

     inductive Positive : Expr S → Prop
       | terminal {T} : AllData T → Positive T
       | step (D) {E} : Positive E → Positive (.pi .dp D E)
     
     namespace Positive

     Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.Expr.AllData

117. theorem OAI.PureTypeSystem.Labelled.Expr.Positive.rename line 1208
118. theorem OAI.PureTypeSystem.Labelled.Expr.Positive.not_pp line 1213
119. theorem OAI.PureTypeSystem.Labelled.Expr.Positive.dp_body line 1218
120. def OAI.PureTypeSystem.Labelled.Expr.Target line 1225

     Source documentation

     The normal target family used in the no-normal-proof obstruction.

     def Target (T : Expr S) : Prop := Positive T ∧ PureTypeSystem.Normal T.erase
     …

     Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.Expr.Positive, OAI.PureTypeSystem.Normal

121. theorem OAI.PureTypeSystem.Labelled.Expr.Target.rename line 1228
122. theorem OAI.PureTypeSystem.Labelled.Expr.Target.normal line 1231
123. theorem OAI.PureTypeSystem.Labelled.Expr.Target.product line 1234
124. inductive OAI.PureTypeSystem.Labelled.Expr.Neutral line 1248
125. theorem OAI.PureTypeSystem.Labelled.WellModed.var_inv line 1255
126. theorem OAI.PureTypeSystem.Labelled.WellModed.app_inv line 1258
127. theorem OAI.PureTypeSystem.Labelled.WellModed.lam_inv line 1262
128. theorem OAI.PureTypeSystem.Labelled.WellModed.normal_proof_shape line 1267

     Source documentation

     A normal-erasure proof has a lambda at the root or a variable-headed spine.

     theorem normal_proof_shape {M : Expr S} (h : WellModed γ M .proof)
         (hn : PureTypeSystem.Normal M.erase) :
         (∃ l A b, M = .lam l A b) ∨ M.Neutral := by
     …

     Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Normal

129. def OAI.PureTypeSystem.Labelled.ProofContext line 1286

     Source documentation

     Only proof variables are constrained. Each is a proof/proof converter whose first argument is one of the positive normal targets. This includes exactly the context shape used by the source, and is stable under data extensions. No converter result is assumed inhabited.

     def ProofContext {S : Type u} (Γ : List (Expr S)) (γ : Nat → Mode) : Prop :=
     …

     Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.Mode

130. theorem OAI.PureTypeSystem.Labelled.ProofContext.data_cons line 1292
131. theorem OAI.PureTypeSystem.Labelled.Expr.Neutral.first_target line 1308

     Source documentation

     The first argument of a normal proof-mode converter spine is itself a strictly smaller normal proof at a positive target.

     theorem first_target (hM : M.Neutral) (h : HasType P Γ M T)
         (hm : WellModed γ M .proof) (hn : PureTypeSystem.Normal M.erase)
         (hΓ : ProofContext Γ γ) :
         (∃ n, M = .var n) ∨
         ∃ Q R, Q.weight < M.weight ∧ R.Target ∧ HasType P Γ Q R ∧
           WellModed γ Q .proof ∧ PureTypeSystem.Normal Q.erase := by
     …

     Mentions: OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Normal, OAI.PureTypeSystem.Labelled.ProofContext

132. theorem OAI.PureTypeSystem.Labelled.no_normal_proof line 1334

     Source documentation

     No normal erasure at a terminal. The stronger form allows a dependent positive telescope: it uses only the outer labels, normality, typing and the decreasing body/first-argument syntax measure.

     theorem no_normal_proof {S : Type u} {P : Specification S}
         {Γ : List (Expr S)} {γ : Nat → Mode} {M T : Expr S}
         (hΓ : ProofContext Γ γ) (hT : T.Target) (h : HasType P Γ M T)
         (hm : WellModed γ M .proof) (hn : PureTypeSystem.Normal M.erase) : False := by
     …

     Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.Mode, OAI.PureTypeSystem.Labelled.ProofContext, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Normal

133. theorem OAI.PureTypeSystem.Labelled.no_proof_at_target line 1362

     Source documentation

     A system-wide WN PTS has no proof-mode inhabitant of these targets in these converter contexts. All later encodings must supply a genuine typing and mode derivation to invoke this obstruction.

     theorem no_proof_at_target {S : Type u} {P : Specification S}
         (hw : SystemWeaklyNormalizing P) {Γ : List (Expr S)} {γ : Nat → Mode} {M T : Expr S}
         (hΓ : ProofContext Γ γ) (hT : T.Target) (h : HasType P Γ M T)
         (hm : WellModed γ M .proof) : False := by
     …

     Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.Mode, OAI.PureTypeSystem.Labelled.ProofContext, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed