/-
  Topolei.Cubical.Face
  ====================
  The face lattice F: distributive lattice generated by (i=0) and (i=1)
  with the fundamental relation (i=0) ∧ (i=1) = 0_F.

  Reference: CCHM §4.1
  Grammar:  ϕ, ψ ::= 0_F | 1_F | (i=0) | (i=1) | ϕ∧ψ | ϕ∨ψ

  Face formulas describe which sub-face of a cube we are on.
  The key invariant: (i=0) and (i=1) are mutually exclusive and jointly exhaustive.
-/

import CubicalTransport.Interval

-- ── Face formulas ─────────────────────────────────────────────────────────────

inductive FaceFormula where
  | bot                        : FaceFormula  -- 0_F
  | top                        : FaceFormula  -- 1_F
  | eq0 (i : DimVar)           : FaceFormula  -- (i = 0)
  | eq1 (i : DimVar)           : FaceFormula  -- (i = 1)
  | meet (ϕ ψ : FaceFormula)  : FaceFormula  -- ϕ ∧ ψ
  | join (ϕ ψ : FaceFormula)  : FaceFormula  -- ϕ ∨ ψ
  deriving Repr, Inhabited

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

def FaceFormula.eval (env : DimVar → Bool) : FaceFormula → Bool
  | .bot       => false
  | .top       => true
  | .eq0 i     => !(env i)
  | .eq1 i     => env i
  | .meet ϕ ψ => ϕ.eval env && ψ.eval env
  | .join ϕ ψ => ϕ.eval env || ψ.eval env

-- ── Fundamental laws ──────────────────────────────────────────────────────────
-- Strategy: simp only [eval] to unfold, then Bool case analysis.
-- Note: `show` is avoided here because `&&`/`||` bind looser than `=` in Lean 4,
-- causing parse surprises. `simp only [eval]` is cleaner and consistent.

namespace FaceFormula

-- (i=0) and (i=1) are mutually exclusive: their meet is always false
theorem eq0_meet_eq1 (i : DimVar) (env : DimVar → Bool) :
    (meet (eq0 i) (eq1 i)).eval env = false := by
  simp only [eval]
  cases env i <;> rfl

-- They are jointly exhaustive: their join is always true
theorem eq0_join_eq1 (i : DimVar) (env : DimVar → Bool) :
    (join (eq0 i) (eq1 i)).eval env = true := by
  simp only [eval]
  cases env i <;> rfl

-- Commutativity
theorem meet_comm (ϕ ψ : FaceFormula) (env : DimVar → Bool) :
    (meet ϕ ψ).eval env = (meet ψ ϕ).eval env := by
  simp only [eval]
  cases ϕ.eval env <;> cases ψ.eval env <;> rfl

theorem join_comm (ϕ ψ : FaceFormula) (env : DimVar → Bool) :
    (join ϕ ψ).eval env = (join ψ ϕ).eval env := by
  simp only [eval]
  cases ϕ.eval env <;> cases ψ.eval env <;> rfl

-- Associativity
theorem meet_assoc (ϕ ψ χ : FaceFormula) (env : DimVar → Bool) :
    (meet ϕ (meet ψ χ)).eval env = (meet (meet ϕ ψ) χ).eval env := by
  simp only [eval]
  cases ϕ.eval env <;> cases ψ.eval env <;> cases χ.eval env <;> rfl

theorem join_assoc (ϕ ψ χ : FaceFormula) (env : DimVar → Bool) :
    (join ϕ (join ψ χ)).eval env = (join (join ϕ ψ) χ).eval env := by
  simp only [eval]
  cases ϕ.eval env <;> cases ψ.eval env <;> cases χ.eval env <;> rfl

-- Identity laws
theorem meet_top (ϕ : FaceFormula) (env : DimVar → Bool) :
    (meet ϕ top).eval env = ϕ.eval env := by
  simp only [eval]
  cases ϕ.eval env <;> rfl

theorem join_bot (ϕ : FaceFormula) (env : DimVar → Bool) :
    (join ϕ bot).eval env = ϕ.eval env := by
  simp only [eval]
  cases ϕ.eval env <;> rfl

theorem meet_bot (ϕ : FaceFormula) (env : DimVar → Bool) :
    (meet ϕ bot).eval env = false := by
  simp only [eval]
  cases ϕ.eval env <;> rfl

theorem join_top (ϕ : FaceFormula) (env : DimVar → Bool) :
    (join ϕ top).eval env = true := by
  simp only [eval]
  cases ϕ.eval env <;> rfl

-- Distributivity
theorem distrib (ϕ ψ χ : FaceFormula) (env : DimVar → Bool) :
    (meet ϕ (join ψ χ)).eval env = (join (meet ϕ ψ) (meet ϕ χ)).eval env := by
  simp only [eval]
  cases ϕ.eval env <;> cases ψ.eval env <;> cases χ.eval env <;> rfl

-- ── Face restriction ──────────────────────────────────────────────────────────

/-- Restrict a face formula by fixing dimension i to value b.
    This is the substitution ϕ(i/b) from CCHM. -/
def restrict (i : DimVar) (b : Bool) : FaceFormula → FaceFormula
  | .bot       => .bot
  | .top       => .top
  | .eq0 j     => if j = i then (if b then .bot else .top) else .eq0 j
  | .eq1 j     => if j = i then (if b then .top else .bot) else .eq1 j
  | .meet ϕ ψ => .meet (restrict i b ϕ) (restrict i b ψ)
  | .join ϕ ψ => .join (restrict i b ϕ) (restrict i b ψ)

theorem eval_restrict (i : DimVar) (b : Bool) (ϕ : FaceFormula) (env : DimVar → Bool) :
    (restrict i b ϕ).eval env =
    ϕ.eval (fun j => if j = i then b else env j) := by
  induction ϕ with
  | bot         => rfl
  | top         => rfl
  | eq0 j       =>
      simp only [restrict, eval]
      by_cases h : j = i
      · subst h
        cases b <;> simp [eval]
      · simp only [if_neg h, eval]
  | eq1 j       =>
      simp only [restrict, eval]
      by_cases h : j = i
      · subst h
        cases b <;> simp [eval]
      · simp only [if_neg h, eval]
  | meet ϕ ψ ih_ϕ ih_ψ => simp only [restrict, eval, ih_ϕ, ih_ψ]
  | join ϕ ψ ih_ϕ ih_ψ => simp only [restrict, eval, ih_ϕ, ih_ψ]

-- Endpoint restriction lemmas (used in composition algorithm)
theorem restrict_eq0_false (i : DimVar) (env : DimVar → Bool) :
    (restrict i false (eq0 i)).eval env = true := by
  simp [restrict, eval]

theorem restrict_eq0_true (i : DimVar) (env : DimVar → Bool) :
    (restrict i true (eq0 i)).eval env = false := by
  simp [restrict, eval]

theorem restrict_eq1_true (i : DimVar) (env : DimVar → Bool) :
    (restrict i true (eq1 i)).eval env = true := by
  simp [restrict, eval]

theorem restrict_eq1_false (i : DimVar) (env : DimVar → Bool) :
    (restrict i false (eq1 i)).eval env = false := by
  simp [restrict, eval]

-- ── Entailment ────────────────────────────────────────────────────────────────

/-- ϕ entails ψ: whenever ϕ holds, ψ holds. -/
def Entails (ϕ ψ : FaceFormula) : Prop :=
  ∀ env : DimVar → Bool, ϕ.eval env = true → ψ.eval env = true

theorem entails_refl (ϕ : FaceFormula) : Entails ϕ ϕ :=
  fun _ h => h

theorem entails_trans (ϕ ψ χ : FaceFormula) :
    Entails ϕ ψ → Entails ψ χ → Entails ϕ χ :=
  fun h1 h2 env hϕ => h2 env (h1 env hϕ)

theorem entails_meet_left (ϕ ψ : FaceFormula) : Entails (meet ϕ ψ) ϕ :=
  fun env h => by
    simp only [eval] at h
    cases hϕ : ϕ.eval env
    · simp [hϕ] at h
    · rfl

theorem entails_join_left (ϕ ψ : FaceFormula) : Entails ϕ (join ϕ ψ) :=
  fun env h => by simp only [eval, h, Bool.true_or]

theorem entails_join_right (ϕ ψ : FaceFormula) : Entails ψ (join ϕ ψ) :=
  fun env h => by simp only [eval, h, Bool.or_true]

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

/-- Syntactic check: `i` does not appear in the face formula. -/
def dimAbsent (i : DimVar) : FaceFormula → Bool
  | .bot       => true
  | .top       => true
  | .eq0 j     => j != i
  | .eq1 j     => j != i
  | .meet ϕ ψ => ϕ.dimAbsent i && ψ.dimAbsent i
  | .join ϕ ψ => ϕ.dimAbsent i && ψ.dimAbsent i

-- ── DimExpr → FaceFormula: "the DimExpr equals 0 / 1" ────────────────────────
-- These translate a DimExpr r into a FaceFormula saying "r = 0" (or "r = 1").
-- Used by FaceFormula.substDim below: when we substitute a dim variable j
-- that appears inside `eq0 j` with a DimExpr r, the result should encode
-- "r = 0" as a face, which — for composite r — is itself a composite face.
--
-- De Morgan at the DimExpr ↔ FaceFormula boundary:
--   (meet r s = 0) ↔ (r = 0 ∨ s = 0)       [meet zero: either factor is 0]
--   (join r s = 0) ↔ (r = 0 ∧ s = 0)       [join zero: both factors are 0]
--   (inv r = 0)    ↔ (r = 1)
-- Dually for "= 1".

mutual
  /-- Build a FaceFormula expressing `r = 0` for an arbitrary DimExpr `r`. -/
  def dimExprEq0 : DimExpr → FaceFormula
    | .zero      => .top
    | .one       => .bot
    | .var k     => .eq0 k
    | .inv r     => dimExprEq1 r
    | .meet r s  => .join (dimExprEq0 r) (dimExprEq0 s)
    | .join r s  => .meet (dimExprEq0 r) (dimExprEq0 s)

  /-- Build a FaceFormula expressing `r = 1` for an arbitrary DimExpr `r`. -/
  def dimExprEq1 : DimExpr → FaceFormula
    | .zero      => .bot
    | .one       => .top
    | .var k     => .eq1 k
    | .inv r     => dimExprEq0 r
    | .meet r s  => .meet (dimExprEq1 r) (dimExprEq1 s)
    | .join r s  => .join (dimExprEq1 r) (dimExprEq1 s)
end

-- ── Face formula substitution by DimExpr ─────────────────────────────────────

/-- Substitute a dimension variable `i` with an arbitrary `DimExpr r`
    throughout a face formula.  Uses `dimExprEq0`/`dimExprEq1` to encode
    the composite faces arising from substitution into `eq0 j`/`eq1 j`. -/
def substDim (i : DimVar) (r : DimExpr) : FaceFormula → FaceFormula
  | .bot       => .bot
  | .top       => .top
  | .eq0 j     => if j = i then dimExprEq0 r else .eq0 j
  | .eq1 j     => if j = i then dimExprEq1 r else .eq1 j
  | .meet ϕ ψ => .meet (ϕ.substDim i r) (ψ.substDim i r)
  | .join ϕ ψ => .join (ϕ.substDim i r) (ψ.substDim i r)

-- ── Correctness: dimExprEq0/1 compute the right predicate ───────────────────
-- The semantic content: `(dimExprEq0 r).eval env = !(r.eval env)`, i.e. the
-- face holds iff r evaluates to 0 (= false in Bool).

mutual
  theorem dimExprEq0_eval (r : DimExpr) (env : DimVar → Bool) :
      (dimExprEq0 r).eval env = !(r.eval env) := by
    cases r with
    | zero => rfl
    | one  => rfl
    | var k => rfl
    | inv s =>
        show (dimExprEq1 s).eval env = _
        rw [dimExprEq1_eval s env]
        simp [DimExpr.eval]
    | meet s t =>
        show ((dimExprEq0 s).join (dimExprEq0 t)).eval env = _
        simp only [eval]
        rw [dimExprEq0_eval s env, dimExprEq0_eval t env]
        simp [DimExpr.eval, Bool.not_and]
    | join s t =>
        show ((dimExprEq0 s).meet (dimExprEq0 t)).eval env = _
        simp only [eval]
        rw [dimExprEq0_eval s env, dimExprEq0_eval t env]
        simp [DimExpr.eval, Bool.not_or]

  theorem dimExprEq1_eval (r : DimExpr) (env : DimVar → Bool) :
      (dimExprEq1 r).eval env = r.eval env := by
    cases r with
    | zero => rfl
    | one  => rfl
    | var k => rfl
    | inv s =>
        show (dimExprEq0 s).eval env = _
        rw [dimExprEq0_eval s env]
        simp [DimExpr.eval]
    | meet s t =>
        show ((dimExprEq1 s).meet (dimExprEq1 t)).eval env = _
        simp only [eval]
        rw [dimExprEq1_eval s env, dimExprEq1_eval t env]
        simp [DimExpr.eval]
    | join s t =>
        show ((dimExprEq1 s).join (dimExprEq1 t)).eval env = _
        simp only [eval]
        rw [dimExprEq1_eval s env, dimExprEq1_eval t env]
        simp [DimExpr.eval]
end

-- ── Endpoint specialisations: substDim at .zero / .one agrees with restrict ──

theorem substDim_zero (i : DimVar) (ϕ : FaceFormula) :
    ϕ.substDim i .zero = ϕ.restrict i false := by
  induction ϕ with
  | bot => rfl
  | top => rfl
  | eq0 j => by_cases h : j = i <;> simp [substDim, restrict, h, dimExprEq0]
  | eq1 j => by_cases h : j = i <;> simp [substDim, restrict, h, dimExprEq1]
  | meet ϕ ψ ihϕ ihψ => simp [substDim, restrict, ihϕ, ihψ]
  | join ϕ ψ ihϕ ihψ => simp [substDim, restrict, ihϕ, ihψ]

theorem substDim_one (i : DimVar) (ϕ : FaceFormula) :
    ϕ.substDim i .one = ϕ.restrict i true := by
  induction ϕ with
  | bot => rfl
  | top => rfl
  | eq0 j => by_cases h : j = i <;> simp [substDim, restrict, h, dimExprEq0]
  | eq1 j => by_cases h : j = i <;> simp [substDim, restrict, h, dimExprEq1]
  | meet ϕ ψ ihϕ ihψ => simp [substDim, restrict, ihϕ, ihψ]
  | join ϕ ψ ihϕ ihψ => simp [substDim, restrict, ihϕ, ihψ]

-- ── substDim is identity when dim is absent ──────────────────────────────────

theorem substDim_of_absent (i : DimVar) (r : DimExpr)
    (ϕ : FaceFormula) (h : ϕ.dimAbsent i = true) :
    ϕ.substDim i r = ϕ := by
  induction ϕ with
  | bot => rfl
  | top => rfl
  | eq0 j =>
      simp only [dimAbsent, bne_iff_ne] at h
      simp [substDim, if_neg h]
  | eq1 j =>
      simp only [dimAbsent, bne_iff_ne] at h
      simp [substDim, if_neg h]
  | meet ϕ ψ ihϕ ihψ =>
      simp only [dimAbsent, Bool.and_eq_true] at h
      simp [substDim, ihϕ h.1, ihψ h.2]
  | join ϕ ψ ihϕ ihψ =>
      simp only [dimAbsent, Bool.and_eq_true] at h
      simp [substDim, ihϕ h.1, ihψ h.2]

-- ── dimExprEq{0,1} dim-absence preservation ────────────────────────────────
-- Mutual recursion because dimExprEq0 and dimExprEq1 refer to each other
-- on `.inv`.

mutual
  /-- When `r` doesn't mention `j`, neither does `dimExprEq0 r`. -/
  theorem dimExprEq0_dimAbsent (j : DimVar) : (r : DimExpr) →
      r.dimAbsent j = true → (dimExprEq0 r).dimAbsent j = true
    | .zero, _ => rfl
    | .one,  _ => rfl
    | .var k, h => by
        simp only [DimExpr.dimAbsent, bne_iff_ne] at h
        simp [dimExprEq0, dimAbsent, bne_iff_ne, h]
    | .inv r, h => by
        simp only [DimExpr.dimAbsent] at h
        show (dimExprEq1 r).dimAbsent j = true
        exact dimExprEq1_dimAbsent j r h
    | .meet r s, h => by
        simp only [DimExpr.dimAbsent, Bool.and_eq_true] at h
        show ((dimExprEq0 r).join (dimExprEq0 s)).dimAbsent j = true
        simp only [dimAbsent, Bool.and_eq_true]
        exact ⟨dimExprEq0_dimAbsent j r h.1, dimExprEq0_dimAbsent j s h.2⟩
    | .join r s, h => by
        simp only [DimExpr.dimAbsent, Bool.and_eq_true] at h
        show ((dimExprEq0 r).meet (dimExprEq0 s)).dimAbsent j = true
        simp only [dimAbsent, Bool.and_eq_true]
        exact ⟨dimExprEq0_dimAbsent j r h.1, dimExprEq0_dimAbsent j s h.2⟩

  /-- When `r` doesn't mention `j`, neither does `dimExprEq1 r`. -/
  theorem dimExprEq1_dimAbsent (j : DimVar) : (r : DimExpr) →
      r.dimAbsent j = true → (dimExprEq1 r).dimAbsent j = true
    | .zero, _ => rfl
    | .one,  _ => rfl
    | .var k, h => by
        simp only [DimExpr.dimAbsent, bne_iff_ne] at h
        simp [dimExprEq1, dimAbsent, bne_iff_ne, h]
    | .inv r, h => by
        simp only [DimExpr.dimAbsent] at h
        show (dimExprEq0 r).dimAbsent j = true
        exact dimExprEq0_dimAbsent j r h
    | .meet r s, h => by
        simp only [DimExpr.dimAbsent, Bool.and_eq_true] at h
        show ((dimExprEq1 r).meet (dimExprEq1 s)).dimAbsent j = true
        simp only [dimAbsent, Bool.and_eq_true]
        exact ⟨dimExprEq1_dimAbsent j r h.1, dimExprEq1_dimAbsent j s h.2⟩
    | .join r s, h => by
        simp only [DimExpr.dimAbsent, Bool.and_eq_true] at h
        show ((dimExprEq1 r).join (dimExprEq1 s)).dimAbsent j = true
        simp only [dimAbsent, Bool.and_eq_true]
        exact ⟨dimExprEq1_dimAbsent j r h.1, dimExprEq1_dimAbsent j s h.2⟩
end

/-- `substDim j s` on `dimExprEq0 r` is identity when `r` doesn't mention `j`. -/
theorem dimExprEq0_substDim_of_absent (j : DimVar) (s : DimExpr)
    (r : DimExpr) (h : r.dimAbsent j = true) :
    (dimExprEq0 r).substDim j s = dimExprEq0 r :=
  substDim_of_absent j s _ (dimExprEq0_dimAbsent j r h)

/-- `substDim j s` on `dimExprEq1 r` is identity when `r` doesn't mention `j`. -/
theorem dimExprEq1_substDim_of_absent (j : DimVar) (s : DimExpr)
    (r : DimExpr) (h : r.dimAbsent j = true) :
    (dimExprEq1 r).substDim j s = dimExprEq1 r :=
  substDim_of_absent j s _ (dimExprEq1_dimAbsent j r h)

-- ── dimAbsent after substDim (i becomes absent after substituting i → r) ──

/-- After `substDim i r ϕ`, `i` is absent from the result — provided `r`
    itself doesn't mention `i`.  Needed downstream in `CTerm.dimAbsent_after_substDim`. -/
theorem dimAbsent_after_substDim (i : DimVar) (r : DimExpr)
    (hr : r.dimAbsent i = true) (ϕ : FaceFormula) :
    (ϕ.substDim i r).dimAbsent i = true := by
  induction ϕ with
  | bot => rfl
  | top => rfl
  | eq0 j =>
      simp only [substDim]
      by_cases hji : j = i
      · rw [hji, if_pos rfl]; exact dimExprEq0_dimAbsent i r hr
      · simp only [if_neg hji, dimAbsent, bne_iff_ne]; exact hji
  | eq1 j =>
      simp only [substDim]
      by_cases hji : j = i
      · rw [hji, if_pos rfl]; exact dimExprEq1_dimAbsent i r hr
      · simp only [if_neg hji, dimAbsent, bne_iff_ne]; exact hji
  | meet ϕ ψ ihϕ ihψ =>
      simp only [substDim, dimAbsent, Bool.and_eq_true]
      exact ⟨ihϕ, ihψ⟩
  | join ϕ ψ ihϕ ihψ =>
      simp only [substDim, dimAbsent, Bool.and_eq_true]
      exact ⟨ihϕ, ihψ⟩

-- ── substDim commutes with itself on disjoint dim variables ─────────────────

/-- Substituting disjoint dims `i` and `j` (with the RHS DimExprs not
    mentioning the opposite side's binder) commutes.  Required for the
    `CTerm.substDim_comm_aux` mutual induction through the new `transp`/
    `comp` arms that now substitute in the face formula. -/
theorem substDim_comm (i j : DimVar) (r s : DimExpr) (hij : i ≠ j)
    (hrj : r.dimAbsent j = true) (hsi : s.dimAbsent i = true)
    (ϕ : FaceFormula) :
    (ϕ.substDim i r).substDim j s = (ϕ.substDim j s).substDim i r := by
  induction ϕ with
  | bot => rfl
  | top => rfl
  | eq0 k =>
      by_cases hki : k = i
      · subst hki
        simp only [substDim, ite_true, if_neg hij]
        exact dimExprEq0_substDim_of_absent j s r hrj
      · by_cases hkj : k = j
        · subst hkj
          simp only [substDim, if_neg hki, ite_true]
          exact (dimExprEq0_substDim_of_absent i r s hsi).symm
        · simp [substDim, if_neg hki, if_neg hkj]
  | eq1 k =>
      by_cases hki : k = i
      · subst hki
        simp only [substDim, ite_true, if_neg hij]
        exact dimExprEq1_substDim_of_absent j s r hrj
      · by_cases hkj : k = j
        · subst hkj
          simp only [substDim, if_neg hki, ite_true]
          exact (dimExprEq1_substDim_of_absent i r s hsi).symm
        · simp [substDim, if_neg hki, if_neg hkj]
  | meet ϕ ψ ihϕ ihψ => simp [substDim, ihϕ, ihψ]
  | join ϕ ψ ihϕ ihψ => simp [substDim, ihϕ, ihψ]

-- ── Normalisation (Stage 4.3, 2026-04-23) ────────────────────────────────────
--
-- After `substDim`, face formulas can contain terms like `.meet .top φ`
-- or `.join .bot φ` (e.g. `.substDim i .zero` on `.eq0 i` produces
-- `.top` as a sub-term which may need propagation).  Rust's cubical
-- evaluator needs canonicalised faces to make dispatch deterministic:
-- the existing Glue-transport axioms hinge on `φ.substDim i .one = .bot`
-- or `= .top` literal equalities, which only hold after normalisation.
--
-- Reductions implemented (mirrors the semantic laws already in this
-- file):
--   · `.meet .top φ → φ`,   `.meet φ .top → φ`
--   · `.meet .bot _ → .bot`, `.meet _ .bot → .bot`
--   · `.join .bot φ → φ`,   `.join φ .bot → φ`
--   · `.join .top _ → .top`, `.join _ .top → .top`
--
-- Mutually-exclusive literal reductions (`.meet (.eq0 i) (.eq1 i) → .bot`,
-- etc.) are deliberately skipped — they require decidable equality on
-- `DimVar` in the reduction step and don't affect any current axiom.

@[extern "topolei_cubical_face_normalize"]
private opaque normalizeRust : FaceFormula → FaceFormula

/-- Canonical form under literal-identity / absorption reductions. -/
@[implemented_by normalizeRust]
def normalize : FaceFormula → FaceFormula
  | .bot     => .bot
  | .top     => .top
  | .eq0 i   => .eq0 i
  | .eq1 i   => .eq1 i
  | .meet ϕ ψ =>
      match normalize ϕ, normalize ψ with
      | .bot, _    => .bot
      | _, .bot    => .bot
      | .top, nψ   => nψ
      | nϕ, .top   => nϕ
      | nϕ, nψ     => .meet nϕ nψ
  | .join ϕ ψ =>
      match normalize ϕ, normalize ψ with
      | .top, _    => .top
      | _, .top    => .top
      | .bot, nψ   => nψ
      | nϕ, .bot   => nϕ
      | nϕ, nψ     => .join nϕ nψ

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

private theorem normalize_meet_aux (ϕ ψ : FaceFormula) (env : DimVar → Bool) :
    ((normalize (FaceFormula.meet ϕ ψ)).eval env) =
    (((normalize ϕ).eval env) && ((normalize ψ).eval env)) := by
  show (match normalize ϕ, normalize ψ with
        | FaceFormula.bot, _ => FaceFormula.bot
        | _, FaceFormula.bot => FaceFormula.bot
        | FaceFormula.top, nψ => nψ
        | nϕ, FaceFormula.top => nϕ
        | nϕ, nψ => FaceFormula.meet nϕ nψ).eval env =
      (((normalize ϕ).eval env) && ((normalize ψ).eval env))
  cases hϕ : normalize ϕ <;> cases hψ : normalize ψ <;> simp [eval]

private theorem normalize_join_aux (ϕ ψ : FaceFormula) (env : DimVar → Bool) :
    ((normalize (FaceFormula.join ϕ ψ)).eval env) =
    (((normalize ϕ).eval env) || ((normalize ψ).eval env)) := by
  show (match normalize ϕ, normalize ψ with
        | FaceFormula.top, _ => FaceFormula.top
        | _, FaceFormula.top => FaceFormula.top
        | FaceFormula.bot, nψ => nψ
        | nϕ, FaceFormula.bot => nϕ
        | nϕ, nψ => FaceFormula.join nϕ nψ).eval env =
      (((normalize ϕ).eval env) || ((normalize ψ).eval env))
  cases hϕ : normalize ϕ <;> cases hψ : normalize ψ <;> simp [eval]

/-- Normalisation is semantically transparent. -/
theorem normalize_preserves_eval (ϕ : FaceFormula) (env : DimVar → Bool) :
    (normalize ϕ).eval env = ϕ.eval env := by
  induction ϕ with
  | bot     => rfl
  | top     => rfl
  | eq0 i   => rfl
  | eq1 i   => rfl
  | meet ϕ ψ ihϕ ihψ =>
      have h := normalize_meet_aux ϕ ψ env
      rw [h, ihϕ, ihψ]
      rfl
  | join ϕ ψ ihϕ ihψ =>
      have h := normalize_join_aux ϕ ψ env
      rw [h, ihϕ, ihψ]
      rfl

end FaceFormula