|
| 1 | +/- Reversibility ↔ CNO Bridge — Lean 4 mirror of the Coq A2 development |
| 2 | +
|
| 3 | + Mirrors the theorems added to proofs/coq/common/CNO.v (the "reversibility |
| 4 | + ↔ CNO bridge" the MAA framework / aletheia cites). See PROOF-STATUS.adoc. |
| 5 | +
|
| 6 | + ┌─ VERIFICATION STATUS ──────────────────────────────────────────────────┐ |
| 7 | + │ NOT machine-checked in the environment where this file was written: │ |
| 8 | + │ the Lean toolchain and Mathlib cache download from GitHub release │ |
| 9 | + │ assets, which the egress policy blocked (HTTP 403). This file is a │ |
| 10 | + │ best-effort transcription against the CNO.lean API and is registered in │ |
| 11 | + │ lakefile.lean as a NON-default `lean_lib`, so the standard `lake build` │ |
| 12 | + │ is unaffected by it. To verify: │ |
| 13 | + │ cd proofs/lean4 && lake exe cache get && lake build CNOBridge │ |
| 14 | + │ and `#print axioms` on each theorem. Treat as unverified until then. │ |
| 15 | + └─────────────────────────────────────────────────────────────────────────┘ |
| 16 | +
|
| 17 | + Modelling note (honest cross-prover difference): Lean's `eval` is a TOTAL |
| 18 | + FUNCTION and `ProgramState.eq` INCLUDES the program counter, whereas Coq's |
| 19 | + `eval` is a relation and `=st=` EXCLUDES the PC. So this Lean mirror states |
| 20 | + the bridge with SYNTACTIC equality of evaluated states — a stronger, cleaner |
| 21 | + form that needs no determinism lemma (free for a function) and no |
| 22 | + "up-to-=st=" slack on the backward direction. It is therefore not a literal |
| 23 | + transcription of the Coq statement but its functional-model analogue, |
| 24 | + consistent with the repo's "each prover checks its own formalisation" stance. |
| 25 | +
|
| 26 | + Author: Jonathan D. A. Jewell |
| 27 | + Project: Absolute Zero |
| 28 | + License: MPL-2.0 |
| 29 | +-/ |
| 30 | + |
| 31 | +import CNO |
| 32 | + |
| 33 | +namespace CNOBridge |
| 34 | + |
| 35 | +open CNO |
| 36 | + |
| 37 | +/-- `reverses p p_inv`: `p_inv` undoes `p` on every state. In Lean's functional |
| 38 | + model this is `∀ s, eval p_inv (eval p s) = s` — the body of `CNO.reversible`. -/ |
| 39 | +def reverses (p p_inv : Program) : Prop := |
| 40 | + ∀ s, eval p_inv (eval p s) = s |
| 41 | + |
| 42 | +/-- The repo's `reversible` is exactly "there exists a (one-sided) left inverse". -/ |
| 43 | +theorem reversible_iff_exists_reverses (p : Program) : |
| 44 | + reversible p ↔ ∃ p_inv, reverses p p_inv := Iff.rfl |
| 45 | + |
| 46 | +/-- CNO-equivalence to the no-op, functional form: the two programs evaluate to |
| 47 | + the same state from every start state. -/ |
| 48 | +def cnoEquiv (p1 p2 : Program) : Prop := |
| 49 | + ∀ s, eval p1 s = eval p2 s |
| 50 | + |
| 51 | +/-- Core lemma: a left inverse sequenced after `p` computes the identity on |
| 52 | + every state. Uses only `eval_seqComp` (Coq needed `eval_app` + |
| 53 | + `eval_deterministic`; determinism is free here because `eval` is a function). -/ |
| 54 | +theorem reverses_seq_computes_identity {p p_inv : Program} |
| 55 | + (h : reverses p p_inv) : ∀ s, eval (seqComp p p_inv) s = s := by |
| 56 | + intro s |
| 57 | + rw [eval_seqComp] |
| 58 | + exact h s |
| 59 | + |
| 60 | +/-- Repackaged as CNO-equivalence to the empty program (the canonical no-op). -/ |
| 61 | +theorem cnoEquiv_seq_empty_of_reverses {p p_inv : Program} |
| 62 | + (h : reverses p p_inv) : cnoEquiv (seqComp p p_inv) [] := by |
| 63 | + intro s |
| 64 | + show eval (seqComp p p_inv) s = eval [] s |
| 65 | + have hnil : eval [] s = s := rfl |
| 66 | + rw [hnil] |
| 67 | + exact reverses_seq_computes_identity h s |
| 68 | + |
| 69 | +/-- Forward bridge (the faithful direction of the aletheia contract): a |
| 70 | + two-sided inverse makes BOTH composites CNO-equivalent to the no-op. -/ |
| 71 | +theorem reversible_bridge_forward {p : Program} |
| 72 | + (h : ∃ p_inv, reverses p p_inv ∧ reverses p_inv p) : |
| 73 | + ∃ p_inv, cnoEquiv (seqComp p p_inv) [] ∧ cnoEquiv (seqComp p_inv p) [] := by |
| 74 | + obtain ⟨p_inv, hpp, hpi⟩ := h |
| 75 | + exact ⟨p_inv, cnoEquiv_seq_empty_of_reverses hpp, |
| 76 | + cnoEquiv_seq_empty_of_reverses hpi⟩ |
| 77 | + |
| 78 | +/-- Backward bridge: from "the composite is a no-op" recover the inverse. In |
| 79 | + Lean's functional/PC-inclusive model this is exact (SYNTACTIC), with no |
| 80 | + up-to-`=st=` slack and no termination hypothesis — the two facts Coq needed |
| 81 | + (its `reversible_bridge_backward_upto`) because its `eval` is relational and |
| 82 | + `=st=` drops the PC. -/ |
| 83 | +theorem reversible_bridge_backward {p p_inv : Program} |
| 84 | + (h : cnoEquiv (seqComp p p_inv) []) : reverses p p_inv := by |
| 85 | + intro s |
| 86 | + have hs := h s |
| 87 | + rw [eval_seqComp] at hs |
| 88 | + -- hs : eval p_inv (eval p s) = eval [] s, and eval [] s = s definitionally |
| 89 | + exact hs |
| 90 | + |
| 91 | +/-- Corollary: in the functional model the forward and backward directions |
| 92 | + combine into a genuine biconditional for a single inverse `p_inv`. -/ |
| 93 | +theorem reverses_iff_cnoEquiv_seq_empty (p p_inv : Program) : |
| 94 | + reverses p p_inv ↔ cnoEquiv (seqComp p p_inv) [] := |
| 95 | + ⟨cnoEquiv_seq_empty_of_reverses, reversible_bridge_backward⟩ |
| 96 | + |
| 97 | +end CNOBridge |
0 commit comments