OAI/Computability/TypeSystem/Typing.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.PureTypeSystem.Lookup line 10

   Source documentation

   A declaration's type viewed in the full newest-first context.

   inductive Lookup {S : Type u} : List (Expr S) → Nat → Expr S → Prop
     | zero (A Γ) : Lookup (A :: Γ) 0 (A.rename Nat.succ)
     | succ {Γ n A} (B) : Lookup Γ n A → Lookup (B :: Γ) (n + 1) (A.rename Nat.succ)
   
   namespace HasType
   
   variable {S : Type u} {P : Specification S}

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

2. theorem OAI.PureTypeSystem.HasType.sort_of_valid line 18
3. theorem OAI.PureTypeSystem.HasType.product_domain line 26

   Source documentation

   Domain generation alone precedes substitution and does not need any exchange or context-substitution theorem.

   theorem product_domain {Γ : List (Expr S)} {M T : Expr S} (h : HasType P Γ M T) :
       ∀ A B, M = .pi A B → ∃ s, HasType P Γ A (.sort s) := by
   …

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

4. theorem OAI.PureTypeSystem.Converts.subst line 56
5. theorem OAI.PureTypeSystem.Converts.rename line 64
6. def OAI.PureTypeSystem.TypedSubstitution line 76

   Source documentation

   A simultaneous substitution respects each declared variable's exact type. This is a premise only of the substitution metatheorem, not of the main target.

   def TypedSubstitution {S : Type u} (P : Specification S)
       (Γ Δ : List (Expr S)) (σ : Nat → Expr S) : Prop :=
   …

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

7. theorem OAI.PureTypeSystem.TypedSubstitution.tail line 85
8. theorem OAI.PureTypeSystem.TypedSubstitution.lift line 91
9. theorem OAI.PureTypeSystem.HasType.subst line 111
10. theorem OAI.PureTypeSystem.Expr.subst_var_rename line 138
11. theorem OAI.PureTypeSystem.Expr.subst_lift_single line 142
12. theorem OAI.PureTypeSystem.HasType.lookup line 153
13. theorem OAI.PureTypeSystem.TypedSubstitution.identity line 168
14. theorem OAI.PureTypeSystem.TypedSubstitution.weaken line 173
15. theorem OAI.PureTypeSystem.TypedSubstitution.single line 180
16. theorem OAI.PureTypeSystem.HasType.rename line 196
17. theorem OAI.PureTypeSystem.HasType.instantiate line 205
18. theorem OAI.PureTypeSystem.HasType.weaken_under line 210
19. theorem OAI.PureTypeSystem.HasType.context_head_conversion line 225
20. def OAI.PureTypeSystem.HasType.Generation line 244

    Source documentation

    Generation is stated up to conversion, without any functionality premise.

    def Generation (P : Specification S) (Γ : List (Expr S))
        (M T : Expr S) : Prop :=
    …

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

21. theorem OAI.PureTypeSystem.HasType.generation line 257
22. theorem OAI.PureTypeSystem.HasType.generation_pi line 304
23. theorem OAI.PureTypeSystem.HasType.generation_lam line 310
24. theorem OAI.PureTypeSystem.HasType.generation_app line 315
25. theorem OAI.PureTypeSystem.HasType.regularity line 321

    Source documentation

    Correctness of types, including the unsorted literal-sort alternative.

    theorem regularity {Γ : List (Expr S)} {M A : Expr S} (h : HasType P Γ M A) :
        (∃ s, A = .sort s) ∨ (∃ s, HasType P Γ A (.sort s)) := by
    …

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

26. theorem OAI.PureTypeSystem.HasType.product_type_sorted line 339
27. theorem OAI.PureTypeSystem.Converts.pi line 351
28. theorem OAI.PureTypeSystem.Converts.pi_not_sort line 357
29. theorem OAI.PureTypeSystem.Converts.sort_inj line 364
30. theorem OAI.PureTypeSystem.Converts.instantiate_right line 367
31. theorem OAI.PureTypeSystem.HasType.application_type_sorted_aux line 382
32. theorem OAI.PureTypeSystem.HasType.application_type_sorted line 407
33. theorem OAI.PureTypeSystem.HasType.abstraction_type_sorted line 411
34. theorem OAI.PureTypeSystem.HasType.conversion_from_sort line 421

    Source documentation

    Reconstructing a sorted expression at its original expected type does not require a sorting of a terminal (unsorted) sort.

    theorem conversion_from_sort {Γ : List (Expr S)} {M T : Expr S} {s : S}
        (h : HasType P Γ M (.sort s))
        (hT : (∃ t, T = .sort t) ∨ ∃ t, HasType P Γ T (.sort t))
        (hc : Converts T (.sort s)) : HasType P Γ M T := by
    …

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

35. theorem OAI.PureTypeSystem.HasType.subject_reduction line 432

    Source documentation

    Subject reduction at the exact original type, including binder annotations.

    theorem subject_reduction {Γ : List (Expr S)} {M N T : Expr S}
        (h : HasType P Γ M T) (hr : Beta M N) : HasType P Γ N T := by
    …

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

36. theorem OAI.PureTypeSystem.HasType.subject_reduces line 478
37. theorem OAI.PureTypeSystem.Normal.of_map line 490
38. theorem OAI.PureTypeSystem.Normal.app_left line 494
39. theorem OAI.PureTypeSystem.Normal.app_right line 497
40. theorem OAI.PureTypeSystem.Normal.lam_domain line 500
41. theorem OAI.PureTypeSystem.Normal.lam_body line 503
42. theorem OAI.PureTypeSystem.Normal.pi_domain line 506
43. theorem OAI.PureTypeSystem.Normal.pi_body line 509
44. theorem OAI.PureTypeSystem.Normal.pi line 512
45. theorem OAI.PureTypeSystem.Normal.lam line 518
46. def OAI.PureTypeSystem.Expr.normalForm line 532

    Source documentation

    Choice of the unique full beta normal form when it exists. The fallback is irrelevant on legal syntax under the standing system-wide WN hypothesis.

    noncomputable def normalForm (M : Expr S) : Expr S := by
    …

    Mentions: OAI.PureTypeSystem.Expr

47. theorem OAI.PureTypeSystem.Expr.normalForm_spec line 536
48. theorem OAI.PureTypeSystem.Expr.normalForm_eq line 541
49. theorem OAI.PureTypeSystem.Expr.normalForm_of_normal line 547
50. theorem OAI.PureTypeSystem.Expr.normalForm_converts line 550
51. theorem OAI.PureTypeSystem.Expr.normalForm_pi line 557
52. theorem OAI.PureTypeSystem.HasType.weaklyNormalizing line 569
53. theorem OAI.PureTypeSystem.HasType.type_weaklyNormalizing line 572
54. theorem OAI.PureTypeSystem.HasType.normalForm line 575
55. theorem OAI.PureTypeSystem.HasType.normalize_type line 579
56. inductive OAI.PureTypeSystem.Neutral line 589

    Source documentation

    The variable-headed spines used by the manuscript.

    inductive Neutral {S : Type u} : Expr S → Prop
      | var (n) : Neutral (.var n)
      | app {f a} : Neutral f → Neutral (.app f a)
    
    namespace HasType
    
    variable {S : Type u} {P : Specification S} {Γ : List (Expr S)}

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

57. theorem OAI.PureTypeSystem.HasType.sort_cannot_have_product_type line 597
58. theorem OAI.PureTypeSystem.HasType.product_cannot_have_product_type line 602
59. theorem OAI.PureTypeSystem.HasType.lambda_cannot_have_sort_type line 607
60. theorem OAI.PureTypeSystem.HasType.neutral_unique line 614

    Source documentation

    No functionality is needed for neutral uniqueness: the declaration fixes its head type, and product compatibility fixes every successive codomain.

    theorem neutral_unique {M A B : Expr S} (hn : Neutral M)
        (hA : HasType P Γ M A) (hB : HasType P Γ M B) : Converts A B := by
    …

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

61. theorem OAI.PureTypeSystem.HasType.normal_shape line 635
62. theorem OAI.PureTypeSystem.HasType.sorted_normal_shape line 651
63. inductive OAI.PureTypeSystem.TypingTree line 665
64. theorem OAI.PureTypeSystem.TypingTree.typing line 686

    Source documentation

    Root expected judgment, including the potentially unsorted final sort.

    theorem typing (t : TypingTree P Γ M T) : HasType P Γ M T := by
    …

    Mentions: OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.HasType

65. def OAI.PureTypeSystem.TypingTree.retarget line 695

    Source documentation

    Retarget only the root; all core data and all children are unchanged.

    def retarget {T' : Expr S} (t : TypingTree P Γ M T)
        (ht : HasType P Γ M T') (hc : Converts T' T) : TypingTree P Γ M T' := by
    …

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

66. theorem OAI.PureTypeSystem.TypingTree.nonempty line 706

    Source documentation

    Generation proves existence of finite stored trees without eliminating a Prop-valued typing derivation into data or assuming unique formation triples.

    theorem nonempty (h : HasType P Γ M T) : Nonempty (TypingTree P Γ M T) := by
    …

    Mentions: OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.TypingTree

67. def OAI.PureTypeSystem.TypingTree.ofTyping line 725
68. def OAI.PureTypeSystem.TypingTree.DeclRenaming line 729

    Source documentation

    A genuine variable renaming sends declarations to declarations, rather than merely to terms that happen to have convertible types.

    def DeclRenaming (Γ Δ : List (Expr S)) (ρ : Nat → Nat) : Prop :=
    …

    Mentions: OAI.PureTypeSystem.Expr

69. theorem OAI.PureTypeSystem.TypingTree.DeclRenaming.typed line 734
70. theorem OAI.PureTypeSystem.TypingTree.DeclRenaming.lift line 738
71. def OAI.PureTypeSystem.TypingTree.rename line 751

    Source documentation

    Thinning/reindexing transports every stored witness and preserves the whole tree shape. Binder annotations are transported too.

    noncomputable def rename (t : TypingTree P Γ M T) {Δ : List (Expr S)} (hΔ : ValidContext P Δ)
        (ρ : Nat → Nat) (hρ : DeclRenaming Γ Δ ρ) :
        TypingTree P Δ (M.rename ρ) (T.rename ρ) := by
    …

    Mentions: OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ValidContext, OAI.PureTypeSystem.TypingTree.DeclRenaming

72. theorem OAI.PureTypeSystem.TypingTree.DeclRenaming.weaken line 771
73. abbrev OAI.PureTypeSystem.TypingTree.StoredSubstitution line 776

    Source documentation

    Substitution carries stored trees at all declaration occurrences.

    abbrev StoredSubstitution (P : Specification S) (Γ Δ : List (Expr S))
        (σ : Nat → Expr S) : Type u :=
    …

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

74. theorem OAI.PureTypeSystem.TypingTree.StoredSubstitution.typed line 782
75. def OAI.PureTypeSystem.TypingTree.StoredSubstitution.lift line 785
76. def OAI.PureTypeSystem.TypingTree.subst line 813

    Source documentation

    Capture-avoiding substitution grafts the given trees at variables. It retains core choices and recurses through the annotation at each binder.

    noncomputable def subst (t : TypingTree P Γ M T) {Δ : List (Expr S)}
        (hΔ : ValidContext P Δ) (σ : Nat → Expr S) (ts : StoredSubstitution P Γ Δ σ) :
        TypingTree P Δ (M.subst σ) (T.subst σ) := by
    …

    Mentions: OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ValidContext, OAI.PureTypeSystem.TypingTree.StoredSubstitution

77. def OAI.PureTypeSystem.Expr.ProperPart line 835
78. theorem OAI.PureTypeSystem.Expr.ProperPart.child line 838
79. theorem OAI.PureTypeSystem.Expr.ProperPart.subterm line 839
80. theorem OAI.PureTypeSystem.Expr.ProperPart.trans_right line 842
81. theorem OAI.PureTypeSystem.Expr.ProperPart.trans_left line 846
82. theorem OAI.PureTypeSystem.Expr.Subterm.apps_head line 852
83. theorem OAI.PureTypeSystem.Expr.ProperPart.apps_arg line 859
84. theorem OAI.PureTypeSystem.Expr.subst_apps line 867
85. theorem OAI.PureTypeSystem.HasType.spine_shape line 876
86. theorem OAI.PureTypeSystem.HasType.app_spine line 892
87. theorem OAI.PureTypeSystem.HasType.apps_head line 904
88. theorem OAI.PureTypeSystem.HasType.apps_arg line 913
89. theorem OAI.PureTypeSystem.stronglyNormalizing_of_application line 928

    Source documentation

    The syntactic application principle implying strong normalization. This principle is proved from candidate interfaces, not assumed on the PTS normalization theorem.

    theorem stronglyNormalizing_of_application
        {S : Type u} {P : Specification S}
        (applySN : ∀ {Γ f a D E}, HasType P Γ f (.pi D E) → HasType P Γ a D →
          StronglyNormalizing f → StronglyNormalizing a → StronglyNormalizing (.app f a)) :
        SystemStronglyNormalizing P := by
    …

    Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.StronglyNormalizing, OAI.PureTypeSystem.SystemStronglyNormalizing

90. theorem OAI.PureTypeSystem.exists_bad_application line 960

    Source documentation

    A failed full-normalization theorem has an exact, well-typed application counterexample whose two children are already strongly normalizing.

    theorem exists_bad_application {S : Type u} {P : Specification S}
        (h : ¬ SystemStronglyNormalizing P) :
        ∃ Γ f a D E, HasType P Γ f (.pi D E) ∧ HasType P Γ a D ∧
          StronglyNormalizing f ∧ StronglyNormalizing a ∧ ¬ StronglyNormalizing (.app f a) := by
    …

    Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.SystemStronglyNormalizing, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.StronglyNormalizing

91. theorem OAI.PureTypeSystem.Normal.rename line 976