IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCTypeTheoryParse

   1/-
   2  PrimitiveRecognitionCalculus/PRCTypeTheoryParse.lean
   3
   4  Item 4 of the δ frontier, second corpus parse: Martin-Löf type theory / CIC,
   5  faithfully encoded, shown to contain δ.
   6
   7  Prior δ4 work gave a toy type-theory witness, `ofTwoDistinct (Sum.inl ())
   8  (Sum.inr ())`. This module does the genuine thing using the type theory's own
   9  foundational machinery.
  10
  11  The canonical two-element type of Martin-Löf type theory is `𝟚` (Lean's `Bool`),
  12  with two closed terms `false` and `true`. The type theory's own way of working
  13  with this type is governed by:
  14
  15  * CANONICITY (`canonicity`): every closed term of `𝟚` reduces to one of the two
  16    canonical constructors. The type has EXACTLY two inhabitants; the distinction
  17    is not an artifact of notation, it is the full content of the type.
  18  * NO-CONFUSION / constructor disjointness (`no_confusion`): the two canonical
  19    terms are distinct. This is the type theory's own mechanism (the recursor /
  20    large elimination) for telling its constructors apart, the analog of the axiom
  21    of extensionality for sets.
  22
  23  `ttSystem` parses this foundation into the `FormalSystem` interface: tokens are
  24  closed terms of `𝟚`, the discrimination relation is the type theory's term
  25  inequality, the endpoints are the two canonical constructors. It is `Expressive`,
  26  so it realizes the δ core, and it falls on the δ side of the distinction
  27  dichotomy.
  28
  29  HONEST BOUNDARY. We encode the two-element type and its canonicity, which is all δ
  30  needs. We do not formalize the full term/derivation calculus of MLTT (Π, Σ, the
  31  identity type, universes). The δ core only requires the canonical two-term
  32  distinction, which `𝟚` supplies; richer type structure does not change the δ
  33  conclusion.
  34
  35  No project-local axioms. No sorry.
  36-/
  37
  38import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy
  39
  40namespace IndisputableMonolith
  41namespace Foundation
  42namespace PrimitiveRecognitionCalculus
  43namespace TypeTheoryParse
  44
  45open FormalSystem
  46
  47/-- The canonical two-element type `𝟚` of Martin-Löf type theory / CIC, here Lean's
  48own `Bool`. Its two closed terms are `false` and `true`. -/
  49abbrev Two := Bool
  50
  51/-- **Canonicity.** Every closed term of `𝟚` is one of the two canonical
  52constructors. The type has exactly two inhabitants. -/
  53theorem canonicity (b : Two) : b = false ∨ b = true := by
  54  cases b
  55  · exact Or.inl rfl
  56  · exact Or.inr rfl
  57
  58/-- **No-confusion / constructor disjointness.** The two canonical terms are
  59distinct: this is the recursor's verdict, the type theory's own distinction. -/
  60theorem no_confusion : (false : Two) ≠ true := by decide
  61
  62/-- MLTT parsed into the `FormalSystem` interface. Tokens are closed terms of `𝟚`;
  63the discrimination relation is term inequality; the endpoints are the two canonical
  64constructors; the expression order is the derivation-length order. -/
  65def ttSystem : FormalSystem where
  66  Token := Two
  67  Expr := ℕ
  68  distinguishes := fun a b => a ≠ b
  69  exprExtends := fun m n => m ≤ n
  70  endpointToken := fun e =>
  71    match e.side with
  72    | Side.left => false
  73    | Side.right => true
  74  traceExpr := Trace.length
  75  traceExpr_extends := fun h => InevitabilityInstances.length_le_of_extends h
  76
  77theorem ttSystem_expressive : ttSystem.Expressive := by
  78  show (false : Two) ≠ true
  79  decide
  80
  81/-- **MLTT contains the δ core.** -/
  82theorem ttSystem_embeds_delta : Nonempty (PRCEmbeddingInto ttSystem) :=
  83  FormalSystemEmbeddingTarget_proved ttSystem ttSystem_expressive
  84
  85theorem ttSystem_exprReflexive : DistinctionDichotomy.ExprReflexive ttSystem :=
  86  fun n => Nat.le_refl n
  87
  88theorem ttSystem_not_degenerate : ¬ DistinctionDichotomy.Degenerate ttSystem :=
  89  DistinctionDichotomy.not_degenerate_of_realizesDelta ttSystem ttSystem_embeds_delta
  90
  91/-- **The faithful parse, packaged.** Type theory's two-element type satisfies
  92canonicity (exactly two closed terms) and no-confusion (they are distinct), and the
  93foundation realizes the δ core. -/
  94theorem type_theory_realizes_delta :
  95    (∀ b : Two, b = false ∨ b = true)
  96      ∧ ((false : Two) ≠ true)
  97      ∧ Nonempty (PRCEmbeddingInto ttSystem) :=
  98  ⟨canonicity, no_confusion, ttSystem_embeds_delta⟩
  99
 100end TypeTheoryParse
 101end PrimitiveRecognitionCalculus
 102end Foundation
 103end IndisputableMonolith
 104