/-
  Topolei.Cubical.CompLaws
  ========================
  Residual step-level axiom for composition: subject reduction (C4).

  C1 (`comp_full`) and C2 (`comp_empty`), formerly stated here as
  step-level axioms, are now NbE theorems in `Cubical/Readback.lean`
  (`readback_comp_full` / `readback_comp_empty`).  The Rust backend's
  discharge obligations for composition reduce to: the eval-level
  axioms in `Eval.lean`, the readback-level axioms in `Readback.lean`,
  and the C4 residual below.

  Note on CCHM C3 (`transp = comp_{[φ↦t₀]} t₀`):
    CCHM expresses transport as a specialised composition.  That
    specialisation is only *typed* when the system body coincides with
    the base (u = t₀) and the compatibility `t₀[i:=0] = t₀` holds —
    i.e. `L.binder` is absent from `t₀`.  Stating it would duplicate
    the constant-line transport identity (`readback_transp_const_id`).
    The real CCHM reduction (`transp = hcomp + fill`) lives at the
    eval level; see `vCompFun` / `vApp_vCompFun` in `Eval.lean`.

  Why C4 stays step-level: same reason as T3 — needs a typing-
  preservation lemma on `eval`/`readback` (Stream B #2a).
-/

import CubicalTransport.System
import CubicalTransport.TransportLaws
import CubicalTransport.ValueTyping

-- ── Subject reduction for composition ────────────────────────────────────────

/-- **C4 (composition subject reduction)** — stepping a well-typed
    composition preserves the output type.

    **Now a theorem, not an axiom.**  Stage 2.3 consolidation: follows
    from `HasType.comp` and `CTerm.step_preserves_type` (ValueTyping.lean).
    Parallel to `transp_step_preserves` (T3).

    The `HasType.comp` constructor requires a compatibility side-condition
    on the system body (`u[i:=0] = t₀` wherever `φ ∩ (i=0)` is inhabited).
    Callers that cannot produce this side-condition should fall through
    to a per-callsite argument rather than using this theorem. -/
theorem comp_step_preserves (Γ : Ctx) (L : DimLine) (φ : FaceFormula)
    (u t₀ : CTerm)
    (ht : HasType Γ t₀ L.at0)
    (hu : HasType Γ u L.at1)
    (hc : ∀ env : DimVar → Bool,
        φ.eval env = true → env L.binder = false →
        CTerm.substDimBool L.binder false u = t₀) :
    HasType Γ (CTerm.step (.comp L.binder L.body φ u t₀)) L.at1 :=
  CTerm.step_preserves_type Γ _ _ (HasType.comp L ht hu hc)

-- ── Composition over schema-defined inductive types (REL1) ──────────────────
-- Composition over `.ind S params` flows through `eval_comp_stuck`
-- (`.ind ≠ .pi`).  Derived theorems below make the case explicit.
-- REL1.1 / REL2: pointwise distribution through ctor args.

/-- Composition over a non-trivial `.ind` line reduces to a stuck
    `ncomp` neutral.  Derived from `eval_comp_stuck`. -/
theorem eval_comp_ind (env : CEnv) (i : DimVar)
    (S : CTypeSchema) (params : List CType)
    (φ : FaceFormula) (u t : CTerm)
    (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
    (hA : CType.dimAbsent i (.ind S params) = false) :
    eval env (.comp i (.ind S params) φ u t) =
    .vneu (.ncomp i (.ind S params) φ (eval env u) (eval env t)) :=
  eval_comp_stuck env i (.ind S params) φ u t hφ₁ hφ₂ hA
    (by intro _ _ h; nomatch h)

/-- Composition over a constant `.ind` line reduces to homogeneous
    composition.  Derived from `eval_comp_const`. -/
theorem eval_comp_ind_const (env : CEnv) (i : DimVar)
    (S : CTypeSchema) (params : List CType)
    (φ : FaceFormula) (u t : CTerm)
    (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
    (hA : CType.dimAbsent i (.ind S params) = true) :
    eval env (.comp i (.ind S params) φ u t) =
    vHCompValue (.ind S params) φ (eval env (.plam i u)) (eval env t) :=
  eval_comp_const env i (.ind S params) φ u t hφ₁ hφ₂ hA

/-- Composition over `.ind` at `φ = .top`: the system covers everything,
    so the result is the tube body at `i := 1`.  Direct corollary of C1. -/
theorem eval_comp_ind_top (env : CEnv) (i : DimVar)
    (S : CTypeSchema) (params : List CType) (u t : CTerm) :
    eval env (.comp i (.ind S params) .top u t) =
    eval env (u.substDim i .one) :=
  eval_comp_top env i (.ind S params) u t

/-- Composition over `.ind` at `φ = .bot`: the system contributes nothing,
    so the result is transport of the base.  Direct corollary of C2. -/
theorem eval_comp_ind_bot (env : CEnv) (i : DimVar)
    (S : CTypeSchema) (params : List CType) (u t : CTerm) :
    eval env (.comp i (.ind S params) .bot u t) =
    eval env (.transp i (.ind S params) .bot t) :=
  eval_comp_bot env i (.ind S params) u t