OAI/Computability/TypeSystem/Values.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

The actual candidate bases and the three kinds of observation values. Plain indices retain their exact normalized expression tag. All coordinates are candidates, rather than arbitrary sets of terms.

  1. theorem OAI.PureTypeSystem.PrimaryEdge.target_feasible line 14
  2. theorem OAI.PureTypeSystem.ObservationLayers.nonempty line 23
  3. theorem OAI.PureTypeSystem.ActiveLayer.nonempty line 32
  4. theorem OAI.PureTypeSystem.ActiveLayer.classify line 34
  5. abbrev OAI.PureTypeSystem.ObservationValues.Candidate line 49
  6. abbrev OAI.PureTypeSystem.ObservationValues.ActualType line 50
  7. abbrev OAI.PureTypeSystem.ObservationValues.Base line 51
  8. def OAI.PureTypeSystem.ObservationValues.topBase line 53
  9. def OAI.PureTypeSystem.ObservationValues.Base.update line 56

    Source documentation

    The exact coordinate update used at product syntax.

    noncomputable def Base.update (b : Base Ω) (T : ActualType Ω) (A : Candidate Ω T.val) : Base Ω :=
…

    Mentions: OAI.PureTypeSystem.ObservationValues.Base, OAI.PureTypeSystem.ObservationValues.ActualType, OAI.PureTypeSystem.ObservationValues.Candidate

  10. theorem OAI.PureTypeSystem.ObservationValues.Base.update_same line 59
  11. theorem OAI.PureTypeSystem.ObservationValues.Base.update_other line 62
  12. abbrev OAI.PureTypeSystem.ObservationValues.PlainValue line 68
  13. abbrev OAI.PureTypeSystem.ObservationValues.Plus line 69
  14. abbrev OAI.PureTypeSystem.ObservationValues.Minus line 70
  15. inductive OAI.PureTypeSystem.ObservationValues.RawValue line 72
  16. def OAI.PureTypeSystem.ObservationValues.Fits line 78

    Source documentation

    The tag and sign checks for an actual normalized type.

    def Fits (T : Expr S) : RawValue (hw := hw) Ω C hno → Prop
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ObservationValues.RawValue

  17. abbrev OAI.PureTypeSystem.ObservationValues.Value line 83
  18. structure OAI.PureTypeSystem.ObservationValues.ActiveType line 85
  19. abbrev OAI.PureTypeSystem.ObservationValues.ActiveType.ofActual line 93
  20. def OAI.PureTypeSystem.ObservationValues.ActiveType.actual line 105
  21. def OAI.PureTypeSystem.ObservationValues.plainDefault line 108
  22. def OAI.PureTypeSystem.ObservationValues.distinguished line 111
  23. def OAI.PureTypeSystem.ObservationValues.RawValue.base line 124
  24. def OAI.PureTypeSystem.ObservationValues.withBase line 130

    Source documentation

    Updating only the base keeps every nonempty observation unchanged.

    noncomputable def withBase (T : ActiveType Ω C) (b : Base Ω) : Value (hw := hw) Ω C hno T.type := by
…

    Mentions: OAI.PureTypeSystem.ObservationValues.ActiveType, OAI.PureTypeSystem.ObservationValues.Base, OAI.PureTypeSystem.ObservationValues.Value

  25. theorem OAI.PureTypeSystem.ObservationValues.withBase_base line 145
  26. def OAI.PureTypeSystem.ObservationValues.project line 157

    Source documentation

    Invalid exit tags receive exactly the distinguished target.

    noncomputable def project (T : ActiveType Ω C) (v : RawValue (hw := hw) Ω C hno) : Value (hw := hw) Ω C hno T.type :=
…

    Mentions: OAI.PureTypeSystem.ObservationValues.ActiveType, OAI.PureTypeSystem.ObservationValues.RawValue, OAI.PureTypeSystem.ObservationValues.Value

  27. theorem OAI.PureTypeSystem.ObservationValues.project_valid line 160
  28. def OAI.PureTypeSystem.ObservationValues.RawValue.LevelEq line 175
  29. def OAI.PureTypeSystem.ObservationValues.RawValue.Bounded line 181
  30. theorem OAI.PureTypeSystem.ObservationValues.RawValue.level_refl line 186
  31. theorem OAI.PureTypeSystem.ObservationValues.RawValue.level_mono line 189
  32. theorem OAI.PureTypeSystem.ObservationValues.RawValue.bounded_mono line 194
  33. theorem OAI.PureTypeSystem.ObservationValues.RawValue.exists_bound line 199
  34. theorem OAI.PureTypeSystem.ObservationValues.RawValue.level_base line 205
  35. theorem OAI.PureTypeSystem.FreeLayer.path_sign line 218
  36. structure OAI.PureTypeSystem.ObservationValues.FrameKey line 230

    Source documentation

    A frame's key has the exact normalized domain and active target.

    structure FrameKey (T : ActiveType Ω C) where
…

    Mentions: OAI.PureTypeSystem.ObservationValues.ActiveType

  37. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.sorted line 242
  38. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.domain_normal line 245
  39. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.body_normal line 247
  40. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.domain_sorted line 249
  41. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.target_sorted line 253
  42. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.profile_data line 259
  43. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.target_path line 269
  44. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.domain_active line 275
  45. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.domain_edge line 280
  46. def OAI.PureTypeSystem.ObservationValues.FrameKey.target line 285
  47. def OAI.PureTypeSystem.ObservationValues.FrameKey.domainType line 295
  48. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.plain_target line 298
  49. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.plain_domain line 302
  50. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.free_target_sign line 306
  51. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.free_domain_sign line 313
  52. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.domain_direct line 321

    Source documentation

    The third binder fact: quantified active payloads in a component's product candidate are direct and hence can never be free minus.

    theorem domain_direct (hC : IsComponent (PrimaryEdge P) C)
    (hK : Ω.profile T.type ∈ C) (hL : Ω.profile (a.target hw).type ∈ C)
    (hd : ActiveLayer P C (Ω.profile a.domain)) : DirectLayer P C (Ω.profile a.domain) := by
…

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.ActiveLayer, OAI.PureTypeSystem.DirectLayer

  53. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.domain_not_minus line 330
  54. def OAI.PureTypeSystem.ObservationValues.PayloadFits line 340

    Source documentation

    Absence is mandatory at inactive domains. There are no latent values.

    def PayloadFits (D : Expr S) (p : Option (RawValue (hw := hw) Ω C hno)) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ObservationValues.RawValue

  55. theorem OAI.PureTypeSystem.ObservationValues.Fits.active line 347
  56. abbrev OAI.PureTypeSystem.ObservationValues.PlusFrame line 354
  57. abbrev OAI.PureTypeSystem.ObservationValues.MinusFrame line 356
  58. def OAI.PureTypeSystem.ObservationValues.plusPayload line 359
  59. def OAI.PureTypeSystem.ObservationValues.minusPayload line 365
  60. def OAI.PureTypeSystem.ObservationValues.Gate line 372

    Source documentation

    Exact gates for continue/exit operations at free lambdas.

    def Gate (T : ActiveType Ω C) (q : Expr S)
    (p : Option (RawValue (hw := hw) Ω C hno)) (exit : Bool) : Prop :=
…

    Mentions: OAI.PureTypeSystem.ObservationValues.ActiveType, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ObservationValues.RawValue

  61. theorem OAI.PureTypeSystem.Converts.app line 381
  62. theorem OAI.PureTypeSystem.Converts.lam line 387
  63. theorem OAI.PureTypeSystem.Expr.Scoped.subst_converts line 396
  64. theorem OAI.PureTypeSystem.Lookup.exists_of_lt line 415
  65. theorem OAI.PureTypeSystem.Lookup.unique line 425
  66. theorem OAI.PureTypeSystem.ContextTower.HasType.actual_type line 435
  67. theorem OAI.PureTypeSystem.ContextTower.HasType.actual_expression line 441
  68. def OAI.PureTypeSystem.ObservationValues.Parameter.Bounded line 453
  69. def OAI.PureTypeSystem.ObservationValues.Parameter.LevelEq line 456
  70. theorem OAI.PureTypeSystem.ObservationValues.Parameter.level_refl line 462
  71. theorem OAI.PureTypeSystem.ObservationValues.Parameter.level_mono line 467
  72. theorem OAI.PureTypeSystem.ObservationValues.Parameter.bounded_mono line 472
  73. theorem OAI.PureTypeSystem.ObservationValues.Parameter.exists_bound line 475
  74. structure OAI.PureTypeSystem.ObservationValues.Environment line 485

    Source documentation

    Typed raw substitutions with precisely one observation parameter per active actual declaration and none at inactive declarations.

    structure Environment (Γ : List (Expr S)) where
…

    Mentions: OAI.PureTypeSystem.Expr

  75. def OAI.PureTypeSystem.ObservationValues.Environment.Bounded line 494
  76. def OAI.PureTypeSystem.ObservationValues.Environment.ImageCompatible line 496
  77. def OAI.PureTypeSystem.ObservationValues.Environment.LevelEq line 499
  78. theorem OAI.PureTypeSystem.ObservationValues.Environment.bounded_mono line 502
  79. theorem OAI.PureTypeSystem.ObservationValues.Environment.exists_bound line 505
  80. theorem OAI.PureTypeSystem.ObservationValues.Environment.level_refl line 519
  81. theorem OAI.PureTypeSystem.ObservationValues.Environment.level_mono line 522
  82. def OAI.PureTypeSystem.ObservationValues.Environment.cons line 527

    Source documentation

    Binding a raw actual term does not normalize or evaluate its syntax.

    def cons {A a : Expr S} (ha : Ω.HasType a (A.subst e.images))
    (p : Option (RawValue (hw := hw) Ω C hno))
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ObservationValues.RawValue

  83. theorem OAI.PureTypeSystem.ObservationValues.Environment.bounded_cons line 540
  84. theorem OAI.PureTypeSystem.ObservationValues.Environment.actual_expr_eq line 550
  85. theorem OAI.PureTypeSystem.ObservationValues.Environment.actual_type_eq line 557
  86. theorem OAI.PureTypeSystem.WeaklyNormalizing.pi_domain line 568
  87. theorem OAI.PureTypeSystem.WeaklyNormalizing.pi_body line 572
  88. theorem OAI.PureTypeSystem.Expr.instantiate_liftSub line 580
  89. theorem OAI.PureTypeSystem.ContextTower.HasType.denormalize_type line 593
  90. theorem OAI.PureTypeSystem.ObservationValues.PayloadFits.exists_of_actual line 605
  91. structure OAI.PureTypeSystem.ObservationValues.ProductInstance line 613

    Source documentation

    A product's exact stored formation data and its raw environment.

    structure ProductInstance where
…
  92. def OAI.PureTypeSystem.ObservationValues.ProductInstance.rawDomain line 627
  93. def OAI.PureTypeSystem.ObservationValues.ProductInstance.rawBody line 628
  94. def OAI.PureTypeSystem.ObservationValues.ProductInstance.domainNF line 629
  95. def OAI.PureTypeSystem.ObservationValues.ProductInstance.bodyNF line 630
  96. def OAI.PureTypeSystem.ObservationValues.ProductInstance.rawTarget line 631
  97. def OAI.PureTypeSystem.ObservationValues.ProductInstance.targetNF line 633
  98. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.rawDomain_typed line 635
  99. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.rawProduct_typed line 638
  100. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.domain_typed line 641
  101. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.domain_normal line 643
  102. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.body_normal line 645
  103. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.product_nf line 648
  104. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.product_typed line 652
  105. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.rawArgument line 656
  106. def OAI.PureTypeSystem.ObservationValues.ProductInstance.extend line 659
  107. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.rawTarget_typed line 664
  108. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.target_typed line 668
  109. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.target_normal line 671
  110. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.target_eq line 674
  111. def OAI.PureTypeSystem.ObservationValues.ProductInstance.testers line 684

    Source documentation

    The tester set uses the domain Read precisely at this primary component.

    noncomputable def testers (d : Candidate Ω t.domainNF) : Set (Expr S) :=
…

    Mentions: OAI.PureTypeSystem.ObservationValues.Candidate, OAI.PureTypeSystem.Expr

  112. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.testers_top line 687
  113. abbrev OAI.PureTypeSystem.ObservationValues.ProductInstance.BodyReads line 695

    Source documentation

    Every raw tester and every matching payload has its own body Read. This quantification is over all payloads, not only semantic realizers.

    abbrev BodyReads := ∀ (n : Expr S), Ω.HasType n t.domainNF →
…

    Mentions: OAI.PureTypeSystem.Expr

  114. def OAI.PureTypeSystem.ObservationValues.ProductInstance.fibers line 698
  115. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.fibers_candidate line 705
  116. def OAI.PureTypeSystem.ObservationValues.ProductInstance.candidate line 718
  117. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.candidate_top line 723
  118. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.candidate_body line 726
  119. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.candidate_outside line 735