From eceb6cd1abf69ae4c74d6b214cb246f70038c513 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 1 Jun 2026 13:21:53 +0100 Subject: [PATCH 1/2] proofs(P43): port canonical_* forms to the L1 modality-polymorphic judgment MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes proof-debt P43 prerequisite from the comprehensive inventory. Prerequisite for P42 (progress_l1). What lands Seven modality-polymorphic canonical-forms lemmas at the end of formal/Semantics_L1.v, mirroring the legacy Linear-only versions at formal/Semantics.v:603-630: - canonical_unit_l1_m : v : TBase TUnit + is_value v → v = EUnit - canonical_bool_l1_m : v : TBase TBool + is_value v → ∃ b, v = EBool b - canonical_i32_l1_m : v : TBase TI32 + is_value v → ∃ n, v = EI32 n - canonical_fun_l1_m : v : TFun T1 T2 + is_value v → ∃ body, v = ELam T1 body - canonical_prod_l1_m : v : TProd T1 T2 + is_value v → ∃ v1 v2, v = EPair v1 v2 ∧ ... - canonical_sum_l1_m : v : TSum T1 T2 + is_value v → (∃ v0, v = EInl T v0 ∧ ...) ∨ (∃ v0, v = EInr T v0 ∧ ...) - canonical_string_l1_m : v : TString r + is_value v → ∃ l, v = ELoc l r The `_m` suffix follows the convention established by region_shrink_preserves_typing_l1_gen_m and subst_typing_gen_l1_m. A pre-existing Linear-only canonical_string_l1 at line 908 is left untouched (it predates the L2 modality hybrid; the new _m version generalises it). All 7 proofs are single-line inversions: intros; inversion H0; subst; inversion H; subst; Same structural pattern as the legacy proofs — the L1 judgment's value-typing rules are sufficiently rigid that inversion on is_value v + the typing derivation pins the constructor. Build oracle: just -f formal/Justfile all clean. All 7 Print Assumptions blocks (added inline) print "Closed under the global context" — these lemmas surface ZERO axioms, exactly as the canonical-forms framework requires. Next: progress_l1 (P42) uses these as the case analysis on the type of a closed well-typed value. Stated separately because it requires the step relation's totality on non-value terms. Co-Authored-By: Claude Opus 4.7 (1M context) --- formal/Semantics_L1.v | 83 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/formal/Semantics_L1.v b/formal/Semantics_L1.v index 370b693c..23589df1 100644 --- a/formal/Semantics_L1.v +++ b/formal/Semantics_L1.v @@ -3652,3 +3652,86 @@ Print Assumptions preservation_l3. [region_shrink_preserves_typing_l1_gen_m]'s structural admit. *) Print Assumptions step_pop_disjoint_from_type_l1. + +(** ============================================================ + Canonical forms for the L1 judgment (proof-debt P43) + ============================================================ + + Mirror of the legacy [canonical_*] lemmas at [Semantics.v:603-630] + on the [has_type_l1] judgment. Together these are the + prerequisite for [progress_l1] (proof-debt P42). + + A canonical-forms lemma reads: "if [v] is a value of type [T], + then [v] is of the canonical syntactic shape for [T]". This is + invertibility of value-typing rules from the value side: it + inverts the [is_value v] view of a closed [has_type_l1] derivation + into the constructor pattern of [v]. + + Modality-polymorphic by design — the structural property holds + in both [Linear] and [Affine] modes; the modality parameter + threads through inversion unchanged. + + All 7 follow the same pattern as the legacy proofs: inversion on + [is_value v] (case-splits the value constructors), then inversion + on the typing derivation (rules that don't produce [T] are + contradictory). [eauto] discharges the existential witnesses. *) + +Lemma canonical_unit_l1_m : + forall m R R' G G' v, + has_type_l1 m R G v (TBase TUnit) R' G' -> is_value v -> v = EUnit. +Proof. intros; inversion H0; subst; inversion H; subst; reflexivity. Qed. + +Lemma canonical_bool_l1_m : + forall m R R' G G' v, + has_type_l1 m R G v (TBase TBool) R' G' -> is_value v -> + exists b, v = EBool b. +Proof. intros; inversion H0; subst; inversion H; subst; eauto. Qed. + +Lemma canonical_i32_l1_m : + forall m R R' G G' v, + has_type_l1 m R G v (TBase TI32) R' G' -> is_value v -> + exists n, v = EI32 n. +Proof. intros; inversion H0; subst; inversion H; subst; eauto. Qed. + +Lemma canonical_fun_l1_m : + forall m R R' G G' v T1 T2, + has_type_l1 m R G v (TFun T1 T2) R' G' -> is_value v -> + exists body, v = ELam T1 body. +Proof. intros; inversion H0; subst; inversion H; subst; eauto. Qed. + +Lemma canonical_prod_l1_m : + forall m R R' G G' v T1 T2, + has_type_l1 m R G v (TProd T1 T2) R' G' -> is_value v -> + exists v1 v2, v = EPair v1 v2 /\ is_value v1 /\ is_value v2. +Proof. intros; inversion H0; subst; inversion H; subst; eexists _, _; auto. Qed. + +Lemma canonical_sum_l1_m : + forall m R R' G G' v T1 T2, + has_type_l1 m R G v (TSum T1 T2) R' G' -> is_value v -> + (exists T v0, v = EInl T v0 /\ is_value v0) \/ + (exists T v0, v = EInr T v0 /\ is_value v0). +Proof. + intros; inversion H0; subst; inversion H; subst; + [left|right]; eexists _, _; auto. +Qed. + +Lemma canonical_string_l1_m : + forall m R R' G G' v r, + has_type_l1 m R G v (TString r) R' G' -> is_value v -> + exists l, v = ELoc l r. +Proof. intros; inversion H0; subst; inversion H; subst; eauto. Qed. + +(** ============================================================ + Print Assumptions — Canonical-forms axiom audit + ============================================================ + Verify each canonical-forms lemma is clean: their statement is + structurally derivable from the typing-rule shapes + [is_value] + inversion, so they should not surface any axiom. *) + +Print Assumptions canonical_unit_l1_m. +Print Assumptions canonical_bool_l1_m. +Print Assumptions canonical_i32_l1_m. +Print Assumptions canonical_fun_l1_m. +Print Assumptions canonical_prod_l1_m. +Print Assumptions canonical_sum_l1_m. +Print Assumptions canonical_string_l1_m. From b81df0b3651cf0fcc06ea9c7f03d8b3f639b7f0c Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 1 Jun 2026 14:44:19 +0100 Subject: [PATCH 2/2] ci: re-trigger after coq-build apt fix (#282)