@@ -33,19 +33,25 @@ inductive Ty : Type where
3333 | dist : Ty → Ty
3434 -- Echo types (structured loss; see `hyperpolymath/echo-types`). `echo T` is
3535 -- a proof-relevant retained-loss residue over `T`, distinct from `T`;
36- -- `echoR T` is its strict, non-recoverable weakening. These are type
37- -- *formers* only in this Lean development: no `Expr` constructor introduces
38- -- or eliminates them and `HasType` assigns no expression an echo type, so
39- -- the carrier's metatheory (Progress/Preservation below) is unaffected.
40- -- NOTE: the Rust checker `bet-check` now carries the *typing rules* for the
41- -- echo operations — introduction `echo : 'a → Echo 'a`, the functor/comonad
42- -- surface `echo_map`/`echo_output` (counit)/`echo_duplicate`, the residue
36+ -- `echoR T` is its strict, non-recoverable weakening.
37+ -- TP-5 (DISCHARGED below): `echo T` is now modelled at the term level by the
38+ -- `Expr.echoIntro` (introduction, `T → echo T`) and `Expr.echoElim`
39+ -- (elimination / the `echo_output` counit projection, `echo T → T`)
40+ -- constructors, with typing rules `tEchoIntro`/`tEchoElim`, the β-rule
41+ -- `echoElimIntro`, congruences `echoIntroStep`/`echoElimStep`, the canonical
42+ -- forms lemma `canonical_echo`, and Progress/Preservation re-established over
43+ -- the extended calculus. The intro/elim pair is a single-subexpression,
44+ -- non-binding, ghost former (modelled exactly like `distPure`/`sample`).
45+ -- TP-5b (DEFERRED): `echoR T` remains a type *former* only (no `Expr`
46+ -- constructor introduces or eliminates it), and the richer Rust surface
47+ -- ops — the functor/comonad `echo_map`/`echo_duplicate`, the residue
4348 -- lowering `echo_to_residue : Echo 'a → EchoR 'a`, and the probabilistic
44- -- bridge `sample_echo : Dist 'a → Echo 'a` (all type-level / ghost; the
45- -- ungraded shadow of `EchoGradedComonad.agda`). Mirroring those rules here
46- -- and re-establishing Progress/Preservation is tracked as obligation TP-5
47- -- (PROOF-NEEDS.md), deferred until the runtime residue representation is
48- -- settled.
49+ -- bridge `sample_echo : Dist 'a → Echo 'a` (the ungraded shadow of
50+ -- `EchoGradedComonad.agda`) — are not modelled here. They compose from
51+ -- `echoIntro`/`echoElim` plus the existing forms (e.g. `echo_map g` is
52+ -- `λx. echoIntro (g (echoElim x))`) and are tracked as TP-5b, deferred
53+ -- until the runtime residue representation is settled. The Rust checker
54+ -- `bet-check` carries their type-level / ghost typing rules.
4955 | echo : Ty → Ty
5056 | echoR : Ty → Ty
5157 deriving DecidableEq, Repr
@@ -66,6 +72,8 @@ inductive Expr : Type where
6672 | sample : Expr → Expr -- sample e (Dist T → T)
6773 | distPure : Expr → Expr -- return/pure for Dist (wraps value)
6874 | distBind : Expr → Expr → Expr -- bind : Dist A → (A → Dist B) → Dist B
75+ | echoIntro : Expr → Expr -- echo intro: T → echo T (retain loss)
76+ | echoElim : Expr → Expr -- echo elim / echo_output: echo T → T
6977 deriving Repr
7078
7179-- ════════════════════════════════════════════════════════════════════════════
@@ -81,6 +89,7 @@ inductive IsValue : Expr → Prop where
8189 | litUnit : IsValue Expr.litUnit
8290 | lam : IsValue (Expr.lam t body)
8391 | distPure : IsValue v → IsValue (Expr.distPure v)
92+ | echoIntro : IsValue v → IsValue (Expr.echoIntro v)
8493
8594/-- Values are decidable (we need this for case analysis in proofs). -/
8695def isValue : Expr → Bool
@@ -91,6 +100,7 @@ def isValue : Expr → Bool
91100 | Expr.litUnit => true
92101 | Expr.lam _ _ => true
93102 | Expr.distPure v => isValue v
103+ | Expr.echoIntro v => isValue v
94104 | _ => false
95105
96106-- ════════════════════════════════════════════════════════════════════════════
@@ -152,6 +162,12 @@ inductive HasType : Ctx → Expr → Ty → Prop where
152162 | tDistBind : HasType Γ e₁ (Ty.dist A) →
153163 HasType Γ e₂ (Ty.arrow A (Ty.dist B)) →
154164 HasType Γ (Expr.distBind e₁ e₂) (Ty.dist B)
165+ /-- T-EchoIntro: echo introduction — T → echo T -/
166+ | tEchoIntro : HasType Γ e T →
167+ HasType Γ (Expr.echoIntro e) (Ty.echo T)
168+ /-- T-EchoElim: echo elimination (echo_output counit) — echo T → T -/
169+ | tEchoElim : HasType Γ e (Ty.echo T) →
170+ HasType Γ (Expr.echoElim e) T
155171
156172-- ════════════════════════════════════════════════════════════════════════════
157173-- Section 4. Substitution
@@ -173,6 +189,8 @@ def shift (amount : Int) (cutoff : Nat) : Expr → Expr
173189 | Expr.sample e => Expr.sample (shift amount cutoff e)
174190 | Expr.distPure e => Expr.distPure (shift amount cutoff e)
175191 | Expr.distBind e₁ e₂ => Expr.distBind (shift amount cutoff e₁) (shift amount cutoff e₂)
192+ | Expr.echoIntro e => Expr.echoIntro (shift amount cutoff e)
193+ | Expr.echoElim e => Expr.echoElim (shift amount cutoff e)
176194
177195/-- Substitute expression `s` for variable `j` in expression `e`. -/
178196def subst (j : Nat) (s : Expr) : Expr → Expr
@@ -190,6 +208,8 @@ def subst (j : Nat) (s : Expr) : Expr → Expr
190208 | Expr.sample e => Expr.sample (subst j s e)
191209 | Expr.distPure e => Expr.distPure (subst j s e)
192210 | Expr.distBind e₁ e₂ => Expr.distBind (subst j s e₁) (subst j s e₂)
211+ | Expr.echoIntro e => Expr.echoIntro (subst j s e)
212+ | Expr.echoElim e => Expr.echoElim (subst j s e)
193213
194214/-- Top-level substitution: replace variable 0 and shift down. -/
195215def substTop (s : Expr) (e : Expr) : Expr :=
@@ -265,6 +285,15 @@ inductive Step : Expr → Expr → Prop where
265285 | distBindStep2 : IsValue v →
266286 Step e₂ e₂' →
267287 Step (Expr.distBind v e₂) (Expr.distBind v e₂')
288+ -- EchoElim of echoIntro: echoElim (echoIntro v) → v (counit β-rule)
289+ | echoElimIntro : IsValue v →
290+ Step (Expr.echoElim (Expr.echoIntro v)) v
291+ -- EchoIntro congruence
292+ | echoIntroStep : Step e e' →
293+ Step (Expr.echoIntro e) (Expr.echoIntro e')
294+ -- EchoElim congruence
295+ | echoElimStep : Step e e' →
296+ Step (Expr.echoElim e) (Expr.echoElim e')
268297
269298-- ════════════════════════════════════════════════════════════════════════════
270299-- Section 6. Canonical forms lemma
@@ -283,6 +312,7 @@ theorem canonical_arrow {v : Expr} {S T : Ty} :
283312 | litString => cases ht
284313 | litUnit => cases ht
285314 | distPure _ => cases ht
315+ | echoIntro _ => cases ht
286316
287317/-- Canonical forms: a closed value of Bool type must be a boolean literal. -/
288318theorem canonical_bool {v : Expr} :
@@ -297,6 +327,7 @@ theorem canonical_bool {v : Expr} :
297327 | litUnit => cases ht
298328 | lam => cases ht
299329 | distPure _ => cases ht
330+ | echoIntro _ => cases ht
300331
301332/-- Canonical forms: a closed value of Dist T must be distPure of a value. -/
302333theorem canonical_dist {v : Expr} {T : Ty} :
@@ -311,6 +342,21 @@ theorem canonical_dist {v : Expr} {T : Ty} :
311342 | litString => cases ht
312343 | litUnit => cases ht
313344 | lam => cases ht
345+ | echoIntro _ => cases ht
346+
347+ /-- Canonical forms: a closed value of `echo T` must be `echoIntro` of a value. -/
348+ theorem canonical_echo {Γ : Ctx} {e : Expr} {T : Ty}
349+ (ht : HasType Γ e (Ty.echo T)) (hv : IsValue e) :
350+ ∃ v, e = Expr.echoIntro v ∧ IsValue v := by
351+ cases hv with
352+ | echoIntro hv' => cases ht with | tEchoIntro h => exact ⟨_, rfl, hv'⟩
353+ | litInt => cases ht
354+ | litFloat => cases ht
355+ | litBool => cases ht
356+ | litString => cases ht
357+ | litUnit => cases ht
358+ | lam => cases ht
359+ | distPure _ => cases ht
314360
315361-- ════════════════════════════════════════════════════════════════════════════
316362-- Section 7. Progress theorem
@@ -381,6 +427,17 @@ theorem progress {e : Expr} {T : Ty} (ht : HasType [] e T) :
381427 obtain ⟨_, rfl, hvw⟩ := canonical_dist ht1 hv1
382428 exact ⟨_, Step.distBindPure hvw⟩
383429 · exact ⟨_, Step.distBindStep1 hs1⟩
430+ | tEchoIntro _ ihe =>
431+ rcases ihe hΓ with hve | ⟨_, hse⟩
432+ · left; exact IsValue.echoIntro hve
433+ · right; exact ⟨_, Step.echoIntroStep hse⟩
434+ | tEchoElim hte ihe =>
435+ right
436+ rcases ihe hΓ with hve | ⟨_, hse⟩
437+ · subst hΓ
438+ obtain ⟨w, rfl, hvw⟩ := canonical_echo hte hve
439+ exact ⟨w, Step.echoElimIntro hvw⟩
440+ · exact ⟨_, Step.echoElimStep hse⟩
384441
385442-- ════════════════════════════════════════════════════════════════════════════
386443-- Section 8. Weakening and substitution lemmas
@@ -542,6 +599,14 @@ theorem shift_preserves_typing
542599 intro k U hk
543600 simp only [shift]
544601 exact HasType.tDistBind (ih1 k U hk) (ih2 k U hk)
602+ | tEchoIntro _ ih =>
603+ intro k U hk
604+ simp only [shift]
605+ exact HasType.tEchoIntro (ih k U hk)
606+ | tEchoElim _ ih =>
607+ intro k U hk
608+ simp only [shift]
609+ exact HasType.tEchoElim (ih k U hk)
545610
546611/-- Shift down then up cancels: `shift (-1) k (shift 1 k e) = e`.
547612 Holds unconditionally because every variable that gets shifted up by `shift 1 k`
@@ -628,6 +693,16 @@ theorem shift_down_shift_up (e : Expr) :
628693 (shift (-1 ) k (shift 1 k e₂))
629694 = Expr.distBind e₁ e₂
630695 rw [ih1, ih2]
696+ | echoIntro e ih =>
697+ intro k
698+ show shift (-1 ) k (Expr.echoIntro (shift 1 k e)) = Expr.echoIntro e
699+ show Expr.echoIntro (shift (-1 ) k (shift 1 k e)) = Expr.echoIntro e
700+ rw [ih]
701+ | echoElim e ih =>
702+ intro k
703+ show shift (-1 ) k (Expr.echoElim (shift 1 k e)) = Expr.echoElim e
704+ show Expr.echoElim (shift (-1 ) k (shift 1 k e)) = Expr.echoElim e
705+ rw [ih]
631706
632707/-- General shift-shift commutation: for `i ≤ j`,
633708 `shift 1 i (shift 1 j e) = shift 1 (j+1) (shift 1 i e)`.
@@ -742,6 +817,20 @@ theorem shift_one_comm_general (e : Expr) :
742817 show Expr.distBind (shift 1 i (shift 1 j e₁)) (shift 1 i (shift 1 j e₂))
743818 = Expr.distBind (shift 1 (j+1 ) (shift 1 i e₁)) (shift 1 (j+1 ) (shift 1 i e₂))
744819 rw [ih1 i j hij, ih2 i j hij]
820+ | echoIntro e ih =>
821+ intros i j hij
822+ show shift 1 i (Expr.echoIntro (shift 1 j e))
823+ = shift 1 (j+1 ) (Expr.echoIntro (shift 1 i e))
824+ show Expr.echoIntro (shift 1 i (shift 1 j e))
825+ = Expr.echoIntro (shift 1 (j+1 ) (shift 1 i e))
826+ rw [ih i j hij]
827+ | echoElim e ih =>
828+ intros i j hij
829+ show shift 1 i (Expr.echoElim (shift 1 j e))
830+ = shift 1 (j+1 ) (Expr.echoElim (shift 1 i e))
831+ show Expr.echoElim (shift 1 i (shift 1 j e))
832+ = Expr.echoElim (shift 1 (j+1 ) (shift 1 i e))
833+ rw [ih i j hij]
745834
746835/-- Specialisation of `shift_one_comm_general` at i = 0. -/
747836theorem shift_one_comm (e : Expr) :
@@ -912,6 +1001,18 @@ theorem substAt_preserves_typing :
9121001 exact HasType.tDistBind
9131002 (ih1 Γ k S _ v ht1 hv hk)
9141003 (ih2 Γ k S _ v ht2 hv hk)
1004+ | echoIntro e ih =>
1005+ intros Γ k S T v hbody hv hk
1006+ cases hbody with
1007+ | tEchoIntro ht =>
1008+ simp only [subst, shift]
1009+ exact HasType.tEchoIntro (ih Γ k S _ v ht hv hk)
1010+ | echoElim e ih =>
1011+ intros Γ k S T v hbody hv hk
1012+ cases hbody with
1013+ | tEchoElim ht =>
1014+ simp only [subst, shift]
1015+ exact HasType.tEchoElim (ih Γ k S _ v ht hv hk)
9151016
9161017-- ════════════════════════════════════════════════════════════════════════════
9171018-- Section 9. Preservation theorem
@@ -1004,6 +1105,17 @@ theorem preservation {Γ : Ctx} {e e' : Expr} {T : Ty}
10041105 | distBindStep2 _ _ ih =>
10051106 cases ht with
10061107 | tDistBind ht1 ht2 => exact HasType.tDistBind ht1 (ih ht2)
1108+ | echoElimIntro _ =>
1109+ cases ht with
1110+ | tEchoElim hte =>
1111+ cases hte with
1112+ | tEchoIntro he => exact he
1113+ | echoIntroStep _ ih =>
1114+ cases ht with
1115+ | tEchoIntro hte => exact HasType.tEchoIntro (ih hte)
1116+ | echoElimStep _ ih =>
1117+ cases ht with
1118+ | tEchoElim hte => exact HasType.tEchoElim (ih hte)
10071119
10081120-- ════════════════════════════════════════════════════════════════════════════
10091121-- Section 10. Type safety (corollary)
@@ -1159,6 +1271,9 @@ theorem value_no_step {v e : Expr} (hv : IsValue v) : ¬ Step v e := by
11591271 | distPure hv' =>
11601272 cases hs with
11611273 | distPureStep hs' => exact value_no_step hv' hs'
1274+ | echoIntro hv' =>
1275+ cases hs with
1276+ | echoIntroStep hs' => exact value_no_step hv' hs'
11621277
11631278-- ════════════════════════════════════════════════════════════════════════════
11641279-- End of formalisation
0 commit comments