Interface.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

The exact local obligations used when advancing a primary component. This is an internal interface, not a hypothesis of the main PTS theorem.

def OAI.PureTypeSystem.Expected line 12
Source documentation
Expected types include unsorted literal sorts (the regularity alternative).
```
def Expected {S : Type u} (P : Specification S) (Γ : List (Expr S)) (A : Expr S) : Prop :=
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.Expr
theorem OAI.PureTypeSystem.Expected.of_type line 16
theorem OAI.PureTypeSystem.Expected.sorted line 17
theorem OAI.PureTypeSystem.Expected.wn line 18
theorem OAI.PureTypeSystem.Expected.weaken line 22
def OAI.PureTypeSystem.Expr.extend line 31
theorem OAI.PureTypeSystem.Expr.extend_zero line 34
theorem OAI.PureTypeSystem.Expr.extend_succ line 35
theorem OAI.PureTypeSystem.Expr.subst_raise_extend line 36
theorem OAI.PureTypeSystem.Expr.instantiate_extended line 39
structure OAI.PureTypeSystem.Processed line 51
Source documentation
Ground=top has already been proved on U; U is predecessor closed and contains every strict predecessor of the component currently processed.
```
structure Processed {S : Type u} {P : Specification S} (Ω : ContextTower P)
    (U C : Set (Set S)) : Prop where
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.ContextTower
structure OAI.PureTypeSystem.ComponentInterface line 62
Source documentation
Environments carry arbitrary typed raw images. Extension collections are nonempty, and retain old parameters. Product tests range over all listed extensions; specialization can select the normal argument's tested payload.
```
structure ComponentInterface {S : Type u} {P : Specification S} (Ω : ContextTower P)
    (hw : SystemWeaklyNormalizing P) (C : Set (Set S)) where
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.ContextTower, OAI.PureTypeSystem.SystemWeaklyNormalizing
def OAI.PureTypeSystem.ComponentInterface.Admissible line 102
theorem OAI.PureTypeSystem.ComponentInterface.admissible_extension line 109
theorem OAI.PureTypeSystem.ComponentInterface.fresh_extension line 131
Source documentation
Sending a binder to a fresh typed variable always preserves admissibility. SN of that instance reflects back to the open substituted body by substitution reflection, so no global renaming or reduction-height bound is needed.
```
theorem fresh_extension {Γ : List (Expr S)} {D : Expr S} {s : S}
    (e : J.Env Γ) (hD : HasType P Γ D (.sort s)) (ha : J.Admissible (U := U) e) :
…
```
Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType
theorem OAI.PureTypeSystem.Expected.subst_wn line 147
theorem OAI.PureTypeSystem.Expected.actual line 153
theorem OAI.PureTypeSystem.ContextTower.profile_subst_path line 165
theorem OAI.PureTypeSystem.ContextTower.profile_instantiate_product_path line 172

theorem OAI.PureTypeSystem.Candidates.ground_application_subst line 190

Source documentation

G propagates through the normal form of a raw dependent product.

theorem ground_application_subst {Γ : List (Expr S)} {D E n h : Expr S} {s : S}
    {σ : Nat → Expr S} (hp : HasType P Γ (.pi D E) (.sort s))
    (hσ : Ω.TypedSubstitution Γ σ)
    (hh : h ∈ Ground Ω ((Expr.pi D E).subst σ).normalForm)
    (hn : n ∈ Top Ω (D.subst σ).normalForm) :
    Expr.app h n ∈ Ground Ω (E.subst (Expr.extend σ n)).normalForm := by
…

Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Candidates.Ground, OAI.PureTypeSystem.Candidates.Top, OAI.PureTypeSystem.Expr.extend

theorem OAI.PureTypeSystem.Processed.subst_closed line 232
theorem OAI.PureTypeSystem.Processed.subst_before line 236
theorem OAI.PureTypeSystem.Processed.top_ground_generic line 240
def OAI.PureTypeSystem.ComponentInterface.Transported line 258
Source documentation
The extra neutral invariant is exactly the G-prefix invariant in the manuscript's spine argument.
```
def Transported {Γ : List (Expr S)} (M A : Expr S) (e : J.Env Γ) : Prop :=
…
```
Mentions: OAI.PureTypeSystem.Expr
theorem OAI.PureTypeSystem.ComponentInterface.Transported.sn line 265
theorem OAI.PureTypeSystem.ComponentInterface.Transported.convert line 268
theorem OAI.PureTypeSystem.ComponentInterface.transported_of_ground line 280
theorem OAI.PureTypeSystem.ComponentInterface.transported_at_sort line 284
theorem OAI.PureTypeSystem.ComponentInterface.transported_var line 295
theorem OAI.PureTypeSystem.ComponentInterface.transported_neutral_app line 313
Source documentation
Propagation for a neutral prefix. Unlike a candidate, G has application closure; the processed invariant handles the sole transition out of C.
```
theorem transported_neutral_app {Γ : List (Expr S)} {f n D E : Expr S} {s : S}
    (hp : HasType P Γ (.pi D E) (.sort s)) (hn : HasType P Γ n D)
    (hf : Neutral f) (e : J.Env Γ)
    (hfr : J.Transported f (.pi D E) e) (hnr : J.Transported n D e) :
    J.Transported (.app f n) (E.instantiate n) e := by
…
```
Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Neutral
theorem OAI.PureTypeSystem.Candidates.application_subst_type line 352
def OAI.PureTypeSystem.Candidates.RawProduct line 368
theorem OAI.PureTypeSystem.Candidates.rawProduct_candidate line 373