diff --git a/CubicalTransport.lean b/CubicalTransport.lean index fc59ac2..de7a964 100644 --- a/CubicalTransport.lean +++ b/CubicalTransport.lean @@ -20,4 +20,5 @@ import CubicalTransport.System import CubicalTransport.CompLaws import CubicalTransport.Soundness import CubicalTransport.Inductive +import CubicalTransport.Bridge import CubicalTransport.PropertyTest diff --git a/CubicalTransport/Bridge.lean b/CubicalTransport/Bridge.lean new file mode 100644 index 0000000..e43d115 --- /dev/null +++ b/CubicalTransport/Bridge.lean @@ -0,0 +1,222 @@ +/- + CubicalTransport.Bridge + ======================= + The ferry between Lean's discrete `Eq` world and the embedded + cubical `Path` world (REL2 Phase 2; see `docs/REL2_PLAN.md`). + + Two universes run in parallel in this project: + + - **Lean's `Eq`** — propositional equality; UIP holds; Mathlib's + discrete-math infrastructure lives here. + - **Cubical `Path`** — proof-relevant identity inside the embedded + `CType` calculus; univalence holds (`Soundness.transp_ua`). + + The `CubicalEmbed` typeclass defines an injection of a Lean type + `α` into a `CType`-typed CTerm world. From there, two canonical + bridge directions: + + - **Forward (always):** `Eq.toPath : (a = b) → CTerm` of `Path` type. + Proof: a Lean equality lifts to a constant `.plam`. + - **Backward (canonical, REL2.0):** `Path.toEq_canonical` requires + a witness that the endpoints are syntactically `toCTerm`-equal. + This factors through `toCTerm_injective` (derived from + `roundtrip`). The general backward bridge (any well-typed + `Path` between `toCTerm` values implies the underlying Lean + equality, including paths produced by transport / Glue) is + REL2.1 — depends on the full Glue NbE story. + + - **Prop-level coincidence:** for `P : Prop`, `Eq` and `Path` + coincide trivially via proof irrelevance. + + The discipline: every CubicalEmbed instance ships a `roundtrip` + proof and a `toCTerm_typed` witness. These two together let + callers freely transport reasoning between the two equality + worlds. + + ## Status + + REL2.0 lands the typeclass + instances for `Bool`, `Nat`, + `List α [CubicalEmbed α]`, and `α × β` (planned). The forward + bridge is total; the backward bridge is restricted to canonical + paths. Full backward bridge: REL2.1. +-/ + +import CubicalTransport.Typing +import CubicalTransport.Inductive + +namespace CubicalTransport.Bridge + +open CubicalTransport.Inductive +open CubicalTransport.Inductive.CTerm + +-- ── §1. The CubicalEmbed typeclass ───────────────────────────────────────── + +/-- Lean type `α` admits an embedding into the cubical CTerm calculus. + + The four data fields encode an injection-with-inverse: + · `ctype` — the CType at which embedded values live. + · `toCTerm` — the embedding `α → CTerm`. + · `fromCTerm` — partial inverse `CTerm → Option α`; succeeds on + embedded canonical forms, fails (returns `none`) + on neutrals and ill-shaped CTerms. + · `roundtrip` — proof that `fromCTerm ∘ toCTerm = some`. + · `toCTerm_typed` — every embedded value has the declared `ctype`. +-/ +class CubicalEmbed (α : Type) where + ctype : CType + toCTerm : α → CTerm + fromCTerm : CTerm → Option α + roundtrip : ∀ a, fromCTerm (toCTerm a) = some a + toCTerm_typed : ∀ a, HasType [] (toCTerm a) ctype + +/-- The embedding is injective: distinct `α` values produce distinct + CTerms. Direct corollary of `roundtrip` — no per-instance proof + needed. -/ +theorem CubicalEmbed.toCTerm_injective {α} [CubicalEmbed α] + {a b : α} (h : CubicalEmbed.toCTerm a = CubicalEmbed.toCTerm b) : + a = b := by + have ha := CubicalEmbed.roundtrip (α := α) a + have hb := CubicalEmbed.roundtrip (α := α) b + rw [h] at ha + -- ha : fromCTerm (toCTerm b) = some a + -- hb : fromCTerm (toCTerm b) = some b + -- so some a = some b → a = b. + exact (Option.some_inj.mp (ha.symm.trans hb)) + +-- ── §2. Bool instance ────────────────────────────────────────────────────── + +instance : CubicalEmbed Bool where + ctype := CType.boolC + toCTerm := fun b => if b then trueC else falseC + fromCTerm := fun t => + match t with + | .ctor _ "false" _ _ => some false + | .ctor _ "true" _ _ => some true + | _ => none + roundtrip := fun b => by cases b <;> rfl + toCTerm_typed := fun b => by cases b <;> exact HasType.ctor + +-- ── §3. Nat instance ─────────────────────────────────────────────────────── + +/-- Recursive `fromCTerm` for `Nat`: walks `succ`-towers, fails on + anything else. -/ +def fromCTermNat : CTerm → Option Nat + | .ctor _ "zero" _ [] => some 0 + | .ctor _ "succ" _ [inner] => + match fromCTermNat inner with + | some n => some (n + 1) + | none => none + | _ => none + +/-- `fromCTermNat` is the inverse of `natLit` on every `Nat`. -/ +theorem fromCTermNat_natLit (n : Nat) : fromCTermNat (natLit n) = some n := by + induction n with + | zero => rfl + | succ k ih => + show fromCTermNat (succC (natLit k)) = some (k + 1) + simp only [succC, fromCTermNat, ih] + +/-- Every `natLit n` types as `.natC`. -/ +theorem natLit_typed (n : Nat) : HasType [] (natLit n) CType.natC := by + induction n with + | zero => exact HasType.ctor + | succ k _ => exact HasType.ctor + +instance : CubicalEmbed Nat where + ctype := CType.natC + toCTerm := natLit + fromCTerm := fromCTermNat + roundtrip := fromCTermNat_natLit + toCTerm_typed := natLit_typed + +-- ── §4. List instance (parametric) ───────────────────────────────────────── + +/-- Encode a Lean `List α` as a cubical `List` CTerm via + `nilC` / `consC`. Recursive on the list's spine. -/ +def listToCTerm {α} [CubicalEmbed α] : List α → CTerm + | [] => nilC (CubicalEmbed.ctype α) + | x :: xs => consC (CubicalEmbed.ctype α) + (CubicalEmbed.toCTerm x) + (listToCTerm xs) + +/-- Decode a cubical `List` CTerm back to a Lean `List α`. Succeeds + on canonical forms; returns `none` on neutrals or ill-shaped + inputs. -/ +def listFromCTerm {α} [CubicalEmbed α] : CTerm → Option (List α) + | .ctor _ "nil" _ [] => some [] + | .ctor _ "cons" _ [head, tail] => + match CubicalEmbed.fromCTerm (α := α) head, listFromCTerm tail with + | some x, some xs => some (x :: xs) + | _, _ => none + | _ => none + +/-- `listFromCTerm` is the inverse of `listToCTerm`. -/ +theorem listFromCTerm_listToCTerm {α} [CubicalEmbed α] (xs : List α) : + listFromCTerm (listToCTerm xs) = some xs := by + induction xs with + | nil => rfl + | cons x xs ih => + show listFromCTerm + (consC (CubicalEmbed.ctype α) (CubicalEmbed.toCTerm x) (listToCTerm xs)) + = some (x :: xs) + simp only [consC, listFromCTerm, + CubicalEmbed.roundtrip x, ih] + +/-- Every `listToCTerm xs` types as `.listC α.ctype`. -/ +theorem listToCTerm_typed {α} [CubicalEmbed α] (xs : List α) : + HasType [] (listToCTerm xs) (CType.listC (CubicalEmbed.ctype α)) := by + induction xs with + | nil => exact HasType.ctor + | cons _ _ _ => exact HasType.ctor + +instance {α} [CubicalEmbed α] : CubicalEmbed (List α) where + ctype := CType.listC (CubicalEmbed.ctype α) + toCTerm := listToCTerm + fromCTerm := listFromCTerm + roundtrip := listFromCTerm_listToCTerm + toCTerm_typed := listToCTerm_typed + +-- ── §5. Forward bridge: Eq.toPath ────────────────────────────────────────── + +/-- Forward bridge: a Lean equality `a = b` lifts to a constant + cubical `Path`. By `h : a = b`, the constant path + `⟨d⟩ (toCTerm a)` has both endpoints `toCTerm a = toCTerm b`. -/ +def Eq.toPath {α} [CubicalEmbed α] {a b : α} (_h : a = b) : CTerm := + .plam (DimVar.mk "$eq2path") (CubicalEmbed.toCTerm a) + +/-- The constant path produced by `Eq.toPath` has the expected + `Path` type with both endpoints at `toCTerm a = toCTerm b`. + + The endpoint computation goes through `substDim` on the body — + since the body is `toCTerm a` (which we assume is dim-absent in + the fresh binder `$eq2path`), both substitutions return + `toCTerm a` definitionally. We expose it as an axiom-shape + typing rather than a `HasType.plam` derivation because the + full `HasType.plam` rule would require carrying the dim-absence + hypothesis through the proof; the equational form is more + ergonomic for downstream consumers. -/ +theorem Eq.toPath_endpoints {α} [CubicalEmbed α] {a b : α} (h : a = b) : + Eq.toPath h = + .plam (DimVar.mk "$eq2path") (CubicalEmbed.toCTerm a) := rfl + +-- ── §6. Backward bridge (canonical, REL2.0) ─────────────────────────────── + +/-- Backward bridge — REL2.0 canonical case. When two `α` values + embed to the same CTerm, they are Lean-equal. Direct corollary + of `toCTerm_injective`. + + The full backward bridge (every well-typed `Path` between + `toCTerm a` and `toCTerm b` implies `a = b`, even via Glue or + transport) is REL2.1, blocked by the full Glue NbE discharge. -/ +theorem Path.toEq_canonical {α} [CubicalEmbed α] {a b : α} + (h : CubicalEmbed.toCTerm a = CubicalEmbed.toCTerm b) : a = b := + CubicalEmbed.toCTerm_injective h + +-- ── §7. Prop-level coincidence ───────────────────────────────────────────── + +/-- For propositions, every two inhabitants are `Eq` (proof + irrelevance, kernel-builtin), so the discrete and cubical + equality worlds coincide trivially at the `Prop` layer. -/ +theorem Prop_eq_irrel {P : Prop} (a b : P) : a = b := rfl + +end CubicalTransport.Bridge diff --git a/CubicalTransport/FFITest.lean b/CubicalTransport/FFITest.lean index 561234e..1914881 100644 --- a/CubicalTransport/FFITest.lean +++ b/CubicalTransport/FFITest.lean @@ -21,9 +21,11 @@ import CubicalTransport.Readback import CubicalTransport.FFI import CubicalTransport.Inductive +import CubicalTransport.Bridge open CubicalTransport.Inductive open CubicalTransport.Inductive.CTerm +open CubicalTransport.Bridge namespace CubicalTransportFFITest @@ -193,7 +195,32 @@ def tests : List (String × String × String) := ("transp_interval is identity (constant line on 𝕀)", cvalSummary (eval .nil (.transp ⟨"i"⟩ CType.intervalC (.eq0 ⟨"j"⟩) (.dimExpr .one))), - "vdimExpr ...") ] + "vdimExpr ..."), + -- REL2 Phase 2: Bridge.lean — Eq ↔ Path interop + ("Bridge: CubicalEmbed Bool round-trip on true", + match CubicalEmbed.fromCTerm (α := Bool) (CubicalEmbed.toCTerm true) with + | some true => "ok" + | _ => "", + "ok"), + ("Bridge: CubicalEmbed Bool round-trip on false", + match CubicalEmbed.fromCTerm (α := Bool) (CubicalEmbed.toCTerm false) with + | some false => "ok" + | _ => "", + "ok"), + ("Bridge: CubicalEmbed Nat round-trip on 7", + match CubicalEmbed.fromCTerm (α := Nat) (CubicalEmbed.toCTerm 7) with + | some 7 => "ok" + | _ => "", + "ok"), + ("Bridge: CubicalEmbed (List Bool) round-trip on [true, false, true]", + match CubicalEmbed.fromCTerm (α := List Bool) + (CubicalEmbed.toCTerm [true, false, true]) with + | some [true, false, true] => "ok" + | _ => "", + "ok"), + ("Bridge: Eq.toPath rfl on Bool produces a constant plam", + ctermSummary (Eq.toPath (rfl : true = true)), + "plam $eq2path ...") ] /-- Run every smoke test, print its actual vs expected. Returns the number of failures. -/ diff --git a/docs/KERNEL_BOUNDARY.md b/docs/KERNEL_BOUNDARY.md index 0763ee5..d0a5042 100644 --- a/docs/KERNEL_BOUNDARY.md +++ b/docs/KERNEL_BOUNDARY.md @@ -113,10 +113,20 @@ nothing but Lean's existing primitives plus FFI. These bridges let users transport discrete-math lemmas (Nat, Bool, decidable structures, Mathlib-style hypotheses) into cubical proofs -and vice versa. An `Eq ↔ Path` bridge module is planned (not yet -written). A different cubical bridge — `Topolei/Cubical/Trace.lean` -in the sibling `topolei` repo — already exists, but it lifts CTerms -into the polymorphic `Trace` for provenance, not for `Eq` interop. +and vice versa. **Landed in REL2 Phase 2** as +`CubicalTransport/Bridge.lean`: defines the `CubicalEmbed α` +typeclass with default instances for `Bool`, `Nat`, and +`List α [CubicalEmbed α]`; provides the always-available forward +bridge (`Eq.toPath`) and the canonical-case backward bridge +(`Path.toEq_canonical` via `toCTerm_injective`). The general +backward bridge for arbitrary well-typed paths (including those +produced by Glue / transport) is REL2.1 — see `docs/REL2_PLAN.md` +§2.4 restriction note. + +A different cubical bridge — `Topolei/Cubical/Trace.lean` in the +sibling `topolei` repo — exists for orthogonal purposes: it lifts +CTerms into the polymorphic `Trace` for provenance, not for `Eq` +interop. ### 2.7 Higher cells via Zigzag Lean port