OAI/Computability/TypeSystem/Contexts.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Finite generic contexts may have arbitrary raw actual images in the saturated tower. Every such substitution is witnessed in one finite prefix; no normalization or strong-normalization of the images is assumed.

  1. def OAI.PureTypeSystem.Expr.Scoped line 16

    Source documentation

    Every free index is below the context length.

    def Scoped : Nat → Expr S → Prop
  | n, .var i => i < n
  | _, .sort _ => True
  | n, .app M N => Scoped n M ∧ Scoped n N
  | n, .lam A b => Scoped n A ∧ Scoped (n+1) b
  | n, .pi A B => Scoped n A ∧ Scoped (n+1) B

namespace Scoped

variable {n m : Nat} {M : Expr S}

    Mentions: OAI.PureTypeSystem.Expr

  2. theorem OAI.PureTypeSystem.Expr.Scoped.rename line 27
  3. theorem OAI.PureTypeSystem.Expr.Scoped.mono line 40
  4. theorem OAI.PureTypeSystem.Expr.Scoped.rename_congr line 43
  5. theorem OAI.PureTypeSystem.Expr.Scoped.subst line 57
  6. theorem OAI.PureTypeSystem.Expr.Scoped.instantiate line 72
  7. def OAI.PureTypeSystem.Expr.reverseIndex line 84

    Source documentation

    Reversal identifies de Bruijn indices in a finite context with fixed levels. Outside that context it is the identity.

    def reverseIndex (n i : Nat) : Nat := if i < n then n - 1 - i else i
  8. theorem OAI.PureTypeSystem.Expr.reverseIndex_lt line 86
  9. theorem OAI.PureTypeSystem.Expr.reverseIndex_involutive line 90
  10. theorem OAI.PureTypeSystem.Expr.reverseIndex_twice line 95
  11. theorem OAI.PureTypeSystem.Expr.Scoped.reverseIndex line 101
  12. theorem OAI.PureTypeSystem.Expr.Scoped.reverseIndex_succ line 105
  13. theorem OAI.PureTypeSystem.HasType.scope line 120
  14. theorem OAI.PureTypeSystem.Beta.scope line 139
  15. theorem OAI.PureTypeSystem.Reduces.scope line 153
  16. theorem OAI.PureTypeSystem.WeaklyNormalizing.rename line 164
  17. theorem OAI.PureTypeSystem.WeaklyNormalizing.reverseIndex_iff line 169
  18. structure OAI.PureTypeSystem.ContextTower line 182

    Source documentation

    Finite prefixes of a common context, using fixed-level names when viewed outside a prefix. Every sortable fixed-level expression is declared arbitrarily late. Bound variables remain de Bruijn indices and are never declared here.

    structure ContextTower {S : Type u} (P : Specification S) where
…

    Mentions: OAI.PureTypeSystem.Specification

  19. structure OAI.PureTypeSystem.ContextTowerConstruction.Stage line 195
  20. def OAI.PureTypeSystem.ContextTowerConstruction.enumeration line 202
  21. theorem OAI.PureTypeSystem.ContextTowerConstruction.enumeration_surjective line 206
  22. def OAI.PureTypeSystem.ContextTowerConstruction.scheduled line 210
  23. theorem OAI.PureTypeSystem.ContextTowerConstruction.scheduled_late line 212
  24. def OAI.PureTypeSystem.ContextTowerConstruction.next line 219
  25. def OAI.PureTypeSystem.ContextTowerConstruction.stages line 226
  26. def OAI.PureTypeSystem.ContextTowerConstruction.contexts line 234
  27. theorem OAI.PureTypeSystem.ContextTowerConstruction.valid line 236
  28. theorem OAI.PureTypeSystem.ContextTowerConstruction.length line 238
  29. theorem OAI.PureTypeSystem.ContextTowerConstruction.step line 240
  30. theorem OAI.PureTypeSystem.ContextTowerConstruction.rename_next line 244
  31. theorem OAI.PureTypeSystem.ContextTowerConstruction.rename_mono line 261
  32. theorem OAI.PureTypeSystem.ContextTowerConstruction.at_scheduled line 270
  33. theorem OAI.PureTypeSystem.ContextTowerConstruction.saturated line 278
  34. def OAI.PureTypeSystem.ContextTowerConstruction.tower line 298
  35. def OAI.PureTypeSystem.ContextTower.HasType line 312

    Source documentation

    A global judgment is witnessed in a finite prefix of the tower.

    def HasType (M A : Expr S) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Expr

  36. theorem OAI.PureTypeSystem.ContextTower.at_next line 316
  37. theorem OAI.PureTypeSystem.ContextTower.at_mono line 333
  38. theorem OAI.PureTypeSystem.ContextTower.HasType.scope line 346
  39. theorem OAI.PureTypeSystem.ContextTower.HasType.weaklyNormalizing line 354
  40. theorem OAI.PureTypeSystem.ContextTower.HasType.type_weaklyNormalizing line 359
  41. theorem OAI.PureTypeSystem.ContextTower.HasType.common line 364
  42. theorem OAI.PureTypeSystem.ContextTower.fresh_variable line 375
  43. theorem OAI.PureTypeSystem.ContextTower.HasType.application line 398
  44. theorem OAI.PureTypeSystem.ContextTower.HasType.conversion line 405
  45. theorem OAI.PureTypeSystem.ContextTower.HasType.subject_reduces line 410
  46. theorem OAI.PureTypeSystem.ContextTower.HasType.regularity line 414
  47. theorem OAI.PureTypeSystem.ContextTower.HasType.normalForm line 424
  48. theorem OAI.PureTypeSystem.ContextTower.HasType.normalize_type line 428
  49. def OAI.PureTypeSystem.ContextTower.TypedSubstitution line 443
  50. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.tail line 449
  51. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.common_stage line 457

    Source documentation

    One common stage suffices for every declaration image, despite the substitution being presented as a total function on indices.

    theorem common_stage (h : Ω.TypedSubstitution Γ σ) :
    ∃ k, ∀ n A, Lookup Γ n A →
      PureTypeSystem.HasType P (Ω.context k) ((σ n).rename (Expr.reverseIndex k))
        ((A.subst σ).rename (Expr.reverseIndex k)) := by
…

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

  52. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.cons line 475

    Source documentation

    Extension assigns a raw term to the fresh generic binder.

    theorem cons {A a : Expr S} (h : Ω.TypedSubstitution Γ σ)
    (ha : Ω.HasType a (A.subst σ)) : Ω.TypedSubstitution (A :: Γ) (fun n => match n with
      | 0 => a | n+1 => σ n) := by
…

    Mentions: OAI.PureTypeSystem.Expr

  53. theorem OAI.PureTypeSystem.ContextTower.HasType.subst line 488

    Source documentation

    Arbitrary typed substitution from a finite generic context to the tower.

    theorem subst (h : PureTypeSystem.HasType P Γ M A) (hσ : Ω.TypedSubstitution Γ σ) :
    Ω.HasType (M.subst σ) (A.subst σ) := by
…

    Mentions: OAI.PureTypeSystem.HasType

  54. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.comp line 500
  55. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.identity line 507

    Source documentation

    The tower's finite-prefix identity environment uses global names.

    theorem identity (n : Nat) : Ω.TypedSubstitution (Ω.context n) (.var ∘ Expr.reverseIndex n) := by
…

    Mentions: OAI.PureTypeSystem.Expr.reverseIndex