/-
  Topolei.Cubical.Interval
  ========================
  The interval I: free de Morgan algebra on dimension variables.

  Reference: CCHM §3
  Grammar:  r, s ::= 0 | 1 | i | 1−r | r∧s | r∨s

  Strategy: prove the de Morgan laws *semantically* — they hold for every
  Boolean assignment of the dimension variables. Sound because Bool is itself
  a de Morgan algebra and DimExpr is freely generated over it.
-/

-- ── Dimension variables ───────────────────────────────────────────────────────

structure DimVar where
  name : String
  deriving DecidableEq, Repr

-- ── The Interval ──────────────────────────────────────────────────────────────

inductive DimExpr where
  | zero                  : DimExpr
  | one                   : DimExpr
  | var  (i : DimVar)     : DimExpr
  | inv  (r : DimExpr)    : DimExpr    -- 1 − r
  | meet (r s : DimExpr)  : DimExpr    -- r ∧ s
  | join (r s : DimExpr)  : DimExpr    -- r ∨ s
  deriving Repr, Inhabited

-- ── Semantic evaluation ───────────────────────────────────────────────────────

def DimExpr.eval (env : DimVar → Bool) : DimExpr → Bool
  | .zero     => false
  | .one      => true
  | .var i    => env i
  | .inv r    => !(r.eval env)
  | .meet r s => r.eval env && s.eval env
  | .join r s => r.eval env || s.eval env

-- ── de Morgan algebra laws ────────────────────────────────────────────────────
-- All proved by simp-unfolding eval and then Bool case analysis.
-- We use `simp only [eval]` (not plain `simp`) to avoid over-simplification
-- that would leave `<;> rfl` with no goals.

namespace DimExpr

theorem inv_zero (env : DimVar → Bool) :
    (inv zero).eval env = (one).eval env := by
  simp only [eval]; rfl

theorem inv_one (env : DimVar → Bool) :
    (inv one).eval env = (zero).eval env := by
  simp only [eval]; rfl

theorem inv_inv (r : DimExpr) (env : DimVar → Bool) :
    (inv (inv r)).eval env = r.eval env := by
  simp only [eval]; cases r.eval env <;> rfl

theorem inv_meet (r s : DimExpr) (env : DimVar → Bool) :
    (inv (meet r s)).eval env = (join (inv r) (inv s)).eval env := by
  simp only [eval]; cases r.eval env <;> cases s.eval env <;> rfl

theorem inv_join (r s : DimExpr) (env : DimVar → Bool) :
    (inv (join r s)).eval env = (meet (inv r) (inv s)).eval env := by
  simp only [eval]; cases r.eval env <;> cases s.eval env <;> rfl

theorem meet_comm (r s : DimExpr) (env : DimVar → Bool) :
    (meet r s).eval env = (meet s r).eval env := by
  simp only [eval]; cases r.eval env <;> cases s.eval env <;> rfl

theorem join_comm (r s : DimExpr) (env : DimVar → Bool) :
    (join r s).eval env = (join s r).eval env := by
  simp only [eval]; cases r.eval env <;> cases s.eval env <;> rfl

theorem meet_assoc (r s t : DimExpr) (env : DimVar → Bool) :
    (meet r (meet s t)).eval env = (meet (meet r s) t).eval env := by
  simp only [eval]
  cases r.eval env <;> cases s.eval env <;> cases t.eval env <;> rfl

theorem join_assoc (r s t : DimExpr) (env : DimVar → Bool) :
    (join r (join s t)).eval env = (join (join r s) t).eval env := by
  simp only [eval]
  cases r.eval env <;> cases s.eval env <;> cases t.eval env <;> rfl

theorem meet_one (r : DimExpr) (env : DimVar → Bool) :
    (meet r one).eval env = r.eval env := by
  simp only [eval]; cases r.eval env <;> rfl

theorem one_meet (r : DimExpr) (env : DimVar → Bool) :
    (meet one r).eval env = r.eval env := by
  simp only [eval]; cases r.eval env <;> rfl

theorem join_zero (r : DimExpr) (env : DimVar → Bool) :
    (join r zero).eval env = r.eval env := by
  simp only [eval]; cases r.eval env <;> rfl

theorem zero_join (r : DimExpr) (env : DimVar → Bool) :
    (join zero r).eval env = r.eval env := by
  simp only [eval]; cases r.eval env <;> rfl

theorem meet_zero (r : DimExpr) (env : DimVar → Bool) :
    (meet r zero).eval env = false := by
  simp only [eval]; cases r.eval env <;> rfl

theorem join_one (r : DimExpr) (env : DimVar → Bool) :
    (join r one).eval env = true := by
  simp only [eval]; cases r.eval env <;> rfl

theorem meet_distrib_join (r s t : DimExpr) (env : DimVar → Bool) :
    (meet r (join s t)).eval env = (join (meet r s) (meet r t)).eval env := by
  simp only [eval]
  cases r.eval env <;> cases s.eval env <;> cases t.eval env <;> rfl

theorem join_distrib_meet (r s t : DimExpr) (env : DimVar → Bool) :
    (join r (meet s t)).eval env = (meet (join r s) (join r t)).eval env := by
  simp only [eval]
  cases r.eval env <;> cases s.eval env <;> cases t.eval env <;> rfl

-- r ∧ (1−r) = 0  and  r ∨ (1−r) = 1  hold semantically (not in the free algebra)
theorem meet_inv_self (r : DimExpr) (env : DimVar → Bool) :
    (meet r (inv r)).eval env = false := by
  simp only [eval]; cases r.eval env <;> rfl

theorem join_inv_self (r : DimExpr) (env : DimVar → Bool) :
    (join r (inv r)).eval env = true := by
  simp only [eval]; cases r.eval env <;> rfl

-- ── Substitution ──────────────────────────────────────────────────────────────

def subst (i : DimVar) (r : DimExpr) : DimExpr → DimExpr
  | .zero     => .zero
  | .one      => .one
  | .var j    => if j = i then r else .var j
  | .inv s    => .inv (subst i r s)
  | .meet s t => .meet (subst i r s) (subst i r t)
  | .join s t => .join (subst i r s) (subst i r t)

theorem eval_subst (i : DimVar) (r s : DimExpr) (env : DimVar → Bool) :
    (subst i r s).eval env =
    s.eval (fun j => if j = i then r.eval env else env j) := by
  induction s with
  | zero      => rfl
  | one       => rfl
  | var j     =>
      simp only [subst, eval]
      by_cases h : j = i <;> simp [h, eval]
  | inv s ih  => simp only [subst, eval, ih]
  | meet s t ih_s ih_t => simp only [subst, eval, ih_s, ih_t]
  | join s t ih_s ih_t => simp only [subst, eval, ih_s, ih_t]

theorem eval_subst_zero (i : DimVar) (s : DimExpr) (env : DimVar → Bool) :
    (subst i zero s).eval env =
    s.eval (fun j => if j = i then false else env j) := by
  simp [eval_subst, eval]

theorem eval_subst_one (i : DimVar) (s : DimExpr) (env : DimVar → Bool) :
    (subst i one s).eval env =
    s.eval (fun j => if j = i then true else env j) := by
  simp [eval_subst, eval]

theorem eval_subst_inv (i : DimVar) (s : DimExpr) (env : DimVar → Bool) :
    (subst i (inv (var i)) s).eval env =
    s.eval (fun j => if j = i then !(env i) else env j) := by
  simp [eval_subst, eval]

-- ── Dimension absence ────────────────────────────────────────────────────────

/-- Syntactic check: `i` does not appear in the dim expression. -/
def dimAbsent (i : DimVar) : DimExpr → Bool
  | .zero      => true
  | .one       => true
  | .var j     => j != i
  | .inv r     => r.dimAbsent i
  | .meet r s  => r.dimAbsent i && s.dimAbsent i
  | .join r s  => r.dimAbsent i && s.dimAbsent i

/-- Bool endpoints have `dimAbsent = true` for every dimension. -/
theorem dimAbsent_endpoint (i : DimVar) (b : Bool) :
    (if b then DimExpr.one else DimExpr.zero).dimAbsent i = true := by
  cases b <;> rfl

-- ── Normalisation (Stage 4.1, 2026-04-23) ────────────────────────────────────
--
-- Reduce DimExprs to a canonical form by pushing `inv` reductions to
-- the literals.  Rust's cubical evaluator needs this to canonicalise
-- face formulas (otherwise `.inv .zero ≠ .one` structurally, and face
-- dispatch becomes unreliable).
--
-- Reductions implemented:
--   · `.inv .zero → .one`
--   · `.inv .one  → .zero`
--   · `.inv (.inv r) → r`         (double-negation cancellation)
--
-- The `.meet` / `.join` sub-terms are themselves normalised recursively
-- so that iterated inversion reduces through layers of conjunction /
-- disjunction.  Unit / absorption laws (e.g. `.meet .zero _ → .zero`)
-- are semantically valid but deliberately *not* implemented here — they
-- don't discharge any Lean-side axiom, and adding them would complicate
-- structural termination.  A future `DimExpr.normalize_full` can add
-- them when a well-founded measure is introduced.
--
-- Semantic correctness: `normalize_preserves_eval` shows the normal
-- form has the same Boolean evaluation under every environment.

@[extern "topolei_cubical_dimexpr_normalize"]
private opaque normalizeRust : DimExpr → DimExpr

/-- Canonical form under `inv`-reduction.  Idempotent:
    `normalize (normalize r) = normalize r`. -/
@[implemented_by normalizeRust]
def normalize : DimExpr → DimExpr
  | .zero     => .zero
  | .one      => .one
  | .var i    => .var i
  | .inv r    =>
      match normalize r with
      | .zero    => .one                 -- `.inv .zero` → `.one`
      | .one     => .zero                -- `.inv .one`  → `.zero`
      | .inv s   => s                    -- double-negation cancel
      | nr       => .inv nr              -- opaque; keep wrapped
  | .meet r s => .meet (normalize r) (normalize s)
  | .join r s => .join (normalize r) (normalize s)

-- ── Preservation of evaluation ──────────────────────────────────────────────

/-- Auxiliary lemma: the four-way match inside `normalize (.inv r)`
    produces a DimExpr whose `eval` equals the logical negation of
    `(normalize r).eval env`.  Each literal reduction (`.inv .zero → .one`,
    `.inv .one → .zero`, double-negation cancel) preserves this equation
    under Boolean semantics. -/
private theorem normalize_inv_aux (r : DimExpr) (env : DimVar → Bool) :
    (normalize (.inv r)).eval env = !((normalize r).eval env) := by
  show (match normalize r with
    | .zero => DimExpr.one | .one => DimExpr.zero
    | .inv s => s | nr => DimExpr.inv nr).eval env =
      !((normalize r).eval env)
  cases hnr : normalize r with
  | zero     => rfl
  | one      => rfl
  | var j    => rfl
  | inv s    =>
      -- match returns s; RHS is !((.inv s).eval env) = !(!(s.eval env)).
      show s.eval env = !((DimExpr.inv s).eval env)
      simp [eval]
  | meet a b => rfl
  | join a b => rfl

/-- Normalisation is semantically transparent: the normalised form has
    the same `eval` as the original, under every Bool environment. -/
theorem normalize_preserves_eval (r : DimExpr) (env : DimVar → Bool) :
    (normalize r).eval env = r.eval env := by
  induction r with
  | zero => rfl
  | one  => rfl
  | var i => rfl
  | inv r ih =>
      rw [normalize_inv_aux, ih]
      rfl
  | meet a b ih_a ih_b =>
      show (DimExpr.meet (normalize a) (normalize b)).eval env =
           (DimExpr.meet a b).eval env
      simp only [eval, ih_a, ih_b]
  | join a b ih_a ih_b =>
      show (DimExpr.join (normalize a) (normalize b)).eval env =
           (DimExpr.join a b).eval env
      simp only [eval, ih_a, ih_b]

-- ── Canonical-form literals ─────────────────────────────────────────────────

/-- `.inv .zero` normalises to `.one` — the fundamental literal rule. -/
theorem normalize_inv_zero : normalize (.inv .zero) = .one := rfl

/-- `.inv .one` normalises to `.zero`. -/
theorem normalize_inv_one : normalize (.inv .one) = .zero := rfl

/-- `.inv (.inv r)` normalises to the same value as `r` (semantically).
    Stated via eval rather than syntactically because structural double-
    negation cancellation depends on `r`'s post-normalisation shape. -/
theorem normalize_inv_inv_eval (r : DimExpr) (env : DimVar → Bool) :
    (normalize (.inv (.inv r))).eval env = r.eval env := by
  rw [normalize_preserves_eval]
  simp [eval]

end DimExpr