OAI/Computability/TypeSystem/Wrappers.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

Finite simultaneous normal data witnesses. Feasibility is semantic, so these lemmas do not assume a profile-generation conjecture. The extra inhabitants are genuine fresh context variables.

  1. def OAI.PureTypeSystem.Labelled.Expr.data line 12
  2. theorem OAI.PureTypeSystem.Labelled.Expr.erase_data line 20
  3. theorem OAI.PureTypeSystem.Labelled.Expr.data_rename line 23
  4. theorem OAI.PureTypeSystem.Labelled.Expr.data_subst line 27
  5. theorem OAI.PureTypeSystem.Labelled.Expr.data_instantiate line 35
  6. theorem OAI.PureTypeSystem.Labelled.Expr.data_allData line 41
  7. theorem OAI.PureTypeSystem.Labelled.Expr.data_wellModed line 49
  8. def OAI.PureTypeSystem.Labelled.Expr.arrow line 65

    Source documentation

    Nondependent labelled arrow; its codomain is shifted, not captured.

    def arrow (l : Label) (A B : Expr S) : Expr S := .pi l A (B.rename Nat.succ)

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

  9. def OAI.PureTypeSystem.Labelled.Expr.constLam line 66
  10. theorem OAI.PureTypeSystem.Labelled.Expr.arrow_rename line 68
  11. theorem OAI.PureTypeSystem.Labelled.Expr.arrow_subst line 73
  12. theorem OAI.PureTypeSystem.Labelled.Expr.constLam_rename line 78
  13. theorem OAI.PureTypeSystem.Labelled.Expr.constLam_subst line 83
  14. theorem OAI.PureTypeSystem.Labelled.Expr.instantiate_raise line 88
  15. theorem OAI.PureTypeSystem.Labelled.Beta.data line 94
  16. theorem OAI.PureTypeSystem.Labelled.Converts.data line 108
  17. theorem OAI.PureTypeSystem.Labelled.HasType.data line 118
  18. theorem OAI.PureTypeSystem.Labelled.HasType.arrow line 132
  19. theorem OAI.PureTypeSystem.Labelled.HasType.constLam line 136
  20. theorem OAI.PureTypeSystem.Labelled.HasType.apply_arrow line 141
  21. theorem OAI.PureTypeSystem.Labelled.WellModed.data_subst_congr line 149

    Source documentation

    Data syntax cannot inspect a proof-mode image, even inside annotations.

    theorem data_subst_congr {M : Expr S} {m : Mode} (h : WellModed γ M m)
    (hm : m = .data) (σ τ : Nat → Expr S)
    (he : ∀ n, γ n = .data → σ n = τ n) : M.subst σ = M.subst τ := by
…

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

  22. theorem OAI.PureTypeSystem.Labelled.WellModed.proof_instantiate_irrelevant line 177
  23. theorem OAI.PureTypeSystem.Labelled.WellModed.raise line 186
  24. theorem OAI.PureTypeSystem.Labelled.WellModed.arrow line 190
  25. theorem OAI.PureTypeSystem.Labelled.WellModed.constLam line 193
  26. def OAI.PureTypeSystem.Labelled.SortedAt line 199

    Source documentation

    Sorting at a profile records all source sorting judgments, not an exact profile assertion; wrappers intentionally permit profile growth.

    def SortedAt {S : Type u} (P : Specification S) (Γ : List (Expr S))
    (A : Expr S) (I : Set S) : Prop := ∀ s ∈ I, HasType P Γ A (.sort s)
…

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

  27. theorem OAI.PureTypeSystem.Labelled.SortedAt.mono line 204
  28. theorem OAI.PureTypeSystem.Labelled.SortedAt.arrow line 207
  29. theorem OAI.PureTypeSystem.Labelled.SortedAt.raise line 213
  30. theorem OAI.PureTypeSystem.Labelled.positive_cancel line 219

    Source documentation

    The exact positive product-edge lift/projection beta cancellation.

    theorem positive_cancel {S : Type u} (l : Label) (D e t : Expr S) :
    Beta (.app l (Expr.constLam l D t) e) t := by
…

    Mentions: OAI.PureTypeSystem.Labelled.Label, OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.Beta, OAI.PureTypeSystem.Labelled.Expr.constLam

  31. theorem OAI.PureTypeSystem.Lookup.append_right line 235
  32. theorem OAI.PureTypeSystem.Lookup.append_left line 240
  33. theorem OAI.PureTypeSystem.ValidContext.append line 252
  34. theorem OAI.PureTypeSystem.HasType.append_right line 264
  35. theorem OAI.PureTypeSystem.HasType.append_left line 270
  36. def OAI.PureTypeSystem.HasWitness line 277

    Source documentation

    An actual normal witness of a feasible profile, with a declared inhabitant. All the sorting judgments, rather than one selected sort, are retained.

    def HasWitness {S : Type u} (P : Specification S) (Γ : List (Expr S)) (I : Set S) : Prop :=
…

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

  37. theorem OAI.PureTypeSystem.HasWitness.append_left line 282
  38. theorem OAI.PureTypeSystem.HasWitness.append_right line 286
  39. theorem OAI.PureTypeSystem.FeasibleProfile.witness line 293
  40. theorem OAI.PureTypeSystem.FeasibleProfile.finite_witnesses line 302
  41. structure OAI.PureTypeSystem.Labelled.DataWitnessContext line 320

    Source documentation

    The data context has no proof-mode declarations. Its finite witness terms are literal all-data embeddings and their erased types are normal.

    structure DataWitnessContext {S : Type u} (P : Specification S) (F : Finset (Set S)) where
…

    Mentions: OAI.PureTypeSystem.Specification

  42. theorem OAI.PureTypeSystem.Labelled.ValidContext.data line 329
  43. def OAI.PureTypeSystem.Labelled.DataWitnessContext.ofFeasible line 335
  44. theorem OAI.PureTypeSystem.SignedPath.negative_even_suffix line 358

    Source documentation

    Any odd walk has a negative edge with an even remaining suffix.

    theorem negative_even_suffix {v w : V} (h : SignedPath E v w true) :
    ∃ p g, Reach E v p ∧ E p g true ∧ SignedPath E g w false := by
…

    Mentions: OAI.PureTypeSystem.SignedPath, OAI.PureTypeSystem.Reach

  45. theorem OAI.PureTypeSystem.SignedPath.restrict line 372

    Source documentation

    Restrict a finite walk when all of its intermediate points lie in a set.

    theorem restrict {C : Set V} {v w : V} {p : Bool}
    (h : SignedPath E v w p) (hv : v ∈ C)
    (hi : ∀ z, Reach E v z → Reach E z w → z ∈ C) :
    SignedPath (fun x y p => E x y p ∧ x ∈ C ∧ y ∈ C) v w p := by
…

    Mentions: OAI.PureTypeSystem.SignedPath, OAI.PureTypeSystem.Reach

  46. theorem OAI.PureTypeSystem.IsComponent.all_parities line 388

    Source documentation

    An odd closed walk in an SCC supplies both parities between all vertices.

    theorem all_parities (hC : IsComponent E C) {r v w : V}
    (hr : r ∈ C) (ho : SignedPath E r r true) (hv : v ∈ C) (hw : w ∈ C)
    (b : Bool) : SignedPath E v w b := by
…

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SignedPath

  47. theorem OAI.PureTypeSystem.IsComponent.restrict_path line 397
  48. theorem OAI.PureTypeSystem.IsComponent.return_parity line 403

    Source documentation

    No odd cycle makes the return parity uniquely determined by the outward one.

    theorem return_parity (hC : IsComponent E C) {v w : V} {b : Bool}
    (hv : v ∈ C) (hw : w ∈ C) (hp : SignedPath E v w b)
    (ho : ¬ SignedPath E v v true) : SignedPath E w v b := by
…

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SignedPath

  49. theorem OAI.PureTypeSystem.IsComponent.negative_routes line 412

    Source documentation

    The three internal path roles needed by the first data channel, without assuming that the secondary component itself has an odd cycle.

    theorem negative_routes (hC : IsComponent E C) {J k : V}
    (hJ : J ∈ C) (hk : k ∈ C) (hJk : E J k false)
    (hn : ∃ a ∈ C, ∃ b ∈ C, E a b true) :
    ∃ p ∈ C, ∃ g ∈ C, E p g true ∧ SignedPath E k p true ∧
      SignedPath E p k true ∧ SignedPath E g J false := by
…

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SignedPath

  50. theorem OAI.PureTypeSystem.ForbiddenConfiguration.channel_paths line 448

    Source documentation

    Source choice-of-paths conclusion, retaining the actual triples and all profile and seed hypotheses of the forbidden configuration.

    theorem channel_paths (h : ForbiddenConfiguration P C) :
    ∃ D : Set (Set S), IsComponent (SecondaryEdge P C) D ∧
    ∃ I J k s p n g j h',
      ProfileTriple P I J k ∧ J ∈ D ∧ k ∈ D ∧ ({s} : Set S) ∈ D ∧
      (AxProfile P s).Nonempty ∧ PositivePath (PrimaryEdge P) (AxProfile P s) I ∧
      ProfileTriple P p n g ∧ p ∈ D ∧ g ∈ D ∧ n ∈ ObservationLayers P C ∧
      SignedPath (SecondaryEdge P C) k p true ∧
      SignedPath (SecondaryEdge P C) p k true ∧
      SignedPath (SecondaryEdge P C) g J false ∧
      DirectLayer P C j ∧ SignedPath (SecondaryEdge P C) k j true ∧
      DirectLayer P C h' ∧ SignedPath (SecondaryEdge P C) k h' false ∧
      SignedPath (SecondaryEdge P C) p h' true := by
…

    Mentions: OAI.PureTypeSystem.ForbiddenConfiguration, OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SecondaryEdge, OAI.PureTypeSystem.ProfileTriple, OAI.PureTypeSystem.AxProfile, OAI.PureTypeSystem.PositivePath, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.ObservationLayers, OAI.PureTypeSystem.SignedPath, OAI.PureTypeSystem.DirectLayer

  51. structure OAI.PureTypeSystem.Labelled.Embedding line 493

    Source documentation

    A legal mode-preserving change of names. No hypotheses about convertibility or proof existence are packed into the map.

    structure Embedding {S : Type u} (P : Specification S) (Γ : List (Expr S))
    (γ : Nat → Mode) (Δ : List (Expr S)) (δ : Nat → Mode) where
…

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

  52. def OAI.PureTypeSystem.Labelled.Embedding.refl line 504
  53. theorem OAI.PureTypeSystem.Labelled.Embedding.typing line 510
  54. theorem OAI.PureTypeSystem.Labelled.Embedding.moded line 513
  55. def OAI.PureTypeSystem.Labelled.Embedding.comp line 516
  56. def OAI.PureTypeSystem.Labelled.Embedding.cons line 522
  57. def OAI.PureTypeSystem.Labelled.Embedding.lift line 529
  58. theorem OAI.PureTypeSystem.Labelled.ProofContext.proof_cons line 545
  59. theorem OAI.PureTypeSystem.Labelled.Expr.AllData.wellModed line 557
  60. theorem OAI.PureTypeSystem.Labelled.Expr.Target.arrow line 568
  61. structure OAI.PureTypeSystem.Labelled.WitnessFamily line 576

    Source documentation

    All finite feasible witnesses with their one fixed choice of terminal type. The types remain fixed (up to renaming) during proof-context extensions.

    structure WitnessFamily {S : Type u} (P : Specification S) (Γ : List (Expr S))
    (γ : Nat → Mode) where
…

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

  62. def OAI.PureTypeSystem.Labelled.WitnessFamily.rename line 590
  63. theorem OAI.PureTypeSystem.Labelled.WitnessFamily.exists_family line 600
  64. def OAI.PureTypeSystem.Labelled.Transfer line 622

    Source documentation

    A term transformer under one temporary proof input. No product rule is postulated for its input/output pair; that rule generally does not exist.

    def Transfer {S : Type u} (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

  65. theorem OAI.PureTypeSystem.Labelled.Transfer.refl line 629
  66. theorem OAI.PureTypeSystem.Labelled.Transfer.rename line 632
  67. theorem OAI.PureTypeSystem.Labelled.Transfer.trans line 638
  68. theorem OAI.PureTypeSystem.Labelled.Transfer.positive line 645
  69. theorem OAI.PureTypeSystem.Labelled.Transfer.converter line 656

    Source documentation

    The declared converter is inserted before, not after, the temporary input.

    theorem converter (hC : HasType P Γ (Expr.arrow .pp A B) (.sort r))
    (hA : HasType P Γ A (.sort s)) :
    Transfer P (Expr.arrow .pp A B :: Γ) (modeCons .proof γ)
      (A.rename Nat.succ) (B.rename Nat.succ) := by
…

    Mentions: OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.Expr.arrow, OAI.PureTypeSystem.Labelled.Transfer, OAI.PureTypeSystem.Labelled.modeCons

  70. def OAI.PureTypeSystem.Labelled.Proves line 675

    Source documentation

    An actual labelled inhabitant, retaining its typing and proof mode.

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

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

  71. theorem OAI.PureTypeSystem.Labelled.Proves.rename line 681
  72. theorem OAI.PureTypeSystem.Labelled.Proves.of_var line 686
  73. theorem OAI.PureTypeSystem.Labelled.Proves.apply_arrow line 690
  74. theorem OAI.PureTypeSystem.Labelled.Proves.constLam line 696
  75. theorem OAI.PureTypeSystem.Labelled.Transfer.prove line 707
  76. theorem OAI.PureTypeSystem.Labelled.Transfer.of_proves line 712
  77. theorem OAI.PureTypeSystem.Labelled.Transfer.abstract line 717
  78. theorem OAI.PureTypeSystem.Labelled.Transfer.apply_to line 725

    Source documentation

    An actual argument may be data or proof; its original application label is retained, and the fresh proof input is inserted before the argument is used.

    theorem apply_to {l : Label} {a : Expr S} (ha : HasType P Γ a A)
    (ma : WellModed γ a l.domain) (hl : l.result = .proof)
    (hpi : HasType P Γ (Expr.arrow l A B) (.sort s)) :
    Transfer P Γ γ (Expr.arrow l A B) B := by
…

    Mentions: OAI.PureTypeSystem.Labelled.Label, OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.Expr.arrow, OAI.PureTypeSystem.Labelled.Transfer

  79. theorem OAI.PureTypeSystem.Labelled.Transfer.apply_to_proof line 739
  80. theorem OAI.PureTypeSystem.Labelled.edge_profiles line 751
  81. def OAI.PureTypeSystem.Labelled.Carries line 760

    Source documentation

    The converter-routing construction retains its finite admissible context, its exact renaming of the original input, and the normal positive carried type.

    def Carries (Γ : List (Expr S)) (γ : Nat → Mode) (T : Expr S) (J : Set S) : Prop :=
…

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

  82. theorem OAI.PureTypeSystem.Labelled.WitnessFamily.carry_edge line 770
  83. theorem OAI.PureTypeSystem.Labelled.WitnessFamily.carry_path line 812

    Source documentation

    Each negative edge resets the carried type to a fixed terminal, and is followed by its own positive lift. Thus every converter domain stays positive.

    theorem carry_path {b : Bool} (hp : SignedPath (PrimaryEdge P) I J b)
    (hI : FeasibleProfile P I) (hv : ValidContext P Γ) (hc : ProofContext Γ γ)
    (hT : T.Target) (hm : WellModed γ T .data) (ht : SortedAt P Γ T I) :
    Carries (P := P) Γ γ T J := by
…

    Mentions: OAI.PureTypeSystem.SignedPath, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.FeasibleProfile, OAI.PureTypeSystem.Labelled.ValidContext, OAI.PureTypeSystem.Labelled.ProofContext, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.SortedAt, OAI.PureTypeSystem.Labelled.Carries

  84. theorem OAI.PureTypeSystem.Labelled.WitnessFamily.terminal_transfer line 833

    Source documentation

    Terminal-converter existence. Both terminal types are the original, fixed witnesses; only legal renaming is applied.

    theorem terminal_transfer {C : Set (Set S)} (hC : IsComponent (PrimaryEdge P) C)
    {I₁ J₁ K₁ I₂ J₂ K₂ : Set S}
    (h₁ : ProfileTriple P I₁ J₁ K₁) (hk₁ : K₁ ∈ C)
    (h₂ : ProfileTriple P I₂ J₂ K₂) (hi₂ : I₂ ∈ C)
    (hv : ValidContext P Γ) (hc : ProofContext Γ γ) :
    ∃ Δ δ, ∃ e : Embedding P Γ γ Δ δ, ProofContext Δ δ ∧
      Transfer P Δ δ ((W.type J₁).rename e.names) ((W.type J₂).rename e.names) := by
…

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.ProfileTriple, OAI.PureTypeSystem.Labelled.ValidContext, OAI.PureTypeSystem.Labelled.ProofContext, OAI.PureTypeSystem.Labelled.Embedding, OAI.PureTypeSystem.Labelled.Transfer, OAI.PureTypeSystem.Labelled.WitnessFamily.rename

  85. def OAI.PureTypeSystem.Labelled.TerminalProfile line 862

    Source documentation

    The fixed terminals are exactly the codomains of the internal domain edges of the logic SCC. This includes the chosen logical bottom.

    def TerminalProfile (P : Specification S) (C : Set (Set S)) (J : Set S) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Specification

  86. theorem OAI.PureTypeSystem.Labelled.TerminalProfile.feasible line 865
  87. theorem OAI.PureTypeSystem.Labelled.WitnessFamily.finite_terminal_network line 876

    Source documentation

    Previously constructed routes survive every new converter declaration. The finite induction performs all context extensions before any logical input.

    theorem finite_terminal_network (hC : IsComponent (PrimaryEdge P) C)
    (F : Finset (Set S × Set S))
    (hF : ∀ q ∈ F, TerminalProfile P C q.1 ∧ TerminalProfile P C q.2)
    (hv : ValidContext P Γ) (hc : ProofContext Γ γ) :
    ∃ Δ δ, ∃ e : Embedding P Γ γ Δ δ, ProofContext Δ δ ∧
      ∀ q ∈ F, Transfer P Δ δ ((W.type q.1).rename e.names) ((W.type q.2).rename e.names) := by
…

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.Labelled.TerminalProfile, OAI.PureTypeSystem.Labelled.ValidContext, OAI.PureTypeSystem.Labelled.ProofContext, OAI.PureTypeSystem.Labelled.Embedding, OAI.PureTypeSystem.Labelled.Transfer, OAI.PureTypeSystem.Labelled.WitnessFamily.rename

  88. theorem OAI.PureTypeSystem.Labelled.WitnessFamily.terminal_network line 900

    Source documentation

    One fixed finite legal context has every pairwise terminal transfer.

    theorem terminal_network [Fintype S] (hC : IsComponent (PrimaryEdge P) C)
    (hv : ValidContext P Γ) (hc : ProofContext Γ γ) :
    ∃ Δ δ, ∃ e : Embedding P Γ γ Δ δ, ProofContext Δ δ ∧
      ∀ J J', TerminalProfile P C J → TerminalProfile P C J' →
        Transfer P Δ δ ((W.type J).rename e.names) ((W.type J').rename e.names) := by
…

    Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.Labelled.ValidContext, OAI.PureTypeSystem.Labelled.ProofContext, OAI.PureTypeSystem.Labelled.Embedding, OAI.PureTypeSystem.Labelled.TerminalProfile, OAI.PureTypeSystem.Labelled.Transfer, OAI.PureTypeSystem.Labelled.WitnessFamily.rename

  89. def OAI.PureTypeSystem.Labelled.ProofParity line 914

    Source documentation

    Uniform proof transport records open callbacks, not a meta-level implication between propositions. Every operation returns an actual typed term.

    def ProofParity {Γ : List (Expr S)} {γ : Nat → Mode}
    (W : WitnessFamily P Γ γ) (C : Set (Set S)) (A B : Expr S) (b : Bool) : Prop :=
…

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

  90. theorem OAI.PureTypeSystem.Labelled.ProofParity.refl line 934
  91. theorem OAI.PureTypeSystem.Labelled.ProofParity.positive line 939

    Source documentation

    Positive paths retain the literal data witness used by projection.

    theorem positive (h : ProofParity W C A B b)
    (hB : HasType P Γ B (.sort s)) (hD : HasType P Γ D (.sort t))
    (mD : WellModed γ D .data) {d : Expr S}
    (hd : HasType P Γ d D) (md : WellModed γ d .data)
    (hpi : HasType P Γ (Expr.arrow .dp D B) (.sort r)) :
    ProofParity W C A (Expr.arrow .dp D B) b := by
…

    Mentions: OAI.PureTypeSystem.Labelled.ProofParity, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.Expr.arrow

  92. theorem OAI.PureTypeSystem.Labelled.ProofParity.negative line 969

    Source documentation

    Each negative edge uses its fixed terminal; even/odd callbacks are composed only with the predeclared terminal terms.

    theorem negative (h : ProofParity W C A B b)
    (τ : ∀ J J', TerminalProfile P C J → TerminalProfile P C J' →
      Transfer P Γ γ (W.type J) (W.type J'))
    {J₀ : Set S} (hJ₀ : TerminalProfile P C J₀)
    (hB : HasType P Γ B (.sort s)) (mB : WellModed γ B .data)
    (hpi : HasType P Γ (Expr.arrow .pp B (W.type J₀)) (.sort r)) :
    ProofParity W C A (Expr.arrow .pp B (W.type J₀)) (!b) := by
…

    Mentions: OAI.PureTypeSystem.Labelled.ProofParity, OAI.PureTypeSystem.Labelled.TerminalProfile, OAI.PureTypeSystem.Labelled.Transfer, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.Expr.arrow

  93. def OAI.PureTypeSystem.Labelled.Continuation line 1010

    Source documentation

    A continuation is tested after every legal extension; callbacks are actual open terms with one proof input, not arbitrary functions on inhabitation.

    def Continuation {Γ : List (Expr S)} {γ : Nat → Mode} (W : WitnessFamily P Γ γ)
    (C : Set (Set S)) (Q : Expr S) : Prop :=
…

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

  94. def OAI.PureTypeSystem.Labelled.StableExtraction line 1019

    Source documentation

    The extraction property proved for sorted stable telescopes. It is not an extra PTS rule: the following constructors explicitly build its proof terms.

    def StableExtraction {Γ : List (Expr S)} {γ : Nat → Mode} (W : WitnessFamily P Γ γ)
    (C : Set (Set S)) (Q : Expr S) : Prop :=
…

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

  95. theorem OAI.PureTypeSystem.Labelled.Continuation.rename line 1027
  96. theorem OAI.PureTypeSystem.Labelled.Transfer.project_pi line 1040

    Source documentation

    Project a dependent product at its newly opened raw argument, retaining the argument's actual data/proof label.

    theorem project_pi {l : Label} (hA : HasType P Γ A (.sort s))
    (hpi : HasType P Γ (.pi l A B) (.sort t)) (hl : l.result = .proof) :
    Transfer P (A :: Γ) (modeCons l.domain γ) ((Expr.pi l A B).rename Nat.succ) B := by
…

    Mentions: OAI.PureTypeSystem.Labelled.Label, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.Transfer, OAI.PureTypeSystem.Labelled.modeCons, OAI.PureTypeSystem.Labelled.Transfer.rename

  97. theorem OAI.PureTypeSystem.Labelled.StableExtraction.rename line 1064
  98. theorem OAI.PureTypeSystem.Labelled.StableExtraction.terminal line 1071
  99. theorem OAI.PureTypeSystem.Labelled.StableExtraction.product line 1082

    Source documentation

    Dependent telescope step. The continuation is threaded under the raw binder; the raw projection supplies the callback at exactly that locally opened value.

    theorem product {l : Label} (hA : HasType P Γ A (.sort s))
    (mA : WellModed γ A .data) (hpi : HasType P Γ (.pi l A B) (.sort t))
    (hl : l.result = .proof)
    (hB : StableExtraction (W.rename (Embedding.cons hA l.domain)) C B) :
    StableExtraction W C (.pi l A B) := by
…

    Mentions: OAI.PureTypeSystem.Labelled.Label, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.StableExtraction, OAI.PureTypeSystem.Labelled.Embedding.cons

  100. theorem OAI.PureTypeSystem.Labelled.StableExtraction.arrow line 1120

    Source documentation

    Constant arrows are the special telescope step used by every path edge.

    theorem arrow {l : Label} (hA : HasType P Γ A (.sort s))
    (mA : WellModed γ A .data) (hpi : HasType P Γ (Expr.arrow l A B) (.sort t))
    (hl : l.result = .proof) (hB : StableExtraction W C B) :
    StableExtraction W C (Expr.arrow l A B) :=
…

    Mentions: OAI.PureTypeSystem.Labelled.Label, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.Expr.arrow, OAI.PureTypeSystem.Labelled.StableExtraction

  101. theorem OAI.PureTypeSystem.Labelled.ProofParity.into line 1132
  102. theorem OAI.PureTypeSystem.Labelled.ProofParity.down line 1138

    Source documentation

    Stable even-path retraction, including dependent stable telescopes.

    theorem down (h : ProofParity W C A B false) (hs : StableExtraction W C A)
    (hB : HasType P Γ B (.sort t)) : Transfer P Γ γ B A := by
…

    Mentions: OAI.PureTypeSystem.Labelled.ProofParity, OAI.PureTypeSystem.Labelled.StableExtraction, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.Transfer

  103. inductive OAI.PureTypeSystem.Labelled.ProofWrapper line 1154

    Source documentation

    Fixed hygienic wrapper syntax. The code is selected once from a path, never reselected when an input is substituted or its sorting profile grows.

    inductive ProofWrapper (S : Type u)
  | identity
  | positive : ProofWrapper S → Expr S → ProofWrapper S
  | negative : ProofWrapper S → Expr S → ProofWrapper S

namespace ProofWrapper

    Mentions: OAI.PureTypeSystem.Labelled.Expr

  104. def OAI.PureTypeSystem.Labelled.ProofWrapper.apply line 1161
  105. def OAI.PureTypeSystem.Labelled.ProofWrapper.rename line 1166
  106. def OAI.PureTypeSystem.Labelled.ProofWrapper.subst line 1171
  107. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.apply_rename line 1176
  108. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.apply_subst line 1180
  109. def OAI.PureTypeSystem.Labelled.ProofWrapper.containsNegative line 1184
  110. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.rename_id line 1189
  111. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.rename_comp line 1192
  112. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.instantiate_raise line 1196
  113. inductive OAI.PureTypeSystem.Labelled.ProofWrapper.Formed line 1202

    Source documentation

    A path certificate retaining exactly its terminals, witness types and edge roles. Inclusion is a literal identity; there is no type-level cast.

    inductive Formed {Γ : List (Expr S)} {γ : Nat → Mode} (W : WitnessFamily P Γ γ)
    (C : Set (Set S)) (I : Set S) : Set S → Bool → ProofWrapper S → Prop
  | identity : Formed W C I I false .identity
  | inclusion {J K b R} : Formed W C I J b R → K ⊆ J → Formed W C I K b R
  | positive {A J K b R} : Formed W C I J b R → ProfileTriple P A J K →
      Formed W C I K b (.positive R (W.type A))
  | negative {J B K b R} : Formed W C I J b R → ProfileTriple P J B K → J ∈ C → K ∈ C →
      Formed W C I K (!b) (.negative R (W.type B))

namespace Formed
variable {Γ : List (Expr S)} {γ : Nat → Mode} {W : WitnessFamily P Γ γ}
    {C : Set (Set S)} {I J K : Set S} {a b : Bool} {R : ProofWrapper S}

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

  114. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.rename line 1215
  115. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.edge line 1224
  116. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.path line 1231
  117. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.sound line 1242

    Source documentation

    The fixed code has the actual profile sorting, mode, and parity operations.

    theorem sound (h : Formed W C I J b R)
    (τ : ∀ J J', TerminalProfile P C J → TerminalProfile P C J' →
      Transfer P Γ γ (W.type J) (W.type J'))
    {T : Expr S} (ht : SortedAt P Γ T I) (mt : WellModed γ T .data) :
    SortedAt P Γ (R.apply T) J ∧ WellModed γ (R.apply T) .data ∧
      ProofParity W C T (R.apply T) b := by
…

    Mentions: OAI.PureTypeSystem.Labelled.ProofWrapper.Formed, OAI.PureTypeSystem.Labelled.TerminalProfile, OAI.PureTypeSystem.Labelled.Transfer, OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.SortedAt, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.ProofParity

  118. theorem OAI.PureTypeSystem.Labelled.ProofWrapper.Formed.stable line 1269

    Source documentation

    Every code preserves stable extraction; a negative-containing code creates it even for an initially arbitrary data type.

    theorem stable (h : Formed W C I J b R)
    (τ : ∀ J J', TerminalProfile P C J → TerminalProfile P C J' →
      Transfer P Γ γ (W.type J) (W.type J'))
    {T : Expr S} (ht : SortedAt P Γ T I) (mt : WellModed γ T .data) :
    (StableExtraction W C T → StableExtraction W C (R.apply T)) ∧
      (R.containsNegative = true → StableExtraction W C (R.apply T)) := by
…

    Mentions: OAI.PureTypeSystem.Labelled.ProofWrapper.Formed, OAI.PureTypeSystem.Labelled.TerminalProfile, OAI.PureTypeSystem.Labelled.Transfer, OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.SortedAt, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.StableExtraction