Skip to content

proof(L1.F): discharge loc_retype_at_R_l1 axiom via region-liveness invariant#162

Merged
hyperpolymath merged 1 commit into
proof/l1-region-threading-designfrom
proof/l1f-region-liveness
May 27, 2026
Merged

proof(L1.F): discharge loc_retype_at_R_l1 axiom via region-liveness invariant#162
hyperpolymath merged 1 commit into
proof/l1-region-threading-designfrom
proof/l1f-region-liveness

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Replaces the unsound Axiom loc_retype_at_R_l1 in formal/Semantics_L1.v with:

  1. Lemma loc_retype_at_R_l1 — Qed-able; takes In r R_inner as a hypothesis. Pure consequence of T_Loc_L1. No axiom.
  2. Axiom region_liveness_at_split_l1 — narrower, well-formed axiom isolating the genuine structural property still owed by the L1 type system.

The old axiom typed ELoc l r : TString r at an ARBITRARY R_inner, which directly contradicts T_Loc_L1's In r R premise — it was strictly unsound.

What discharged directly (no axiom)

  • T_Lam_L1 case: body's R = outer R, so In rv R (Hregv) is exactly what T_Loc_L1 wants.
  • T_Region_L1 case: body's R = r :: R, so In rv (r :: R) follows from In rv R by right; exact Hregv.

What still needs the (narrower) axiom

Seven compound rules at nine call sites need In rv R1 where R1 is the threading output of the first sub-derivation:
T_StringConcat_L1, T_Let_L1, T_LetLin_L1, T_App_L1, T_Pair_L1, T_Case_L1 (×2), T_If_L1 (×2).

Each site now reads:

apply loc_retype_at_R_l1.
eapply region_liveness_at_split_l1; eassumption.

Why the narrower axiom isn't yet closeable

T_Var_Lin_L1 doesn't enforce In rv R at the use site of a TString rv variable, so adversarial L1 derivations exist where the threading pops rv from R1 via T_Region_Active_L1 with binder rv. The axiom would close after one of:

  • (a) Strengthen T_Var_Lin_L1 (and analogous consumers like T_Drop_L1) to require In r R for TString r-typed variables. The axiom then closes by routine structural induction.
  • (b) Add a no-region-pop-of-rv side condition to subst_typing_gen_l1, externalising the obligation to callers.
  • (c) Carry In rv R_intermediate through the substitution-lemma induction directly via a strengthened statement.

Documented in the file header (see the new section "Region-liveness invariant for L1 substitution").

Net effect

Before After
1 strictly UNSOUND axiom 1 sound axiom (narrower)
11 axiom call sites 9 axiom call sites + 2 direct discharges
Statement could prove False Statement captures a real, narrow obligation

subst_typing_gen_l1 and subst_preserves_typing_l1 still Qed. The 6 admits in preservation_l1 and 2 admits in region_shrink_preserves_typing_l1_gen are untouched (out of scope per task brief).

Test plan

  • coq_makefile -f _CoqProject -o Makefile && make is clean (verified locally on coqc 8.18.0)
  • Counterexample.v still compiles (bad_input_untypable_l1 unchanged)
  • grep -nE "^\s*admit\.|^Axiom |Admitted\." Semantics_L1.v shows: 6 admits + 2 Admitted (unchanged from parent branch) + 1 Axiom (the new narrower one)

Targets proof/l1-region-threading-design, NOT main.

🤖 Generated with Claude Code

…nvariant

Replaces the unsound [Axiom loc_retype_at_R_l1] (which typed [ELoc l r] at
ARBITRARY [R_inner], contradicting [T_Loc_L1]'s premise) with:

1. [Lemma loc_retype_at_R_l1] - Qed-able; requires [In r R_inner] as
   hypothesis. Pure consequence of [T_Loc_L1].

2. [Axiom region_liveness_at_split_l1] - narrower, well-formed axiom
   capturing the genuinely-missing structural property: in a sub-derivation
   [R; G |=L1 e1 : T1 -| R1; G'] with [In rv R], [In rv R1] holds.

Two compound-rule sites discharge directly with no axiom:
- T_Lam_L1: body's R = outer R, so [In rv R] (Hregv) suffices.
- T_Region_L1: body's R = [r :: R], so [In rv (r :: R)] follows trivially.

The remaining 9 sites (T_StringConcat / T_Let / T_LetLin / T_App / T_Pair /
T_Case x2 / T_If x2) invoke [region_liveness_at_split_l1] on Htype1 to
derive [In rv R1], then apply [Lemma loc_retype_at_R_l1].

Closure analysis (in file header): the residual axiom is genuinely
non-trivial because [T_Var_Lin_L1] doesn't enforce [In rv R] at the use
site of a [TString rv] variable, so adversarial derivations exist where
the threading pops [rv] from [R1] via [T_Region_Active_L1] with binder
[rv]. Three closure approaches documented:
- (a) Strengthen [T_Var_Lin_L1] and consumers to enforce region liveness
- (b) Add a "no-region-pop-of-rv" side condition to [subst_typing_gen_l1]
- (c) Carry [In rv R_intermediate] through the induction directly

All Qed unchanged (subst_typing_gen_l1, subst_preserves_typing_l1).
Counterexample.v still compiles. The 6 admits in preservation_l1 + the 2
in region_shrink_preserves_typing_l1_gen are untouched per task scope.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath merged commit 70054e4 into proof/l1-region-threading-design May 27, 2026
@hyperpolymath hyperpolymath deleted the proof/l1f-region-liveness branch May 27, 2026 00:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant