Proofs/l1 region countmap setoid#312
Merged
Merged
Conversation
…ation stage 1 Forks an L1-only region-environment carrier (region_env_l1 := region_name -> nat) away from the first-occurrence list, reasoned up to a pointwise-equality setoid (renv_eq) — axiom-free (no funext; Print Assumptions clean). Stage 1 of owner-selected route (C) for closing the L1 region-shrink admit: the list's remove_first_L1 pops a SPECIFIC list occurrence, so the admit needs list-structure agreement that no multiset transport provides (confirmed by the file's own design note + a coqc goal-dump; see L1-REGION-REFOUNDATION-PLAN.md REVISION/CORRECTION 2026-06-16). The count-map removes first-occurrence dependence by construction. Adds RegionEnvL1.v: carrier, renv_eq setoid (Equivalence), operations (cntL1/liveL1/enterL1/exitL1/emptyL1), coordinate lemmas, Proper instances. Keystone enter_exit_id (cntL1 r R >= 1 -> enterL1 r (exitL1 r R) =R= R) closes the cnt=1 corner of the admit; Print Assumptions: closed under global context. Stage 2 (migrate has_type_l1 onto the carrier + Proper-on-judgment) and ADMIT 2 restatement are follow-ups. No judgment migrated yet; nothing downstream changed; 4+1 admits unchanged; full project builds green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…no admit removed yet) Replaces the soundness SMELL of the false region_liveness_at_split_l1_gen (In rv R -> In rv R'; witness ERegion rv (EI32 5) at R=[rv]) with TRUE, axiom-free counterparts proven beside it (build green, Print Assumptions clean): - expr_no_exit_of_region rv e (honest side condition) - cnt_preserved_no_exit_l1_gen (Qed): no exit of rv => cnt rv invariant - region_liveness_no_exit_l1_gen (Qed): the honest In rv R -> In rv R' 13-site call-site audit (subst_typing_gen_l1_m): ALL 13 are class-3. The only local hypothesis is In rv R (outer); output_shape_at_l1 carries no region info; the no-exit side condition is not locally dischargeable (e1 is an opaque induction var). The obligation they smuggle IS the dangling-region / eliminator-fork problem: the 4 L1 admits are 4 faces of ONE region-liveness-through-reduction invariant. ADMIT 2 is NOT independently closable. Net: 4+1 admits UNCHANGED (false lemma retained, still used by 13 sites). Honest 4->3 path documented inline + plan doc: thread expr_no_exit_of_region through subst_typing_gen_l1_m, discharge the 13 sites via the TRUE lemma, delete the false lemma, relocate the obligation to preservation_l1 (capstone). Staged as a follow-on (signature change through a ~30-case induction). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…hine-checked, no admit closed) Minimal 2-segment EDrop(EVar j)/ERegion choreography experiment for the region-liveness eliminator fork. A 3-lens adversarial verify (wf_300a9737) sharpened the verdict: subject reduction RELOCATES region-liveness into a projection-coherence side condition (= expr_no_exit_of_region promoted to a foundational invariant) — it does NOT carry coherently. - formal/L1ChoreoExperiment.v: 5 Qed lemmas, axiom-free (Print Assumptions clean), wired into the build. EDrop(EVar j) is the wrong probe (reduces by S_Drop with R unchanged, never crosses S_Region_Exit; carried unconditionally). The only boundary-crossing term ERegion rv _ fails the relocated coherence condition (region_frame_breaks_no_exit). The apparatus-level obligation close_derives_coherence is named honestly (bare Definition, never proved) and proved incompatible with any inner same-region re-frame (close_derives_coherence_needs_no_inner_exit). - formal/L1-CHOREO-EXPERIMENT.md: the decisive finding + corrected next experiment — target the congruence cases (S_Let/App/Pair/Case Semantics_L1.v:3271-3284), NOT the already-Qed'd clean region exit. Routes for admits 1/2 (deterministic carrier refactor) vs 3/4 (choreographic) stay independent. Closes no admit, adds no axiom. Semantics_L1 admits unchanged (4); legacy preservation untouched (1). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ation — axiom-free
The general region_shrink statement was FALSE-as-stated: the witness
ERegion r (ERegion r EUnit) consumes two ambient copies of r (nested
T_Region_Active_L1) yet is expr_strictly_free_of_region r (that
predicate descends through ERegion unconditionally); it types at
[r;r] -> [] but not at remove_first r [r;r] = [r]. So the admitted
region_shrink_preserves_typing_l1_gen_m could never close.
Replace it with region_shrink_msperm: region-shrink holds whenever the
OUTPUT env is a multiset-permutation of the input. This threads through
every compound rule via the monotonicity squeeze (count_occ_le_l1_m in
both directions) — no list (order) equality needed, so the feared
list-vs-multiset wall never bites — and makes the T_Region_Active_L1
(+ _Echo) shadowed sub-case VACUOUS: an active region strictly drops
its r-count, so its output can never be a multiset-perm of its input.
region_shrink_{neutral,value} follow as axiom-free corollaries; the
value form (via value_R_G_preserving_l1) is exactly what the
preservation_l3 / S_Region_Exit call sites need.
- Semantics_L1.v: + multiset_perm + region_shrink_msperm (all 36 cases,
Qed) + region_shrink_{neutral,value}; rewire preservation_l3 and the
value wrapper region_shrink_preserves_typing_l1; remove the false
_gen_m / _gen lemmas; honesty pass on the status comments.
- Counterexample_RegionShrink.v (NEW): pins region_shrink_is_FALSE
(6 Qed lemmas) — the regression witness motivating the restriction.
Sibling to Counterexample.v / Counterexample_L2.v.
- _CoqProject: register Counterexample_RegionShrink.v.
Print Assumptions region_shrink_{msperm,neutral,value} = "Closed under
the global context". preservation_l3 is now UNCONDITIONALLY axiom-free.
Semantics_L1 admit inventory 4 -> 3 (region_liveness_at_split_l1_gen,
step_pop_disjoint_from_type_l1, preservation_l1 remain). Clean
from-scratch `make` green (15 files). Independently recompiled; validated
by four adversarial coqc probes.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Route C (count-map carrier migration) is moot: ADMIT 1 was closed via the multiset-perm generalisation (region_shrink_msperm, 0acd7d8) on the existing list carrier instead. Kept banner-marked SUPERSEDED as the record of the explored-and-abandoned migration design + the A'/_Eff decouple analysis. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes #
Type of change
How has this been verified?
Checklist
git commit -S).SPDX-License-Identifier(code/configMPL-2.0,prose
CC-BY-SA-4.0); I did not relicense existing files.Notes for reviewers