OAI/Computability/TypeSystem/OneChild.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PureTypeSystem.OneChildInterpretation.Bits line 12
  2. def OAI.PureTypeSystem.OneChildInterpretation.extendBit line 14
  3. def OAI.PureTypeSystem.OneChildInterpretation.head line 18
  4. def OAI.PureTypeSystem.OneChildInterpretation.eval line 25

    Source documentation

    Both choices are tested at each binder. Specialization will select the extreme choice given by the unique internal support path.

    noncomputable def eval (Γ : List (Expr S)) (A : Expr S) (σ : Nat → Expr S) (θ : Bits) : Set (Expr S) :=
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.OneChildInterpretation.Bits

  5. theorem OAI.PureTypeSystem.OneChildInterpretation.head_rename line 35
  6. theorem OAI.PureTypeSystem.OneChildInterpretation.head_subst line 44
  7. theorem OAI.PureTypeSystem.OneChildInterpretation.head_beta line 53
  8. theorem OAI.PureTypeSystem.OneChildInterpretation.head_reduces line 64
  9. theorem OAI.PureTypeSystem.OneChildInterpretation.head_normalForm line 70
  10. theorem OAI.PureTypeSystem.OneChildInterpretation.eval_pi line 73
  11. theorem OAI.PureTypeSystem.OneChildInterpretation.eval_head line 80
  12. theorem OAI.PureTypeSystem.OneChildInterpretation.eval_sort line 86
  13. theorem OAI.PureTypeSystem.OneChildInterpretation.eval_candidate line 93
  14. theorem OAI.PureTypeSystem.OneChildInterpretation.eval_outside line 128
  15. def OAI.PureTypeSystem.OneChildInterpretation.dropSupport line 135
  16. def OAI.PureTypeSystem.OneChildInterpretation.flipSupport line 140
  17. def OAI.PureTypeSystem.OneChildInterpretation.support line 143
  18. structure OAI.PureTypeSystem.OneChildInterpretation.Environment line 151
  19. def OAI.PureTypeSystem.OneChildInterpretation.R line 156
  20. theorem OAI.PureTypeSystem.OneChildInterpretation.normal_subst_eq line 159
  21. theorem OAI.PureTypeSystem.OneChildInterpretation.R_candidate line 169
  22. theorem OAI.PureTypeSystem.OneChildInterpretation.R_conversion line 177
  23. theorem OAI.PureTypeSystem.OneChildInterpretation.eval_recontext line 190
  24. theorem OAI.PureTypeSystem.OneChildInterpretation.eval_rename line 212
  25. def OAI.PureTypeSystem.OneChildInterpretation.Environment.Ext line 262
  26. theorem OAI.PureTypeSystem.OneChildInterpretation.R_sort line 266
  27. theorem OAI.PureTypeSystem.OneChildInterpretation.R_weakening line 271
  28. theorem OAI.PureTypeSystem.OneChildInterpretation.normal_product line 292
  29. theorem OAI.PureTypeSystem.OneChildInterpretation.R_outside line 323
  30. theorem OAI.PureTypeSystem.OneChildInterpretation.product_iff line 334
  31. def OAI.PureTypeSystem.OneChildInterpretation.CompatibleBits line 371

    Source documentation

    Replaced supported heads are assigned the extremum appropriate to the comparison direction and path parity. Unreplaced heads retain their bit.

    def CompatibleBits (r : Option (Nat × Bool)) (dir : Bool) (σ : Nat → Expr S) (θ ψ : Bits) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.OneChildInterpretation.Bits

  32. def OAI.PureTypeSystem.OneChildInterpretation.Below line 374
  33. theorem OAI.PureTypeSystem.OneChildInterpretation.support_outside line 376
  34. theorem OAI.PureTypeSystem.OneChildInterpretation.support_head line 379
  35. theorem OAI.PureTypeSystem.OneChildInterpretation.bits_domain line 384
  36. theorem OAI.PureTypeSystem.OneChildInterpretation.bits_body line 400
  37. def OAI.PureTypeSystem.OneChildInterpretation.chosenBit line 422
  38. theorem OAI.PureTypeSystem.OneChildInterpretation.bits_single line 427
  39. theorem OAI.PureTypeSystem.OneChildInterpretation.subst_profile_path line 445
  40. theorem OAI.PureTypeSystem.OneChildInterpretation.neutral_compare line 454
  41. theorem OAI.PureTypeSystem.OneChildInterpretation.head_apps line 487
  42. theorem OAI.PureTypeSystem.OneChildInterpretation.normal_app_head line 493
  43. theorem OAI.PureTypeSystem.OneChildInterpretation.compare_subst line 511

    Source documentation

    The one-child polarity comparison at a generic normal type. The post-type may have arbitrary newly exposed normal constructors.

    theorem compare_subst {Γ Δ : List (Expr S)} {A : Expr S} {s : S}
    (hA : HasType P Γ A (.sort s)) (hN : Normal A)
    (hrel : ∃ K ∈ C, Reach (PrimaryEdge P) (Profile P Γ A) K)
    (hΔ : ValidContext P Δ) (δ : Nat → Expr S) (hδ : TypedSubstitution P Γ Δ δ)
    (e : Environment Ω Δ) (θ : Bits) (dir : Bool)
    (hb : CompatibleBits (support (P := P) C Γ A) dir δ θ e.bits) :
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Normal, OAI.PureTypeSystem.Reach, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.Profile, OAI.PureTypeSystem.ValidContext, OAI.PureTypeSystem.TypedSubstitution, OAI.PureTypeSystem.OneChildInterpretation.Environment, OAI.PureTypeSystem.OneChildInterpretation.Bits, OAI.PureTypeSystem.OneChildInterpretation.CompatibleBits, OAI.PureTypeSystem.OneChildInterpretation.support

  44. theorem OAI.PureTypeSystem.OneChildInterpretation.specialization line 658
  45. def OAI.PureTypeSystem.OneChildInterpretation.componentInterface line 686

    Source documentation

    One-child components need no relational exclusion: both fresh extremes are tested, and polarity selects one of those tests at specialization.

    noncomputable def componentInterface : ComponentInterface Ω hw C where
…

    Mentions: OAI.PureTypeSystem.ComponentInterface