/-
  Topolei.Cubical.EvalTest
  ========================
  Roundtrip tests for the evaluator (cells-spec §13 Phase 1 Week 2 test:
  "eval roundtrip for simple terms").

  Each test uses the axiom equations from `Eval.lean` to reduce an
  evaluation call to a normal form and check the expected value.  These
  tests exercise:
    · free variables produce `nvar` neutrals,
    · identity lambda β-reduces correctly,
    · const-function β-reduces correctly (ignoring argument),
    · nested applications compose,
    · path abstractions close over their environment,
    · path applications β-reduce via `substDim`,
    · transport / composition terms produce the expected neutrals.
-/

import CubicalTransport.Eval

-- ── Free variable ───────────────────────────────────────────────────────────

/-- A free variable evaluates to a `nvar` neutral. -/
theorem eval_free_var (x : String) :
    eval .nil (.var x) = .vneu (.nvar x) := by
  rw [eval_var]; rfl

-- ── Identity β-redex ────────────────────────────────────────────────────────

/-- `(λx. x) y` β-reduces to the value of `y`.  With `y` free in the env,
    the result is `vneu (nvar "y")`. -/
theorem eval_identity_beta :
    eval .nil (.app (.lam "x" (.var "x")) (.var "y")) = .vneu (.nvar "y") := by
  rw [eval_app, eval_lam, eval_var]
  -- state: vApp (.vlam .nil "x" (.var "x")) ((CEnv.nil.lookup "y").getD _) = _
  have hlookup : (CEnv.nil.lookup "y").getD (.vneu (.nvar "y")) =
                 .vneu (.nvar "y") := rfl
  rw [hlookup, vApp_vlam, eval_var]
  -- state: ((CEnv.nil.extend "x" (vneu (nvar "y"))).lookup "x").getD _ = _
  simp [CEnv.extend]

-- ── Constant function ───────────────────────────────────────────────────────

/-- `(λx. z) y` β-reduces to the free variable `z`. -/
theorem eval_const_fun_beta :
    eval .nil (.app (.lam "x" (.var "z")) (.var "y")) = .vneu (.nvar "z") := by
  rw [eval_app, eval_lam, eval_var]
  have : (CEnv.nil.lookup "y").getD (.vneu (.nvar "y")) =
         .vneu (.nvar "y") := rfl
  rw [this, vApp_vlam, eval_var]
  -- After extend: lookup "z" in [("x", vneu "y")] → none → default
  simp [CEnv.extend, CEnv.lookup]

-- ── Nested application ──────────────────────────────────────────────────────

/-- `((λx. λy. x) a) b` β-reduces to `a` (K combinator applied). -/
theorem eval_K_combinator :
    eval .nil (.app (.app (.lam "x" (.lam "y" (.var "x"))) (.var "a")) (.var "b"))
    = .vneu (.nvar "a") := by
  rw [eval_app, eval_app, eval_lam, eval_var]
  have ha : (CEnv.nil.lookup "a").getD (.vneu (.nvar "a")) =
            .vneu (.nvar "a") := rfl
  rw [ha, vApp_vlam, eval_lam, eval_var]
  have hb : (CEnv.nil.lookup "b").getD (.vneu (.nvar "b")) =
            .vneu (.nvar "b") := rfl
  rw [hb, vApp_vlam, eval_var]
  -- env is now [("y", vneu "b"), ("x", vneu "a")]; lookup "x" finds "a".
  simp [CEnv.extend, CEnv.lookup]

-- ── Stuck application ──────────────────────────────────────────────────────

/-- Applying a free variable to another yields a stuck `napp` neutral. -/
theorem eval_stuck_app :
    eval .nil (.app (.var "f") (.var "x")) =
    .vneu (.napp (.nvar "f") (.vneu (.nvar "x"))) := by
  rw [eval_app, eval_var, eval_var]
  have hf : (CEnv.nil.lookup "f").getD (.vneu (.nvar "f")) =
            .vneu (.nvar "f") := rfl
  have hx : (CEnv.nil.lookup "x").getD (.vneu (.nvar "x")) =
            .vneu (.nvar "x") := rfl
  rw [hf, hx, vApp_vneu]

-- ── Dimension abstraction and application ──────────────────────────────────

/-- Path abstraction captures its environment as a `vplam`. -/
theorem eval_plam_closure (i : DimVar) (body : CTerm) :
    eval .nil (.plam i body) = .vplam .nil i body :=
  eval_plam _ _ _

/-- Path application β-reduces via `CTerm.substDim`. -/
theorem eval_papp_beta (i : DimVar) (body : CTerm) (r : DimExpr) :
    eval .nil (.papp (.plam i body) r) = eval .nil (body.substDim i r) := by
  rw [eval_papp, eval_plam, vPApp_vplam]

-- ── Transport and composition produce expected neutrals ────────────────────

-- ── Week 3: transport along refl = id ─────────────────────────────────────

/-- T1 at eval level: transport under a `.top` face reduces to its argument.
    (This is the spec's Week 3 test "transport along refl = id".) -/
theorem eval_transp_top_id (i : DimVar) (A : CType) (x : String) :
    eval .nil (.transp i A .top (.var x)) = .vneu (.nvar x) := by
  rw [eval_transp_top, eval_var]; rfl

/-- T2 at eval level: transport along a syntactically constant line reduces
    to its argument.  For `A = .univ`, this holds for any `φ` — via
    `eval_transp_top` when `φ = .top` and via `eval_transp_const` otherwise. -/
theorem eval_transp_const_univ (i : DimVar) (φ : FaceFormula) (x : String) :
    eval .nil (.transp i .univ φ (.var x)) = .vneu (.nvar x) := by
  by_cases hφ : φ = .top
  · subst hφ; rw [eval_transp_top, eval_var]; rfl
  · rw [eval_transp_const _ _ _ _ _ hφ
          (rfl : CType.dimAbsent i .univ = true),
        eval_var]; rfl

/-- T2 also discharges for `pi` when neither side mentions the binder. -/
theorem eval_transp_const_pi (i : DimVar) (φ : FaceFormula) (x : String) :
    eval .nil (.transp i (.pi .univ .univ) φ (.var x)) = .vneu (.nvar x) := by
  have h : CType.dimAbsent i (.pi .univ .univ) = true := rfl
  by_cases hφ : φ = .top
  · subst hφ; rw [eval_transp_top, eval_var]; rfl
  · rw [eval_transp_const _ _ _ _ _ hφ h, eval_var]; rfl

/-- Transport at a free-variable argument under a stuck face and non-constant
    non-pi non-path non-glue line produces a neutral `ntransp`.  The Π, Path,
    and Glue cases are handled by `eval_transp_pi` / `eval_transp_path` /
    the Glue-specific axioms in `Glue.lean`. -/
theorem eval_transp_neu (i : DimVar) (A : CType) (φ : FaceFormula) (x : String)
    (hφ : φ ≠ .top) (hA : CType.dimAbsent i A = false)
    (h_not_pi : ∀ domA codA, A ≠ .pi domA codA)
    (h_not_path : ∀ A₀ a b, A ≠ .path A₀ a b)
    (h_not_glue : ∀ φG T f fInv sec ret coh Ai,
        A ≠ .glue φG T f fInv sec ret coh Ai) :
    eval .nil (.transp i A φ (.var x)) =
    .vneu (.ntransp i A φ (.vneu (.nvar x))) := by
  rw [eval_transp_stuck _ _ _ _ _ hφ hA h_not_pi h_not_path h_not_glue, eval_var]
  rfl

-- ── Π-case with constant domain, varying codomain ────────────────────────────
--
-- Concrete setup: codomain varies in dimension `i` but domain is `.univ`
--   (constant).
--     Body: `pi univ (path univ (var "a") (papp (var "p") (dim-var i)))`.

private def i_dim : DimVar := ⟨"i"⟩

private def codAtype : CType :=
  .path .univ (.var "a") (.papp (.var "p") (DimExpr.var i_dim))

private theorem codAtype_varies : CType.dimAbsent i_dim codAtype = false := by decide

private theorem pi_univ_codA_varies :
    CType.dimAbsent i_dim (.pi .univ codAtype) = false := by decide

/-- vTransp along `pi .univ codAtype` produces a `vTranspFun` closure
    carrying both the (constant) domain and the (varying) codomain. -/
theorem eval_transp_pi_const_dom_example
    (φ : FaceFormula) (hφ : φ ≠ .top) (f : String) :
    eval .nil (.transp i_dim (.pi .univ codAtype) φ (.var f)) =
    .vTranspFun i_dim .univ codAtype φ (.vneu (.nvar f)) := by
  rw [eval_transp_pi _ _ _ _ _ _ hφ pi_univ_codA_varies, eval_var]
  rfl

/-- The CCHM Π β-rule at the value level, const-domain subcase.  The inner
    `vTranspInv` reduces to identity by `vTranspInv_const` (since `.univ`
    is absent from `i_dim`), and the outer `vTransp` on the varying
    codomain stalls into a neutral. -/
theorem vApp_vTranspFun_const_dom_reduces
    (φ : FaceFormula) (hφ : φ ≠ .top) (f y : String) :
    vApp (.vTranspFun i_dim .univ codAtype φ (.vneu (.nvar f))) (.vneu (.nvar y)) =
    .vneu (.ntransp i_dim codAtype φ
            (.vneu (.napp (.nvar f) (.vneu (.nvar y))))) := by
  -- CCHM Π β-rule
  rw [vApp_vTranspFun]
  -- Inverse transport through constant domain `.univ` is identity
  rw [vTranspInv_const i_dim .univ φ _ (rfl : CType.dimAbsent i_dim .univ = true)]
  -- Apply `f` (a neutral) to `y` (a neutral) — stuck `napp`
  rw [vApp_vneu]
  -- Forward transport through the varying codomain — stuck neutral
  rw [vTransp_stuck _ _ _ _ hφ codAtype_varies (by intro _ _ h; nomatch h)]

-- ── Π-case with varying domain, varying codomain ─────────────────────────────
--
-- Concrete setup: BOTH domain and codomain vary in `i` — the full CCHM case
-- where inverse transport is non-trivial.
--     Body: `pi  (path univ (var "a0") (papp (var "p") (dim-var i)))
--               (path univ (var "b0") (papp (var "q") (dim-var i)))`.

private def domAtype : CType :=
  .path .univ (.var "a0") (.papp (.var "p") (DimExpr.var i_dim))

private def codBtype : CType :=
  .path .univ (.var "b0") (.papp (.var "q") (DimExpr.var i_dim))

private theorem domAtype_varies : CType.dimAbsent i_dim domAtype = false := by decide

private theorem codBtype_varies : CType.dimAbsent i_dim codBtype = false := by decide

private theorem pi_varying_all :
    CType.dimAbsent i_dim (.pi domAtype codBtype) = false := by decide

/-- vTransp along a pi with both sides varying still produces a unified
    `vTranspFun` — no special-case logic needed at the line level. -/
theorem eval_transp_pi_varying_dom
    (φ : FaceFormula) (hφ : φ ≠ .top) (f : String) :
    eval .nil (.transp i_dim (.pi domAtype codBtype) φ (.var f)) =
    .vTranspFun i_dim domAtype codBtype φ (.vneu (.nvar f)) := by
  rw [eval_transp_pi _ _ _ _ _ _ hφ pi_varying_all, eval_var]
  rfl

/-- The reversed domain line also varies in `i_dim`.  Reversing substitutes
    `i := inv i` in the right-endpoint `DimExpr.var i_dim`, producing
    `DimExpr.inv (DimExpr.var i_dim)`, which still mentions `i_dim`. -/
private theorem domAtype_reversed_varies :
    CType.dimAbsent i_dim (domAtype.substDimExpr i_dim (.inv (.var i_dim))) = false := by
  decide

/-- Full CCHM Π β-rule in the **varying-domain** case.  Applying a
    `vTranspFun i_dim domAtype codBtype φ f` to `y`:
      1. inverse-transports `y` through `domAtype`  →  stuck
         (`ntransp i_dim (domAtype[i := inv i]) φ y`),
      2. applies `f` to the stuck result            →  stuck `napp`,
      3. forward-transports through `codBtype`      →  stuck `ntransp`.
    All three stalls cascade through the axiom equations without incident. -/
theorem vApp_vTranspFun_varying_dom_reduces
    (φ : FaceFormula) (hφ : φ ≠ .top) (f y : String) :
    vApp (.vTranspFun i_dim domAtype codBtype φ (.vneu (.nvar f))) (.vneu (.nvar y)) =
    .vneu (.ntransp i_dim codBtype φ
            (.vneu (.napp (.nvar f)
              (.vneu (.ntransp i_dim (domAtype.substDimExpr i_dim (.inv (.var i_dim))) φ
                (.vneu (.nvar y))))))) := by
  -- CCHM Π β-rule.
  rw [vApp_vTranspFun]
  -- Inverse transport unfolds to forward transport along the reversed line.
  unfold vTranspInv
  -- The reversed domAtype still varies in i_dim, so vTransp stalls.
  rw [vTransp_stuck _ _ _ _ hφ domAtype_reversed_varies
        (by intro _ _ h; nomatch h)]
  -- Apply the (neutral) f to the (now-neutral) argument → stuck `napp`.
  rw [vApp_vneu]
  -- Forward transport through the varying codomain → stuck `ntransp`.
  rw [vTransp_stuck _ _ _ _ hφ codBtype_varies (by intro _ _ h; nomatch h)]

-- ── Heterogeneous composition: C1, C2, const-line, and stuck ────────────────

/-- **C1 at eval level**: `comp` under a `.top` face reduces to its system
    body substituted at the `.one` endpoint.  Concrete exercise: with
    `u = .var "body"` (a free variable with no dim dependence) and `A = .univ`,
    the substitution is a no-op and the result is `vneu (nvar "body")`. -/
theorem eval_comp_top_example (i : DimVar) (t : String) :
    eval .nil (.comp i .univ .top (.var "body") (.var t)) =
    .vneu (.nvar "body") := by
  rw [eval_comp_top]
  -- (var "body").substDim i .one = var "body" (var case is trivial)
  simp only [CTerm.substDim]
  rw [eval_var]
  rfl

/-- C1 at eval level, with a body that actually uses the line's dim var.
    The substitution replaces the dim, but here `papp (var "p") i` becomes
    `papp (var "p") .one`, which evaluates via `vPApp` on a neutral. -/
theorem eval_comp_top_dim_subst (i : DimVar) (t : String) :
    eval .nil
      (.comp i .univ .top (.papp (.var "p") (.var i)) (.var t)) =
    .vneu (.npapp (.nvar "p") .one) := by
  rw [eval_comp_top]
  -- Reduce `(papp (var "p") (var i)).substDim i .one`:
  --   substDim on papp = papp (t.substDim ..) (DimExpr.subst ..)
  --   var "p" unchanged; DimExpr.subst i .one (var i) collapses via if_true.
  simp only [CTerm.substDim, DimExpr.subst, if_true]
  rw [eval_papp, eval_var]
  have hp : (CEnv.nil.lookup "p").getD (.vneu (.nvar "p")) = .vneu (.nvar "p") := rfl
  rw [hp, vPApp_vneu]

/-- **C2 at eval level**: `comp` under a `.bot` face reduces to `transp`
    under `.bot`.  When the line `A` is constant (here `.univ`), T2 then
    reduces the transport to identity. -/
theorem eval_comp_bot_univ (i : DimVar) (u t : String) :
    eval .nil (.comp i .univ .bot (.var u) (.var t)) =
    .vneu (.nvar t) := by
  rw [eval_comp_bot]
  -- eval (transp i .univ .bot (var t))
  rw [eval_transp_const _ _ _ _ _ (by intro h; nomatch h)
        (rfl : CType.dimAbsent i .univ = true),
      eval_var]
  rfl

/-- **Constant-line comp = hcomp**: when `A` is constant in `i`, het comp
    reduces to plain homogeneous composition.  The tube becomes
    `.plam i u` (a `vplam` closure).  When the whole thing is then
    evaluated at `.top` face, hcomp's top-case fires and `vPApp`s the
    tube at `.one`.  Verify end-to-end with a free-variable system body
    `u = .var "body"` (no dim dependence): the chain is
      comp (top) → substDim i .one → eval "body" → nvar "body". -/
theorem eval_comp_const_line (i : DimVar) (φ : FaceFormula)
    (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot) (t : String) :
    eval .nil (.comp i .univ φ (.var "body") (.var t)) =
    .vneu (.nhcomp .univ φ (.vplam .nil i (.var "body")) (.vneu (.nvar t))) := by
  rw [eval_comp_const _ _ _ _ _ _ hφ₁ hφ₂
        (rfl : CType.dimAbsent i .univ = true)]
  rw [eval_plam, eval_var]
  have : (CEnv.nil.lookup t).getD (.vneu (.nvar t)) = .vneu (.nvar t) := rfl
  rw [this]
  -- `vHCompValue .univ φ (vplam nil i (var "body")) (vneu (nvar t))`
  --   → stuck, since .univ is not .pi.
  exact vHCompValue_stuck _ _ _ _ hφ₁ (by intro _ _ h; nomatch h)

/-- Stuck comp: free variables, non-constant non-pi line, non-top non-bot face. -/
theorem eval_comp_neu (i : DimVar) (A : CType) (φ : FaceFormula) (u t : String)
    (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot) (hA : CType.dimAbsent i A = false)
    (h_not_pi : ∀ domA codA, A ≠ .pi domA codA) :
    eval .nil (.comp i A φ (.var u) (.var t)) =
    .vneu (.ncomp i A φ (.vneu (.nvar u)) (.vneu (.nvar t))) := by
  rw [eval_comp_stuck _ _ _ _ _ _ hφ₁ hφ₂ hA h_not_pi, eval_var, eval_var]
  have hu : (CEnv.nil.lookup u).getD (.vneu (.nvar u)) = .vneu (.nvar u) := rfl
  have ht : (CEnv.nil.lookup t).getD (.vneu (.nvar t)) = .vneu (.nvar t) := rfl
  rw [hu, ht]

-- ── Π hcomp: CCHM β-rule with pointwise reduction ──────────────────────────

/-- **Π hcomp β-rule at `.top`**: `hcomp (pi A B) .top tube base` is
    `vPApp tube .one` by `vHCompValue_top` — the tube covers the whole cube,
    so the composition's result is just the tube at `1`.  Demonstrate with
    a vplam tube: `tube = vplam .nil j (var "u_body")`.  The result is
    `eval .nil ((var "u_body").substDim j .one) = vneu (nvar "u_body")`. -/
theorem vHCompValue_top_reduces (j : DimVar) (base : CVal) :
    vHCompValue (.pi .univ .univ) .top (.vplam .nil j (.var "u_body")) base =
    .vneu (.nvar "u_body") := by
  rw [vHCompValue_top, vPApp_vplam]
  -- (var "u_body").substDim j .one = var "u_body" (no dim usage)
  simp only [CTerm.substDim]
  rw [eval_var]
  rfl

/-- **Π hcomp β-rule** at a non-top face, with concrete structure.
    Apply `hcomp (pi .univ .univ) φ tube base` to `y` where:
      · tube  = `.vneu (.nvar "tube")`         (a free variable),
      · base  = `.vneu (.nvar "base_fn")`      (a free function),
      · y     = `.vneu (.nvar "y")`.
    Expected reduction chain:
      1. `vHCompValue_pi` produces `vHCompFun .univ φ tube base`.
      2. `vApp_vHCompFun` unfolds to
           `vHCompValue .univ φ (.vTubeApp tube y) (vApp base y)`.
      3. `vApp_vneu` reduces `vApp base y` to `napp (nvar "base_fn") y`.
      4. `vHCompValue_stuck` on `.univ` produces the final neutral `nhcomp`. -/
theorem vApp_vHCompFun_reduces (φ : FaceFormula) (hφ : φ ≠ .top) :
    vApp (.vHCompFun .univ φ
            (.vneu (.nvar "tube"))
            (.vneu (.nvar "base_fn")))
         (.vneu (.nvar "y")) =
    .vneu (.nhcomp .univ φ
            (.vTubeApp (.vneu (.nvar "tube")) (.vneu (.nvar "y")))
            (.vneu (.napp (.nvar "base_fn") (.vneu (.nvar "y"))))) := by
  rw [vApp_vHCompFun, vApp_vneu,
      vHCompValue_stuck _ _ _ _ hφ (by intro _ _ h; nomatch h)]

/-- **vTubeApp reduction**: `(λj. (tube @ j) arg) @ r = (tube @ r) arg`.
    Exercised with a vplam tube: `tube = vplam .nil j (var "u_body")`.
    The chain:
      1. `vPApp_vTubeApp` unfolds to `vApp (vPApp tube r) arg`.
      2. `vPApp_vplam` reduces the inner `vPApp` to `eval .nil ("u_body"[j := r])`.
      3. The body doesn't mention j, so the substDim is identity.
      4. `eval_var` looks up "u_body" → `nvar "u_body"`.
      5. `vApp_vneu` produces `napp (nvar "u_body") arg`. -/
theorem vPApp_vTubeApp_reduces (j : DimVar) (r : DimExpr) :
    vPApp (.vTubeApp (.vplam .nil j (.var "u_body")) (.vneu (.nvar "arg"))) r =
    .vneu (.napp (.nvar "u_body") (.vneu (.nvar "arg"))) := by
  rw [vPApp_vTubeApp, vPApp_vplam]
  -- substDim j r (var "u_body") = var "u_body" (no dim dep)
  simp only [CTerm.substDim]
  rw [eval_var]
  have hlook : (CEnv.nil.lookup "u_body").getD (.vneu (.nvar "u_body")) =
               .vneu (.nvar "u_body") := rfl
  rw [hlook, vApp_vneu]

-- ── Path transport: CCHM endpoint reductions ─────────────────────────────────
--
-- Concrete path-transport setup.  A varying path line
--     `path A₀(i) a(i) b(i)`
-- where A₀ = .univ (so it doesn't vary),
--       a  = .var "a_line" (free variable; here conservatively no i-dep,
--            but could have),
--       b  = .papp (.var "b_pt") (DimExpr.var i_dim)   — uses i_dim
-- The right endpoint `b` mentions `i_dim`, so the whole path line varies.

private def pathLine_a : CTerm := .var "a_line"
private def pathLine_b : CTerm := .papp (.var "b_pt") (DimExpr.var i_dim)
private def pathLineA : CType := .path .univ pathLine_a pathLine_b

private theorem pathLineA_varies : CType.dimAbsent i_dim pathLineA = false := by decide

/-- Transport along a varying path line produces a `vPathTransp` closure
    storing the path term (as a CTerm, not a value). -/
theorem eval_transp_path_example
    (φ : FaceFormula) (hφ : φ ≠ .top) (p : String) :
    eval .nil (.transp i_dim pathLineA φ (.var p)) =
    .vPathTransp .nil i_dim .univ pathLine_a pathLine_b φ (.var p) := by
  show eval .nil
    (.transp i_dim (.path .univ pathLine_a pathLine_b) φ (.var p)) = _
  rw [eval_transp_path _ _ _ _ _ _ _ hφ pathLineA_varies]

/-- **Path transport at the `.zero` endpoint**: CCHM's `(j=0)` clause fires,
    yielding the line's left endpoint at `i=1` — here `.var "a_line"`
    (which has no `i`-dep, so its `substDim i .one` is itself). -/
theorem vPApp_vPathTransp_zero_reduces
    (φ : FaceFormula) (p : CTerm) :
    vPApp (.vPathTransp .nil i_dim .univ pathLine_a pathLine_b φ p) .zero =
    .vneu (.nvar "a_line") := by
  rw [vPApp_vPathTransp_zero]
  -- pathLine_a.substDim i_dim .one = pathLine_a (no dim dep; var case)
  show eval .nil (CTerm.substDim i_dim .one (.var "a_line")) = _
  simp only [CTerm.substDim]
  rw [eval_var]; rfl

/-- **Path transport at the `.one` endpoint**: CCHM's `(j=1)` clause fires,
    yielding the line's right endpoint at `i=1`.  Here `pathLine_b` mentions
    `i_dim`, so its `substDim i_dim .one` replaces the dim variable with
    `.one`, producing `papp (var "b_pt") .one`.  Evaluation then gives
    `npapp (nvar "b_pt") .one`. -/
theorem vPApp_vPathTransp_one_reduces
    (φ : FaceFormula) (p : CTerm) :
    vPApp (.vPathTransp .nil i_dim .univ pathLine_a pathLine_b φ p) .one =
    .vneu (.npapp (.nvar "b_pt") .one) := by
  rw [vPApp_vPathTransp_one]
  -- pathLine_b.substDim i_dim .one = papp (var "b_pt") (DimExpr.subst i_dim .one (DimExpr.var i_dim))
  --                                = papp (var "b_pt") .one
  simp only [pathLine_b, CTerm.substDim, DimExpr.subst, if_true]
  rw [eval_papp, eval_var]
  have hb : (CEnv.nil.lookup "b_pt").getD (.vneu (.nvar "b_pt")) =
            .vneu (.nvar "b_pt") := rfl
  rw [hb, vPApp_vneu]

/-- When the path line is fully constant (all of A₀, a, b absent from i),
    transport reduces via T2 at eval level (arm 2), returning the base
    unchanged — no `vPathTransp` produced. -/
theorem eval_transp_constant_path (i : DimVar) (φ : FaceFormula) (p : String) :
    eval .nil (.transp i (.path .univ (.var "a0") (.var "b0")) φ (.var p)) =
    .vneu (.nvar p) := by
  have hA : CType.dimAbsent i (.path .univ (.var "a0") (.var "b0")) = true :=
    rfl
  by_cases hφ : φ = .top
  · subst hφ; rw [eval_transp_top, eval_var]; rfl
  · rw [eval_transp_const _ _ _ _ _ hφ hA, eval_var]
    rfl

-- ── Multi-clause comp reductions ───────────────────────────────────────────────

/-- **Empty multi-clause comp reduces to plain transport.**  A `compN` with
    no clauses has no system — nothing to override, so the result is just
    transport of the base.  Demonstrated with `A = .univ` where transport is
    identity (via T2). -/
theorem eval_compN_empty (i : DimVar) (t : String) :
    eval .nil (.compN i .univ [] (.var t)) = .vneu (.nvar t) := by
  rw [eval_compN, vCompNAtTerm_def]
  -- find? on [] is none; filter on [] is []; [] arm → transport
  simp only [List.find?, List.filter]
  -- Now: eval .nil (.transp i .univ .bot (.var t))
  rw [eval_transp_const _ _ _ _ _ (by intro h; nomatch h)
        (rfl : CType.dimAbsent i .univ = true),
      eval_var]
  rfl

/-- **compN with a `.top`-faced clause fires on that clause**, returning
    the clause's body substituted at `i := .one`.  This is the CCHM
    full-system rule lifted to multi-clause. -/
theorem eval_compN_top_fires (i : DimVar) (u t : String) :
    eval .nil (.compN i .univ [(.top, .var u)] (.var t)) =
    .vneu (.nvar u) := by
  rw [eval_compN, vCompNAtTerm_def]
  -- find? matches the (.top, _) head immediately.
  simp only [List.find?]
  -- Goal: eval .nil ((var u).substDim i .one) = vneu (nvar u)
  simp only [CTerm.substDim]
  rw [eval_var]; rfl

/-- **compN where a `.top` clause is NOT at the head but later**: the
    scanning `find?` still picks it up.  Exercised with clauses
    `[(φ, _), (.top, u)]` for some non-top `φ`. -/
theorem eval_compN_top_later (i : DimVar) (u t : String) (k : DimVar) :
    eval .nil (.compN i .univ
      [(.eq0 k, .var "dummy"), (.top, .var u)] (.var t)) =
    .vneu (.nvar u) := by
  rw [eval_compN, vCompNAtTerm_def]
  -- find? skips (.eq0 k, _), hits (.top, _)
  simp only [List.find?]
  simp only [CTerm.substDim]
  rw [eval_var]; rfl

-- ── Path transport at a composite endpoint (inv .zero = .one) ────────────────
--
-- Demonstrates the key correctness property: even when the applied dim
-- expression isn't literally `.zero` or `.one`, if it *evaluates to* an
-- endpoint (e.g. `.inv .zero = 1`), the multi-clause `dimExprEq1` helper
-- detects this and fires the corresponding clause.

/-- **Path transport at `inv .zero`** (= 1 semantically) fires the (j=1)
    clause of the CCHM multi-clause system, yielding `b(1)`.  Exercises:
      · `FaceFormula.dimExprEq0 (inv .zero) = dimExprEq1 .zero = .bot`
      · `FaceFormula.dimExprEq1 (inv .zero) = dimExprEq0 .zero = .top`
    So the compN system becomes `[(φ, _), (.bot, a), (.top, b)]` and
    `vCompNAtTerm`'s `find?` picks the third clause. -/
theorem vPApp_vPathTransp_inv_zero
    (φ : FaceFormula) (hφ : φ ≠ .top) (hφbot : φ ≠ .bot) (p : CTerm) :
    vPApp (.vPathTransp .nil i_dim .univ pathLine_a pathLine_b φ p)
          (.inv .zero) =
    .vneu (.npapp (.nvar "b_pt") .one) := by
  rw [vPApp_vPathTransp_general _ _ _ _ _ _ _ _
        (by intro h; nomatch h)
        (by intro h; nomatch h)]
  -- After: vCompNAtTerm .nil i_dim .univ
  --          [(φ, p@(inv 0)), (dimExprEq0 (inv 0), a), (dimExprEq1 (inv 0), b)]
  --          (p@(inv 0))
  rw [vCompNAtTerm_def]
  -- Reduce the dimExprEq0/dimExprEq1 at inv .zero:
  --   dimExprEq0 (inv .zero) = dimExprEq1 .zero = .bot
  --   dimExprEq1 (inv .zero) = dimExprEq0 .zero = .top
  simp only [FaceFormula.dimExprEq0, FaceFormula.dimExprEq1]
  -- Now `find?` scans [(φ, _), (.bot, _), (.top, _)].  It skips φ (non-top
  -- by hφ), skips .bot (non-top), hits .top.
  -- The `match φ with .top => ... | _ => ...` on the head first clause
  -- reduces to `| _ => false` since φ ≠ .top.
  have _hφtop_eq : (match φ with | .top => true | _ => false) = false := by
    cases φ <;> first | rfl | exact absurd rfl hφ
  simp only [List.find?]
  -- Now `find?` on [(.bot, a), (.top, b)]: skip .bot, match .top.
  -- Continue reducing:
  show eval .nil (pathLine_b.substDim i_dim .one) = _
  simp only [pathLine_b, CTerm.substDim, DimExpr.subst, if_true]
  rw [eval_papp, eval_var]
  have hb : (CEnv.nil.lookup "b_pt").getD (.vneu (.nvar "b_pt")) =
            .vneu (.nvar "b_pt") := rfl
  rw [hb, vPApp_vneu]

-- ── Heterogeneous Π composition ─────────────────────────────────────────────

/-- **Hetero Π comp produces a `vCompFun`**: evaluating `comp^i (pi A B) φ u t`
    when the pi line genuinely varies packages everything into a closure
    that runs the CCHM β-rule on application. -/
theorem eval_comp_pi_example (u_name t_name : String)
    (φ : FaceFormula) (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot) :
    eval .nil (.comp i_dim (.pi domAtype codBtype) φ
                 (.var u_name) (.var t_name)) =
    .vCompFun .nil i_dim domAtype codBtype φ (.var u_name) (.var t_name) := by
  rw [eval_comp_pi _ _ _ _ _ _ _ hφ₁ hφ₂ pi_varying_all]

/-- **Const-domain hetero Π comp β degenerate case**: when `domA = .univ`
    (const in i), the fill `y_at_i` and `y_at_0` both reduce to `y` (via
    `vTransp_const`).  The inner comp becomes just `comp^i codB φ (u y) (t y)`. -/
theorem vApp_vCompFun_const_dom_example (u_name t_name y_name : String) (φ : FaceFormula) :
    vApp (.vCompFun .nil i_dim .univ codBtype φ (.var u_name) (.var t_name))
         (.vneu (.nvar y_name)) =
    eval (CEnv.nil.extend "$y" (.vneu (.nvar y_name)))
      (.comp i_dim codBtype φ
        (.app (.var u_name)
          (.transp ⟨"$fj"⟩
            ((CType.univ).substDimExpr i_dim
              (.join (.inv (.var ⟨"$fj"⟩)) (.var i_dim)))
            φ (.var "$y")))
        (.app (.var t_name)
          (.transp ⟨"$fj"⟩
            ((CType.univ).substDimExpr i_dim (.inv (.var ⟨"$fj"⟩)))
            φ (.var "$y")))) := by
  rw [vApp_vCompFun]

/-- **Varying-domain hetero Π comp β** also fires, producing the CCHM
    fill-based inner comp term.  Uses `domAtype` (genuinely varying in i). -/
theorem vApp_vCompFun_varying_dom_fires
    (u_name t_name y_name : String) (φ : FaceFormula) :
    vApp (.vCompFun .nil i_dim domAtype codBtype φ (.var u_name) (.var t_name))
         (.vneu (.nvar y_name)) =
    eval (CEnv.nil.extend "$y" (.vneu (.nvar y_name)))
      (.comp i_dim codBtype φ
        (.app (.var u_name)
          (.transp ⟨"$fj"⟩
            (domAtype.substDimExpr i_dim
              (.join (.inv (.var ⟨"$fj"⟩)) (.var i_dim)))
            φ (.var "$y")))
        (.app (.var t_name)
          (.transp ⟨"$fj"⟩
            (domAtype.substDimExpr i_dim (.inv (.var ⟨"$fj"⟩)))
            φ (.var "$y")))) := by
  rw [vApp_vCompFun]

/-- **Spot-check of the fill's endpoint correctness** at the CType level:
    `domAtype.substDimExpr i_dim (.join (.inv (.var fj)) (.var i_dim))`
    is NOT equal to `domAtype` (genuine substitution happens), confirming
    the fill construction is non-trivial. -/
example :
    domAtype.substDimExpr i_dim
      (.join (.inv (.var ⟨"$fj"⟩)) (.var i_dim)) =
    .path .univ (.var "a0")
      (.papp (.var "p") (.join (.inv (.var ⟨"$fj"⟩)) (.var i_dim))) := by
  simp only [domAtype, CType.substDimExpr, CTerm.substDim, DimExpr.subst]
  rfl