From 4296c0a52940d50962b38629fd08dcb14f8c5286 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 12 Jun 2026 16:41:15 +0000 Subject: [PATCH 1/4] =?UTF-8?q?refactor(echo):=20Option=20B=20=E2=80=94=20?= =?UTF-8?q?uniform=20echoVal=20(residue,result);=20lower/residue=20as=20pr?= =?UTF-8?q?ojections;=20capstones=20over=20Step*?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE --- proofs/Tangle.lean | 187 +++++++++++++++++++++++++++++++-------------- 1 file changed, 128 insertions(+), 59 deletions(-) diff --git a/proofs/Tangle.lean b/proofs/Tangle.lean index 181eb81..85052af 100644 --- a/proofs/Tangle.lean +++ b/proofs/Tangle.lean @@ -4,12 +4,12 @@ -- Models the core type system from docs/spec/FORMAL-SEMANTICS.md: -- - Syntax: Expr inductive with Num, Str, Bool, Identity, BraidLit, -- Compose (.), Tensor (|), Pipeline (>>), Close, Add, Eq, and the echo --- constructors EchoClose, Lower, Residue (structured loss) +-- constructors EchoClose, Lower, Residue, EchoVal (structured loss) -- - Typing: HasType inductive relation covering T-Num, T-Str, T-Bool, -- T-Identity, T-Braid, T-Compose-Word, T-Tensor-Word, T-Pipeline, -- T-Close-Word, T-Add-Num, T-Eq-Word, T-Eq-Num, T-Eq-Str, and the echo --- rules T-Echo-Close, T-Lower, T-Residue --- - Semantics: Small-step Step relation (31 rules incl. echo) +-- rules T-Echo-Close, T-Lower, T-Residue, T-Echo-Val +-- - Semantics: Small-step Step relation (38 rules incl. echo) -- -- Theorems proven: -- 1. Progress: well-typed closed terms are values or can step @@ -82,9 +82,12 @@ inductive Expr where -- Echo types (structured loss). `close` is TANGLE's canonical lossy map -- (Word[n] ↠ Word[0]); these constructors give it a residue-retaining -- variant and the two projections, mirroring echo-types' fibre/residue API. - | echoClose : Expr → Expr -- echo-preserving closure (echo-intro for `close`) + -- A formed echo is the value `echoVal residue result`; `echoClose` is the + -- redex that reduces into one, and `lower`/`residue` are its two projections. + | echoClose : Expr → Expr -- echo-preserving closure (redex → echoVal) | lower : Expr → Expr -- project an echo to its result (forget residue) | residue : Expr → Expr -- project an echo to its residue (recover witness) + | echoVal : Expr → Expr → Expr -- formed echo value: (residue, result) deriving DecidableEq, Repr /-- Value predicate: fully reduced expressions. -/ @@ -94,7 +97,7 @@ inductive IsValue : Expr → Prop where | boolLit : ∀ b, IsValue (.boolLit b) | identity : IsValue .identity | braidLit : ∀ gs, IsValue (.braidLit gs) - | echoClose : ∀ {v}, IsValue v → IsValue (.echoClose v) -- a formed echo (residue v retained) + | echoVal : ∀ {r v}, IsValue r → IsValue v → IsValue (.echoVal r v) -- a formed echo value (residue r, result v) -- ═══════════════════════════════════════════════════════════════════════ -- WIDTH @@ -169,6 +172,10 @@ inductive HasType : Ctx → Expr → Ty → Prop where | tResidue (Γ : Ctx) (e : Expr) (ρ τ : Ty) : -- [T-Residue] (recover witness) HasType Γ e (.echo ρ τ) → HasType Γ (.residue e) ρ + | tEchoVal (Γ : Ctx) (r v : Expr) (ρ τ : Ty) : -- [T-Echo-Val] + HasType Γ r ρ → + HasType Γ v τ → + HasType Γ (.echoVal r v) (.echo ρ τ) -- ═══════════════════════════════════════════════════════════════════════ -- SMALL-STEP SEMANTICS @@ -213,24 +220,32 @@ inductive Step : Expr → Expr → Prop where | eqIdId : Step (.eq .identity .identity) (.boolLit true) | eqIdBraid : Step (.eq .identity (.braidLit gs)) (.boolLit (gs == [])) | eqBraidId : Step (.eq (.braidLit gs) .identity) (.boolLit (gs == [])) - -- Echo (structured loss): closure that retains its residue, and the two - -- projections. `lower` collapses to the codomain point (identity : Word[0]); - -- `residue` recovers the witness braid — the fibre element echo-types keeps. + -- Echo (structured loss): `echoClose` is a redex that reduces into a formed + -- echo value `echoVal residue result`; `lower`/`residue` are the two generic + -- projections off a formed echo value. `lower` yields the result component + -- (the codomain point identity : Word[0]); `residue` recovers the witness + -- braid retained in the residue component — the fibre element echo-types keeps. | echoCloseStep : Step e e' → Step (.echoClose e) (.echoClose e') + | echoCloseWord : Step (.echoClose (.braidLit gs)) (.echoVal (.braidLit gs) .identity) + | echoCloseId : Step (.echoClose .identity) (.echoVal .identity .identity) + | echoValLeft : Step r r' → Step (.echoVal r v) (.echoVal r' v) + | echoValRight : IsValue r → Step v v' → Step (.echoVal r v) (.echoVal r v') | lowerStep : Step e e' → Step (.lower e) (.lower e') - | lowerEcho : IsValue v → Step (.lower (.echoClose v)) .identity + | lowerVal : IsValue r → IsValue v → Step (.lower (.echoVal r v)) v | residueStep : Step e e' → Step (.residue e) (.residue e') - | residueEcho : IsValue v → Step (.residue (.echoClose v)) v + | residueVal : IsValue r → IsValue v → Step (.residue (.echoVal r v)) r -- ═══════════════════════════════════════════════════════════════════════ -- LEMMAS -- ═══════════════════════════════════════════════════════════════════════ /-- Values are in normal form. Recursive on the value structure because a - formed echo `echoClose v` is a value exactly when its residue `v` is. -/ + formed echo value `echoVal r v` is a value exactly when both components are. -/ theorem value_no_step {e e' : Expr} (hv : IsValue e) (hs : Step e e') : False := by induction hv generalizing e' with - | echoClose _ ih => cases hs with | echoCloseStep h => exact ih h + | echoVal _ _ ihr ihv => cases hs with + | echoValLeft h => exact ihr h + | echoValRight _ h => exact ihv h | _ => cases hs /-- Canonical forms for Num. -/ @@ -251,13 +266,13 @@ theorem canonical_word : IsValue e → HasType [] e (.word n) → | boolLit => cases ht | identity => left; cases ht with | tIdentity => exact ⟨rfl, rfl⟩ | braidLit gs => right; cases ht with | tBraid => exact ⟨gs, rfl, rfl⟩ - | echoClose _ => cases ht + | echoVal _ _ => cases ht -/-- Canonical forms for Echo[ρ, τ]: a value of echo type is a formed echo - `echoClose v` whose residue `v` is itself a value. This is the canonical - form that lets `lower`/`residue` make progress. -/ +/-- Canonical forms for Echo[ρ, τ]: a value of echo type is a formed echo value + `echoVal r v` whose residue `r` and result `v` are themselves values. This + is the canonical form that lets `lower`/`residue` make progress. -/ theorem canonical_echo : IsValue e → HasType [] e (.echo ρ τ) → - ∃ v, e = .echoClose v ∧ IsValue v := by + ∃ r v, e = .echoVal r v ∧ IsValue r ∧ IsValue v := by intro hv ht cases hv with | num => cases ht @@ -265,7 +280,7 @@ theorem canonical_echo : IsValue e → HasType [] e (.echo ρ τ) → | boolLit => cases ht | identity => cases ht | braidLit => cases ht - | echoClose hv => exact ⟨_, rfl, hv⟩ + | echoVal hr hv => exact ⟨_, _, rfl, hr, hv⟩ -- Width distribution lemmas private theorem foldl_max_init (gs : List Generator) (a : Nat) : @@ -389,21 +404,32 @@ theorem progress : HasType [] e τ → IsValue e ∨ ∃ e', Step e e' := by · exact ⟨_, .eqRight hv₁ hs₂⟩ · exact ⟨_, .eqLeft hs₁⟩ | tEchoClose _ n h => - -- `echoClose e` is a value once `e` is (the residue is retained); else it steps. + -- `echoClose e` is always a redex: it reduces into a formed echo value. + right rcases progress h with hv | ⟨e', hs⟩ - · exact .inl (.echoClose hv) - · exact .inr ⟨_, .echoCloseStep hs⟩ + · rcases canonical_word hv h with ⟨rfl, _⟩ | ⟨gs, rfl, _⟩ + · exact ⟨_, .echoCloseId⟩ + · exact ⟨_, .echoCloseWord⟩ + · exact ⟨_, .echoCloseStep hs⟩ + | tEchoVal _ _ ρ τ hr hv => + -- `echoVal r v` is a value iff both r and v are; otherwise the relevant + -- component steps under `echoValLeft` / `echoValRight`. + rcases progress hr with hvr | ⟨r', hsr⟩ + · rcases progress hv with hvv | ⟨v', hsv⟩ + · exact .inl (.echoVal hvr hvv) + · exact .inr ⟨_, .echoValRight hvr hsv⟩ + · exact .inr ⟨_, .echoValLeft hsr⟩ | tLower _ ρ τ h => right rcases progress h with hv | ⟨e', hs⟩ - · obtain ⟨v, rfl, hv'⟩ := canonical_echo hv h - exact ⟨_, .lowerEcho hv'⟩ + · obtain ⟨r, v, rfl, hr, hvv⟩ := canonical_echo hv h + exact ⟨_, .lowerVal hr hvv⟩ · exact ⟨_, .lowerStep hs⟩ | tResidue _ ρ τ h => right rcases progress h with hv | ⟨e', hs⟩ - · obtain ⟨v, rfl, hv'⟩ := canonical_echo hv h - exact ⟨_, .residueEcho hv'⟩ + · obtain ⟨r, v, rfl, hr, hvv⟩ := canonical_echo hv h + exact ⟨_, .residueVal hr hvv⟩ · exact ⟨_, .residueStep hs⟩ -- ═══════════════════════════════════════════════════════════════════════ @@ -500,21 +526,30 @@ theorem preservation : HasType [] e τ → Step e e' → HasType [] e' τ := by | tEqWord => exact .tBool _ _ | tEqNum _ _ _ h₁ => cases h₁ | tEqStr _ _ _ h₁ => cases h₁ - -- Echo congruence preserves the (residue Word[n], result Word[0]) echo type. + -- Echo congruence preserves types; `echoClose` reduces into a formed echo + -- value `echoVal residue result`; `lower`/`residue` project off it. | echoCloseStep hs ih => cases ht with | tEchoClose _ n h => exact .tEchoClose _ _ n (ih h) + | echoCloseWord => + cases ht with | tEchoClose _ n h => + cases h with | tBraid => exact .tEchoVal _ _ _ _ _ (.tBraid _ _) (.tIdentity _) + | echoCloseId => + cases ht with | tEchoClose _ n h => + cases h with | tIdentity => exact .tEchoVal _ _ _ _ _ (.tIdentity _) (.tIdentity _) + | echoValLeft hs ih => + cases ht with | tEchoVal _ _ _ _ hr hv => exact .tEchoVal _ _ _ _ _ (ih hr) hv + | echoValRight _ hs ih => + cases ht with | tEchoVal _ _ _ _ hr hv => exact .tEchoVal _ _ _ _ _ hr (ih hv) | lowerStep hs ih => cases ht with | tLower _ _ _ h => exact .tLower _ _ _ _ (ih h) + | lowerVal _ _ => + cases ht with | tLower _ _ _ h => + cases h with | tEchoVal _ _ _ _ hr hv => exact hv | residueStep hs ih => cases ht with | tResidue _ _ _ h => exact .tResidue _ _ _ _ (ih h) - -- `lower` yields the codomain point identity : Word[0]; the echo type forces τ = Word[0]. - | lowerEcho hv => - cases ht with | tLower _ _ _ h => - cases h with | tEchoClose _ n _ => exact .tIdentity _ - -- `residue` recovers the witness, whose type is exactly the echo's residue type. - | residueEcho hv => + | residueVal _ _ => cases ht with | tResidue _ _ _ h => - cases h with | tEchoClose _ n h' => exact h' + cases h with | tEchoVal _ _ _ _ hr hv => exact hr -- ═══════════════════════════════════════════════════════════════════════ -- THEOREM 3: DETERMINISM @@ -650,21 +685,35 @@ theorem determinism : Step e e₁ → Step e e₂ → e₁ = e₂ := by | eqRight _ h => exact absurd h (value_no_step .identity) | eqBraidId => rfl -- Echo: congruence is deterministic by IH; the computation rules fire only - -- on a formed echo (a value), so they never race with their congruence rule. + -- on a formed echo value's component, so they never race their congruence. | echoCloseStep hs ih => cases hs₂ with | echoCloseStep h => exact congrArg Expr.echoClose (ih h) + | echoCloseWord => exact absurd hs (value_no_step (.braidLit _)) + | echoCloseId => exact absurd hs (value_no_step .identity) + | echoCloseWord => cases hs₂ with + | echoCloseStep h => exact absurd h (value_no_step (.braidLit _)) + | echoCloseWord => rfl + | echoCloseId => cases hs₂ with + | echoCloseStep h => exact absurd h (value_no_step .identity) + | echoCloseId => rfl + | echoValLeft hs ih => cases hs₂ with + | echoValLeft h => exact congrArg (Expr.echoVal · _) (ih h) + | echoValRight hr _ => exact absurd hs (value_no_step hr) + | echoValRight hr hs ih => cases hs₂ with + | echoValLeft h => exact absurd h (value_no_step hr) + | echoValRight _ h => exact congrArg (Expr.echoVal _ ·) (ih h) | lowerStep hs ih => cases hs₂ with | lowerStep h => exact congrArg Expr.lower (ih h) - | lowerEcho hv => exact absurd hs (value_no_step (.echoClose hv)) + | lowerVal hr hv => exact absurd hs (value_no_step (.echoVal hr hv)) + | lowerVal hr hv => cases hs₂ with + | lowerStep h => exact absurd h (value_no_step (.echoVal hr hv)) + | lowerVal _ _ => rfl | residueStep hs ih => cases hs₂ with | residueStep h => exact congrArg Expr.residue (ih h) - | residueEcho hv => exact absurd hs (value_no_step (.echoClose hv)) - | lowerEcho hv => cases hs₂ with - | lowerStep h => exact absurd h (value_no_step (.echoClose hv)) - | lowerEcho _ => rfl - | residueEcho hv => cases hs₂ with - | residueStep h => exact absurd h (value_no_step (.echoClose hv)) - | residueEcho _ => rfl + | residueVal hr hv => exact absurd hs (value_no_step (.echoVal hr hv)) + | residueVal hr hv => cases hs₂ with + | residueStep h => exact absurd h (value_no_step (.echoVal hr hv)) + | residueVal _ _ => rfl -- ═══════════════════════════════════════════════════════════════════════ -- COROLLARY: TYPE SAFETY @@ -682,29 +731,40 @@ theorem type_safety (ht : HasType [] e τ) (hs : Step e e') : -- `close : Word[n] → Word[0]` is TANGLE's canonical lossy map: it collapses -- every braid to the identity, discarding the word. This mirrors echo-types' -- `collapse : Bool → ⊤` (hyperpolymath/echo-types, EchoResidue.agda). The echo --- constructors above (`echoClose`/`lower`/`residue`, type former `Ty.echo`) --- make that loss *recoverable in the type system*: the residue `Word[n]` is --- retained and projected back out. Progress, Preservation, Determinism, and --- Type Safety (proved above) all cover these constructors — echo types are not --- a bolt-on, they are part of the metatheory. +-- constructors above (`echoClose`/`lower`/`residue`/`echoVal`, type former +-- `Ty.echo`) make that loss *recoverable in the type system*: `echoClose` +-- reduces into a formed echo value `echoVal residue result` from which the +-- residue `Word[n]` is projected back out. Progress, Preservation, +-- Determinism, and Type Safety (proved above) all cover these constructors — +-- echo types are not a bolt-on, they are part of the metatheory. -- -- The three theorems below are the TANGLE instantiation of the echo-types -- `no-section` / `sigma-distinguishes` results: `lower` collapses, `residue` --- distinguishes. +-- distinguishes. They are stated over `StepStar` (multi-step reduction) since +-- `echoClose` now takes two steps to project: reduce to `echoVal`, then project. + +/-- Reflexive-transitive closure of `Step` (multi-step reduction). -/ +inductive StepStar : Expr → Expr → Prop where + | refl : StepStar e e + | head : Step e e' → StepStar e' e'' → StepStar e e'' /-- `lower ∘ echoClose` is the collapsing map: every closed braid lowers to the - identity (the single `Word[0]` value). This is `close` re-derived through the - echo — the step that loses information. -/ + identity (the single `Word[0]` value). `echoClose` first reduces into a + formed echo value `echoVal (braidLit gs) identity`, then `lower` projects out + the result component `identity` — `close` re-derived through the echo, the + step that loses information. -/ theorem echo_lower_collapses (gs : List Generator) : - Step (.lower (.echoClose (.braidLit gs))) .identity := - .lowerEcho (.braidLit gs) + StepStar (.lower (.echoClose (.braidLit gs))) .identity := + .head (.lowerStep .echoCloseWord) (.head (.lowerVal (.braidLit gs) .identity) .refl) /-- `residue ∘ echoClose` recovers the witness: the original braid is retained in - the residue. This is echo-types' `proj₁`/`echo-intro` round-trip — the lossy - `close` becomes reversible once its echo is carried. -/ + the residue. `echoClose` reduces into `echoVal (braidLit gs) identity`, then + `residue` projects out the residue component `braidLit gs`. This is + echo-types' `proj₁`/`echo-intro` round-trip — the lossy `close` becomes + reversible once its echo is carried. -/ theorem echo_residue_recovers (gs : List Generator) : - Step (.residue (.echoClose (.braidLit gs))) (.braidLit gs) := - .residueEcho (.braidLit gs) + StepStar (.residue (.echoClose (.braidLit gs))) (.braidLit gs) := + .head (.residueStep .echoCloseWord) (.head (.residueVal (.braidLit gs) .identity) .refl) /-- **Echo distinguishes what `close` collapses.** Two distinct braids close to the *same* identity (the residue forgotten by `lower`), yet their echoes carry @@ -712,10 +772,10 @@ theorem echo_residue_recovers (gs : List Generator) : echo-types' non-injectivity barrier (`collapse-residue-same` paired with `echo-true≢echo-false` / `no-section-collapse-to-residue`). -/ theorem echo_distinguishes_collapsed {gs₁ gs₂ : List Generator} (h : gs₁ ≠ gs₂) : - (Step (.lower (.echoClose (.braidLit gs₁))) .identity ∧ - Step (.lower (.echoClose (.braidLit gs₂))) .identity) ∧ + (StepStar (.lower (.echoClose (.braidLit gs₁))) .identity ∧ + StepStar (.lower (.echoClose (.braidLit gs₂))) .identity) ∧ (Expr.braidLit gs₁ ≠ Expr.braidLit gs₂) := - ⟨⟨.lowerEcho (.braidLit gs₁), .lowerEcho (.braidLit gs₂)⟩, + ⟨⟨echo_lower_collapses gs₁, echo_lower_collapses gs₂⟩, fun heq => h (Expr.braidLit.inj heq)⟩ /-- The echo round-trip is type-safe: from `e : Word[n]`, `residue` recovers a @@ -782,6 +842,10 @@ def infer (Γ : Ctx) : Expr → Option Ty match infer Γ e with | some (.echo ρ _) => some ρ | _ => none + | .echoVal r v => + match infer Γ r, infer Γ v with + | some ρ, some τ => some (.echo ρ τ) + | _, _ => none /-- **Completeness**: every typing derivation is computed by `infer`. -/ theorem infer_complete {Γ : Ctx} {e : Expr} {τ : Ty} : @@ -845,6 +909,11 @@ theorem infer_sound {Γ : Ctx} {e : Expr} {τ : Ty} : intro h; simp only [infer] at h; split at h next ρ τ' he => injection h with h; subst h; exact .tResidue _ _ ρ τ' (ih he) all_goals simp at h + | echoVal r v ihr ihv => + intro h; simp only [infer] at h; split at h + next ρ τ' he_r he_v => + injection h with h; subst h; exact .tEchoVal _ _ _ ρ τ' (ihr he_r) (ihv he_v) + all_goals simp at h /-- **Decidability of type checking** (TG-2): `infer` decides `HasType`. -/ theorem infer_iff_hasType {Γ : Ctx} {e : Expr} {τ : Ty} : From b2749956f7ed566a0559767509c37ad05b64abf4 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 12 Jun 2026 16:54:33 +0000 Subject: [PATCH 2/4] =?UTF-8?q?feat(echo):=20product=20type=20+=20echoAdd?= =?UTF-8?q?=20=E2=80=94=20structured=20loss=20for=20arithmetic=20(residue?= =?UTF-8?q?=20=3D=20summand=20pair)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE --- proofs/Tangle.lean | 193 +++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 186 insertions(+), 7 deletions(-) diff --git a/proofs/Tangle.lean b/proofs/Tangle.lean index 85052af..15d27ad 100644 --- a/proofs/Tangle.lean +++ b/proofs/Tangle.lean @@ -3,13 +3,15 @@ -- -- Models the core type system from docs/spec/FORMAL-SEMANTICS.md: -- - Syntax: Expr inductive with Num, Str, Bool, Identity, BraidLit, --- Compose (.), Tensor (|), Pipeline (>>), Close, Add, Eq, and the echo --- constructors EchoClose, Lower, Residue, EchoVal (structured loss) +-- Compose (.), Tensor (|), Pipeline (>>), Close, Add, Eq, the echo +-- constructors EchoClose, Lower, Residue, EchoVal (structured loss), and +-- the product constructors Pair, Fst, Snd, EchoAdd -- - Typing: HasType inductive relation covering T-Num, T-Str, T-Bool, -- T-Identity, T-Braid, T-Compose-Word, T-Tensor-Word, T-Pipeline, --- T-Close-Word, T-Add-Num, T-Eq-Word, T-Eq-Num, T-Eq-Str, and the echo --- rules T-Echo-Close, T-Lower, T-Residue, T-Echo-Val --- - Semantics: Small-step Step relation (38 rules incl. echo) +-- T-Close-Word, T-Add-Num, T-Eq-Word, T-Eq-Num, T-Eq-Str, the echo +-- rules T-Echo-Close, T-Lower, T-Residue, T-Echo-Val, and the product +-- rules T-Pair, T-Fst, T-Snd, T-Echo-Add +-- - Semantics: Small-step Step relation (47 rules incl. echo + product) -- -- Theorems proven: -- 1. Progress: well-typed closed terms are values or can step @@ -23,9 +25,13 @@ -- constructors `echoClose`/`lower`/`residue` integrate echo-types -- (hyperpolymath/echo-types: `Echo f y := Σ (x : A), f x ≡ y`) directly into -- the type system: closing a braid through an echo retains the residue, so the --- otherwise-irreversible `close` becomes reversible at the type level. See the +-- otherwise-irreversible `close` becomes reversible at the type level. The +-- product type `Ty.prod ρ σ` carries a second lossy operation, `echoAdd`: +-- ordinary `add` discards which two numbers were summed, but `echoAdd` keeps +-- the summand pair as its residue (residue type `Num × Num`, result `Num`), so +-- distinct summands that collapse to the same sum stay distinguishable. See the -- §ECHO-TYPES section at the foot of the file for the residue-recovery and --- non-injectivity theorems. +-- non-injectivity theorems (both the `close` and `echoAdd` forms). -- -- Note on T-Let: the let binding requires a generalized de Bruijn substitution -- lemma (standard POPLmark machinery); tracked as TG-1. The fragment here @@ -62,6 +68,7 @@ inductive Ty where -- (hyperpolymath/echo-types, Echo.agda): ρ is the -- residue (domain witness x : A), τ is the result -- (codomain point y). See §ECHO-TYPES below. + | prod : Ty → Ty → Ty -- product (pair) type ρ × σ; residue carrier for lossy binary ops deriving DecidableEq, Repr /-- Core expression AST. Mirrors the OCaml AST in compiler/lib/ast.ml. @@ -88,6 +95,10 @@ inductive Expr where | lower : Expr → Expr -- project an echo to its result (forget residue) | residue : Expr → Expr -- project an echo to its residue (recover witness) | echoVal : Expr → Expr → Expr -- formed echo value: (residue, result) + | pair : Expr → Expr → Expr -- product introduction + | fst : Expr → Expr -- first projection + | snd : Expr → Expr -- second projection + | echoAdd : Expr → Expr → Expr -- echo-preserving addition (residue = pair of summands) deriving DecidableEq, Repr /-- Value predicate: fully reduced expressions. -/ @@ -98,6 +109,7 @@ inductive IsValue : Expr → Prop where | identity : IsValue .identity | braidLit : ∀ gs, IsValue (.braidLit gs) | echoVal : ∀ {r v}, IsValue r → IsValue v → IsValue (.echoVal r v) -- a formed echo value (residue r, result v) + | pair : ∀ {a b}, IsValue a → IsValue b → IsValue (.pair a b) -- ═══════════════════════════════════════════════════════════════════════ -- WIDTH @@ -176,6 +188,15 @@ inductive HasType : Ctx → Expr → Ty → Prop where HasType Γ r ρ → HasType Γ v τ → HasType Γ (.echoVal r v) (.echo ρ τ) + | tPair (Γ : Ctx) (a b : Expr) (α β : Ty) : -- [T-Pair] + HasType Γ a α → HasType Γ b β → HasType Γ (.pair a b) (.prod α β) + | tFst (Γ : Ctx) (e : Expr) (α β : Ty) : -- [T-Fst] + HasType Γ e (.prod α β) → HasType Γ (.fst e) α + | tSnd (Γ : Ctx) (e : Expr) (α β : Ty) : -- [T-Snd] + HasType Γ e (.prod α β) → HasType Γ (.snd e) β + | tEchoAdd (Γ : Ctx) (e₁ e₂ : Expr) : -- [T-Echo-Add] + HasType Γ e₁ .num → HasType Γ e₂ .num → + HasType Γ (.echoAdd e₁ e₂) (.echo (.prod .num .num) .num) -- ═══════════════════════════════════════════════════════════════════════ -- SMALL-STEP SEMANTICS @@ -234,6 +255,18 @@ inductive Step : Expr → Expr → Prop where | lowerVal : IsValue r → IsValue v → Step (.lower (.echoVal r v)) v | residueStep : Step e e' → Step (.residue e) (.residue e') | residueVal : IsValue r → IsValue v → Step (.residue (.echoVal r v)) r + -- Product: congruence + projections + | pairLeft : Step a a' → Step (.pair a b) (.pair a' b) + | pairRight : IsValue a → Step b b' → Step (.pair a b) (.pair a b') + | fstStep : Step e e' → Step (.fst e) (.fst e') + | fstPair : IsValue a → IsValue b → Step (.fst (.pair a b)) a + | sndStep : Step e e' → Step (.snd e) (.snd e') + | sndPair : IsValue a → IsValue b → Step (.snd (.pair a b)) b + -- Echo-preserving addition: residue retains the summand pair; result is the sum. + | echoAddLeft : Step e₁ e₁' → Step (.echoAdd e₁ e₂) (.echoAdd e₁' e₂) + | echoAddRight : IsValue e₁ → Step e₂ e₂' → Step (.echoAdd e₁ e₂) (.echoAdd e₁ e₂') + | echoAddNums : Step (.echoAdd (.num n₁) (.num n₂)) + (.echoVal (.pair (.num n₁) (.num n₂)) (.num (n₁ + n₂))) -- ═══════════════════════════════════════════════════════════════════════ -- LEMMAS @@ -246,6 +279,9 @@ theorem value_no_step {e e' : Expr} (hv : IsValue e) (hs : Step e e') : False := | echoVal _ _ ihr ihv => cases hs with | echoValLeft h => exact ihr h | echoValRight _ h => exact ihv h + | pair _ _ iha ihb => cases hs with + | pairLeft h => exact iha h + | pairRight _ h => exact ihb h | _ => cases hs /-- Canonical forms for Num. -/ @@ -267,6 +303,7 @@ theorem canonical_word : IsValue e → HasType [] e (.word n) → | identity => left; cases ht with | tIdentity => exact ⟨rfl, rfl⟩ | braidLit gs => right; cases ht with | tBraid => exact ⟨gs, rfl, rfl⟩ | echoVal _ _ => cases ht + | pair _ _ => cases ht /-- Canonical forms for Echo[ρ, τ]: a value of echo type is a formed echo value `echoVal r v` whose residue `r` and result `v` are themselves values. This @@ -281,6 +318,22 @@ theorem canonical_echo : IsValue e → HasType [] e (.echo ρ τ) → | identity => cases ht | braidLit => cases ht | echoVal hr hv => exact ⟨_, _, rfl, hr, hv⟩ + | pair _ _ => cases ht + +/-- Canonical forms for products: a value of product type is a `pair a b` whose + components `a` and `b` are themselves values. This is the canonical form + that lets `fst`/`snd` make progress. -/ +theorem canonical_prod : IsValue e → HasType [] e (.prod α β) → + ∃ a b, e = .pair a b ∧ IsValue a ∧ IsValue b := by + intro hv ht + cases hv with + | num => cases ht + | str => cases ht + | boolLit => cases ht + | identity => cases ht + | braidLit => cases ht + | echoVal _ _ => cases ht + | pair ha hb => exact ⟨_, _, rfl, ha, hb⟩ -- Width distribution lemmas private theorem foldl_max_init (gs : List Generator) (a : Nat) : @@ -431,6 +484,33 @@ theorem progress : HasType [] e τ → IsValue e ∨ ∃ e', Step e e' := by · obtain ⟨r, v, rfl, hr, hvv⟩ := canonical_echo hv h exact ⟨_, .residueVal hr hvv⟩ · exact ⟨_, .residueStep hs⟩ + | tPair _ _ α β ha hb => + rcases progress ha with hva | ⟨a', hsa⟩ + · rcases progress hb with hvb | ⟨b', hsb⟩ + · exact .inl (.pair hva hvb) + · exact .inr ⟨_, .pairRight hva hsb⟩ + · exact .inr ⟨_, .pairLeft hsa⟩ + | tFst _ α β h => + right + rcases progress h with hv | ⟨e', hs⟩ + · obtain ⟨a, b, rfl, ha, hb⟩ := canonical_prod hv h + exact ⟨_, .fstPair ha hb⟩ + · exact ⟨_, .fstStep hs⟩ + | tSnd _ α β h => + right + rcases progress h with hv | ⟨e', hs⟩ + · obtain ⟨a, b, rfl, ha, hb⟩ := canonical_prod hv h + exact ⟨_, .sndPair ha hb⟩ + · exact ⟨_, .sndStep hs⟩ + | tEchoAdd _ _ h₁ h₂ => + right + rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩ + · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩ + · obtain ⟨n₁, rfl⟩ := canonical_num hv₁ h₁ + obtain ⟨n₂, rfl⟩ := canonical_num hv₂ h₂ + exact ⟨_, .echoAddNums⟩ + · exact ⟨_, .echoAddRight hv₁ hs₂⟩ + · exact ⟨_, .echoAddLeft hs₁⟩ -- ═══════════════════════════════════════════════════════════════════════ -- THEOREM 2: PRESERVATION @@ -550,6 +630,20 @@ theorem preservation : HasType [] e τ → Step e e' → HasType [] e' τ := by | residueVal _ _ => cases ht with | tResidue _ _ _ h => cases h with | tEchoVal _ _ _ _ hr hv => exact hr + -- Product: congruence preserves the product type; projections recover the + -- component types. `echoAdd` reduces into a formed echo value whose residue + -- is the (num, num) summand pair and whose result is the num sum. + | pairLeft hs ih => cases ht with | tPair _ _ α β ha hb => exact .tPair _ _ _ _ _ (ih ha) hb + | pairRight _ hs ih => cases ht with | tPair _ _ α β ha hb => exact .tPair _ _ _ _ _ ha (ih hb) + | fstStep hs ih => cases ht with | tFst _ α β h => exact .tFst _ _ _ _ (ih h) + | fstPair _ _ => cases ht with | tFst _ α β h => cases h with | tPair _ _ _ _ ha hb => exact ha + | sndStep hs ih => cases ht with | tSnd _ α β h => exact .tSnd _ _ _ _ (ih h) + | sndPair _ _ => cases ht with | tSnd _ α β h => cases h with | tPair _ _ _ _ ha hb => exact hb + | echoAddLeft hs ih => cases ht with | tEchoAdd _ _ h₁ h₂ => exact .tEchoAdd _ _ _ (ih h₁) h₂ + | echoAddRight _ hs ih => cases ht with | tEchoAdd _ _ h₁ h₂ => exact .tEchoAdd _ _ _ h₁ (ih h₂) + | echoAddNums => + cases ht with | tEchoAdd _ _ h₁ h₂ => + exact .tEchoVal _ _ _ _ _ (.tPair _ _ _ _ _ (.tNum _ _) (.tNum _ _)) (.tNum _ _) -- ═══════════════════════════════════════════════════════════════════════ -- THEOREM 3: DETERMINISM @@ -714,6 +808,39 @@ theorem determinism : Step e e₁ → Step e e₂ → e₁ = e₂ := by | residueVal hr hv => cases hs₂ with | residueStep h => exact absurd h (value_no_step (.echoVal hr hv)) | residueVal _ _ => rfl + -- Product: congruence is deterministic by IH; projections fire only on a + -- formed pair value, so they never race their congruence rule. `echoAdd` + -- computes only on two `num` values. + | pairLeft hs ih => cases hs₂ with + | pairLeft h => exact congrArg (Expr.pair · _) (ih h) + | pairRight hva _ => exact absurd hs (value_no_step hva) + | pairRight hva hs ih => cases hs₂ with + | pairLeft h => exact absurd h (value_no_step hva) + | pairRight _ h => exact congrArg (Expr.pair _ ·) (ih h) + | fstStep hs ih => cases hs₂ with + | fstStep h => exact congrArg Expr.fst (ih h) + | fstPair ha hb => exact absurd hs (value_no_step (.pair ha hb)) + | fstPair ha hb => cases hs₂ with + | fstStep h => exact absurd h (value_no_step (.pair ha hb)) + | fstPair _ _ => rfl + | sndStep hs ih => cases hs₂ with + | sndStep h => exact congrArg Expr.snd (ih h) + | sndPair ha hb => exact absurd hs (value_no_step (.pair ha hb)) + | sndPair ha hb => cases hs₂ with + | sndStep h => exact absurd h (value_no_step (.pair ha hb)) + | sndPair _ _ => rfl + | echoAddLeft hs ih => cases hs₂ with + | echoAddLeft h => exact congrArg (Expr.echoAdd · _) (ih h) + | echoAddRight hv₁ _ => exact absurd hs (value_no_step hv₁) + | echoAddNums => exact absurd hs (value_no_step (.num _)) + | echoAddRight hv₁ hs ih => cases hs₂ with + | echoAddLeft h => exact absurd h (value_no_step hv₁) + | echoAddRight _ h => exact congrArg (Expr.echoAdd _ ·) (ih h) + | echoAddNums => exact absurd hs (value_no_step (.num _)) + | echoAddNums => cases hs₂ with + | echoAddLeft h => exact absurd h (value_no_step (.num _)) + | echoAddRight _ h => exact absurd h (value_no_step (.num _)) + | echoAddNums => rfl -- ═══════════════════════════════════════════════════════════════════════ -- COROLLARY: TYPE SAFETY @@ -786,6 +913,25 @@ theorem echo_roundtrip_typed (e : Expr) (n : Nat) (h : HasType [] e (.word n)) : HasType [] (.lower (.echoClose e)) (.word 0) := ⟨.tResidue _ _ _ _ (.tEchoClose _ _ n h), .tLower _ _ _ _ (.tEchoClose _ _ n h)⟩ +/-- `echoAdd` recovers the summands: `add` discards which numbers were added, + but the residue retains the pair. -/ +theorem echoAdd_residue_recovers (n₁ n₂ : Int) : + StepStar (.residue (.echoAdd (.num n₁) (.num n₂))) (.pair (.num n₁) (.num n₂)) := + .head (.residueStep .echoAddNums) (.head (.residueVal (.pair (.num _) (.num _)) (.num _)) .refl) + +/-- `lower ∘ echoAdd` is ordinary addition (the lossy result). -/ +theorem echoAdd_lower_sums (n₁ n₂ : Int) : + StepStar (.lower (.echoAdd (.num n₁) (.num n₂))) (.num (n₁ + n₂)) := + .head (.lowerStep .echoAddNums) (.head (.lowerVal (.pair (.num _) (.num _)) (.num _)) .refl) + +/-- **Echo distinguishes what `add` collapses.** 1+3 and 2+2 both lower to 4, + but their residues (the summand pairs) stay distinct. -/ +theorem echoAdd_distinguishes : + (StepStar (.lower (.echoAdd (.num 1) (.num 3))) (.num 4) ∧ + StepStar (.lower (.echoAdd (.num 2) (.num 2))) (.num 4)) ∧ + (Expr.pair (.num 1) (.num 3) ≠ Expr.pair (.num 2) (.num 2)) := + ⟨⟨echoAdd_lower_sums 1 3, echoAdd_lower_sums 2 2⟩, by decide⟩ + -- ═══════════════════════════════════════════════════════════════════════ -- TG-2: DECIDABILITY OF TYPE CHECKING -- ═══════════════════════════════════════════════════════════════════════ @@ -846,6 +992,22 @@ def infer (Γ : Ctx) : Expr → Option Ty match infer Γ r, infer Γ v with | some ρ, some τ => some (.echo ρ τ) | _, _ => none + | .pair a b => + match infer Γ a, infer Γ b with + | some α, some β => some (.prod α β) + | _, _ => none + | .fst e => + match infer Γ e with + | some (.prod α _) => some α + | _ => none + | .snd e => + match infer Γ e with + | some (.prod _ β) => some β + | _ => none + | .echoAdd e₁ e₂ => + match infer Γ e₁, infer Γ e₂ with + | some .num, some .num => some (.echo (.prod .num .num) .num) + | _, _ => none /-- **Completeness**: every typing derivation is computed by `infer`. -/ theorem infer_complete {Γ : Ctx} {e : Expr} {τ : Ty} : @@ -914,6 +1076,23 @@ theorem infer_sound {Γ : Ctx} {e : Expr} {τ : Ty} : next ρ τ' he_r he_v => injection h with h; subst h; exact .tEchoVal _ _ _ ρ τ' (ihr he_r) (ihv he_v) all_goals simp at h + | pair a b iha ihb => + intro h; simp only [infer] at h; split at h + next α β he_a he_b => + injection h with h; subst h; exact .tPair _ _ _ α β (iha he_a) (ihb he_b) + all_goals simp at h + | fst e ih => + intro h; simp only [infer] at h; split at h + next α β he => injection h with h; subst h; exact .tFst _ _ α β (ih he) + all_goals simp at h + | snd e ih => + intro h; simp only [infer] at h; split at h + next α β he => injection h with h; subst h; exact .tSnd _ _ α β (ih he) + all_goals simp at h + | echoAdd e₁ e₂ ih₁ ih₂ => + intro h; simp only [infer] at h; split at h + next he₁ he₂ => injection h with h; subst h; exact .tEchoAdd _ _ _ (ih₁ he₁) (ih₂ he₂) + all_goals simp at h /-- **Decidability of type checking** (TG-2): `infer` decides `HasType`. -/ theorem infer_iff_hasType {Γ : Ctx} {e : Expr} {τ : Ty} : From a21853be75007e8df92c49032383464a95958077 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 12 Jun 2026 16:56:36 +0000 Subject: [PATCH 3/4] chore(gitignore): ignore transient Claude Code agent worktrees .claude/worktrees/ holds throwaway git worktrees used by background agents; never commit them. https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE --- .gitignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitignore b/.gitignore index e338041..60dec36 100644 --- a/.gitignore +++ b/.gitignore @@ -93,3 +93,6 @@ deps/ .cache/ build/ dist/ + +# Claude Code — transient agent worktrees (never committed) +.claude/worktrees/ From 3a5e9a31685b634277593c1b9bcad453880d2d4b Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 12 Jun 2026 17:06:33 +0000 Subject: [PATCH 4/4] =?UTF-8?q?feat(echo):=20echoEq=20=E2=80=94=20structur?= =?UTF-8?q?ed=20loss=20for=20equality=20(residue=20=3D=20operand=20pair)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE --- proofs/Tangle.lean | 197 ++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 187 insertions(+), 10 deletions(-) diff --git a/proofs/Tangle.lean b/proofs/Tangle.lean index 15d27ad..a61be4e 100644 --- a/proofs/Tangle.lean +++ b/proofs/Tangle.lean @@ -5,13 +5,14 @@ -- - Syntax: Expr inductive with Num, Str, Bool, Identity, BraidLit, -- Compose (.), Tensor (|), Pipeline (>>), Close, Add, Eq, the echo -- constructors EchoClose, Lower, Residue, EchoVal (structured loss), and --- the product constructors Pair, Fst, Snd, EchoAdd +-- the product constructors Pair, Fst, Snd, EchoAdd, EchoEq -- - Typing: HasType inductive relation covering T-Num, T-Str, T-Bool, -- T-Identity, T-Braid, T-Compose-Word, T-Tensor-Word, T-Pipeline, -- T-Close-Word, T-Add-Num, T-Eq-Word, T-Eq-Num, T-Eq-Str, the echo --- rules T-Echo-Close, T-Lower, T-Residue, T-Echo-Val, and the product --- rules T-Pair, T-Fst, T-Snd, T-Echo-Add --- - Semantics: Small-step Step relation (47 rules incl. echo + product) +-- rules T-Echo-Close, T-Lower, T-Residue, T-Echo-Val, the product +-- rules T-Pair, T-Fst, T-Snd, T-Echo-Add, and the echo-equality rules +-- T-Echo-Eq-Word, T-Echo-Eq-Num, T-Echo-Eq-Str +-- - Semantics: Small-step Step relation (55 rules incl. echo + product) -- -- Theorems proven: -- 1. Progress: well-typed closed terms are values or can step @@ -26,12 +27,15 @@ -- (hyperpolymath/echo-types: `Echo f y := Σ (x : A), f x ≡ y`) directly into -- the type system: closing a braid through an echo retains the residue, so the -- otherwise-irreversible `close` becomes reversible at the type level. The --- product type `Ty.prod ρ σ` carries a second lossy operation, `echoAdd`: --- ordinary `add` discards which two numbers were summed, but `echoAdd` keeps --- the summand pair as its residue (residue type `Num × Num`, result `Num`), so --- distinct summands that collapse to the same sum stay distinguishable. See the --- §ECHO-TYPES section at the foot of the file for the residue-recovery and --- non-injectivity theorems (both the `close` and `echoAdd` forms). +-- product type `Ty.prod ρ σ` carries two further lossy operations, `echoAdd` +-- and `echoEq`: ordinary `add` discards which two numbers were summed, but +-- `echoAdd` keeps the summand pair as its residue (residue type `Num × Num`, +-- result `Num`); ordinary `eq` discards which two operands were compared, but +-- `echoEq` keeps the operand pair as its residue (residue type `ρ × ρ`, result +-- `Bool`), so distinct inputs that collapse to the same sum or boolean stay +-- distinguishable. See the §ECHO-TYPES section at the foot of the file for the +-- residue-recovery and non-injectivity theorems (the `close`, `echoAdd`, and +-- `echoEq` forms). -- -- Note on T-Let: the let binding requires a generalized de Bruijn substitution -- lemma (standard POPLmark machinery); tracked as TG-1. The fragment here @@ -99,6 +103,7 @@ inductive Expr where | fst : Expr → Expr -- first projection | snd : Expr → Expr -- second projection | echoAdd : Expr → Expr → Expr -- echo-preserving addition (residue = pair of summands) + | echoEq : Expr → Expr → Expr -- echo-preserving equality (residue = operand pair) deriving DecidableEq, Repr /-- Value predicate: fully reduced expressions. -/ @@ -197,6 +202,15 @@ inductive HasType : Ctx → Expr → Ty → Prop where | tEchoAdd (Γ : Ctx) (e₁ e₂ : Expr) : -- [T-Echo-Add] HasType Γ e₁ .num → HasType Γ e₂ .num → HasType Γ (.echoAdd e₁ e₂) (.echo (.prod .num .num) .num) + | tEchoEqWord (Γ : Ctx) (e₁ e₂ : Expr) (n : Nat) : -- [T-Echo-Eq-Word] + HasType Γ e₁ (.word n) → HasType Γ e₂ (.word n) → + HasType Γ (.echoEq e₁ e₂) (.echo (.prod (.word n) (.word n)) .bool) + | tEchoEqNum (Γ : Ctx) (e₁ e₂ : Expr) : -- [T-Echo-Eq-Num] + HasType Γ e₁ .num → HasType Γ e₂ .num → + HasType Γ (.echoEq e₁ e₂) (.echo (.prod .num .num) .bool) + | tEchoEqStr (Γ : Ctx) (e₁ e₂ : Expr) : -- [T-Echo-Eq-Str] + HasType Γ e₁ .str → HasType Γ e₂ .str → + HasType Γ (.echoEq e₁ e₂) (.echo (.prod .str .str) .bool) -- ═══════════════════════════════════════════════════════════════════════ -- SMALL-STEP SEMANTICS @@ -267,6 +281,23 @@ inductive Step : Expr → Expr → Prop where | echoAddRight : IsValue e₁ → Step e₂ e₂' → Step (.echoAdd e₁ e₂) (.echoAdd e₁ e₂') | echoAddNums : Step (.echoAdd (.num n₁) (.num n₂)) (.echoVal (.pair (.num n₁) (.num n₂)) (.num (n₁ + n₂))) + -- Echo-preserving equality: residue retains the operand pair; result is the + -- boolean. Mirrors the 8 `eq` rules; each computation produces + -- `echoVal (pair ) (boolLit )`. + | echoEqLeft : Step e₁ e₁' → Step (.echoEq e₁ e₂) (.echoEq e₁' e₂) + | echoEqRight : IsValue e₁ → Step e₂ e₂' → Step (.echoEq e₁ e₂) (.echoEq e₁ e₂') + | echoEqNums : Step (.echoEq (.num n₁) (.num n₂)) + (.echoVal (.pair (.num n₁) (.num n₂)) (.boolLit (n₁ == n₂))) + | echoEqStrs : Step (.echoEq (.str s₁) (.str s₂)) + (.echoVal (.pair (.str s₁) (.str s₂)) (.boolLit (s₁ == s₂))) + | echoEqBraids : Step (.echoEq (.braidLit gs₁) (.braidLit gs₂)) + (.echoVal (.pair (.braidLit gs₁) (.braidLit gs₂)) (.boolLit (gs₁ == gs₂))) + | echoEqIdId : Step (.echoEq .identity .identity) + (.echoVal (.pair .identity .identity) (.boolLit true)) + | echoEqIdBraid : Step (.echoEq .identity (.braidLit gs)) + (.echoVal (.pair .identity (.braidLit gs)) (.boolLit (gs == []))) + | echoEqBraidId : Step (.echoEq (.braidLit gs) .identity) + (.echoVal (.pair (.braidLit gs) .identity) (.boolLit (gs == []))) -- ═══════════════════════════════════════════════════════════════════════ -- LEMMAS @@ -511,6 +542,36 @@ theorem progress : HasType [] e τ → IsValue e ∨ ∃ e', Step e e' := by exact ⟨_, .echoAddNums⟩ · exact ⟨_, .echoAddRight hv₁ hs₂⟩ · exact ⟨_, .echoAddLeft hs₁⟩ + | tEchoEqWord _ _ n h₁ h₂ => + right + rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩ + · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩ + · rcases canonical_word hv₁ h₁ with ⟨rfl, _⟩ | ⟨gs₁, rfl, _⟩ <;> + rcases canonical_word hv₂ h₂ with ⟨rfl, _⟩ | ⟨gs₂, rfl, _⟩ + · exact ⟨_, .echoEqIdId⟩ + · exact ⟨_, .echoEqIdBraid⟩ + · exact ⟨_, .echoEqBraidId⟩ + · exact ⟨_, .echoEqBraids⟩ + · exact ⟨_, .echoEqRight hv₁ hs₂⟩ + · exact ⟨_, .echoEqLeft hs₁⟩ + | tEchoEqNum _ _ h₁ h₂ => + right + rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩ + · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩ + · obtain ⟨n₁, rfl⟩ := canonical_num hv₁ h₁ + obtain ⟨n₂, rfl⟩ := canonical_num hv₂ h₂ + exact ⟨_, .echoEqNums⟩ + · exact ⟨_, .echoEqRight hv₁ hs₂⟩ + · exact ⟨_, .echoEqLeft hs₁⟩ + | tEchoEqStr _ _ h₁ h₂ => + right + rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩ + · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩ + · obtain ⟨s₁, rfl⟩ := canonical_str hv₁ h₁ + obtain ⟨s₂, rfl⟩ := canonical_str hv₂ h₂ + exact ⟨_, .echoEqStrs⟩ + · exact ⟨_, .echoEqRight hv₁ hs₂⟩ + · exact ⟨_, .echoEqLeft hs₁⟩ -- ═══════════════════════════════════════════════════════════════════════ -- THEOREM 2: PRESERVATION @@ -644,6 +705,50 @@ theorem preservation : HasType [] e τ → Step e e' → HasType [] e' τ := by | echoAddNums => cases ht with | tEchoAdd _ _ h₁ h₂ => exact .tEchoVal _ _ _ _ _ (.tPair _ _ _ _ _ (.tNum _ _) (.tNum _ _)) (.tNum _ _) + -- Echo-preserving equality: congruence rebuilds via `tEchoEq*` + `ih` (the + -- inner type is ambiguous, so case-split on all three `tEchoEq*`); the 6 + -- computation rules invert the matching `tEchoEq*` and build the formed echo + -- value `echoVal (pair ) (boolLit …)`, residue typed via `tPair`. + | echoEqLeft hs ih => + cases ht with + | tEchoEqWord _ _ n h₁ h₂ => exact .tEchoEqWord _ _ _ n (ih h₁) h₂ + | tEchoEqNum _ _ h₁ h₂ => exact .tEchoEqNum _ _ _ (ih h₁) h₂ + | tEchoEqStr _ _ h₁ h₂ => exact .tEchoEqStr _ _ _ (ih h₁) h₂ + | echoEqRight _ hs ih => + cases ht with + | tEchoEqWord _ _ n h₁ h₂ => exact .tEchoEqWord _ _ _ n h₁ (ih h₂) + | tEchoEqNum _ _ h₁ h₂ => exact .tEchoEqNum _ _ _ h₁ (ih h₂) + | tEchoEqStr _ _ h₁ h₂ => exact .tEchoEqStr _ _ _ h₁ (ih h₂) + | echoEqNums => cases ht with + | tEchoEqNum => + exact .tEchoVal _ _ _ _ _ (.tPair _ _ _ _ _ (.tNum _ _) (.tNum _ _)) (.tBool _ _) + | tEchoEqWord _ _ _ _ h₁ => cases h₁ + | tEchoEqStr _ _ _ h₁ => cases h₁ + | echoEqStrs => cases ht with + | tEchoEqStr => + exact .tEchoVal _ _ _ _ _ (.tPair _ _ _ _ _ (.tStr _ _) (.tStr _ _)) (.tBool _ _) + | tEchoEqWord _ _ _ _ h₁ => cases h₁ + | tEchoEqNum _ _ _ h₁ => cases h₁ + | echoEqBraids => cases ht with + | tEchoEqWord _ _ n h₁ h₂ => + exact .tEchoVal _ _ _ _ _ (.tPair _ _ _ _ _ h₁ h₂) (.tBool _ _) + | tEchoEqNum _ _ _ h₁ => cases h₁ + | tEchoEqStr _ _ _ h₁ => cases h₁ + | echoEqIdId => cases ht with + | tEchoEqWord _ _ n h₁ h₂ => + exact .tEchoVal _ _ _ _ _ (.tPair _ _ _ _ _ h₁ h₂) (.tBool _ _) + | tEchoEqNum _ _ _ h₁ => cases h₁ + | tEchoEqStr _ _ _ h₁ => cases h₁ + | echoEqIdBraid => cases ht with + | tEchoEqWord _ _ n h₁ h₂ => + exact .tEchoVal _ _ _ _ _ (.tPair _ _ _ _ _ h₁ h₂) (.tBool _ _) + | tEchoEqNum _ _ _ h₁ => cases h₁ + | tEchoEqStr _ _ _ h₁ => cases h₁ + | echoEqBraidId => cases ht with + | tEchoEqWord _ _ n h₁ h₂ => + exact .tEchoVal _ _ _ _ _ (.tPair _ _ _ _ _ h₁ h₂) (.tBool _ _) + | tEchoEqNum _ _ _ h₁ => cases h₁ + | tEchoEqStr _ _ _ h₁ => cases h₁ -- ═══════════════════════════════════════════════════════════════════════ -- THEOREM 3: DETERMINISM @@ -841,6 +946,51 @@ theorem determinism : Step e e₁ → Step e e₂ → e₁ = e₂ := by | echoAddLeft h => exact absurd h (value_no_step (.num _)) | echoAddRight _ h => exact absurd h (value_no_step (.num _)) | echoAddNums => rfl + -- Echo-preserving equality: same shape as `eq` determinism — congruence is + -- deterministic by IH; computations discharge congruence races via + -- `value_no_step` on the atomic operand values; same-rule → `rfl`. + | echoEqLeft hs ih => cases hs₂ with + | echoEqLeft h => rw [ih h] + | echoEqRight hv _ => exact absurd hs (value_no_step hv) + | echoEqNums => exact absurd hs (value_no_step (.num _)) + | echoEqStrs => exact absurd hs (value_no_step (.str _)) + | echoEqBraids => exact absurd hs (value_no_step (.braidLit _)) + | echoEqIdId => exact absurd hs (value_no_step .identity) + | echoEqIdBraid => exact absurd hs (value_no_step .identity) + | echoEqBraidId => exact absurd hs (value_no_step (.braidLit _)) + | echoEqRight hv hs ih => cases hs₂ with + | echoEqLeft h => exact absurd h (value_no_step hv) + | echoEqRight _ h => exact congrArg (Expr.echoEq _ ·) (ih h) + | echoEqNums => exact absurd hs (value_no_step (.num _)) + | echoEqStrs => exact absurd hs (value_no_step (.str _)) + | echoEqBraids => exact absurd hs (value_no_step (.braidLit _)) + | echoEqIdId => cases hv with | identity => exact absurd hs (value_no_step .identity) + | echoEqIdBraid => cases hv with | identity => exact absurd hs (value_no_step (.braidLit _)) + | echoEqBraidId => cases hv with | braidLit => exact absurd hs (value_no_step .identity) + | echoEqNums => cases hs₂ with + | echoEqLeft h => exact absurd h (value_no_step (.num _)) + | echoEqRight _ h => exact absurd h (value_no_step (.num _)) + | echoEqNums => rfl + | echoEqStrs => cases hs₂ with + | echoEqLeft h => exact absurd h (value_no_step (.str _)) + | echoEqRight _ h => exact absurd h (value_no_step (.str _)) + | echoEqStrs => rfl + | echoEqBraids => cases hs₂ with + | echoEqLeft h => exact absurd h (value_no_step (.braidLit _)) + | echoEqRight _ h => exact absurd h (value_no_step (.braidLit _)) + | echoEqBraids => rfl + | echoEqIdId => cases hs₂ with + | echoEqLeft h => exact absurd h (value_no_step .identity) + | echoEqRight _ h => exact absurd h (value_no_step .identity) + | echoEqIdId => rfl + | echoEqIdBraid => cases hs₂ with + | echoEqLeft h => exact absurd h (value_no_step .identity) + | echoEqRight _ h => exact absurd h (value_no_step (.braidLit _)) + | echoEqIdBraid => rfl + | echoEqBraidId => cases hs₂ with + | echoEqLeft h => exact absurd h (value_no_step (.braidLit _)) + | echoEqRight _ h => exact absurd h (value_no_step .identity) + | echoEqBraidId => rfl -- ═══════════════════════════════════════════════════════════════════════ -- COROLLARY: TYPE SAFETY @@ -932,6 +1082,16 @@ theorem echoAdd_distinguishes : (Expr.pair (.num 1) (.num 3) ≠ Expr.pair (.num 2) (.num 2)) := ⟨⟨echoAdd_lower_sums 1 3, echoAdd_lower_sums 2 2⟩, by decide⟩ +/-- **Echo distinguishes what `eq` collapses.** 1≟2 and 3≟4 both lower to + `false`, but their residues (the operand pairs) stay distinct. -/ +theorem echoEq_distinguishes : + (StepStar (.lower (.echoEq (.num 1) (.num 2))) (.boolLit (1 == 2)) ∧ + StepStar (.lower (.echoEq (.num 3) (.num 4))) (.boolLit (3 == 4))) ∧ + (Expr.pair (.num 1) (.num 2) ≠ Expr.pair (.num 3) (.num 4)) := + ⟨⟨.head (.lowerStep .echoEqNums) (.head (.lowerVal (.pair (.num _) (.num _)) (.boolLit _)) .refl), + .head (.lowerStep .echoEqNums) (.head (.lowerVal (.pair (.num _) (.num _)) (.boolLit _)) .refl)⟩, + by decide⟩ + -- ═══════════════════════════════════════════════════════════════════════ -- TG-2: DECIDABILITY OF TYPE CHECKING -- ═══════════════════════════════════════════════════════════════════════ @@ -1008,6 +1168,12 @@ def infer (Γ : Ctx) : Expr → Option Ty match infer Γ e₁, infer Γ e₂ with | some .num, some .num => some (.echo (.prod .num .num) .num) | _, _ => none + | .echoEq e₁ e₂ => + match infer Γ e₁, infer Γ e₂ with + | some (.word n), some (.word m) => if n = m then some (.echo (.prod (.word n) (.word n)) .bool) else none + | some .num, some .num => some (.echo (.prod .num .num) .bool) + | some .str, some .str => some (.echo (.prod .str .str) .bool) + | _, _ => none /-- **Completeness**: every typing derivation is computed by `infer`. -/ theorem infer_complete {Γ : Ctx} {e : Expr} {τ : Ty} : @@ -1093,6 +1259,17 @@ theorem infer_sound {Γ : Ctx} {e : Expr} {τ : Ty} : intro h; simp only [infer] at h; split at h next he₁ he₂ => injection h with h; subst h; exact .tEchoAdd _ _ _ (ih₁ he₁) (ih₂ he₂) all_goals simp at h + | echoEq e₁ e₂ ih₁ ih₂ => + intro h; simp only [infer] at h; split at h + next n m he₁ he₂ => + split at h + next hnm => + injection h with h; subst h; subst hnm + exact .tEchoEqWord _ _ _ _ (ih₁ he₁) (ih₂ he₂) + next => simp at h + next he₁ he₂ => injection h with h; subst h; exact .tEchoEqNum _ _ _ (ih₁ he₁) (ih₂ he₂) + next he₁ he₂ => injection h with h; subst h; exact .tEchoEqStr _ _ _ (ih₁ he₁) (ih₂ he₂) + all_goals simp at h /-- **Decidability of type checking** (TG-2): `infer` decides `HasType`. -/ theorem infer_iff_hasType {Γ : Ctx} {e : Expr} {τ : Ty} :