cubical-transport-hott-lean4/CubicalTransport/System.lean

/-
  CubicalTransport.System
  ======================
  Step 6 of the transport plan: partial elements — the [φ↦u] of composition.

  A System is a pair (face formula φ, body term u).  It represents a partial
  element defined wherever φ holds.  This is the new concept that separates
  composition from transport: transport has no system, composition has one.

  Compatibility (CompatAt0):
    The system must agree with the base term t₀ on the face φ ∩ (i=0).
    Formally: for every environment where both φ and (i=0) hold, the
    body at i=0 equals t₀.  This is the side-condition of the comp rule.

  Key theorems:
    · compat_bot   — empty system [0_F↦u] is compatible with any t₀ (vacuous)
    · compat_top   — full system [1_F↦u] requires u[i:=0] = t₀
    · compat_mono  — if s is compatible with t₀ and φ' ≤ φ, so is (φ', u)
    · System.Typed — packages the typing judgment on the body
-/

import CubicalTransport.Typing
-- (Typing.lean is below System in the import chain; System cannot be imported
--  from Typing.  The HasType.comp rule uses raw components.  This file provides
--  the System.Valid → HasType.comp convenience bridge.)

-- ── System definition ─────────────────────────────────────────────────────────

/-- A partial element: a face formula and a body term.
    Represents the term `u` defined wherever `φ` holds. -/
structure System where
  face : FaceFormula
  body : CTerm

-- ── Compatibility ─────────────────────────────────────────────────────────────

/-- Compatibility of system `s` with base term `t₀` along dimension `i`.
    Required side-condition for the composition typing rule.
    Meaning: on the face where both `s.face` and `(i = 0)` hold,
    the body of s substituted at i=0 equals t₀. -/
def System.CompatAt0 (s : System) (i : DimVar) (t₀ : CTerm) : Prop :=
  ∀ env : DimVar → Bool,
    s.face.eval env = true →
    env i = false →
    CTerm.substDimBool i false s.body = t₀

-- ── Compatibility lemmas ──────────────────────────────────────────────────────

/-- The empty system [0_F↦u] is compatible with any t₀.
    The face 0_F never holds, so the condition is vacuous. -/
theorem System.compat_bot (i : DimVar) (u t₀ : CTerm) :
    System.CompatAt0 { face := .bot, body := u } i t₀ := by
  intro env hbot _
  simp [FaceFormula.eval] at hbot

/-- The full system [1_F↦u] requires u[i:=0] = t₀.
    The face 1_F always holds, so the condition must hold for every env. -/
theorem System.compat_top_iff (i : DimVar) (u t₀ : CTerm) :
    System.CompatAt0 { face := .top, body := u } i t₀ ↔
    CTerm.substDimBool i false u = t₀ := by
  constructor
  · intro h
    -- apply at any env with env i = false
    have := h (fun _ => false) rfl rfl
    exact this
  · intro heq env _ _
    exact heq

/-- The meet system [φ ∧ ψ ↦ u] is compatible if the ψ-system is.
    (Monotonicity: a stronger face formula still satisfies compat.) -/
theorem System.compat_mono (i : DimVar) (u t₀ : CTerm)
    (φ ψ : FaceFormula)
    (hs : System.CompatAt0 { face := ψ, body := u } i t₀) :
    System.CompatAt0 { face := .meet φ ψ, body := u } i t₀ := by
  intro env hmeet hi
  simp only [FaceFormula.eval, Bool.and_eq_true] at hmeet
  exact hs env hmeet.2 hi

/-- If we tighten the face (φ' entails φ), compat is preserved. -/
theorem System.compat_entails (i : DimVar) (u t₀ : CTerm)
    (φ φ' : FaceFormula)
    (hent : FaceFormula.Entails φ' φ)
    (hs : System.CompatAt0 { face := φ, body := u } i t₀) :
    System.CompatAt0 { face := φ', body := u } i t₀ := by
  intro env hφ' hi
  exact hs env (hent env hφ') hi

-- ── Typed system ──────────────────────────────────────────────────────────────

/-- A typed system: the body has the 1-end type of the line.
    In the comp rule, the system provides the "target" elements on the face φ. -/
structure System.Typed {ℓ : ULevel} (Γ : Ctx) (s : System) (L : DimLine ℓ) : Prop where
  body_typed : HasType Γ s.body L.at1

-- ── Typed system lemmas ───────────────────────────────────────────────────────

/-- Construct a typed system with face `.bot`.  The face is irrelevant to the
    `System.Typed` structure — the body must still be typed at `L.at1`. -/
theorem System.typed_bot {ℓ : ULevel} (Γ : Ctx) (u : CTerm) (L : DimLine ℓ) :
    HasType Γ u L.at1 →
    System.Typed Γ { face := .bot, body := u } L :=
  fun h => { body_typed := h }

/-- Weakening for typed systems. -/
theorem System.Typed.weaken {ℓ ℓB : ULevel} (x : String) (B : CType ℓB) (Γ : Ctx)
    (s : System) (L : DimLine ℓ)
    (hs : System.Typed Γ s L) :
    System.Typed ((x, ⟨ℓB, B⟩) :: Γ) s L :=
  { body_typed := HasType.weaken x B hs.body_typed }

-- ── Joint compatibility + typing ──────────────────────────────────────────────

/-- Package compat and typing together — this is what the comp typing rule needs. -/
structure System.Valid {ℓ : ULevel}
    (Γ : Ctx) (s : System) (L : DimLine ℓ) (i : DimVar) (t₀ : CTerm) : Prop where
  typed  : System.Typed Γ s L
  compat : System.CompatAt0 s i t₀

/-- The empty system is valid for any t₀, given a body typed at L.at1. -/
theorem System.valid_bot {ℓ : ULevel}
    (Γ : Ctx) (u : CTerm) (L : DimLine ℓ) (i : DimVar) (t₀ : CTerm)
    (hu : HasType Γ u L.at1) :
    System.Valid Γ { face := .bot, body := u } L i t₀ :=
  { typed  := { body_typed := hu }
    compat := System.compat_bot i u t₀ }

-- ── Bridge: System.Valid → HasType.comp ──────────────────────────────────────

/-- Convert a System.Valid proof into the raw HasType.comp judgment.
    This is the ergonomic entry point: package everything in System.Valid,
    then call this to produce the typed composition term. -/
theorem HasType.comp_of_valid {ℓ : ULevel}
    (Γ : Ctx) (L : DimLine ℓ) (s : System) (t₀ : CTerm)
    (ht  : HasType Γ t₀ L.at0)
    (hv  : System.Valid Γ s L L.binder t₀) :
    HasType Γ (.comp L.binder L.body s.face s.body t₀) L.at1 :=
  HasType.comp L ht hv.typed.body_typed hv.compat