OAI/Computability/TypeSystem/ObservationReduction.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PureTypeSystem.ObservationValues.Value.asPlus_plus line 13
2. theorem OAI.PureTypeSystem.ObservationValues.Value.asMinus_minus line 16
3. theorem OAI.PureTypeSystem.ObservationValues.plain_beta line 21
4. theorem OAI.PureTypeSystem.ObservationValues.exitValue_tag line 29
5. theorem OAI.PureTypeSystem.ObservationValues.lambdaExit_parameter line 34
6. theorem OAI.PureTypeSystem.ObservationValues.plusContinue_gate line 59
7. theorem OAI.PureTypeSystem.ObservationValues.plusContinue_parameter line 84
8. theorem OAI.PureTypeSystem.ObservationValues.minusContinue_gate line 93
9. theorem OAI.PureTypeSystem.ObservationValues.minusContinue_parameter line 118
10. theorem OAI.PureTypeSystem.ObservationValues.plusLambda_slice line 127
11. theorem OAI.PureTypeSystem.ObservationValues.minusLambda_slice line 133
12. theorem OAI.PureTypeSystem.ObservationValues.lambda_beta line 142

    Source documentation

    The raw lambda equation. The sole representability premise is supplied below from the proved uniform finite-bound lemma for an actual body tree.

    theorem lambda_beta (T : ActiveType Ω C) (act : LambdaAction (hw := hw) Ω C hno T)
    …

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

13. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstraction_beta line 188
14. theorem OAI.PureTypeSystem.ObservationValues.PreResult.application_frame line 207
15. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstractionAction_raw line 223
16. theorem OAI.PureTypeSystem.ObservationValues.application_abstraction_beta line 249
17. structure OAI.PureTypeSystem.ObservationValues.GoodTransport line 293

    Source documentation

    Exact tree transport at a fixed root expectation. Only good observations are equated; raw environments and values are otherwise unrestricted.

    structure GoodTransport {Γ : List (Expr S)} {M N T : Expr S}
        (t : TypingTree P Γ M T) (t' : TypingTree P Γ N T) : Prop where
    …

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.TypingTree

18. theorem OAI.PureTypeSystem.ObservationValues.baseRead_transport line 302
19. theorem OAI.PureTypeSystem.ObservationValues.root_transport line 337
20. theorem OAI.PureTypeSystem.ObservationValues.Environment.cons_images line 412
21. theorem OAI.PureTypeSystem.ObservationValues.GoodTransport.refl line 420
22. theorem OAI.PureTypeSystem.ObservationValues.GoodTransport.parameter_eq line 422
23. theorem OAI.PureTypeSystem.ObservationValues.application_transport line 431
24. theorem OAI.PureTypeSystem.ObservationValues.abstraction_transport line 471
25. theorem OAI.PureTypeSystem.ObservationValues.product_transport line 520
26. theorem OAI.PureTypeSystem.ObservationValues.reduction_transport line 603
27. theorem OAI.PureTypeSystem.ObservationValues.GoodTransport.trans line 682
28. theorem OAI.PureTypeSystem.ObservationValues.reduces_transport line 696
29. theorem OAI.PureTypeSystem.ObservationValues.normalize_transport line 707

    Source documentation

    The good part of any stored tree is transported to a normal stored tree.

    theorem normalize_transport (hC : IsComponent (PrimaryEdge P) C)
        {Γ : List (Expr S)} {M T : Expr S} (t : TypingTree P Γ M T) :
        ∃ t' : TypingTree P Γ M.normalForm T, GoodTransport (hw := hw) Ω C hno t t' :=
    …

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.ObservationValues.GoodTransport

30. theorem OAI.PureTypeSystem.ObservationValues.good_normal_value line 714

    Source documentation

    An arbitrary good active value equals every normal-tree value at a convertible expectation. This does not assume goodness of the target tree.

    theorem good_normal_value (hC : IsComponent (PrimaryEdge P) C)
        {Γ : List (Expr S)} {M T U : Expr S} (t : TypingTree P Γ M T)
        (t' : TypingTree P Γ M.normalForm U) (hc : Converts T U)
        (e : Environment (hw := hw) Ω C hno Γ)
    …

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.Converts, OAI.PureTypeSystem.ObservationValues.Environment

31. theorem OAI.PureTypeSystem.ObservationValues.good_normal_read line 729

    Source documentation

    An arbitrary good literal-sort Read equals its normal-syntax interpretation, even for a different literal expected sort in a nonfunctional specification.

    theorem good_normal_read (hC : IsComponent (PrimaryEdge P) C)
        {Γ : List (Expr S)} {M : Expr S} {s r : S} (t : TypingTree P Γ M (.sort s))
        (t' : TypingTree P Γ M.normalForm (.sort r))
        (e : Environment (hw := hw) Ω C hno Γ) (hg : ReadGood Ω C t e.images) :
    …

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.ObservationValues.Environment, OAI.PureTypeSystem.ObservationValues.ReadGood