OAI/Computability/TypeSystem/Pairs.lean

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PureTypeSystem.Labelled.DataWrapper.reencodeBody_subst line 11
2. theorem OAI.PureTypeSystem.Labelled.Expr.liftSub_succ_natural line 19
3. theorem OAI.PureTypeSystem.Labelled.ChannelCode.pred_subst line 31
4. def OAI.PureTypeSystem.Labelled.ChannelCode.classTag line 37

   Source documentation

   Class and edge query tags in the source's fixed seven structural tags.

   def classTag (t : Fin 3) : Fin 7 := ⟨t.val+1,by omega⟩

5. def OAI.PureTypeSystem.Labelled.ChannelCode.edgeTag line 38
6. def OAI.PureTypeSystem.Labelled.ChannelCode.isClass line 40
7. def OAI.PureTypeSystem.Labelled.ChannelCode.edge line 43
8. def OAI.PureTypeSystem.Labelled.ChannelCode.formExBody line 48
9. def OAI.PureTypeSystem.Labelled.ChannelCode.pairForm line 54
10. def OAI.PureTypeSystem.Labelled.ChannelCode.pairBody line 58
11. def OAI.PureTypeSystem.Labelled.ChannelCode.pairPred line 63
12. theorem OAI.PureTypeSystem.Labelled.ChannelCode.classBody_subst line 66
13. theorem OAI.PureTypeSystem.Labelled.ChannelCode.classPred_subst line 76
14. theorem OAI.PureTypeSystem.Labelled.ChannelCode.unionBody_subst line 80
15. theorem OAI.PureTypeSystem.Labelled.ChannelCode.unionPred_subst line 85
16. theorem OAI.PureTypeSystem.Labelled.ChannelCode.isClass_rename line 90
17. theorem OAI.PureTypeSystem.Labelled.ChannelCode.isClass_subst line 95
18. theorem OAI.PureTypeSystem.Labelled.ChannelCode.edge_rename line 100
19. theorem OAI.PureTypeSystem.Labelled.ChannelCode.edge_subst line 105
20. theorem OAI.PureTypeSystem.Labelled.ChannelCode.formExBody_rename line 111
21. theorem OAI.PureTypeSystem.Labelled.ChannelCode.formExBody_subst line 119
22. theorem OAI.PureTypeSystem.Labelled.ChannelCode.formExBody_instantiate line 128
23. theorem OAI.PureTypeSystem.Labelled.ChannelCode.pairForm_rename line 137
24. theorem OAI.PureTypeSystem.Labelled.ChannelCode.pairForm_subst line 143
25. theorem OAI.PureTypeSystem.Labelled.ChannelCode.pairBody_rename line 149
26. theorem OAI.PureTypeSystem.Labelled.ChannelCode.pairBody_instantiate line 157
27. theorem OAI.PureTypeSystem.Labelled.ChannelCode.pairBody_subst line 164
28. theorem OAI.PureTypeSystem.Labelled.ChannelCode.pairPred_rename line 174
29. theorem OAI.PureTypeSystem.Labelled.ChannelCode.pairPred_subst line 180
30. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.isClass_formula line 198
31. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.edge_formula line 203
32. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.formExBody_family line 211
33. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.pairForm_formula line 232
34. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.pairBody_family line 240
35. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.pairPred_typed line 260
36. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.pairPred_evaluation line 266
37. theorem OAI.PureTypeSystem.Labelled.queryBits_beq line 276
38. theorem OAI.PureTypeSystem.Labelled.queryTag_injective line 281
39. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.tagged_tag line 294
40. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.encode_evaluation line 303
41. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.encode_mark line 317
42. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.encode_payload line 342
43. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.decode_encode line 365
44. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bitBody_subst line 386
45. theorem OAI.PureTypeSystem.Labelled.DoubleCode.recBody_subst line 393
46. theorem OAI.PureTypeSystem.Labelled.DoubleCode.recoveryBody_subst line 407
47. theorem OAI.PureTypeSystem.Labelled.DoubleCode.tagBody_subst line 413
48. theorem OAI.PureTypeSystem.Labelled.DoubleCode.big_rename line 425
49. theorem OAI.PureTypeSystem.Labelled.DoubleCode.big_subst line 427
50. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bpType_rename line 429
51. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bpType_subst line 432
52. theorem OAI.PureTypeSystem.Labelled.DoubleCode.embedBody_subst line 436
53. theorem OAI.PureTypeSystem.Labelled.DoubleCode.decoderBody_rename line 443
54. theorem OAI.PureTypeSystem.Labelled.DoubleCode.decode_rename line 449
55. theorem OAI.PureTypeSystem.Labelled.DoubleCode.decoderBody_subst line 454
56. theorem OAI.PureTypeSystem.Labelled.DoubleCode.decode_subst line 460
57. def OAI.PureTypeSystem.Labelled.DoubleCode.decodeMap line 466

    Source comment

    This body exposes the decoded predicate as a data map on exact BP values.

    def decodeMap (U : DataWrapper S true) (L : LogicCode S) (T : Expr S) :=
    …

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

58. theorem OAI.PureTypeSystem.Labelled.DoubleCode.decodeMap_instantiate line 469
59. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.decodeMap_typed line 479
60. def OAI.PureTypeSystem.Labelled.DoubleCode.bpBottom line 489
61. def OAI.PureTypeSystem.Labelled.DoubleCode.dummy line 490
62. def OAI.PureTypeSystem.Labelled.DoubleCode.isDummy line 491
63. def OAI.PureTypeSystem.Labelled.DoubleCode.markBody line 492
64. def OAI.PureTypeSystem.Labelled.DoubleCode.pointBody line 494
65. def OAI.PureTypeSystem.Labelled.DoubleCode.point line 497
66. theorem OAI.PureTypeSystem.Labelled.DoubleCode.markBody_instantiate line 500
67. theorem OAI.PureTypeSystem.Labelled.DoubleCode.pointBody_instantiate line 503
68. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bpBottom_typed line 514
69. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.dummy_typed line 517
70. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.isDummy_formula line 520
71. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.markBody_family line 524
72. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.pointBody_family line 531
73. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.point_typed line 538
74. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.dummy_law line 553
75. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bottom_mark line 562
76. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.point_evaluation line 576
77. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.point_not_dummy line 587
78. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.point_query line 605
79. def OAI.PureTypeSystem.Labelled.DoubleCode.bundleBody line 632

    Source documentation

    Source Bundle is a fixed data term; no non-dummy proof enters its code.

    def bundleBody (L : LogicCode S) (A d m y : Expr S) :=
    …

    Mentions: OAI.PureTypeSystem.Labelled.Expr

80. def OAI.PureTypeSystem.Labelled.DoubleCode.bundle line 635
81. def OAI.PureTypeSystem.Labelled.DoubleCode.accessBody line 637

    Source documentation

    The outer access predicate, with the exact inner data callback fi.

    def accessBody (L : LogicCode S) (A guard w fi : Expr S) :=
    …

    Mentions: OAI.PureTypeSystem.Labelled.Expr

82. def OAI.PureTypeSystem.Labelled.DoubleCode.accessProbe line 640
83. def OAI.PureTypeSystem.Labelled.DoubleCode.access line 642
84. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bundleBody_instantiate line 645
85. theorem OAI.PureTypeSystem.Labelled.DoubleCode.accessBody_instantiate line 652
86. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bundleBody_family line 667
87. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bundle_typed line 674
88. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bundle_evaluation line 682
89. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.accessBody_family line 692
90. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.accessProbe_typed line 698
91. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.accessProbe_evaluation line 704
92. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bundle_select_true line 719
93. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bundle_select_false line 735
94. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.accessProbe_true line 751
95. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.accessProbe_false line 763
96. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.access_bundle line 780

    Source documentation

    The exact-parameter access calculation. The inner callback is raw typed data, not a selected term depending on the non-dummy proof.

     theorem access_bundle {A d m y guard fi : Expr S} (hA : SortedAt P Γ A I) (mA : WellModed γ A .data)
        (hd : HasType P Γ d A) (md : WellModed γ d .data)
        (hm : HasType P Γ m A) (mm : WellModed γ m .data)
        (hy : HasType P Γ y A) (my : WellModed γ y .data)
        (hg : L.Family A guard) (hfi : DataMap P Γ γ A (R.first.apply A) fi)
        {s : S} (hs : HasType P Γ A (.sort s))
        (hgd : Proves P Γ γ (guard.instantiate d))
        (hgm : Proves P Γ γ (L.neg (guard.instantiate m)))
        (hid : Proves P Γ γ (L.neg (R.first.observe A (fi.instantiate m) d))) :
        Equivalent P Γ γ (R.access L.code A guard (R.bundle L.code A d m y) fi)
          (R.first.observe A (fi.instantiate m) y) := by
    …

    Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.SortedAt, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.Proves, OAI.PureTypeSystem.Labelled.Equivalent

97. def OAI.PureTypeSystem.Labelled.DoubleCode.dummyBody line 809
98. def OAI.PureTypeSystem.Labelled.DoubleCode.queryBody line 811
99. def OAI.PureTypeSystem.Labelled.DoubleCode.innerBody line 813
100. def OAI.PureTypeSystem.Labelled.DoubleCode.innerProbe line 816
101. theorem OAI.PureTypeSystem.Labelled.DoubleCode.dummyBody_instantiate line 819
102. theorem OAI.PureTypeSystem.Labelled.DoubleCode.queryBody_instantiate line 822
103. theorem OAI.PureTypeSystem.Labelled.DoubleCode.innerBody_instantiate line 825
104. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.dummyBody_family line 839
105. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.queryBody_family line 844
106. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.innerBody_family line 849
107. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.innerProbe_typed line 854
108. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.innerProbe_evaluation line 859
109. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.innerProbe_dummy line 868
110. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.innerProbe_point line 882
111. theorem OAI.PureTypeSystem.Labelled.DataMap.compose line 908
112. theorem OAI.PureTypeSystem.Labelled.LogicCode.rename_bottom line 915
113. theorem OAI.PureTypeSystem.Labelled.LogicCode.subst_bottom line 916
114. theorem OAI.PureTypeSystem.Labelled.DoubleCode.rename_first line 922
115. theorem OAI.PureTypeSystem.Labelled.DoubleCode.subst_first line 923
116. theorem OAI.PureTypeSystem.Labelled.DoubleCode.rename_second line 924
117. theorem OAI.PureTypeSystem.Labelled.DoubleCode.subst_second line 925
118. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bpBottom_rename line 926
119. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bpBottom_subst line 930
120. theorem OAI.PureTypeSystem.Labelled.DoubleCode.paramType_rename line 935
121. theorem OAI.PureTypeSystem.Labelled.DoubleCode.paramType_subst line 938
122. theorem OAI.PureTypeSystem.Labelled.DoubleCode.encode_rename line 941
123. theorem OAI.PureTypeSystem.Labelled.DoubleCode.encodeBody_subst line 946
124. theorem OAI.PureTypeSystem.Labelled.DoubleCode.encode_subst line 952
125. theorem OAI.PureTypeSystem.Labelled.DoubleCode.dummyBody_rename line 957
126. theorem OAI.PureTypeSystem.Labelled.DoubleCode.dummyBody_subst line 961
127. theorem OAI.PureTypeSystem.Labelled.DoubleCode.innerBody_rename line 965
128. theorem OAI.PureTypeSystem.Labelled.DoubleCode.innerBody_subst line 971
129. theorem OAI.PureTypeSystem.Labelled.DoubleCode.innerProbe_rename line 978
130. theorem OAI.PureTypeSystem.Labelled.DoubleCode.innerProbe_subst line 983
131. def OAI.PureTypeSystem.Labelled.DoubleCode.innerMap line 989
132. theorem OAI.PureTypeSystem.Labelled.DoubleCode.innerMap_instantiate line 991
133. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.innerMap_typed line 1001
134. theorem OAI.PureTypeSystem.Labelled.DoubleCode.query_rename line 1012
135. theorem OAI.PureTypeSystem.Labelled.DoubleCode.query_subst line 1017
136. def OAI.PureTypeSystem.Labelled.DoubleCode.queryPredBody line 1024

     Source documentation

     The genuine predicate binder of qry_t(m,P), distinct from the parameter binder used by Access.

     def queryPredBody (U : DataWrapper S true) (L : LogicCode S) (t : Fin 8) (T m : Expr S) :=
     …

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

137. theorem OAI.PureTypeSystem.Labelled.DoubleCode.queryPredBody_rename line 1027
138. theorem OAI.PureTypeSystem.Labelled.DoubleCode.queryPredBody_subst line 1033
139. theorem OAI.PureTypeSystem.Labelled.DoubleCode.queryPredBody_instantiate line 1039
140. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.query_formula line 1048
141. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.queryPredBody_family line 1055
142. def OAI.PureTypeSystem.Labelled.DoubleCode.accessMap line 1067
143. def OAI.PureTypeSystem.Labelled.DoubleCode.recoverAccess line 1069
144. theorem OAI.PureTypeSystem.Labelled.DoubleCode.accessMap_instantiate line 1071
145. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.accessMap_typed line 1079
146. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.access_recovery line 1087
147. theorem OAI.PureTypeSystem.Labelled.DoubleCode.carrier_converts line 1132
148. theorem OAI.PureTypeSystem.Labelled.DoubleCode.tower_converts line 1134
149. theorem OAI.PureTypeSystem.Labelled.DoubleCode.paramType_converts line 1138
150. def OAI.PureTypeSystem.Labelled.ProbeCode.atType line 1145
151. def OAI.PureTypeSystem.Labelled.ProbeCode.specialize line 1146
152. def OAI.PureTypeSystem.Labelled.ProbeCode.readBody line 1147
153. def OAI.PureTypeSystem.Labelled.ProbeCode.observe line 1148
154. theorem OAI.PureTypeSystem.Labelled.ProbeCode.atType_rename line 1150
155. theorem OAI.PureTypeSystem.Labelled.ProbeCode.atType_subst line 1153
156. theorem OAI.PureTypeSystem.Labelled.ProbeCode.funType_converts line 1156
157. theorem OAI.PureTypeSystem.Labelled.ProbeCode.atType_converts line 1159
158. theorem OAI.PureTypeSystem.Labelled.ProbeCode.at_body_convert line 1161
159. theorem OAI.PureTypeSystem.Labelled.ProbeCode.readBody_instantiate line 1166
160. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.at_sorted line 1177
161. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.at_mode line 1179
162. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.at_typed line 1181
163. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.at_data line 1186
164. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.readBody_family line 1189
165. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.observe_formula line 1209
166. def OAI.PureTypeSystem.Labelled.ProbeCode.funBuild line 1220

     Source documentation

     Ordinary data abstraction on the single bundle, before even wrapping.

     def funBuild (A Q : Expr S) : Expr S := .lam .dd (R.singleType A) ((R.tail.rename Nat.succ).send Q)

     Mentions: OAI.PureTypeSystem.Labelled.Expr

167. def OAI.PureTypeSystem.Labelled.ProbeCode.wrappedBuild line 1221
168. theorem OAI.PureTypeSystem.Labelled.ProbeCode.funBuild_beta line 1223
169. theorem OAI.PureTypeSystem.Labelled.ProbeCode.funBuild_rename line 1230
170. theorem OAI.PureTypeSystem.Labelled.ProbeCode.funBuild_subst line 1236
171. theorem OAI.PureTypeSystem.Labelled.ProbeCode.wrappedBuild_rename line 1243
172. theorem OAI.PureTypeSystem.Labelled.ProbeCode.wrappedBuild_subst line 1250
173. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.funBuild_typed line 1262
174. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.wrappedBuild_typed line 1274
175. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.funBuild_evaluation line 1280
176. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.wrappedBuild_evaluation line 1295
177. theorem OAI.PureTypeSystem.Labelled.Converts.lam line 1321
178. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.inject_converts line 1328
179. theorem OAI.PureTypeSystem.Labelled.DataTail.send_converts line 1335
180. theorem OAI.PureTypeSystem.Labelled.DataWrapper.congr_build_observe line 1339
181. theorem OAI.PureTypeSystem.Labelled.DataWrapper.build_congr line 1374
182. theorem OAI.PureTypeSystem.Labelled.DataWrapper.observe_congr line 1377
183. theorem OAI.PureTypeSystem.Labelled.ProbeCode.singleType_converts line 1382
184. def OAI.PureTypeSystem.Labelled.ProbeCode.uniform line 1394

     Source documentation

     Uniform V constructor. Q binds w:Single(z-down), then z:Z.

     def uniform (Q : Expr S) : Expr S := .lam .dd R.domain
     …

     Mentions: OAI.PureTypeSystem.Labelled.Expr

185. theorem OAI.PureTypeSystem.Labelled.ProbeCode.uniform_specialize line 1397
186. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.project_typed line 1412
187. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.project_mode line 1414
188. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.raised_project line 1416
189. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.uniform_typed line 1421
190. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.uniform_evaluation line 1432