OAI/Computability/TypeSystem/Response.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PureTypeSystem.Labelled.RelationalCode.recoverLift_convertA line 10
2. theorem OAI.PureTypeSystem.Labelled.RelationalCode.probeFor_body_specialize line 19
3. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.probeFor_evaluation line 36

   Source documentation

   Uniform-probe evaluation before access recovery. No non-dummy assumption is needed for the uniform lambda's beta and wrapper cancellations.

   theorem probeFor_evaluation {A i w : Expr S}
       (hA : HasType P Γ A (.sort R.probe.seed)) (mA : WellModed γ A .data)
       (hi : HasType P Γ i (R.channel.predicateType R.probe.carrier)) (mi : WellModed γ i .data)
       (hw : HasType P Γ w (R.probe.singleType A)) (mw : WellModed γ w .data) :
       Equivalent P Γ γ (R.probe.observe A (R.probeFor L.code KY.code KP.code i) w)
         (R.recoverLift L.code KY.code KP.code A i w) := by
   …

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

4. theorem OAI.PureTypeSystem.Labelled.RelationalCode.Formed.probeFor_rounded line 66

   Source documentation

   The source rounded probe law. The assumption is the explicit non-dummy conjunct of Adm; all other equalities are typed cancellation proofs.

   theorem probeFor_rounded {A m i y : Expr S}
       (hA : HasType P Γ A (.sort R.probe.seed)) (mA : WellModed γ A .data)
       (hm : HasType P Γ m (R.probe.paramType A)) (mm : WellModed γ m .data)
       (hi : HasType P Γ i (R.channel.predicateType R.probe.carrier)) (mi : WellModed γ i .data)
       (hy : HasType P Γ y (R.channel.logicalType (R.baseType A))) (my : WellModed γ y .data)
       (hnd : Proves P Γ γ (L.neg (R.probe.doubled.isDummy L.code (R.probe.rawType A) m))) :
       Equivalent P Γ γ (R.diamond L.code A m (R.probeFor L.code KY.code KP.code i) y)
         (R.channel.eval R.probe.carrier i (R.lift L.code KY.code KP.code A m
           (R.channel.round (R.baseType A) y))) := by
   …

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

5. def OAI.PureTypeSystem.Labelled.SpecializedCode.diamond line 113
6. def OAI.PureTypeSystem.Labelled.SpecializedCode.part line 115
7. def OAI.PureTypeSystem.Labelled.SpecializedCode.sb line 117
8. def OAI.PureTypeSystem.Labelled.SpecializedCode.lift line 119
9. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.diamond_rename line 122
10. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.part_rename line 126
11. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.sb_rename line 130
12. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.lift_rename line 134
13. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.carrier_typed_rename line 147
14. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.xPred_typed_rename line 153
15. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_typed line 157
16. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diamond_formula line 162
17. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_evaluation line 168
18. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.lift_typed line 174
19. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.sb_formula line 179
20. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.lift_primitive_evaluation line 185
21. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.lift_evaluation line 192
22. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.probe_rounded line 200
23. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.goodBody_subst line 211
24. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.relation_subst line 215
25. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.relational_subst line 220
26. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.diamond_subst line 221
27. def OAI.PureTypeSystem.Labelled.SpecializedCode.respStep line 225
28. def OAI.PureTypeSystem.Labelled.SpecializedCode.respAtBody line 227
29. def OAI.PureTypeSystem.Labelled.SpecializedCode.respAt line 229
30. def OAI.PureTypeSystem.Labelled.SpecializedCode.respBody line 231
31. def OAI.PureTypeSystem.Labelled.SpecializedCode.response line 233
32. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respStep_rename line 235
33. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respStep_subst line 238
34. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respAtBody_rename line 241
35. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respAtBody_subst line 245
36. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respAtBody_instantiate line 249
37. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respAt_rename line 252
38. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respAt_subst line 255
39. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respBody_rename line 258
40. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respBody_subst line 262
41. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.respBody_instantiate line 266
42. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.response_rename line 269
43. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.response_subst line 272
44. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.respStep_formula line 286
45. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.respAtBody_family line 293
46. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.respAt_formula line 307
47. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.respBody_family line 314
48. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.response_formula line 325
49. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.respAt_intro line 339
50. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.respAt_elim line 352
51. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.response_intro line 362
52. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.response_elim_one line 374
53. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.response_elim line 383
54. def OAI.PureTypeSystem.Labelled.SpecializedCode.responsePredStep line 399
55. def OAI.PureTypeSystem.Labelled.SpecializedCode.responsePredBody line 401
56. def OAI.PureTypeSystem.Labelled.SpecializedCode.responsePred line 403
57. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.responsePredStep_rename line 405
58. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.responsePredStep_subst line 409
59. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.responsePredBody_rename line 413
60. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.responsePredBody_subst line 417
61. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.responsePredBody_instantiate line 421
62. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.responsePred_rename line 424
63. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.responsePred_subst line 428
64. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePredStep_formula line 443
65. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePredBody_family line 450
66. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePred_typed line 461
67. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePred_evaluation line 467
68. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.comparison_refl line 486
69. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.sb_equivalent line 493
70. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.le_lift_congr line 507
71. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.lift_congr line 526
72. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_probe_eval_compare line 549
73. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_probe_compare line 578
74. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.lift_le_pred_congr line 596
75. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.lift_validStep line 614
76. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.lift_validAt line 635
77. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.lift_valid line 646
78. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.round_relation line 663
79. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_exact line 668
80. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.probe_exact line 679
81. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.probe_respStep line 695
82. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.probe_respAt line 725
83. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.probe_response line 739
84. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePred_exact line 758
85. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePred_respect line 774
86. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePred_extStep line 794
87. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePred_extAt line 818
88. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePred_extensional line 832