OAI/Computability/TypeSystem/Congruence.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PureTypeSystem.ObservationValues.lambdaValue_congr line 11
  2. theorem OAI.PureTypeSystem.ObservationValues.applyValue_congr line 23
  3. theorem OAI.PureTypeSystem.ObservationValues.withBase_congr line 38
  4. theorem OAI.PureTypeSystem.ObservationValues.distinguished_congr line 46
  5. theorem OAI.PureTypeSystem.ObservationValues.PreResult.parameter_congr line 58
  6. theorem OAI.PureTypeSystem.ObservationValues.PreResult.val_congr line 67
  7. theorem OAI.PureTypeSystem.ObservationValues.PreResult.baseRead_congr line 78

    Source documentation

    A cross-context form of base projection congruence. The literal-sort condition is retained: arbitrary retargeting preserves Val, not every unused Read coordinate.

    theorem baseRead_congr (h : HasType P Γ M T) (h' : HasType P Δ M' T')
    (hM : (M.subst e.images).normalForm = (M'.subst f.images).normalForm)
    (hT : (T.subst e.images).normalForm = (T'.subst f.images).normalForm)
    (hS : (∃ s : S, T = .sort s ∧ ({s} : Set S) ∈ C) ↔
      (∃ s : S, T' = .sort s ∧ ({s} : Set S) ∈ C))
    (v : ActiveLayer P C (Ω.profile (T.subst e.images).normalForm) →
      Value (hw := hw) Ω C hno (T.subst e.images).normalForm)
…

    Mentions: OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.ObservationValues.PreResult.sort, OAI.PureTypeSystem.ActiveLayer, OAI.PureTypeSystem.ObservationValues.Value

  8. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstractionAction_congr line 113
  9. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstraction_val_congr line 133
  10. theorem OAI.PureTypeSystem.ObservationValues.PreResult.application_val_congr line 151
  11. theorem OAI.PureTypeSystem.ObservationValues.PreResult.productCandidate_congr line 180
  12. theorem OAI.PureTypeSystem.ObservationValues.PreResult.product_val_congr line 200
  13. theorem OAI.PureTypeSystem.ObservationValues.PreResult.product_read_congr line 231
  14. theorem OAI.PureTypeSystem.Expr.Scoped.subst_congr line 259
  15. theorem OAI.PureTypeSystem.Expr.rename_eq_sort line 280
  16. def OAI.PureTypeSystem.ObservationValues.Environment.Reindexed line 294

    Source documentation

    Matching old raw images and parameters under declaration reindexing. No equality is imposed on undeclared indices.

    def Reindexed (e : Environment (hw := hw) Ω C hno Γ)
…

    Mentions: OAI.PureTypeSystem.ObservationValues.Environment

  17. theorem OAI.PureTypeSystem.ObservationValues.Environment.Reindexed.raw_eq line 302
  18. theorem OAI.PureTypeSystem.ObservationValues.Environment.Reindexed.expr_eq line 307
  19. theorem OAI.PureTypeSystem.ObservationValues.Environment.Reindexed.type_eq line 310
  20. theorem OAI.PureTypeSystem.ObservationValues.Environment.Reindexed.cons line 313
  21. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_rename line 326
  22. def OAI.PureTypeSystem.TypingTree.recontext line 413

    Source documentation

    Context conversion retains every nonvariable core and all sort choices.

    noncomputable def recontext (t : TypingTree P Γ M T) (h : ContextEquivalent P Γ Δ) :
    TypingTree P Δ M T := by
…

    Mentions: OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.ContextEquivalent

  23. def OAI.PureTypeSystem.ObservationValues.Environment.SameData line 434
  24. theorem OAI.PureTypeSystem.ObservationValues.Environment.SameData.raw_eq line 440
  25. theorem OAI.PureTypeSystem.ObservationValues.Environment.SameData.expr_eq line 441
  26. theorem OAI.PureTypeSystem.ObservationValues.Environment.SameData.cons line 443
  27. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_recontext line 459
  28. def OAI.PureTypeSystem.Expr.consSub line 541
  29. theorem OAI.PureTypeSystem.ContextTower.profile_sort line 547
  30. theorem OAI.PureTypeSystem.FeasibleProfile.singleton line 560
  31. def OAI.PureTypeSystem.ObservationValues.baseGood line 572

    Source documentation

    Goodness is deliberately independent of observation parameters.

    def baseGood (M T : Expr S) (σ : Nat → Expr S) (v : Prop) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Expr

  32. def OAI.PureTypeSystem.ObservationValues.goodness line 578
  33. abbrev OAI.PureTypeSystem.ObservationValues.ValGood line 599
  34. abbrev OAI.PureTypeSystem.ObservationValues.ReadGood line 601
  35. def OAI.PureTypeSystem.ObservationValues.Relevant line 604
  36. theorem OAI.PureTypeSystem.ObservationValues.Relevant.pred line 608
  37. theorem OAI.PureTypeSystem.ObservationValues.relevant_actual_mem line 616
  38. theorem OAI.PureTypeSystem.ObservationValues.normal_baseGood line 626
  39. theorem OAI.PureTypeSystem.ObservationValues.normal_good line 636
  40. theorem OAI.PureTypeSystem.ObservationValues.normal_tree_independence line 714

    Source documentation

    Normal-syntax values forget all stored generation choices; normal Reads also forget their literal sort choice. No functionality hypothesis is used.

    theorem normal_tree_independence {Γ : List (Expr S)} {M T : Expr S}
    (t : TypingTree P Γ M T) : Normal M →
    ∀ {U : Expr S} (t' : TypingTree P Γ M U) (e : Environment (hw := hw) Ω C hno Γ),
…

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.Normal, OAI.PureTypeSystem.ObservationValues.Environment

  41. def OAI.PureTypeSystem.ContextTower.TypedSubstitution.Compatible line 817
  42. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.Compatible.expr_eq line 822
  43. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.Compatible.type_eq line 827
  44. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.Compatible.expr_profile line 832
  45. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.Compatible.type_profile line 836
  46. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.Compatible.cons line 841
  47. theorem OAI.PureTypeSystem.ContextTower.TypedSubstitution.Compatible.cons_same line 848
  48. theorem OAI.PureTypeSystem.ObservationValues.baseGood_congr line 859
  49. theorem OAI.PureTypeSystem.ObservationValues.goodness_compatible line 865
  50. theorem OAI.PureTypeSystem.Neutral.of_rename line 932
  51. theorem OAI.PureTypeSystem.Neutral.rename_iff line 939
  52. theorem OAI.PureTypeSystem.Expr.consSub_liftRen line 943
  53. theorem OAI.PureTypeSystem.ObservationValues.baseGood_rename line 951
  54. theorem OAI.PureTypeSystem.ObservationValues.goodness_rename line 955
  55. theorem OAI.PureTypeSystem.ObservationValues.valGood_retarget line 1025
  56. theorem OAI.PureTypeSystem.ContextTower.profile_converts line 1033
  57. theorem OAI.PureTypeSystem.ContextTower.instantiate_profile_ascent line 1040
  58. theorem OAI.PureTypeSystem.ContextTower.neutral_profile_ascent line 1051
  59. def OAI.PureTypeSystem.ObservationValues.SubstitutionGuard line 1080

    Source documentation

    Only nonneutral replacements need the activity guard. Variables that remain neutral are harmless even at a skipped clause.

    def SubstitutionGuard (Γ : List (Expr S)) (σ ξ : Nat → Expr S) : Prop :=
…

    Mentions: OAI.PureTypeSystem.Expr

  60. theorem OAI.PureTypeSystem.ObservationValues.neutral_subst_of_inactive line 1085
  61. theorem OAI.PureTypeSystem.ObservationValues.skipped_application_subst line 1099
  62. theorem OAI.PureTypeSystem.ObservationValues.skipped_read_subst line 1115
  63. theorem OAI.PureTypeSystem.ObservationValues.distinguished_base line 1134
  64. theorem OAI.PureTypeSystem.ObservationValues.PreResult.baseRead_eq line 1146
  65. theorem OAI.PureTypeSystem.ObservationValues.PreResult.product_read_base line 1155
  66. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_read_base line 1172
  67. theorem OAI.PureTypeSystem.ObservationValues.baseGood_active_iff line 1190
  68. theorem OAI.PureTypeSystem.ObservationValues.readGood_active_iff line 1202