/-
  Topolei.Cubical.Subst
  =====================
  Dimension substitution for CType (Step 1 of the transport plan).

  CTerm already has  substDim : DimVar → DimExpr → CTerm → CTerm  (Syntax.lean).
  Here we add:

    CTerm.substDimBool : DimVar → Bool → CTerm → CTerm
      — specialises substDim to the two canonical endpoints (false = 0, true = 1).
      — Defined as a thin wrapper; no new recursion.

    CType.substDim : DimVar → Bool → CType → CType
      — Substitutes a dimension variable with a Bool endpoint throughout a type.
      — CType.path recurses into its CTerm endpoints via substDimBool.

  Key theorems:
    · Reduction lemmas (univ, pi, path) — proved by rfl.
    · substDimBool_eq_substDim — the wrapper unfolds correctly.
    · substDim_false_of_env / substDim_true_of_env — face connection:
        the Bool environment value at i selects which endpoint substitution applies.
    · substDim_idem — substituting twice at the same Bool is idempotent.

  Note: substDim_comm (disjoint dimensions commute) is deferred;
  it requires DimExpr.subst commutativity, which needs its own treatment.
-/

import CubicalTransport.Syntax

-- ── CTerm.substDimBool ────────────────────────────────────────────────────────

/-- Specialise CTerm.substDim to a Bool endpoint.
    false → substitute i with DimExpr.zero (the i=0 face)
    true  → substitute i with DimExpr.one  (the i=1 face) -/
def CTerm.substDimBool (i : DimVar) (b : Bool) (t : CTerm) : CTerm :=
  t.substDim i (if b then .one else .zero)

-- Unfolds to substDim by definition.
theorem CTerm.substDimBool_eq_substDim (i : DimVar) (b : Bool) (t : CTerm) :
    t.substDimBool i b = t.substDim i (if b then .one else .zero) := rfl

theorem CTerm.substDimBool_false (i : DimVar) (t : CTerm) :
    t.substDimBool i false = t.substDim i .zero := rfl

theorem CTerm.substDimBool_true (i : DimVar) (t : CTerm) :
    t.substDimBool i true = t.substDim i .one := rfl

-- ── CType.substDim ────────────────────────────────────────────────────────────
-- Substitute dimension variable i with Bool endpoint b throughout a type.
-- Path type endpoints are terms, so we delegate to CTerm.substDimBool.
--
-- `.ind S params` recurses pointwise through the parameter list via an
-- explicit mutually-recursive helper (`CType.substDim.params`); this
-- is the standard way to thread structural recursion through a
-- `List CType` field of a CType constructor.

mutual
  def CType.substDim (i : DimVar) (b : Bool) : CType → CType
    | .univ       => .univ
    | .pi A B     => .pi (A.substDim i b) (B.substDim i b)
    | .path A a t => .path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b)
    | .sigma A B  => .sigma (A.substDim i b) (B.substDim i b)
    | .glue φ T f fInv sec ret coh A =>
        .glue (φ.substDim i (if b then .one else .zero))
          (T.substDim i b)
          (f.substDimBool i b) (fInv.substDimBool i b)
          (sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
          (A.substDim i b)
    -- REL1: schema-defined inductive.  Recurse into params; the schema
    -- itself is static (its boundary CTerms are the schema's data, not
    -- caller-substituted dim-bound terms).
    | .ind S params => .ind S (CType.substDim.params i b params)

  /-- Pointwise `substDim` through a list of CType parameters. -/
  def CType.substDim.params (i : DimVar) (b : Bool) : List CType → List CType
    | []         => []
    | A :: rest  => A.substDim i b :: CType.substDim.params i b rest
end

-- ── CType.substDimExpr ────────────────────────────────────────────────────────
-- Substitute dimension variable `i` with an arbitrary `DimExpr r` throughout
-- a type.  Generalises `CType.substDim`, which fixes `r` to a Bool endpoint.
--
-- Used for *line reversal* in transport: the reversed line is
-- `A[i := inv i]`, which cannot be expressed as a Bool-endpoint
-- substitution because `inv i` is an open DimExpr.

mutual
  def CType.substDimExpr (i : DimVar) (r : DimExpr) : CType → CType
    | .univ       => .univ
    | .pi A B     => .pi (A.substDimExpr i r) (B.substDimExpr i r)
    | .path A a t => .path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r)
    | .sigma A B  => .sigma (A.substDimExpr i r) (B.substDimExpr i r)
    | .glue φ T f fInv sec ret coh A =>
        .glue (φ.substDim i r)
          (T.substDimExpr i r)
          (f.substDim i r) (fInv.substDim i r)
          (sec.substDim i r) (ret.substDim i r) (coh.substDim i r)
          (A.substDimExpr i r)
    | .ind S params => .ind S (CType.substDimExpr.params i r params)

  /-- Pointwise `substDimExpr` through a list of CType parameters. -/
  def CType.substDimExpr.params (i : DimVar) (r : DimExpr) : List CType → List CType
    | []         => []
    | A :: rest  => A.substDimExpr i r :: CType.substDimExpr.params i r rest
end

-- ── Reduction lemmas ──────────────────────────────────────────────────────────
-- All proved by rfl: substDim is defined by pattern matching, so these
-- hold definitionally.

namespace CType

theorem substDim_univ (i : DimVar) (b : Bool) :
    (univ).substDim i b = .univ := rfl

theorem substDim_pi (i : DimVar) (b : Bool) (A B : CType) :
    (pi A B).substDim i b = .pi (A.substDim i b) (B.substDim i b) := rfl

theorem substDim_path (i : DimVar) (b : Bool) (A : CType) (a t : CTerm) :
    (path A a t).substDim i b =
    .path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b) := rfl

theorem substDim_sigma (i : DimVar) (b : Bool) (A B : CType) :
    (sigma A B).substDim i b = .sigma (A.substDim i b) (B.substDim i b) := rfl

theorem substDim_glue (i : DimVar) (b : Bool) (φ : FaceFormula) (T : CType)
    (f fInv sec ret coh : CTerm) (A : CType) :
    (glue φ T f fInv sec ret coh A).substDim i b =
    .glue (φ.substDim i (if b then .one else .zero))
      (T.substDim i b)
      (f.substDimBool i b) (fInv.substDimBool i b)
      (sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
      (A.substDim i b) := rfl

theorem substDim_ind (i : DimVar) (b : Bool) (S : CTypeSchema) (params : List CType) :
    (ind S params).substDim i b = .ind S (CType.substDim.params i b params) := rfl

-- ── substDimExpr reduction lemmas ─────────────────────────────────────────────

theorem substDimExpr_univ (i : DimVar) (r : DimExpr) :
    (univ).substDimExpr i r = .univ := rfl

theorem substDimExpr_pi (i : DimVar) (r : DimExpr) (A B : CType) :
    (pi A B).substDimExpr i r =
    .pi (A.substDimExpr i r) (B.substDimExpr i r) := rfl

theorem substDimExpr_path (i : DimVar) (r : DimExpr) (A : CType) (a t : CTerm) :
    (path A a t).substDimExpr i r =
    .path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r) := rfl

theorem substDimExpr_sigma (i : DimVar) (r : DimExpr) (A B : CType) :
    (sigma A B).substDimExpr i r =
    .sigma (A.substDimExpr i r) (B.substDimExpr i r) := rfl

theorem substDimExpr_glue (i : DimVar) (r : DimExpr) (φ : FaceFormula) (T : CType)
    (f fInv sec ret coh : CTerm) (A : CType) :
    (glue φ T f fInv sec ret coh A).substDimExpr i r =
    .glue (φ.substDim i r)
      (T.substDimExpr i r)
      (f.substDim i r) (fInv.substDim i r)
      (sec.substDim i r) (ret.substDim i r) (coh.substDim i r)
      (A.substDimExpr i r) := rfl

theorem substDimExpr_ind (i : DimVar) (r : DimExpr) (S : CTypeSchema) (params : List CType) :
    (ind S params).substDimExpr i r = .ind S (CType.substDimExpr.params i r params) := rfl

-- The Bool-endpoint `substDim` is exactly `substDimExpr` at the canonical
-- endpoint `DimExpr`.  Proof is by pattern-matching `def` (rather than the
-- `induction` tactic) because `CType` is mutually inductive with `CTerm`.
-- `CTerm.substDimBool` is defined as `CTerm.substDim` at the same DimExpr,
-- so the path case closes by unfolding both.
--
-- `.ind` recurses into params via `substDim_eq_substDimExpr.params`,
-- a structurally-recursive helper that establishes pointwise equality
-- on the parameter list.

mutual
  def substDim_eq_substDimExpr (i : DimVar) (b : Bool) :
      (A : CType) →
      A.substDim i b = A.substDimExpr i (if b then DimExpr.one else DimExpr.zero)
    | .univ => rfl
    | .pi A B => by
        show CType.pi (A.substDim i b) (B.substDim i b) =
             CType.pi (A.substDimExpr i _) (B.substDimExpr i _)
        rw [substDim_eq_substDimExpr i b A, substDim_eq_substDimExpr i b B]
    | .path A a t => by
        show CType.path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b) =
             CType.path (A.substDimExpr i _) (a.substDim i _) (t.substDim i _)
        rw [substDim_eq_substDimExpr i b A,
            CTerm.substDimBool_eq_substDim,
            CTerm.substDimBool_eq_substDim]
    | .sigma A B => by
        show CType.sigma (A.substDim i b) (B.substDim i b) =
             CType.sigma (A.substDimExpr i _) (B.substDimExpr i _)
        rw [substDim_eq_substDimExpr i b A, substDim_eq_substDimExpr i b B]
    | .glue φ T f fInv sec ret coh A => by
        show CType.glue
               (φ.substDim i (if b then DimExpr.one else DimExpr.zero))
               (T.substDim i b)
               (f.substDimBool i b) (fInv.substDimBool i b)
               (sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
               (A.substDim i b)
           = CType.glue
               (φ.substDim i _)
               (T.substDimExpr i _)
               (f.substDim i _) (fInv.substDim i _)
               (sec.substDim i _) (ret.substDim i _) (coh.substDim i _)
               (A.substDimExpr i _)
        rw [substDim_eq_substDimExpr i b T,
            substDim_eq_substDimExpr i b A,
            CTerm.substDimBool_eq_substDim,
            CTerm.substDimBool_eq_substDim,
            CTerm.substDimBool_eq_substDim,
            CTerm.substDimBool_eq_substDim,
            CTerm.substDimBool_eq_substDim]
    | .ind S params => by
        show CType.ind S (CType.substDim.params i b params)
           = CType.ind S (CType.substDimExpr.params i _ params)
        rw [substDim_eq_substDimExpr.params i b params]

  /-- Helper: pointwise equality between `substDim.params` and
      `substDimExpr.params` at the canonical endpoint DimExpr. -/
  def substDim_eq_substDimExpr.params (i : DimVar) (b : Bool) :
      (params : List CType) →
      CType.substDim.params i b params =
      CType.substDimExpr.params i (if b then DimExpr.one else DimExpr.zero) params
    | []         => rfl
    | A :: rest => by
        show A.substDim i b :: CType.substDim.params i b rest
           = A.substDimExpr i _ :: CType.substDimExpr.params i _ rest
        rw [substDim_eq_substDimExpr i b A,
            substDim_eq_substDimExpr.params i b rest]
end

-- ── Face connection ───────────────────────────────────────────────────────────
-- These lemmas state the relationship between the Bool dimension environment
-- and which endpoint substitution applies.
--
-- Semantics: env i = false means we are at the i=0 face (eq0 i holds).
--            env i = true  means we are at the i=1 face (eq1 i holds).
-- The correct substitution to apply is therefore substDim i (env i).

/-- At the i=0 face (env i = false), substDim i (env i) is substDim i false. -/
theorem substDim_at_false (i : DimVar) (A : CType) (env : DimVar → Bool)
    (h : env i = false) :
    A.substDim i (env i) = A.substDim i false := by
  rw [h]

/-- At the i=1 face (env i = true), substDim i (env i) is substDim i true. -/
theorem substDim_at_true (i : DimVar) (A : CType) (env : DimVar → Bool)
    (h : env i = true) :
    A.substDim i (env i) = A.substDim i true := by
  rw [h]

-- ── Deferred: idempotence and commutativity ───────────────────────────────────
-- substDim_idem   : (A.substDim i b).substDim i b = A.substDim i b
-- substDim_comm   : for i ≠ j, (A.substDim i b).substDim j c = (A.substDim j c).substDim i b
--
-- Both require simultaneous induction over the CType/CTerm mutual inductive,
-- which needs a `mutual` proof block or a size-indexed recursor.
-- Deferred to a later pass after the DimLine and transport layers are in place.
--
-- Correctness argument (informal):
-- · After substDim i b, every DimExpr referencing i becomes zero or one
--   (neither of which contains free variables), so a second substDim i b
--   finds nothing left to substitute. Idempotence follows.
-- · Substituting disjoint dimensions i ≠ j affects non-overlapping parts
--   of every DimExpr (DimExpr.subst is capture-avoiding), so order is irrelevant.

theorem substDim_comm_univ (i j : DimVar) (b c : Bool) :
    ((univ : CType).substDim i b).substDim j c =
    ((univ : CType).substDim j c).substDim i b := rfl

end CType

-- Note: dimAbsent, substDimBool_idem, and substDim_idem are proved in DimLine.lean,
-- which is downstream in the import chain and has access to dimAbsent predicates.