cubical-transport-hott-lean4/CubicalTransport/Question.lean

/-
  CubicalTransport.Question — The universal question form
  =======================================================
  Implements `docs/QUESTIONS.md` Level 1 (structural reification only).

  The CCHM partial-element-filler problem `comp i A φ u t` is *the*
  universal cubical question.  This module reifies that question as
  a Lean record `CompQ`, defines `ask` (run the engine), `Equiv`
  (answers coincide), and a vocabulary of classifying predicates
  that pin specific question shapes (`IsConstLine`, `IsFullFace`,
  `IsPathLine`, …).

  Level 1 commitment: structural reification only.  Existing
  `eval_comp_*` axioms are restated as classifier-conditioned
  `CompQ.Equiv` theorems.  Runtime / soundness behaviour unchanged;
  call sites continue to work via `q.ask`-equality lemmas.

  Levels 2 and 3 (routing through questions, question-driven proofs)
  are deferred — see QUESTIONS.md §4.

  Companion: `docs/QUESTIONS.md` (philosophy), `docs/ALGEBRA_PLAN.md`
  (the macro layer this enables), `docs/EULERIAN.md` (poetic record).
-/

import CubicalTransport.TransportLaws
import CubicalTransport.CompLaws
import CubicalTransport.DecEq

namespace Question

-- ── CompQ — the universal question, reified ─────────────────────────────────

/-- The CCHM partial-element-filler question, reified as data.

    Given a type-line `body` along binder `binder`, a face `φ`, a
    partial element `u` defined on `φ`, and a base `t` at `binder = 0`,
    `CompQ.ask` produces the engine's universal answer — a total
    element at `binder = 1` agreeing with `u` on `φ` and with `t` at
    `binder = 0`.

    Every cubical operation in the engine (`transp`, `hcomp`, `compN`,
    Path β/η, Glue β/η, univalence-transport) is a specialisation of
    this single shape.  See QUESTIONS.md §1 for the table. -/
structure CompQ where
  env    : CEnv
  binder : DimVar
  body   : CType
  φ      : FaceFormula
  u      : CTerm
  t      : CTerm

/-- "Asking" a question runs the engine on a `.comp` term.  Equivalent
    to `vCompAtTerm` by `Eval.lean`'s `.comp` arm of `eval`, but
    routed through `eval (.comp …)` so that the existing
    `eval_comp_*` axioms apply directly. -/
def CompQ.ask (q : CompQ) : CVal :=
  eval q.env (.comp q.binder q.body q.φ q.u q.t)

/-- Two questions are *equivalent* when their engine answers coincide.

    This is the coarsest useful relation: questions with different
    parameters can have the same answer.  It is reflexive, symmetric,
    and transitive (it's just `Eq` on `CVal`).  It is *not* the same
    as `q₁ = q₂` — two questions can share an answer without being
    syntactically identical. -/
def CompQ.Equiv (q₁ q₂ : CompQ) : Prop := q₁.ask = q₂.ask

@[refl] theorem CompQ.Equiv.refl (q : CompQ) : q.Equiv q := rfl

@[symm] theorem CompQ.Equiv.symm {q₁ q₂ : CompQ}
    (h : q₁.Equiv q₂) : q₂.Equiv q₁ := Eq.symm h

theorem CompQ.Equiv.trans {q₁ q₂ q₃ : CompQ}
    (h₁ : q₁.Equiv q₂) (h₂ : q₂.Equiv q₃) : q₁.Equiv q₃ :=
  Eq.trans h₁ h₂

/-- Smart constructor: every transport `transpⁱ A φ t` is the
    degenerate question `compⁱ A φ t t` (no side condition: the
    partial element equals the base).  See QUESTIONS.md §1, table
    row 1.

    The CompQ answer agrees with `eval env (.transp i A φ t)` when
    the base is constant in the line binder (the standard cubical
    typing premise); the engine's `vCompAtTerm` substitutes
    `t.substDim i .one` on the full-face case while `transp` runs
    `eval env t` directly.  See `CompQ.ask_of_transport_full_face`
    for the bridging lemma. -/
def CompQ.ofTransp (env : CEnv) (i : DimVar) (A : CType)
    (φ : FaceFormula) (t : CTerm) : CompQ :=
  { env := env, binder := i, body := A, φ := φ, u := t, t := t }

-- ── Classifiers — the meta-vocabulary of question shapes ─────────────────────

/-- The line is constant in its binder — `comp` reduces to `hcomp`
    (or to identity, on a full face). -/
def IsConstLine (q : CompQ) : Prop :=
  q.body.dimAbsent q.binder = true

/-- The face is the full face — the partial element covers the whole
    space, so the answer is its `binder := 1` value. -/
def IsFullFace (q : CompQ) : Prop := q.φ = .top

/-- The face is the empty face — only the base contributes; the
    question reduces to plain transport. -/
def IsEmptyFace (q : CompQ) : Prop := q.φ = .bot

/-- The base equals the partial element — this is a transport
    expressed in `comp` form, not a heterogeneous composition. -/
def IsTransport (q : CompQ) : Prop := q.u = q.t

/-- The line is a Path type — Path-specific reductions apply. -/
def IsPathLine (q : CompQ) : Prop :=
  ∃ A₀ a b, q.body = .path A₀ a b

/-- The line is a Glue type — Glue-specific reductions apply. -/
def IsGlueLine (q : CompQ) : Prop :=
  ∃ ψ T f fInv s r c A,
    q.body = .glue ψ T f fInv s r c A

/-- The line is a Π type — CCHM Π reductions apply. -/
def IsPiLine (q : CompQ) : Prop :=
  ∃ domA codA, q.body = .pi domA codA

/-- The line is a Σ type — Σ reductions apply (REL2.x). -/
def IsSigmaLine (q : CompQ) : Prop :=
  ∃ A B, q.body = .sigma A B

/-- The line is a schema-defined inductive — REL1 reductions apply. -/
def IsIndLine (q : CompQ) : Prop :=
  ∃ S params, q.body = .ind S params

/-- The line is the cubical interval — REL2 transport-on-𝕀 is
    identity (the interval is dim-absent in itself). -/
def IsIntervalLine (q : CompQ) : Prop :=
  q.body = .interval

/-- The line is the universe — universe-transport reductions apply
    (currently stuck; CCHM univalence-transport via `uaLine`). -/
def IsUnivLine (q : CompQ) : Prop :=
  q.body = .univ

-- ── Decidability for every classifier ───────────────────────────────────────
-- All classifiers are `Decidable`.  Syntactic ones (face / body-tag /
-- u=t equality) reduce directly to `DecidableEq` on existing types
-- (`FaceFormula`, `CType`, `CTerm` — the latter via the mutual
-- `decEq` block in `DecEq.lean`).  Existential body-shape classifiers
-- (`IsPathLine`, `IsGlueLine`, `IsPiLine`, `IsSigmaLine`, `IsIndLine`)
-- use `match h : q.body with` to inspect the head constructor and
-- reconstruct the existential witness.

instance (q : CompQ) : Decidable (IsConstLine q) :=
  inferInstanceAs (Decidable (q.body.dimAbsent q.binder = true))

instance (q : CompQ) : Decidable (IsFullFace q) :=
  inferInstanceAs (Decidable (q.φ = .top))

instance (q : CompQ) : Decidable (IsEmptyFace q) :=
  inferInstanceAs (Decidable (q.φ = .bot))

instance (q : CompQ) : Decidable (IsTransport q) :=
  inferInstanceAs (Decidable (q.u = q.t))

instance (q : CompQ) : Decidable (IsIntervalLine q) :=
  inferInstanceAs (Decidable (q.body = .interval))

instance (q : CompQ) : Decidable (IsUnivLine q) :=
  inferInstanceAs (Decidable (q.body = .univ))

instance (q : CompQ) : Decidable (IsPathLine q) :=
  match h : q.body with
  | .path A₀ a b => isTrue ⟨A₀, a, b, h⟩
  | .univ | .pi _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : CompQ) : Decidable (IsPiLine q) :=
  match h : q.body with
  | .pi domA codA => isTrue ⟨domA, codA, h⟩
  | .univ | .path _ _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : CompQ) : Decidable (IsSigmaLine q) :=
  match h : q.body with
  | .sigma A B => isTrue ⟨A, B, h⟩
  | .univ | .pi _ _ | .path _ _ _ | .glue _ _ _ _ _ _ _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : CompQ) : Decidable (IsGlueLine q) :=
  match h : q.body with
  | .glue ψ T f fInv s r c A => isTrue ⟨ψ, T, f, fInv, s, r, c, A, h⟩
  | .univ | .pi _ _ | .path _ _ _ | .sigma _ _ | .ind _ _ | .interval =>
      isFalse (fun ⟨_, _, _, _, _, _, _, _, hp⟩ => by rw [hp] at h; cases h)

instance (q : CompQ) : Decidable (IsIndLine q) :=
  match h : q.body with
  | .ind S params => isTrue ⟨S, params, h⟩
  | .univ | .pi _ _ | .path _ _ _ | .sigma _ _ | .glue _ _ _ _ _ _ _ _ | .interval =>
      isFalse (fun ⟨_, _, hp⟩ => by rw [hp] at h; cases h)

-- ── Restated axioms — classifier-conditioned question equivalence ─────────────
-- Level 1: each existing `eval_comp_*` axiom is restated as a
-- theorem about `CompQ.ask`.  These are derived (not new axioms);
-- they exist to give the question-form vocabulary first-class
-- access to the engine's reduction graph.
--
-- The pattern is always the same: classifiers on the LHS, an
-- equation about `q.ask` on the RHS.  Future Level 2 work will
-- chain these via `simp` on `CompQ.Equiv`.

namespace CompQ

/-- C1 in question form: full-face question's answer is the
    partial element substituted at `binder := 1`. -/
@[simp]
theorem ask_of_full_face (q : CompQ) (h : IsFullFace q) :
    q.ask = eval q.env (q.u.substDim q.binder .one) := by
  unfold ask
  rw [show q.φ = .top from h]
  exact eval_comp_top q.env q.binder q.body q.u q.t

/-- C2 in question form: empty-face question's answer is plain
    transport on the base. -/
@[simp]
theorem ask_of_empty_face (q : CompQ) (h : IsEmptyFace q) :
    q.ask = eval q.env (.transp q.binder q.body .bot q.t) := by
  unfold ask
  rw [show q.φ = .bot from h]
  exact eval_comp_bot q.env q.binder q.body q.u q.t

/-- Constant-line question: when the type doesn't vary along
    `binder`, heterogeneous comp reduces to `vHCompValue` (hcomp).
    Requires the face is neither full nor empty (those have their
    own theorems above). -/
@[simp]
theorem ask_of_const_line (q : CompQ)
    (hC : IsConstLine q)
    (hφ₁ : ¬ IsFullFace q) (hφ₂ : ¬ IsEmptyFace q) :
    q.ask = vHCompValue q.body q.φ
      (eval q.env (.plam q.binder q.u)) (eval q.env q.t) := by
  unfold ask
  exact eval_comp_const q.env q.binder q.body q.φ q.u q.t hφ₁ hφ₂ hC

/-- Helper: the negation of `IsConstLine` rewrites to the `= false`
    form expected by `eval_comp_pi` / `eval_comp_stuck`. -/
private theorem dimAbsent_eq_false_of_not_isConstLine (q : CompQ)
    (h : ¬ IsConstLine q) :
    CType.dimAbsent q.binder q.body = false := by
  unfold IsConstLine at h
  match hb : CType.dimAbsent q.binder q.body with
  | true  => exact absurd hb h
  | false => rfl

/-- Π-line question: hetero comp on a Π type packages into a
    `vCompFun` closure that runs CCHM Π β at application time.
    Requires the face is non-trivial and the line genuinely varies. -/
theorem ask_of_pi_line (q : CompQ)
    (hP : IsPiLine q)
    (hφ₁ : ¬ IsFullFace q) (hφ₂ : ¬ IsEmptyFace q)
    (hC : ¬ IsConstLine q) :
    ∃ domA codA, q.body = .pi domA codA ∧
      q.ask = .vCompFun q.env q.binder domA codA q.φ q.u q.t := by
  obtain ⟨domA, codA, hbody⟩ := hP
  refine ⟨domA, codA, hbody, ?_⟩
  unfold ask
  rw [hbody]
  apply eval_comp_pi q.env q.binder domA codA q.φ q.u q.t hφ₁ hφ₂
  have := dimAbsent_eq_false_of_not_isConstLine q hC
  rw [hbody] at this
  exact this

/-- Stuck question: face non-trivial, line genuinely varies, and
    type is neither Π nor any reducing shape — answer is a `ncomp`
    neutral.  Refinement of this for `IsIndLine`, `IsSigmaLine`,
    `IsIntervalLine`, etc., is Level 2 work. -/
theorem ask_of_stuck (q : CompQ)
    (hφ₁ : ¬ IsFullFace q) (hφ₂ : ¬ IsEmptyFace q)
    (hC : ¬ IsConstLine q)
    (hP : ¬ IsPiLine q) :
    q.ask = .vneu (.ncomp q.binder q.body q.φ
      (eval q.env q.u) (eval q.env q.t)) := by
  unfold ask
  apply eval_comp_stuck q.env q.binder q.body q.φ q.u q.t hφ₁ hφ₂
  · exact dimAbsent_eq_false_of_not_isConstLine q hC
  · intro domA codA hb
    exact hP ⟨domA, codA, hb⟩

-- ── Transport-shaped corollary ──────────────────────────────────────────────

/-- Transport-shaped question (`u = t`) under a full face: when the
    base is constant in the line binder (the cubical typing premise),
    the answer is `eval env t`.  This is the bridge between
    `CompQ.ofTransp` and the legacy `eval_transp_top` axiom. -/
@[simp]
theorem ask_of_transport_full_face (q : CompQ)
    (hT : IsTransport q) (hφ : IsFullFace q)
    (hi : q.t.dimAbsent q.binder = true) :
    q.ask = eval q.env q.t := by
  rw [ask_of_full_face q hφ, show q.u = q.t from hT,
      CTerm.substDim_of_absent q.binder .one q.t hi]

end CompQ

-- ── Level 2 — automated routing through `simp` ──────────────────────────────
-- The `@[simp]` attribute on the classifier-conditioned theorems above
-- lets Lean's `simp` rewrite `q.ask` automatically when a syntactic
-- classifier hypothesis is in scope.  These examples exercise the
-- routing on representative shapes; they also serve as sanity checks
-- that the simp-set composes (none of the lemmas mask each other).

example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
    let q : CompQ := ⟨env, i, A, .top, u, t⟩
    q.ask = eval env (u.substDim i .one) := by
  simp [CompQ.ask_of_full_face, IsFullFace]

example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
    let q : CompQ := ⟨env, i, A, .bot, u, t⟩
    q.ask = eval env (.transp i A .bot t) := by
  simp [CompQ.ask_of_empty_face, IsEmptyFace]

/-- The interval-line question with `u = t` (transport-shaped) and
    a base that doesn't depend on the binder reduces to `eval env t`.
    Demonstrates Level 2 chaining: full-face ⊕ transport ⊕ dim-absent
    base composed automatically by `simp`. -/
example (env : CEnv) (i : DimVar) (t : CTerm)
    (hi : t.dimAbsent i = true) :
    (CompQ.ofTransp env i .interval .top t).ask = eval env t := by
  apply CompQ.ask_of_transport_full_face
  · rfl
  · rfl
  · exact hi

end Question