OAI/Computability/TypeSystem/Logic.lean

GitHub source file

283 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.of_path line 15
2. structure OAI.PureTypeSystem.Labelled.QuantifierRoute line 22

   Source documentation

   Quantification uses the displayed direct-vertex annotation throughout.

   structure QuantifierRoute {Γ : List (Expr S)} {γ : Nat → Mode}
       (W : WitnessFamily P Γ γ) (C : Set (Set S)) (b I : Set S) where
   …

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

3. def OAI.PureTypeSystem.Labelled.QuantifierRoute.rename line 35
4. theorem OAI.PureTypeSystem.Labelled.QuantifierRoute.exists_route line 45
5. structure OAI.PureTypeSystem.Labelled.LogicSetup line 56

   Source documentation

   Actual finite ambient context data for the source's classical logical calculus. All fields are constructed below from fixed graph paths and terms.

   structure LogicSetup (P : Specification S) (Γ : List (Expr S)) (γ : Nat → Mode)
       (C : Set (Set S)) where
   …

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

6. def OAI.PureTypeSystem.Labelled.LogicSetup.rename line 79
7. def OAI.PureTypeSystem.Labelled.LogicSetup.bottom line 97
8. theorem OAI.PureTypeSystem.Labelled.LogicSetup.terminal_base line 99
9. def OAI.PureTypeSystem.Labelled.LogicSetup.Formula line 102
10. theorem OAI.PureTypeSystem.Labelled.LogicSetup.Formula.rename line 105
11. theorem OAI.PureTypeSystem.Labelled.LogicSetup.bottom_formula line 109
12. theorem OAI.PureTypeSystem.Labelled.LogicSetup.exists_setup line 115

    Source documentation

    The ambient proof declarations are only the actual terminal converters, and hence the no-normal-proof criterion applies to the eventual bottom inhabitant.

    theorem exists_setup [Fintype S] (C : Set (Set S)) (hC : IsComponent (PrimaryEdge P) C)
        (ho : ∃ r ∈ C, SignedPath (PrimaryEdge P) r r true)
        (ht : ∃ I J K, ProfileTriple P I J K ∧ I ∈ C ∧ J ∈ C ∧ K ∈ C) :
        ∃ Γ γ, ProofContext Γ γ ∧ Nonempty (LogicSetup P Γ γ C) := by
    …

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.SignedPath, OAI.PureTypeSystem.ProfileTriple, OAI.PureTypeSystem.Labelled.ProofContext, OAI.PureTypeSystem.Labelled.LogicSetup

13. def OAI.PureTypeSystem.Labelled.LogicSetup.imp line 133
14. theorem OAI.PureTypeSystem.Labelled.LogicSetup.imp_rename line 136
15. theorem OAI.PureTypeSystem.Labelled.LogicSetup.bottom_rename line 140
16. theorem OAI.PureTypeSystem.Labelled.LogicSetup.Formula.sorted line 143
17. theorem OAI.PureTypeSystem.Labelled.LogicSetup.raw_imp line 148
18. theorem OAI.PureTypeSystem.Labelled.LogicSetup.imp_formula line 159
19. theorem OAI.PureTypeSystem.Labelled.LogicSetup.imp_intro line 164
20. theorem OAI.PureTypeSystem.Labelled.LogicSetup.imp_elim line 175
21. theorem OAI.PureTypeSystem.Labelled.LogicSetup.imp_intro_future line 187

    Source documentation

    Logical abstraction is uniform in every future typing/mode embedding. This is stronger than a meta-level map on the inhabitants in one context.

    theorem imp_intro_future (hA : L.Formula A) (hB : L.Formula B)
        (h : ∀ (Δ : List (Expr S)) (δ : Nat → Mode) (e : Embedding P Γ γ Δ δ),
          Proves P Δ δ (A.rename e.names) → Proves P Δ δ (B.rename e.names)) :
        Proves P Γ γ (L.imp A B) := by
    …

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

22. theorem OAI.PureTypeSystem.Labelled.LogicSetup.imp_future_iff line 194
23. theorem OAI.PureTypeSystem.Labelled.LogicSetup.explosion line 205

    Source documentation

    Stable extraction plus the actual finite converters gives ex falso.

    theorem explosion (hA : L.Formula A) (hf : Proves P Γ γ L.bottom) : Proves P Γ γ A := by
    …

    Mentions: OAI.PureTypeSystem.Labelled.Proves

24. theorem OAI.PureTypeSystem.Labelled.LogicSetup.dne line 218

    Source documentation

    Double negation elimination uses callbacks at each terminal, and therefore constructs labelled terms for every stable formula, including dependent ones.

    theorem dne (hA : L.Formula A)
        (hw : Proves P Γ γ (L.imp (L.imp A L.bottom) L.bottom)) : Proves P Γ γ A := by
    …

    Mentions: OAI.PureTypeSystem.Labelled.Proves

25. def OAI.PureTypeSystem.Labelled.LogicSetup.all line 252

    Source documentation

    The route is selected by its original direct annotation, not by a later sorting profile of the domain.

    def all (R : QuantifierRoute L.witnesses C L.base I) (T Q : Expr S) : Expr S :=
    …

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

26. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_rename line 255
27. theorem OAI.PureTypeSystem.Labelled.LogicSetup.raw_all line 261
28. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_formula line 279
29. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_intro line 287
30. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_elim line 301
31. theorem OAI.PureTypeSystem.Labelled.Transfer.of_conversion line 328
32. def OAI.PureTypeSystem.Labelled.Equivalent line 335

    Source documentation

    Logical equivalence retains two actual typed open proof transformers. No data term is ever replaced using this relation.

    def Equivalent (P : Specification S) (Γ : List (Expr S)) (γ : Nat → Mode) (A B : Expr S) : Prop :=
    …

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

33. theorem OAI.PureTypeSystem.Labelled.Equivalent.refl line 339
34. theorem OAI.PureTypeSystem.Labelled.Equivalent.symm line 341
35. theorem OAI.PureTypeSystem.Labelled.Equivalent.trans line 342
36. theorem OAI.PureTypeSystem.Labelled.Equivalent.rename line 345
37. theorem OAI.PureTypeSystem.Labelled.Equivalent.of_conversion line 348
38. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.apply_converts line 355
39. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.odd_negative line 364
40. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.edge_negative line 371
41. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.path_negative line 379
42. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.exists_even_negative line 389
43. inductive OAI.PureTypeSystem.Labelled.PositiveDataWrapper line 400

    Source documentation

    A fixed all-positive data path, with its original dummy argument values.

    inductive PositiveDataWrapper (S : Type u)
      | identity
      | step : PositiveDataWrapper S → Expr S → Expr S → PositiveDataWrapper S
    namespace PositiveDataWrapper

    Mentions: OAI.PureTypeSystem.Labelled.Expr

44. def OAI.PureTypeSystem.Labelled.PositiveDataWrapper.apply line 405
45. def OAI.PureTypeSystem.Labelled.PositiveDataWrapper.inject line 409
46. def OAI.PureTypeSystem.Labelled.PositiveDataWrapper.project line 413
47. def OAI.PureTypeSystem.Labelled.PositiveDataWrapper.rename line 417
48. def OAI.PureTypeSystem.Labelled.PositiveDataWrapper.subst line 421
49. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.apply_rename line 425
50. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.inject_rename line 428
51. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.project_rename line 431
52. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.apply_subst line 434
53. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.inject_subst line 437
54. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.project_subst line 440
55. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.rename_comp line 443
56. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.rename_id line 446
57. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.instantiate_raise line 448
58. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.project_reduces line 452
59. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.cancel line 458
60. inductive OAI.PureTypeSystem.Labelled.PositiveDataWrapper.Formed line 464
61. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.Formed.rename line 473
62. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.Formed.path line 480
63. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.Formed.sorted line 490
64. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.Formed.modes line 497
65. theorem OAI.PureTypeSystem.Labelled.PositiveDataWrapper.Formed.typed line 509
66. structure OAI.PureTypeSystem.Labelled.DataTail line 526
67. def OAI.PureTypeSystem.Labelled.DataTail.carrier line 534
68. def OAI.PureTypeSystem.Labelled.DataTail.send line 535
69. def OAI.PureTypeSystem.Labelled.DataTail.read line 536
70. def OAI.PureTypeSystem.Labelled.DataTail.rename line 537
71. def OAI.PureTypeSystem.Labelled.DataTail.subst line 539
72. theorem OAI.PureTypeSystem.Labelled.DataTail.carrier_rename line 542
73. theorem OAI.PureTypeSystem.Labelled.DataTail.send_rename line 544
74. theorem OAI.PureTypeSystem.Labelled.DataTail.read_rename line 547
75. theorem OAI.PureTypeSystem.Labelled.DataTail.carrier_subst line 550
76. theorem OAI.PureTypeSystem.Labelled.DataTail.send_subst line 552
77. theorem OAI.PureTypeSystem.Labelled.DataTail.read_subst line 555
78. theorem OAI.PureTypeSystem.Labelled.DataTail.rename_comp line 558
79. theorem OAI.PureTypeSystem.Labelled.DataTail.rename_id line 561
80. theorem OAI.PureTypeSystem.Labelled.DataTail.instantiate_raise line 563
81. structure OAI.PureTypeSystem.Labelled.DataTail.Formed line 567
82. theorem OAI.PureTypeSystem.Labelled.DataTail.Formed.rename line 580
83. theorem OAI.PureTypeSystem.Labelled.DataTail.Formed.sort_sorted line 587
84. theorem OAI.PureTypeSystem.Labelled.DataTail.Formed.carrier_sorted line 592
85. theorem OAI.PureTypeSystem.Labelled.DataTail.Formed.carrier_mode line 594
86. theorem OAI.PureTypeSystem.Labelled.DataTail.Formed.send_typed line 597
87. theorem OAI.PureTypeSystem.Labelled.DataTail.Formed.read_formula line 602
88. theorem OAI.PureTypeSystem.Labelled.DataTail.Formed.read_send line 610
89. theorem OAI.PureTypeSystem.Labelled.DataTail.Formed.exists_tail line 627
90. inductive OAI.PureTypeSystem.Labelled.DataWrapper line 645

    Source documentation

    A retained data path, with fixed tail codes and fixed positive witnesses.

    inductive DataWrapper (S : Type u) : Bool → Type u
      | identity : DataWrapper S false
      | positive {b} : DataWrapper S b → Expr S → Expr S → DataWrapper S b
      | negative {b} : DataWrapper S b → DataTail S → DataWrapper S (!b)
    namespace DataWrapper

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

91. def OAI.PureTypeSystem.Labelled.DataWrapper.apply line 651
92. def OAI.PureTypeSystem.Labelled.DataWrapper.rename line 656
93. def OAI.PureTypeSystem.Labelled.DataWrapper.subst line 661
94. def OAI.PureTypeSystem.Labelled.DataWrapper.depth line 666
95. theorem OAI.PureTypeSystem.Labelled.DataWrapper.depth_rename line 671
96. def OAI.PureTypeSystem.Labelled.DataWrapper.argRen line 675
97. def OAI.PureTypeSystem.Labelled.DataWrapper.argSub line 676
98. theorem OAI.PureTypeSystem.Labelled.apply_rename line 696
99. theorem OAI.PureTypeSystem.Labelled.apply_subst line 699
100. theorem OAI.PureTypeSystem.Labelled.rename_comp line 702
101. theorem OAI.PureTypeSystem.Labelled.rename_id line 705
102. theorem OAI.PureTypeSystem.Labelled.instantiate_raise line 707
103. theorem OAI.PureTypeSystem.Labelled.argRen_comp line 711
104. theorem OAI.PureTypeSystem.Labelled.rename_build_observe line 715
105. theorem OAI.PureTypeSystem.WitnessFamily.rename_comp line 755
106. theorem OAI.PureTypeSystem.WitnessFamily.rename_refl line 759
107. theorem OAI.PureTypeSystem.LogicSetup.Formula.rename_comp_iff line 767
108. theorem OAI.PureTypeSystem.LogicSetup.Formula.rename_refl_iff line 774
109. def OAI.PureTypeSystem.LogicSetup.Family line 782

     Source documentation

     A raw callback with uniform stable instances in every subsequent context. This is an internal syntax interface, not a hypothesis on the PTS.

     def Family (L : LogicSetup P Γ γ C) (T Q : Expr S) : Prop :=
     …

     Mentions: OAI.PureTypeSystem.Expr

110. theorem OAI.PureTypeSystem.LogicSetup.Family.rename line 789
111. theorem OAI.PureTypeSystem.LogicSetup.Family.instantiate line 800
112. theorem OAI.PureTypeSystem.LogicSetup.Family.opened line 807
113. theorem OAI.PureTypeSystem.LogicSetup.Family.rename_comp_iff line 818
114. def OAI.PureTypeSystem.LogicSetup.DataArg line 828

     Source documentation

     Even builders accept a raw data element; odd builders accept a raw callback.

     def DataArg (L : LogicSetup P Γ γ C) (b : Bool) (T a : Expr S) : Prop :=
     …

     Mentions: OAI.PureTypeSystem.Expr

115. theorem OAI.PureTypeSystem.LogicSetup.DataArg.rename line 833
116. theorem OAI.PureTypeSystem.LogicSetup.DataArg.rename_comp_iff line 839
117. inductive OAI.PureTypeSystem.DataWrapper.Formed line 849
118. theorem OAI.PureTypeSystem.DataWrapper.Formed.rename line 863
119. theorem OAI.PureTypeSystem.DataWrapper.Formed.sorted line 871
120. theorem OAI.PureTypeSystem.DataWrapper.Formed.mode line 879
121. theorem OAI.PureTypeSystem.DataWrapper.Formed.edge line 887
122. theorem OAI.PureTypeSystem.DataWrapper.Formed.path line 899
123. theorem OAI.PureTypeSystem.DataWrapper.Formed.positive_path line 909
124. theorem OAI.PureTypeSystem.DataWrapper.Formed.sound_rename line 925

     Source documentation

     Uniform typing includes all future raw input types, so negative-edge callbacks are checked under their fresh data variable without a closure axiom.

     theorem sound_rename (h : Formed L I J R) :
         ∀ (Δ : List (Expr S)) (δ : Nat → Mode) (e : Embedding P Γ γ Δ δ)
           (T : Expr S), SortedAt P Δ T I → WellModed δ T .data →
         (∀ a, (L.rename e).DataArg b T a →
           HasType P Δ ((R.rename e.names).build T a) ((R.rename e.names).apply T) ∧
           WellModed δ ((R.rename e.names).build T a) .data) ∧
         (∀ w a, HasType P Δ w ((R.rename e.names).apply T) → WellModed δ w .data →
           (L.rename e).DataArg (!b) T a → (L.rename e).Formula ((R.rename e.names).observe T w a)) := by
     …

     Mentions: OAI.PureTypeSystem.DataWrapper.Formed, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType

125. theorem OAI.PureTypeSystem.DataWrapper.Formed.sound line 1006

     Source documentation

     The four displayed operations of the manuscript, on the fixed unrenamed code.

     theorem sound (h : Formed L I J R) {T : Expr S} (hT : SortedAt P Γ T I)
         (mT : WellModed γ T .data) :
         (∀ a, L.DataArg b T a → HasType P Γ (R.build T a) (R.apply T) ∧ WellModed γ (R.build T a) .data) ∧
         (∀ w a, HasType P Γ w (R.apply T) → WellModed γ w .data →
           L.DataArg (!b) T a → L.Formula (R.observe T w a)) := by
     …

     Mentions: OAI.PureTypeSystem.DataWrapper.Formed, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType

126. def OAI.PureTypeSystem.DataWrapper.reindex line 1034

     Source documentation

     Concatenate retained wrapper syntax, never selecting new positive witnesses.

     def reindex {b c : Bool} (h : b = c) (R : DataWrapper S b) : DataWrapper S c := h ▸ R

127. theorem OAI.PureTypeSystem.DataWrapper.apply_reindex line 1035
128. theorem OAI.PureTypeSystem.DataWrapper.rename_reindex line 1037
129. def OAI.PureTypeSystem.DataWrapper.append line 1040
130. theorem OAI.PureTypeSystem.DataWrapper.apply_append line 1045
131. theorem OAI.PureTypeSystem.DataWrapper.append_rename line 1052
132. theorem OAI.PureTypeSystem.DataWrapper.Formed.reindex line 1060
133. theorem OAI.PureTypeSystem.DataWrapper.Formed.append line 1067
134. inductive FiniteClassical.Formula line 1081
135. def FiniteClassical.Formula.neg line 1088
136. def FiniteClassical.Formula.eval line 1089
137. def FiniteClassical.Formula.sign line 1094
138. def FiniteClassical.Formula.support line 1096
139. inductive FiniteClassical.Derives line 1104
140. theorem FiniteClassical.Derives.mono line 1113
141. theorem FiniteClassical.Derives.weaken line 1120
142. theorem FiniteClassical.Derives.cut line 1123
143. theorem FiniteClassical.Derives.absurd line 1136
144. theorem FiniteClassical.Derives.by_cases line 1139
145. theorem FiniteClassical.Derives.signed line 1158

     Source documentation

     The signed recursive branch of the source's truth-table compiler.

     theorem signed [DecidableEq α] (v : α → Bool) (A : Formula α)
         (h : ∀ a ∈ A.support, Derives Γ ((Formula.atom a).sign (v a))) :
         Derives Γ (A.sign (A.eval v)) := by
     …

     Mentions: FiniteClassical.Formula, FiniteClassical.Derives

146. theorem FiniteClassical.Derives.branch line 1178

     Source documentation

     Exhaustive finite case elimination, with no evaluation reflection axiom.

     theorem branch [DecidableEq α] (s : Finset α)
         (h : ∀ v : α → Bool, Derives ((fun A => ∃ a ∈ s, A = (Formula.atom a).sign (v a)) ∪ Γ) R) :
         Derives Γ R := by
     …

     Mentions: FiniteClassical.Derives

147. theorem FiniteClassical.Derives.tautology line 1219

     Source documentation

     Boolean truth-table validity compiles to a finite typed-use derivation.

     theorem tautology [DecidableEq α] (A : Formula α) (h : ∀ v, A.eval v = true) : Derives Γ A := by
     …

     Mentions: FiniteClassical.Formula, FiniteClassical.Derives

148. def PureTypeSystem.Labelled.LogicSetup.interpret line 1236
149. theorem PureTypeSystem.Labelled.LogicSetup.interpret_rename line 1241
150. theorem PureTypeSystem.Labelled.LogicSetup.interpret_formula line 1249
151. theorem PureTypeSystem.Labelled.LogicSetup.propositional_sound line 1258

     Source documentation

     Compilation of every node of the finite classical derivation to actual labelled typing/proof-mode judgments.

      theorem propositional_sound {Ξ : Set (FiniteClassical.Formula α)} {F : FiniteClassical.Formula α}
         (h : FiniteClassical.Derives Ξ F) (a : α → Expr S) (ha : ∀ i, L.Formula (a i))
         (hp : ∀ Q ∈ Ξ, Proves P Γ γ (L.interpret a Q)) : Proves P Γ γ (L.interpret a F) := by
     …

     Mentions: FiniteClassical.Formula, FiniteClassical.Derives

152. theorem PureTypeSystem.Labelled.LogicSetup.propositional_tautology line 1276
153. def FiniteClassical.Formula.top line 1286
154. def FiniteClassical.Formula.conj line 1287
155. def FiniteClassical.Formula.disj line 1288
156. def FiniteClassical.Formula.iff line 1289
157. def FiniteClassical.Formula.chain line 1290
158. def PureTypeSystem.Labelled.LogicSetup.top line 1301
159. def PureTypeSystem.Labelled.LogicSetup.neg line 1302
160. def PureTypeSystem.Labelled.LogicSetup.conj line 1303
161. def PureTypeSystem.Labelled.LogicSetup.disj line 1304
162. def PureTypeSystem.Labelled.LogicSetup.iff line 1305
163. theorem PureTypeSystem.Labelled.LogicSetup.top_formula line 1307
164. theorem PureTypeSystem.Labelled.LogicSetup.neg_formula line 1308
165. theorem PureTypeSystem.Labelled.LogicSetup.conj_formula line 1309
166. theorem PureTypeSystem.Labelled.LogicSetup.disj_formula line 1311
167. theorem PureTypeSystem.Labelled.LogicSetup.iff_formula line 1313
168. theorem PureTypeSystem.Labelled.LogicSetup.top_rename line 1316
169. theorem PureTypeSystem.Labelled.LogicSetup.neg_rename line 1318
170. theorem PureTypeSystem.Labelled.LogicSetup.conj_rename line 1321
171. theorem PureTypeSystem.Labelled.LogicSetup.disj_rename line 1324
172. theorem PureTypeSystem.Labelled.LogicSetup.iff_rename line 1327
173. theorem PureTypeSystem.Labelled.LogicSetup.propositional_consequence line 1332

     Source documentation

     Arbitrary finite propositional chaining, compiled to actual open terms.

     theorem propositional_consequence {α : Type v} (a : α → Expr S) (ha : ∀ i, L.Formula (a i))
         (hs : List (FiniteClassical.Formula α)) (Q : FiniteClassical.Formula α)
         (hv : ∀ v, (FiniteClassical.Formula.chain hs Q).eval v = true)
         (hp : ∀ R ∈ hs, Proves P Γ γ (L.interpret a R)) :
         Proves P Γ γ (L.interpret a Q) := by
     …

     Mentions: FiniteClassical.Formula, FiniteClassical.Formula.chain

174. theorem PureTypeSystem.Labelled.LogicSetup.top_intro line 1346
175. theorem PureTypeSystem.Labelled.LogicSetup.conj_intro line 1350
176. theorem PureTypeSystem.Labelled.LogicSetup.conj_left line 1364
177. theorem PureTypeSystem.Labelled.LogicSetup.conj_right line 1376
178. theorem PureTypeSystem.Labelled.LogicSetup.iff_of_equivalent line 1388
179. theorem PureTypeSystem.Labelled.LogicSetup.equivalent_of_iff line 1393
180. theorem PureTypeSystem.Labelled.Converts.app line 1408
181. theorem PureTypeSystem.Labelled.ProofWrapper.subst_rename line 1415
182. theorem PureTypeSystem.Labelled.ProofWrapper.rename_subst line 1418
183. theorem PureTypeSystem.Labelled.PositiveDataWrapper.subst_rename line 1423
184. theorem PureTypeSystem.Labelled.PositiveDataWrapper.rename_subst line 1426
185. theorem PureTypeSystem.Labelled.PositiveDataWrapper.project_converts line 1429
186. theorem PureTypeSystem.Labelled.DataTail.subst_rename line 1436
187. theorem PureTypeSystem.Labelled.DataTail.rename_subst line 1440
188. theorem PureTypeSystem.Labelled.DataTail.read_converts line 1444
189. theorem PureTypeSystem.Labelled.DataWrapper.subst_rename line 1449
190. theorem PureTypeSystem.Labelled.DataWrapper.rename_subst line 1452
191. theorem PureTypeSystem.Labelled.DataWrapper.argSub_shift line 1456
192. theorem PureTypeSystem.Labelled.DataWrapper.subst_build_observe line 1467
193. theorem PureTypeSystem.Labelled.DataWrapper.observe_converts line 1496
194. theorem PureTypeSystem.Labelled.DataWrapper.observe_open line 1504

     Source documentation

     The exact substitution equation exposed by a negative-edge beta step.

     theorem observe_open {b} (R : DataWrapper S b) (T a v : Expr S) :
         ((R.rename Nat.succ).observe (T.rename Nat.succ) (.var 0)
           (a.rename (argRen (!b) Nat.succ))).instantiate v = R.observe T v a := by
     …

195. theorem PureTypeSystem.Labelled.DataWrapper.build_rename line 1519
196. theorem PureTypeSystem.Labelled.DataWrapper.observe_rename line 1522
197. theorem PureTypeSystem.Labelled.DataWrapper.build_subst line 1525
198. theorem PureTypeSystem.Labelled.DataWrapper.observe_subst line 1528
199. def PureTypeSystem.Labelled.Expr.compose line 1535

     Source documentation

     Composition of one-variable open terms, preserving the common ambient context. No logical equivalence is used as a data equality.

     def compose (f g : Expr S) : Expr S := (f.rename (liftRen Nat.succ)).instantiate g

200. theorem PureTypeSystem.Labelled.Expr.compose_instantiate line 1537
201. theorem PureTypeSystem.Labelled.Expr.compose_rename line 1546
202. def PureTypeSystem.Labelled.DataMap line 1557

     Source documentation

     An ordinary raw data callback. Its uniformity is a consequence of the already proved labelled substitution theorem.

     def DataMap (P : Specification S) (Γ : List (Expr S)) (γ : Nat → Mode)
         (T U f : Expr S) : Prop :=
     …

203. theorem PureTypeSystem.Labelled.DataMap.apply line 1563
204. theorem PureTypeSystem.Labelled.DataMap.rename line 1569
205. theorem PureTypeSystem.Labelled.LogicSetup.Family.compose line 1580
206. def PureTypeSystem.Labelled.DataWrapper.evalCallback line 1590
207. theorem PureTypeSystem.Labelled.DataWrapper.evalCallback_instantiate line 1593
208. theorem PureTypeSystem.Labelled.DataWrapper.evalCallback_rename line 1598
209. theorem PureTypeSystem.Labelled.DataWrapper.Formed.evalCallback_family line 1609
210. def PureTypeSystem.Labelled.DataWrapper.reencode line 1619
211. theorem PureTypeSystem.Labelled.DataWrapper.reencode_rename line 1622
212. theorem PureTypeSystem.Labelled.DataWrapper.Formed.reencode_typed line 1630
213. def PureTypeSystem.Labelled.DataWrapper.cancelFormula line 1637
214. theorem PureTypeSystem.Labelled.DataWrapper.cancelFormula_swap line 1640
215. theorem PureTypeSystem.Labelled.DataWrapper.negative_beta line 1643
216. theorem PureTypeSystem.Labelled.DataWrapper.Formed.cancellation line 1662
217. theorem PureTypeSystem.Labelled.Expr.compose_subst line 1706
218. theorem PureTypeSystem.Labelled.DataWrapper.evalCallback_subst line 1719
219. theorem PureTypeSystem.Labelled.DataWrapper.reencode_subst line 1727
220. def PureTypeSystem.Labelled.DataWrapper.reencodeBody line 1731
221. theorem PureTypeSystem.Labelled.DataWrapper.reencodeBody_instantiate line 1734
222. theorem PureTypeSystem.Labelled.DataWrapper.reencodeBody_rename line 1739
223. theorem PureTypeSystem.Labelled.DataWrapper.Formed.reencode_map line 1750
224. theorem PureTypeSystem.Labelled.DataWrapper.Formed.reencode_evaluation line 1761
225. structure PureTypeSystem.Labelled.LogicCode line 1773

     Source documentation

     Raw code for the already constructed logical operations. This separates syntax naturality from the dependent typing certificate of a logic setup.

     structure LogicCode (S : Type u) where
     …

226. def PureTypeSystem.Labelled.LogicCode.rename line 1779
227. def PureTypeSystem.Labelled.LogicCode.subst line 1780
228. def PureTypeSystem.Labelled.LogicCode.imp line 1781
229. def PureTypeSystem.Labelled.LogicCode.neg line 1782
230. def PureTypeSystem.Labelled.LogicCode.top line 1783
231. def PureTypeSystem.Labelled.LogicCode.conj line 1784
232. def PureTypeSystem.Labelled.LogicCode.disj line 1785
233. def PureTypeSystem.Labelled.LogicCode.iff line 1786
234. def PureTypeSystem.Labelled.LogicCode.cond line 1787
235. def PureTypeSystem.Labelled.LogicCode.sign line 1788
236. theorem PureTypeSystem.Labelled.LogicCode.rename_comp line 1790
237. theorem PureTypeSystem.Labelled.LogicCode.instantiate_raise line 1792
238. theorem PureTypeSystem.Labelled.LogicCode.rename_lift_instantiate line 1794
239. theorem PureTypeSystem.Labelled.LogicCode.imp_rename line 1801
240. theorem PureTypeSystem.Labelled.LogicCode.imp_subst line 1804
241. theorem PureTypeSystem.Labelled.LogicCode.neg_rename line 1807
242. theorem PureTypeSystem.Labelled.LogicCode.neg_subst line 1810
243. theorem PureTypeSystem.Labelled.LogicCode.top_rename line 1813
244. theorem PureTypeSystem.Labelled.LogicCode.top_subst line 1815
245. theorem PureTypeSystem.Labelled.LogicCode.conj_rename line 1817
246. theorem PureTypeSystem.Labelled.LogicCode.conj_subst line 1820
247. theorem PureTypeSystem.Labelled.LogicCode.disj_rename line 1823
248. theorem PureTypeSystem.Labelled.LogicCode.disj_subst line 1826
249. theorem PureTypeSystem.Labelled.LogicCode.iff_rename line 1829
250. theorem PureTypeSystem.Labelled.LogicCode.iff_subst line 1832
251. theorem PureTypeSystem.Labelled.LogicCode.cond_rename line 1835
252. theorem PureTypeSystem.Labelled.LogicCode.cond_subst line 1838
253. theorem PureTypeSystem.Labelled.LogicCode.sign_rename line 1841
254. theorem PureTypeSystem.Labelled.LogicCode.sign_subst line 1844
255. theorem PureTypeSystem.Labelled.LogicCode.sign_instantiate_raise line 1847
256. def PureTypeSystem.Labelled.LogicSetup.code line 1854
257. theorem PureTypeSystem.Labelled.LogicSetup.code_rename line 1855
258. theorem PureTypeSystem.Labelled.LogicSetup.cond_formula line 1856
259. theorem PureTypeSystem.Labelled.LogicSetup.sign_formula line 1859
260. theorem PureTypeSystem.Labelled.LogicSetup.Family.constant line 1866
261. theorem PureTypeSystem.Labelled.LogicSetup.Family.code_imp line 1873
262. theorem PureTypeSystem.Labelled.LogicSetup.Family.code_neg line 1880
263. theorem PureTypeSystem.Labelled.LogicSetup.Family.code_sign line 1883
264. theorem PureTypeSystem.Labelled.LogicSetup.Family.code_conj line 1888
265. theorem PureTypeSystem.Labelled.LogicSetup.Family.code_disj line 1892
266. theorem PureTypeSystem.Labelled.LogicSetup.Family.code_iff line 1896
267. theorem PureTypeSystem.Labelled.LogicSetup.Family.code_cond line 1900
268. def PureTypeSystem.Labelled.DataWrapper.contraCallback line 1908

     Source documentation

     The other slot of odd evaluation, exposed as an actual raw callback.

     def contraCallback (R : DataWrapper S true) (T t : Expr S) : Expr S :=
     …

269. theorem PureTypeSystem.Labelled.DataWrapper.contraCallback_instantiate line 1911
270. theorem PureTypeSystem.Labelled.DataWrapper.contraCallback_rename line 1916
271. theorem PureTypeSystem.Labelled.DataWrapper.contraCallback_subst line 1923
272. theorem PureTypeSystem.Labelled.DataWrapper.Formed.contraCallback_family line 1934
273. inductive PTSPropositional.Node line 1951
274. def PTSPropositional.Node.neg line 1956
275. def PTSPropositional.Node.conj line 1957
276. def PTSPropositional.Node.disj line 1958
277. def PTSPropositional.Node.iff line 1959
278. def PTSPropositional.reify line 1961
279. def PTSPropositional.Node.syntax line 1996
280. def PTSPropositional.atomFunction line 2001
281. def PTSPropositional.truthCases line 2009
282. def PTSPropositional.memCases line 2017
283. def PTSPropositional.formulaProof line 2028