Skip to content

Commit 267cce2

Browse files
hyperpolymathhyperpolymath
authored
proof(L2): TypingL2.v + Modality.v skeleton — Linear⇒Affine weakening Qed (#168)
## Summary Layer 2 of the four-layer preservation redesign (`PRESERVATION-DESIGN.md` §5). Encodes the modality as a judgment parameter and ships the **headline §5 weakening lemma** `weaken_modality : Linear ⇒ Affine` as Qed. Mirrors `echo-types/proofs/agda/EchoLinear.agda`'s `weaken` at the typing-derivation layer. ## What's in this PR ### `formal/Modality.v` | Item | Kind | |---|---| | `Modality = {Linear, Affine}` | inductive | | `modality_le` thin-poset at sort Type | inductive | | `modality_le_refl` / `modality_le_trans` / `modality_le_prop` | Qed, **all K-free** | ### `formal/TypingL2.v` | Item | Kind | |---|---| | `has_type_l2 : Modality → region_env → ctx → expr → ty → region_env → ctx → Type` | inductive (1 constructor in this skeleton) | | `L2_lift_l1` | the single constructor: any L1 derivation lifts to L2 at either mode | | `lift_l1_to_linear` / `lift_l1_to_affine` | convenience entry points | | `project_l2_to_l1` | inverse projection (no info loss) | | **`weaken_modality`** — the §5 headline | **Qed** | | `weaken_modality_le` — general modality-poset weakening | Definition | | `weaken_modality_le_id_linear` / `_id_affine` / `_strict_is_weaken_modality` | Qed | ## Axiom status **Every lemma in this PR is closed under the global context** — zero K, zero UIP, zero new axioms. Verified via `Print Assumptions` on `modality_le_trans`, `modality_le_prop`, `weaken_modality`, `weaken_modality_le`, `weaken_modality_le_strict_is_weaken_modality`. Note: this is *cleaner* than L3 Phase 1's `Mode` poset in `Echo.v`, which uses `dependent destruction` for `mode_le_trans` and `degrade_mode_comp` (documented K proof-debt). L2's `modality_le_trans` uses the K-free motive trick from the start; the L3.K cleanup task (#6 in session tracker) can mirror this pattern. ## What's NOT in this PR (forward-looking, separate PRs) - **Mode-specific `T_Lam_*_L2`** — Linear requires `(T1, true)` on body output; Affine permits `(T1, true_or_unused)`. Adding these introduces mode-switch cases in `weaken_modality`'s proof. - **Mode-specific `T_Drop_*_L2`** — Linear: obligation-discharge; Affine: implicit drop with `LEcho Affine` residue (cross-layer with L3; see `Echo.v`'s `no_section_collapse_to_residue` for why the residue is structurally well-defined). - **Branch-meet for `T_Case_*_L2` / `T_If_*_L2`** — Linear exact `(R', G')` match vs Affine thin-poset meet. - **Top-level closure constraint** — Linear: `G = G' = []`; Affine: `G' may carry unused linear bindings`. - **No-leak / no-duplicate / resource-exact / garbage-residue-inhabited** proof obligations (§5 table). - **Effect-typed `TFun`** — resolves L1's lambda-rigidity gap per §4.8. ## Cross-layer dependency note L1's `S_App_Step2` / `S_Pair_Step2` admits in `preservation_l1` are explicitly L2/L3-gated by `Semantics_L1.v`'s design notes (§4.8). The L2 mode-specific `T_Lam_*_L2` constructors are the mechanism that closes them in a follow-up. ## Branch base Stacked off `proof/l1-region-threading-design` (PR #153, currently auto-merge-armed pending governance CI rerun). Will rebase to `main` once #153 lands. ## Test plan - [x] `coqc 8.18.0` builds `Modality.v` + `TypingL2.v` cleanly, 0 admits - [x] Clean full-project rebuild passes — 9 .v files - [x] `Print Assumptions weaken_modality` returns `Closed under the global context` — headline result is K-free, zero axioms - [x] No new axioms introduced beyond what L1/L3 already document - [ ] CI green - [ ] Review: judgment shape matches §5; the single-constructor skeleton is appropriate as a "first slice" parallel to L3's #166; the mode-specific rules are correctly out of scope Refs `PRESERVATION-DESIGN.md` §5, `echo-types/proofs/agda/EchoLinear.agda`, PR #153, PR #166, PR #167. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
1 parent ff9b0e3 commit 267cce2

3 files changed

Lines changed: 308 additions & 0 deletions

File tree

‎formal/Modality.v‎

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
(* SPDX-License-Identifier: PMPL-1.0-or-later *)
2+
(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
3+
4+
(** * Ephapax L2 — Modality (the typing-layer mode parameter)
5+
6+
This file defines the modality parameter that the L2 typing
7+
judgment carries. Per PRESERVATION-DESIGN.md §5, the modality
8+
[ℓ ∈ {Linear, Affine}] lives on the judgment:
9+
10+
[R ; G ⊢_ℓ e : T -| R' ; G']
11+
12+
The two sublanguages share [Syntax.v] and [Semantics.v]; they
13+
differ in which derivations the typing relation admits.
14+
15+
Why a separate datatype from [Echo.Mode]: [Mode] (defined in
16+
[Echo.v]) classifies *echoes* — the L3 residue layer's
17+
propositional / proof-relevant distinction. [Modality] (defined
18+
here) classifies *typing derivations* — the L2 layer's strict /
19+
relaxed consumption discipline. They happen to be isomorphic
20+
(both are [{Linear, Affine}] with the same poset) but live at
21+
distinct conceptual layers; the L4 dyadic-interaction layer
22+
couples them via the project-level mode declaration.
23+
24+
Cross-layer bridges are deferred to a follow-up.
25+
26+
===== Properties of this layer =====
27+
28+
- [Modality]: enumerated type with [Linear] and [Affine].
29+
- [modality_le]: thin poset; [Linear ⊑ Linear], [Linear ⊑
30+
Affine], [Affine ⊑ Affine]. [Linear ≤ Affine] expresses that
31+
Linear is the more restrictive mode (so every Linear derivation
32+
is also an Affine derivation, modulo the same syntax).
33+
- [modality_le_refl] / [modality_le_trans] / [modality_le_prop]:
34+
structural properties, all Qed.
35+
36+
Both K-free properties of this layer are inherited by the L2
37+
typing judgment: any rule that quantifies over modality can use
38+
[modality_le_prop] to discriminate proofs and [modality_le_trans]
39+
to compose mode-weakenings. *)
40+
41+
Inductive Modality : Type :=
42+
| Linear : Modality
43+
| Affine : Modality.
44+
45+
(** The thin poset on [Modality]: [Linear] is the strict mode
46+
(more restrictive), [Affine] the relaxed mode (permits implicit
47+
drops). [Linear ⊑ Affine] captures that every Linear derivation
48+
can be viewed as an Affine derivation. *)
49+
50+
Inductive modality_le : Modality -> Modality -> Type :=
51+
| Linear_le_Linear : modality_le Linear Linear
52+
| Linear_le_Affine : modality_le Linear Affine
53+
| Affine_le_Affine : modality_le Affine Affine.
54+
55+
Lemma modality_le_refl : forall m, modality_le m m.
56+
Proof. intros [|]; constructor. Qed.
57+
58+
(** Helper: when the first modality is [Affine], the second is
59+
[Affine] too. K-free via a motive trick. *)
60+
61+
Definition modality_le_affine_first
62+
(m2 : Modality) (H : modality_le Affine m2) : m2 = Affine :=
63+
match H in modality_le mA mB
64+
return
65+
(match mA return Prop with
66+
| Affine => mB = Affine
67+
| Linear => True
68+
end)
69+
with
70+
| Linear_le_Linear => I
71+
| Linear_le_Affine => I
72+
| Affine_le_Affine => eq_refl
73+
end.
74+
75+
(** [Defined] (not [Qed]) so [modality_le_trans] is transparent.
76+
Built by raw dependent pattern matching with a motive trick;
77+
K-free, no [dependent destruction]. *)
78+
79+
Definition modality_le_trans
80+
(m1 m2 m3 : Modality)
81+
(H12 : modality_le m1 m2) : modality_le m2 m3 -> modality_le m1 m3 :=
82+
match H12 in modality_le mA mB
83+
return modality_le mB m3 -> modality_le mA m3
84+
with
85+
| Linear_le_Linear => fun h => h
86+
| Linear_le_Affine =>
87+
fun h =>
88+
eq_rect Affine (fun m => modality_le Linear m)
89+
Linear_le_Affine m3
90+
(eq_sym (modality_le_affine_first m3 h))
91+
| Affine_le_Affine => fun h => h
92+
end.
93+
94+
(** Propositionality of the modality order. K-free. *)
95+
96+
Lemma modality_le_prop :
97+
forall m1 m2 (p q : modality_le m1 m2), p = q.
98+
Proof.
99+
intros m1 m2 p q.
100+
destruct p;
101+
refine
102+
match q as q'
103+
in modality_le mA mB
104+
return
105+
(match mA, mB return modality_le mA mB -> Prop with
106+
| Linear, Linear => fun q'' => Linear_le_Linear = q''
107+
| Linear, Affine => fun q'' => Linear_le_Affine = q''
108+
| Affine, Affine => fun q'' => Affine_le_Affine = q''
109+
| _, _ => fun _ => True
110+
end q')
111+
with
112+
| Linear_le_Linear => eq_refl
113+
| Linear_le_Affine => eq_refl
114+
| Affine_le_Affine => eq_refl
115+
end.
116+
Qed.

‎formal/TypingL2.v‎

Lines changed: 190 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,190 @@
1+
(* SPDX-License-Identifier: PMPL-1.0-or-later *)
2+
(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
3+
4+
(** * Ephapax L2 — Modality-parameterised typing judgment (skeleton)
5+
6+
Layer 2 of the four-layer preservation redesign
7+
([PRESERVATION-DESIGN.md] §5). The L2 judgment
8+
9+
[R ; G ⊢_ℓ e : T -| R' ; G']
10+
11+
extends [has_type_l1] (the R-threaded judgment from [TypingL1.v])
12+
with a modality parameter [ℓ ∈ {Linear, Affine}]. Most typing
13+
rules are modality-polymorphic (rule shape identical in both
14+
modes); the mode-specific rules are [T_Lam], [T_Drop], and the
15+
branch-meet of [T_Case] / [T_If].
16+
17+
===== Scope of this skeleton =====
18+
19+
Per design-doc §5 and the same "first slice" framing used for
20+
L3 (#166), this PR ships:
21+
22+
- The [has_type_l2] inductive shape — currently with a single
23+
[L2_lift_l1] constructor that lifts any L1 derivation into the
24+
L2 judgment at either mode. This is sound: per §5's
25+
preservation table, "[Affine derivations are L1-safe by
26+
weakening]" and Linear derivations are precisely the strict
27+
L1 derivations.
28+
29+
- [weaken_modality] — the headline §5 lemma, Qed. In this
30+
skeleton the proof is a single induction; future PRs will add
31+
mode-specific constructors and the proof body will gain mode-
32+
switch cases. The Linear→Affine arrow exists as a real proof
33+
term from day one.
34+
35+
What is NOT in this skeleton (forward-looking, separate PRs):
36+
37+
- Mode-specific [T_Lam_Linear_L2] / [T_Lam_Affine_L2]
38+
constructors. Per §5 table, Linear's [T_Lam] requires
39+
[(T1, true) :: G] on body output (the bound linear variable
40+
MUST be consumed); Affine's [T_Lam] permits
41+
[(T1, true_or_unused) :: G]. The L2 Phase 2 PR adds both as
42+
distinct constructors and re-proves [weaken_modality] with the
43+
added mode switch.
44+
45+
- Mode-specific [T_Drop_Linear_L2] / [T_Drop_Affine_L2]. Linear's
46+
[T_Drop] discharges an obligation to consume; Affine's permits
47+
implicit drop with an [LEcho Affine] residue produced (cross-
48+
layer with L3 — see [Echo.v]'s [no_section_collapse_to_residue]
49+
for why the residue is structurally well-defined).
50+
51+
- Mode-specific branch-meet for [T_Case_Linear_L2] / [T_If_*]:
52+
Linear requires both branches to agree on [(R', G')] exactly;
53+
Affine permits a thin-poset meet on outputs.
54+
55+
- Top-level closure constraint: Linear requires [G = G' = []];
56+
Affine requires [G = []] but [G'] may carry unused linear
57+
bindings.
58+
59+
- The no-leak / no-duplicate / resource-exact / garbage-residue-
60+
inhabited proof obligations (§5 table). Each is a separate
61+
lemma stated against [has_type_l2 Linear] or [has_type_l2
62+
Affine].
63+
64+
Cross-layer dependencies that block ulterior work:
65+
66+
- L1's lambda-rigidity gap (§4.8 of PRESERVATION-DESIGN.md +
67+
Semantics_L1.v's preservation_l1 admits) is resolved at the L2
68+
level by introducing effect-typed [TFun] in mode-specific
69+
[T_Lam_*_L2]. L2 Phase 2 + L3 Phase 3 jointly close the L1
70+
gap. *)
71+
72+
From Ephapax Require Import Syntax Typing TypingL1 Modality.
73+
74+
(** ===== The L2 judgment (skeleton) =====
75+
76+
A single constructor that lifts any L1 derivation into either
77+
mode. Future PRs add mode-specific rules. *)
78+
79+
Inductive has_type_l2
80+
: Modality ->
81+
region_env -> ctx -> expr -> ty -> region_env -> ctx -> Type :=
82+
| L2_lift_l1 :
83+
forall m R G e T R' G',
84+
TypingL1.has_type_l1 R G e T R' G' ->
85+
has_type_l2 m R G e T R' G'.
86+
87+
(** Notation following the Agda upstream [_;_⊢_ℓ_:_-|_;_]. *)
88+
89+
Reserved Notation "R ';' G '|=L2(' m ')' e ':' T '-|' R' ';' G'"
90+
(at level 70, G at next level, e at next level, T at next level, R' at next level).
91+
92+
Notation "R ';' G '|=L2(' m ')' e ':' T '-|' R' ';' G'" :=
93+
(has_type_l2 m R G e T R' G').
94+
95+
(** Convenience wrappers: an L1 derivation immediately gives an L2
96+
derivation at either mode. These are the entry points the L1
97+
consumers should use to upgrade to L2 framing. *)
98+
99+
Definition lift_l1_to_linear
100+
{R G e T R' G'}
101+
(H : TypingL1.has_type_l1 R G e T R' G') :
102+
has_type_l2 Linear R G e T R' G' :=
103+
L2_lift_l1 Linear R G e T R' G' H.
104+
105+
Definition lift_l1_to_affine
106+
{R G e T R' G'}
107+
(H : TypingL1.has_type_l1 R G e T R' G') :
108+
has_type_l2 Affine R G e T R' G' :=
109+
L2_lift_l1 Affine R G e T R' G' H.
110+
111+
(** Projection: extract the underlying L1 derivation from an L2 one.
112+
Witnesses that the L2 skeleton is a strict extension — no
113+
information loss vs L1. *)
114+
115+
Definition project_l2_to_l1
116+
{m R G e T R' G'}
117+
(H : has_type_l2 m R G e T R' G') :
118+
TypingL1.has_type_l1 R G e T R' G' :=
119+
match H with
120+
| L2_lift_l1 _ _ _ _ _ _ _ H1 => H1
121+
end.
122+
123+
(** ===== Headline §5 lemma: Linear ⇒ Affine weakening =====
124+
125+
Every Linear derivation is an Affine derivation. Mirrors
126+
[EchoLinear.agda]'s [weaken : LEcho linear → LEcho affine] but
127+
at the typing-derivation layer rather than the echo layer.
128+
129+
Proof: induction on the L2 derivation. In this skeleton there is
130+
one constructor case; future mode-specific constructors will
131+
introduce mode-switch cases. *)
132+
133+
Theorem weaken_modality :
134+
forall {R G e T R' G'},
135+
has_type_l2 Linear R G e T R' G' ->
136+
has_type_l2 Affine R G e T R' G'.
137+
Proof.
138+
intros R G e T R' G' H.
139+
apply lift_l1_to_affine.
140+
exact (project_l2_to_l1 H).
141+
Qed.
142+
143+
(** Idempotence at [Affine]: an Affine derivation re-weakened to
144+
Affine is the same derivation. Trivial in this skeleton; lets
145+
callers chain mode-weakenings without case analysis. *)
146+
147+
Theorem weaken_modality_affine_id :
148+
forall {R G e T R' G'} (H : has_type_l2 Affine R G e T R' G'),
149+
has_type_l2 Affine R G e T R' G'.
150+
Proof. intros; exact H. Qed.
151+
152+
(** General modality weakening: dispatch on a [modality_le] proof.
153+
For any [m1 ⊑ m2], a derivation at [m1] gives one at [m2]. *)
154+
155+
Definition weaken_modality_le
156+
{m1 m2 : Modality} (p : modality_le m1 m2)
157+
{R G e T R' G'}
158+
(H : has_type_l2 m1 R G e T R' G') :
159+
has_type_l2 m2 R G e T R' G' :=
160+
match p in modality_le mA mB
161+
return has_type_l2 mA R G e T R' G' ->
162+
has_type_l2 mB R G e T R' G'
163+
with
164+
| Linear_le_Linear => fun h => h
165+
| Linear_le_Affine => fun h => weaken_modality h
166+
| Affine_le_Affine => fun h => h
167+
end H.
168+
169+
(** Composition law: two successive modality-weakenings agree with
170+
a single weakening along the composed ordering. Mirrors
171+
[Echo.degrade_mode_comp] one layer up.
172+
173+
Trivial in this skeleton; future mode-specific rules will make
174+
this a real composition theorem (the Linear → Affine arrow
175+
becomes interesting once the modes differ on rule premises). *)
176+
177+
Lemma weaken_modality_le_id_linear :
178+
forall {R G e T R' G'} (H : has_type_l2 Linear R G e T R' G'),
179+
weaken_modality_le Linear_le_Linear H = H.
180+
Proof. reflexivity. Qed.
181+
182+
Lemma weaken_modality_le_id_affine :
183+
forall {R G e T R' G'} (H : has_type_l2 Affine R G e T R' G'),
184+
weaken_modality_le Affine_le_Affine H = H.
185+
Proof. reflexivity. Qed.
186+
187+
Lemma weaken_modality_le_strict_is_weaken_modality :
188+
forall {R G e T R' G'} (H : has_type_l2 Linear R G e T R' G'),
189+
weaken_modality_le Linear_le_Affine H = weaken_modality H.
190+
Proof. reflexivity. Qed.

‎formal/_CoqProject‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,5 @@ Semantics.v
1111
Semantics_L1.v
1212
Counterexample.v
1313
Echo.v
14+
Modality.v
15+
TypingL2.v

0 commit comments

Comments
 (0)