Components.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PureTypeSystem.Neutral.apps_head line 11
def OAI.PureTypeSystem.ComponentInterface.Transports line 26

theorem OAI.PureTypeSystem.ComponentInterface.open_sn line 31

Source documentation

Reflection of the fresh-variable instance proves SN of the open body.

theorem open_sn {Γ : List (Expr S)} {D b B : Expr S} {s : S}
    (hb : HasType P (D :: Γ) b B) (hD : HasType P Γ D (.sort s))
    (ih : J.Transports (U := U) b) (e : J.Env Γ) (ha : J.Admissible (U := U) e) :
…

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

theorem OAI.PureTypeSystem.ComponentInterface.transports_lam line 43
theorem OAI.PureTypeSystem.ComponentInterface.sn_fundamental line 82
Source documentation
Strongly-normalizing substitution transport, including a neutral G-prefix invariant.
```
theorem sn_fundamental {M : Expr S} (hs : StronglyNormalizing M) :
    J.Transports (U := U) M := by
…
```
Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.StronglyNormalizing
theorem OAI.PureTypeSystem.StronglyNormalizing.reverseIndex line 154

inductive OAI.PureTypeSystem.Candidates.StackAt line 163

Source documentation

A single finite prefix supporting every exact typing of a tested stack.

inductive StackAt (k : Nat) : Expr S → List (Expr S) → Prop
  | nil (T) : StackAt k T []
  | cons {D E n ns} :
      HasType P (Ω.context k) (n.rename (Expr.reverseIndex k)) (D.rename (Expr.reverseIndex k)) →
      StronglyNormalizing n → StackAt k (E.instantiate n).normalForm ns →
      StackAt k (.pi D E) (n :: ns)
namespace StackAt
variable {Ω} {k j : Nat} {T : Expr S} {ns : List (Expr S)}

Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Expr.reverseIndex, OAI.PureTypeSystem.StronglyNormalizing

theorem OAI.PureTypeSystem.Candidates.StackAt.mono line 171
theorem OAI.PureTypeSystem.Candidates.StackAt.tested line 176
theorem OAI.PureTypeSystem.Candidates.TestedStack.common_stage line 183
theorem OAI.PureTypeSystem.ComponentInterface.identity_admissible line 201
theorem OAI.PureTypeSystem.ComponentInterface.identity_actual line 212
theorem OAI.PureTypeSystem.ComponentInterface.run_stack line 225
theorem OAI.PureTypeSystem.ComponentInterface.advance line 279
Source documentation
Advancing a component uses one identity evaluation, not a new substitution choice at each stack prefix.
```
theorem advance {T : Expr S} (hT : ActualType Ω T) (hC : Ω.profile T ∈ C) :
    Ground Ω T = Top Ω T := by
…
```
Mentions: OAI.PureTypeSystem.Expr
theorem OAI.PureTypeSystem.Beta.rename_source line 310
Source documentation
Renaming cannot create a redex, and every renamed step has an exact source.
```
theorem rename_source {M N : Expr S} {ρ : Nat → Nat} (h : Beta (M.rename ρ) N) :
    ∃ M', Beta M M' ∧ N = M'.rename ρ := by
…
```
Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Beta
theorem OAI.PureTypeSystem.StronglyNormalizing.rename line 344
theorem OAI.PureTypeSystem.ContextTower.variable_substitution line 360
Source documentation
Every valid finite context has a variable-valued interpretation in the saturated tower. Substitution reflection does not require these names to be surjective or even injective.
```
theorem variable_substitution {Γ : List (Expr S)} (hΓ : ValidContext P Γ) :
    ∃ ρ : Nat → Nat, Ω.TypedSubstitution Γ (Expr.var ∘ ρ) := by
…
```
Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ValidContext
theorem OAI.PureTypeSystem.all_ground_eq_top line 376
Source documentation
Finite primary-component induction. The supplied interfaces are consumed one at a time, and Ground=Top is only used at strict predecessor components.
```
theorem all_ground_eq_top {S : Type u} [Fintype S] {P : Specification S}
    (Ω : ContextTower P) (hw : SystemWeaklyNormalizing P)
    (interfaces : ∀ C, IsComponent (PrimaryEdge P) C →
      Nonempty (ComponentInterface.{u,v} Ω hw C)) :
    ∀ {T}, ActualType Ω T → Ground Ω T = Top Ω T := by
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.ContextTower, OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge
theorem OAI.PureTypeSystem.application_sn_of_ground line 418
Source documentation
Once all actual types have Ground=Top, typed application preserves SN. Types and annotations are normalized using WN, not assumed SN.
```
theorem application_sn_of_ground {S : Type u} {P : Specification S}
    (Ω : ContextTower P) (hw : SystemWeaklyNormalizing P)
    (hground : ∀ {T}, ActualType Ω T → Ground Ω T = Top Ω T)
    {Γ : List (Expr S)} {f a D E : Expr S}
    (hf : HasType P Γ f (.pi D E)) (ha : HasType P Γ a D)
    (hsf : StronglyNormalizing f) (hsa : StronglyNormalizing a) :
    StronglyNormalizing (.app f a) := by
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.ContextTower, OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.StronglyNormalizing