OAI/Computability/TypeSystem/Evaluation.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Total observation operations. The minus lambda pack is provisional off the representable behaviors; the finite-bound theorem proves that the evaluator never takes that provisional branch.

  1. theorem OAI.PureTypeSystem.ActualPlain.Node.ext line 14
  2. abbrev OAI.PureTypeSystem.ObservationValues.ActiveType.plainNode line 25
  3. theorem OAI.PureTypeSystem.ObservationValues.ActiveType.ext line 28
  4. def OAI.PureTypeSystem.ObservationValues.Value.plain line 34
  5. theorem OAI.PureTypeSystem.ObservationValues.Value.plain_exists line 37
  6. def OAI.PureTypeSystem.ObservationValues.Value.asPlain line 50
  7. theorem OAI.PureTypeSystem.ObservationValues.Value.plain_asPlain line 53
  8. theorem OAI.PureTypeSystem.ObservationValues.Value.asPlain_plain line 56
  9. theorem OAI.PureTypeSystem.ObservationValues.Value.plus_exists line 61
  10. theorem OAI.PureTypeSystem.ObservationValues.Value.minus_exists line 69
  11. def OAI.PureTypeSystem.ObservationValues.Value.asPlus line 77
  12. def OAI.PureTypeSystem.ObservationValues.Value.asMinus line 79
  13. theorem OAI.PureTypeSystem.ObservationValues.Value.asPlus_spec line 82
  14. theorem OAI.PureTypeSystem.ObservationValues.Value.asMinus_spec line 84
  15. def OAI.PureTypeSystem.ObservationValues.ActualPlainKey.frame line 90
  16. def OAI.PureTypeSystem.ObservationValues.ActualPlainKey.payload line 95

    Source documentation

    Decode a plain frame's unique optional domain coordinate.

    noncomputable def payload {n : ActualPlain.Node Ω C} (a : ActualPlain.Key Ω C n)
    (p : (ActualPlain.schema hw).FrameParameters (ActualPlain.Space (hw := hw) hno (Base Ω)) a) :
…

    Mentions: OAI.PureTypeSystem.ActualPlain.Node, OAI.PureTypeSystem.ActualPlain.Key, OAI.PureTypeSystem.ActualPlain.schema, OAI.PureTypeSystem.ActualPlain.Space, OAI.PureTypeSystem.ObservationValues.Base

  17. theorem OAI.PureTypeSystem.ObservationValues.ActualPlainKey.payload_fits line 102
  18. def OAI.PureTypeSystem.ObservationValues.ActualPlainKey.parameters line 111

    Source documentation

    Encode the matching typed plain payload without changing its tag.

    noncomputable def parameters {n : ActualPlain.Node Ω C} (a : ActualPlain.Key Ω C n)
    (p : Option (RawValue (hw := hw) Ω C hno)) (hp : PayloadFits Ω C hno a.domain p) :
…

    Mentions: OAI.PureTypeSystem.ActualPlain.Node, OAI.PureTypeSystem.ActualPlain.Key, OAI.PureTypeSystem.ObservationValues.RawValue, OAI.PureTypeSystem.ObservationValues.PayloadFits

  19. theorem OAI.PureTypeSystem.ObservationValues.ActualPlainKey.payload_parameters line 125
  20. theorem OAI.PureTypeSystem.ObservationValues.ActualPlainKey.payload_injective line 141
  21. theorem OAI.PureTypeSystem.ObservationValues.ActualPlainKey.parameters_payload line 149
  22. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.ext line 159
  23. abbrev OAI.PureTypeSystem.ObservationValues.FrameKey.plainKey line 169
  24. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.free_target line 174
  25. def OAI.PureTypeSystem.ObservationValues.packMinus line 185

    Source documentation

    A represented minus behavior is packed without changing any observation.

    noncomputable def packMinus
    (t : FreeObservations.Table (Expr S) (PlainValue (hw := hw) Ω C hno) (Base Ω)
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Table, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ObservationValues.PlainValue, OAI.PureTypeSystem.ObservationValues.Base

  26. theorem OAI.PureTypeSystem.ObservationValues.packMinus_spec line 191
  27. theorem OAI.PureTypeSystem.ObservationValues.packMinus_stage line 199
  28. def OAI.PureTypeSystem.ObservationValues.Gate.frame line 222
  29. theorem OAI.PureTypeSystem.ObservationValues.Gate.argument line 224
  30. theorem OAI.PureTypeSystem.ObservationValues.Gate.payload line 225
  31. theorem OAI.PureTypeSystem.ObservationValues.Gate.plain line 227
  32. theorem OAI.PureTypeSystem.ObservationValues.Gate.not_plain line 230
  33. theorem OAI.PureTypeSystem.ObservationValues.Gate.unique line 233
  34. abbrev OAI.PureTypeSystem.ObservationValues.LambdaAction line 237
  35. def OAI.PureTypeSystem.ObservationValues.tagPlain line 241
  36. theorem OAI.PureTypeSystem.ObservationValues.tagPlain_spec line 245
  37. def OAI.PureTypeSystem.ObservationValues.plainLambda line 250

    Source documentation

    The actual plain prefix operation, with the unique optional payload.

    noncomputable def plainLambda (T : ActiveType Ω C) (hp : PlainLayer P C (Ω.profile T.type))
    (act : LambdaAction (hw := hw) Ω C hno T) : Value (hw := hw) Ω C hno T.type := by
…

    Mentions: OAI.PureTypeSystem.ObservationValues.ActiveType, OAI.PureTypeSystem.PlainLayer, OAI.PureTypeSystem.ObservationValues.LambdaAction, OAI.PureTypeSystem.ObservationValues.Value

  38. def OAI.PureTypeSystem.ObservationValues.lambdaExit line 261

    Source documentation

    The same gate is used for plus and minus exits; the opposite payload space differs, but the exact plain target tag is always retained.

    noncomputable def lambdaExit {X : Type u}
    (decode : FreeObservations.Payload (PlainValue (hw := hw) Ω C hno) X →
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Payload, OAI.PureTypeSystem.ObservationValues.PlainValue

  39. def OAI.PureTypeSystem.ObservationValues.plusContinue line 271
  40. def OAI.PureTypeSystem.ObservationValues.minusContinue line 278
  41. def OAI.PureTypeSystem.ObservationValues.plusLambda line 285
  42. def OAI.PureTypeSystem.ObservationValues.minusLambdaBehavior line 295
  43. def OAI.PureTypeSystem.ObservationValues.lambdaValue line 300
  44. def OAI.PureTypeSystem.ObservationValues.FrameKey.plusParameter line 316
  45. def OAI.PureTypeSystem.ObservationValues.FrameKey.minusParameter line 327
  46. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.plusPayload_parameter line 338
  47. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.minusPayload_parameter line 349
  48. def OAI.PureTypeSystem.ObservationValues.exitValue line 361
  49. def OAI.PureTypeSystem.ObservationValues.plainApply line 368

    Source documentation

    Plain application, separated to keep dependent prefix casts abstract.

    noncomputable def plainApply (T : ActiveType Ω C) (hT : PlainLayer P C (Ω.profile T.type))
    (v : Value (hw := hw) Ω C hno T.type) (a : FrameKey Ω C T)
…

    Mentions: OAI.PureTypeSystem.ObservationValues.ActiveType, OAI.PureTypeSystem.PlainLayer, OAI.PureTypeSystem.ObservationValues.Value, OAI.PureTypeSystem.ObservationValues.FrameKey

  50. def OAI.PureTypeSystem.ObservationValues.applyValue line 379

    Source documentation

    Exact application: plain next, free continue slice, or checked exit.

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

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

  51. abbrev OAI.PureTypeSystem.ObservationValues.Environment.actualType line 414
  52. abbrev OAI.PureTypeSystem.ObservationValues.Environment.activeType line 417
  53. abbrev OAI.PureTypeSystem.ObservationValues.Environment.actualExpression line 421
  54. theorem OAI.PureTypeSystem.ObservationValues.Environment.type_convert_eq line 424
  55. theorem OAI.PureTypeSystem.ObservationValues.Environment.expression_convert_eq line 430
  56. def OAI.PureTypeSystem.ObservationValues.ProductInstance.ofFormation line 439
  57. def OAI.PureTypeSystem.ObservationValues.ProductInstance.ofFunction line 454
  58. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.frame_domain line 461
  59. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.frame_body line 464
  60. def OAI.PureTypeSystem.ObservationValues.ProductInstance.frameEnvironment line 467
  61. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.frame_type line 472
  62. def OAI.PureTypeSystem.ObservationValues.ProductInstance.argumentFrame line 481

    Source documentation

    A function's normalized argument frame, formed at the exact stored product, not at an independently chosen derivation of that product.

    noncomputable def argumentFrame {T : ActiveType Ω C} (he : T.type = .pi t.domainNF t.bodyNF)
    {n : Expr S} (hn : Ω.HasType n t.domainNF)
    (ha : ActiveLayer P C (Ω.profile (t.targetNF n))) : FrameKey Ω C T where
…

    Mentions: OAI.PureTypeSystem.ObservationValues.ActiveType, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ActiveLayer, OAI.PureTypeSystem.ObservationValues.FrameKey

  63. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.argumentFrame_type line 504
  64. def OAI.PureTypeSystem.ObservationValues.PayloadFits.value line 530
  65. theorem OAI.PureTypeSystem.ObservationValues.PayloadFits.value_spec line 536
  66. structure OAI.PureTypeSystem.ObservationValues.PreResult line 543
  67. def OAI.PureTypeSystem.ObservationValues.PreResult.parameter line 550
  68. theorem OAI.PureTypeSystem.ObservationValues.PreResult.parameter_fits line 553
  69. def OAI.PureTypeSystem.ObservationValues.PreResult.baseRead line 562

    Source documentation

    The source base Read clause. For nonliteral expected types this extra coordinate is unused; no additional semantic assertion is made about it.

    noncomputable def baseRead (h : HasType P Γ M T)
    (v : ActiveLayer P C (Ω.profile (T.subst e.images).normalForm) →
      Value (hw := hw) Ω C hno (T.subst e.images).normalForm) :
…

    Mentions: OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.ActiveLayer, OAI.PureTypeSystem.ObservationValues.Value

  70. def OAI.PureTypeSystem.ObservationValues.PreResult.baseResult line 574
  71. def OAI.PureTypeSystem.ObservationValues.PreResult.lookup line 579
  72. def OAI.PureTypeSystem.ObservationValues.PreResult.sort line 590
  73. abbrev OAI.PureTypeSystem.ObservationValues.PreResult.productData line 596
  74. def OAI.PureTypeSystem.ObservationValues.PreResult.productCandidate line 601
  75. def OAI.PureTypeSystem.ObservationValues.PreResult.product line 611
  76. def OAI.PureTypeSystem.ObservationValues.PreResult.abstractionAction line 627
  77. def OAI.PureTypeSystem.ObservationValues.PreResult.abstraction line 643
  78. def OAI.PureTypeSystem.ObservationValues.PreResult.applicationValue line 649
  79. def OAI.PureTypeSystem.ObservationValues.PreResult.application line 674
  80. def OAI.PureTypeSystem.ObservationValues.preEvaluate line 686

    Source documentation

    Structural recursion retaining every stored role choice. The annotation child at a lambda is immaterial to its observation value, but is retained in the input tree for the fundamental normalization lemma. Representability follows from the uniform finite-bound theorem.

    noncomputable def preEvaluate {Γ : List (Expr S)} {M T : Expr S} (t : TypingTree P Γ M T) :
    ∀ e : Environment (hw := hw) Ω C hno Γ, PreResult Ω C hno M T e := by
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.ObservationValues.Environment, OAI.PureTypeSystem.ObservationValues.PreResult