OAI/Computability/TypeSystem/Relations.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PureTypeSystem.Labelled.ChannelCode.evalPredBody line 11

   Source documentation

   The predicate-variable callback P ↦ P@y.

   def evalPredBody (T y : Expr S) := (R.rename Nat.succ).eval (T.rename Nat.succ) (.var 0) (y.rename Nat.succ)

   Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.ChannelCode.eval

2. def OAI.PureTypeSystem.Labelled.ChannelCode.compareBody line 12
3. def OAI.PureTypeSystem.Labelled.ChannelCode.relation line 15

   Source documentation

   Source observational relation, with its actual Good predicate callback.

   def relation (L : LogicCode S) (K : QuantifierCode S) (T G y z : Expr S) :=
   …

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

4. theorem OAI.PureTypeSystem.Labelled.ChannelCode.evalPredBody_rename line 18
5. theorem OAI.PureTypeSystem.Labelled.ChannelCode.evalPredBody_instantiate line 24
6. theorem OAI.PureTypeSystem.Labelled.ChannelCode.compareBody_rename line 28
7. theorem OAI.PureTypeSystem.Labelled.ChannelCode.compareBody_instantiate line 33
8. theorem OAI.PureTypeSystem.Labelled.ChannelCode.relation_rename line 41
9. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.evalPredBody_family line 52
10. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.compareBody_family line 60
11. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.relation_formula line 66
12. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.relation_elim line 75
13. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.relation_intro line 90
14. theorem OAI.PureTypeSystem.Labelled.LogicSetup.Formula.equivalent_refl line 120
15. theorem OAI.PureTypeSystem.Labelled.LogicSetup.Formula.equivalent_trans line 124
16. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.relation_refl line 138
17. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.relation_symm line 145
18. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.relation_trans line 161
19. structure OAI.PureTypeSystem.Labelled.ThreeCopyCode line 193

    Source documentation

    Five odd segments and the original source channel for tagged copies.

    structure ThreeCopyCode (S : Type u) where
    …

20. def OAI.PureTypeSystem.Labelled.ThreeCopyCode.rename line 200
21. def OAI.PureTypeSystem.Labelled.ThreeCopyCode.subst line 202
22. def OAI.PureTypeSystem.Labelled.ThreeCopyCode.firstType line 204
23. def OAI.PureTypeSystem.Labelled.ThreeCopyCode.middleType line 205
24. def OAI.PureTypeSystem.Labelled.ThreeCopyCode.carrier line 206
25. def OAI.PureTypeSystem.Labelled.ThreeCopyCode.bitInner line 207
26. def OAI.PureTypeSystem.Labelled.ThreeCopyCode.bitOuter line 209
27. def OAI.PureTypeSystem.Labelled.ThreeCopyCode.observe line 210
28. def OAI.PureTypeSystem.Labelled.ThreeCopyCode.tagged line 213
29. structure OAI.PureTypeSystem.Labelled.ThreeCopyCode.Formed line 218
30. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.Formed.rename line 227
31. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.Formed.tagged_typed line 232
32. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.Formed.bitOuter_formula line 238
33. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.Formed.bitInner_formula line 242
34. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.Formed.observe_formula line 247
35. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.Formed.tagged_bitOuter line 253
36. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.Formed.tagged_bitInner line 259
37. theorem OAI.PureTypeSystem.Labelled.ThreeCopyCode.Formed.tagged_observe line 271
38. def OAI.PureTypeSystem.Labelled.ChannelReturn.copies line 296
39. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.copies_formed line 297
40. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.copies_type line 299
41. def OAI.PureTypeSystem.Labelled.ChannelCode.roundRespectBody line 305
42. def OAI.PureTypeSystem.Labelled.ChannelCode.roundRespect line 309
43. def OAI.PureTypeSystem.Labelled.ChannelCode.goodBody line 311
44. theorem OAI.PureTypeSystem.Labelled.ChannelCode.roundRespectBody_rename line 315
45. theorem OAI.PureTypeSystem.Labelled.ChannelCode.roundRespectBody_instantiate line 322
46. theorem OAI.PureTypeSystem.Labelled.ChannelCode.roundRespect_rename line 327
47. theorem OAI.PureTypeSystem.Labelled.ChannelCode.roundRespectBody_subst line 332
48. theorem OAI.PureTypeSystem.Labelled.ChannelCode.roundRespect_subst line 341
49. theorem OAI.PureTypeSystem.Labelled.ChannelCode.goodBody_rename line 346
50. theorem OAI.PureTypeSystem.Labelled.ChannelCode.goodBody_instantiate line 353
51. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.roundRespectBody_family line 364
52. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.roundRespect_formula line 378
53. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.roundRespect_elim line 386
54. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.goodBody_family line 399
55. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.good_round line 410
56. theorem OAI.PureTypeSystem.Labelled.LogicSetup.Formula.equivalent_of_future line 427

    Source documentation

    Binder-safe packaging of a pair of uniform proof transformers.

    theorem equivalent_of_future (hA : L.Formula A) (hB : L.Formula B)
        (hab : ∀ Δ δ (e : Embedding P Γ γ Δ δ),
          Proves P Δ δ (A.rename e.names) → Proves P Δ δ (B.rename e.names))
        (hba : ∀ Δ δ (e : Embedding P Γ γ Δ δ),
          Proves P Δ δ (B.rename e.names) → Proves P Δ δ (A.rename e.names)) : Equivalent P Γ γ A B := by
    …

    Mentions: OAI.PureTypeSystem.Labelled.Embedding, OAI.PureTypeSystem.Labelled.Proves, OAI.PureTypeSystem.Labelled.Equivalent

57. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.relation_round line 447
58. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.relation_congr line 469
59. theorem OAI.PureTypeSystem.Labelled.Expr.liftSub_single_liftRen_succ line 512
60. theorem OAI.PureTypeSystem.Labelled.LogicCode.guardBody_subst line 518
61. theorem OAI.PureTypeSystem.Labelled.LogicCode.guardAll_subst line 524
62. theorem OAI.PureTypeSystem.Labelled.ChannelCode.evalPredBody_subst line 532
63. theorem OAI.PureTypeSystem.Labelled.ChannelCode.compareBody_subst line 538
64. theorem OAI.PureTypeSystem.Labelled.ChannelCode.relation_subst line 544
65. def OAI.PureTypeSystem.Labelled.ChannelCode.classBody line 551

    Source documentation

    Source class callback w ↦ (w ∼ y); G retains its predicate binder.

    def classBody (L : LogicCode S) (K : QuantifierCode S) (T G y : Expr S) :=
    …

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

66. def OAI.PureTypeSystem.Labelled.ChannelCode.classPred line 554
67. def OAI.PureTypeSystem.Labelled.ChannelCode.unionBody line 556
68. def OAI.PureTypeSystem.Labelled.ChannelCode.unionPred line 558
69. theorem OAI.PureTypeSystem.Labelled.ChannelCode.classBody_rename line 561
70. theorem OAI.PureTypeSystem.Labelled.ChannelCode.classBody_instantiate line 569
71. theorem OAI.PureTypeSystem.Labelled.ChannelCode.unionBody_instantiate line 576
72. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.classBody_family line 590
73. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.unionBody_family line 601
74. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.classPred_typed line 607
75. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.unionPred_typed line 614
76. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.class_evaluation line 622
77. def OAI.PureTypeSystem.Labelled.LogicCode.negBody line 645
78. def OAI.PureTypeSystem.Labelled.LogicCode.ex line 646
79. theorem OAI.PureTypeSystem.Labelled.LogicCode.negBody_rename line 647
80. theorem OAI.PureTypeSystem.Labelled.LogicCode.negBody_instantiate line 651
81. theorem OAI.PureTypeSystem.Labelled.LogicCode.negBody_subst line 653
82. theorem OAI.PureTypeSystem.Labelled.LogicCode.ex_rename line 658
83. theorem OAI.PureTypeSystem.Labelled.LogicCode.ex_subst line 661
84. theorem OAI.PureTypeSystem.Labelled.LogicSetup.ex_formula line 672
85. theorem OAI.PureTypeSystem.Labelled.LogicSetup.ex_intro line 676
86. theorem OAI.PureTypeSystem.Labelled.LogicSetup.ex_elim line 702

    Source documentation

    The elimination target has no free locally opened witness. Its callback is uniform over every future embedding, preserving the source freshness condition.

    theorem ex_elim (hB : L.Formula B) (hp : Proves P Γ γ (L.code.ex K.code T Q))
        (hh : ∀ Δ δ (e : Embedding P Γ γ Δ δ) a,
          HasType P Δ a (T.rename e.names) → WellModed δ a .data →
          Proves P Δ δ ((Q.rename (Expr.liftRen e.names)).instantiate a) →
          Proves P Δ δ (B.rename e.names)) : Proves P Γ γ B := by
    …

    Mentions: OAI.PureTypeSystem.Labelled.Proves, OAI.PureTypeSystem.Labelled.Embedding, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.Expr.liftRen

87. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_map_future line 750

    Source documentation

    Explicit uniform quantifier transport; no fixture of local witnesses leaks.

    theorem all_map_future
        (hh : ∀ Δ δ (e : Embedding P Γ γ Δ δ) a,
          HasType P Δ a (T.rename e.names) → WellModed δ a .data →
          Proves P Δ δ ((Q.rename (Expr.liftRen e.names)).instantiate a) →
          Proves P Δ δ ((R.rename (Expr.liftRen e.names)).instantiate a))
        (hp : Proves P Γ γ (K.code.all T Q)) : Proves P Γ γ (K.code.all T R) := by
    …

    Mentions: OAI.PureTypeSystem.Labelled.Embedding, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.Proves, OAI.PureTypeSystem.Labelled.Expr.liftRen

88. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_equivalent_future line 764
89. theorem OAI.PureTypeSystem.Labelled.LogicSetup.ex_equivalent_future line 795
90. theorem OAI.PureTypeSystem.Labelled.ChannelCode.pred_rename line 814
91. def OAI.PureTypeSystem.Labelled.ChannelCode.evalBody line 819
92. def OAI.PureTypeSystem.Labelled.ChannelCode.predCompareBody line 820
93. def OAI.PureTypeSystem.Labelled.ChannelCode.predCompare line 822
94. theorem OAI.PureTypeSystem.Labelled.ChannelCode.evalBody_rename line 825
95. theorem OAI.PureTypeSystem.Labelled.ChannelCode.evalBody_instantiate line 831
96. theorem OAI.PureTypeSystem.Labelled.ChannelCode.evalBody_subst line 835
97. theorem OAI.PureTypeSystem.Labelled.ChannelCode.predCompareBody_rename line 840
98. theorem OAI.PureTypeSystem.Labelled.ChannelCode.predCompareBody_subst line 845
99. theorem OAI.PureTypeSystem.Labelled.ChannelCode.predCompareBody_instantiate line 851
100. theorem OAI.PureTypeSystem.Labelled.ChannelCode.predCompare_rename line 857
101. theorem OAI.PureTypeSystem.Labelled.ChannelCode.predCompare_subst line 861
102. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.evalBody_family line 871
103. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.predCompareBody_family line 878
104. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.predCompare_formula line 884
105. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.predCompare_elim line 892
106. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.predCompare_intro line 904
107. theorem OAI.PureTypeSystem.Labelled.LogicSetup.disj_equivalent line 932
108. theorem OAI.PureTypeSystem.Labelled.ChannelCode.classPred_rename line 941
109. theorem OAI.PureTypeSystem.Labelled.ChannelCode.unionBody_rename line 946
110. theorem OAI.PureTypeSystem.Labelled.ChannelCode.unionPred_rename line 952
111. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.union_evaluation line 966
112. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.class_comparison line 993