Conversation
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
…eleton Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
…aries) Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
Replace the `apply TODO` stub with a real, buildable development:
- the compiler is now written out explicitly on top of `trec_boundaries`
(the elaborated typerec term), because
`infer_compiler_simple_autoinj 4 target_multilanguage ...` produces an
empty `ttd` case and a hole-ridden `dtt` case; `dtt_case_wf`/`ttd_case_wf`
check the hand-written cases;
- one standalone `eq_term` lemma per boundary equation. 5 of 13 are Qed
("dtt True", "dtt False", "ttd True", "ttd False", "dtt ulambda
mismatch"); the 8 that need `"typerec func"`, the substitution
equations, or the two `star` equations are individually `Admitted` and
marked `(* ISSUE: see STATUS.md *)`;
- `simple_multilang_compiler_preserving` is `Admitted` with the same
marker; names and the `preserving_db` hint are unchanged so
PolyBoundaries.v / TyperecPartialEval.v still resolve.
"dtt star"/"ttd star" look genuinely false: the compiler turns
`#"dtt" #"*" "e"` into `app (ret (lambda #"*" (ret #"hd"))) "e"` with `"e"`
an expression variable, but STLC-beta only fires on a `#"ret" "v"`
argument, so the left side is a normal form distinct from `"e"`.
STATUS.md Stage F records the method, wall time and evidence for every
attempt and every equation.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
…to target Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
… exp_subst Source change (user decision), Boundaries.v: the "dtt func" rule's premise "v" : #"val" "G" #"*" is replaced by "e" : #"exp" (#"ext" "G" #"*") #"*" with #"ulambda" "e" substituted for "v" on both sides. With an arbitrary value the rule overlapped "dtt uT/uF mismatch", so the source proved #"Error" (#"->" "A" "B") = #"ret" (#"lambda" ...), which no compiler can preserve into a target whose #"Error" is inert. TrecTerms.v: trec_func_case_unelab is rewritten so that the two components of the #"pair" are literally the compiled images of the two boundary rules' right-hand sides (let-shaped), and the #".2" (dtt) component eagerly checks its untyped argument with #"bool?"/#"mif", erroring out on #"uT"/#"uF". trec_func_case_sort is unchanged. SimpleMultilangCompiler.v: the two #"exp_subst" equations are split into per-typerec-case leaves; star_case_subst and bool_case_subst are Qed (3s each), func_case_subst is the single remaining obstruction (TIMEOUT 900s). "ttd func" now terminates in 65s instead of saturating forever, but reports the sides unequal; it and the other four remain Admitted with ISSUE markers. Whole chain rebuilt green; STATUS.md updated (stages C, E, F, G). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
Replace the cut-free In-membership enumeration over whole languages (193s / 6.5GB for source_multilanguage, OOM at the 7GB ceiling) by a reflective inversion: turn In into a named_list_lookup_err equation via all_fresh, and bound the possible rule names with a forallb check discharged by vm_compute. Closed (all axiom-free): can_eliminate_typerec and ty_inversion_lemma_tml were Admitted, ty_inversion_lemma' and compiled_types_are_simple are re-proved. Whole-file build: 3m00s + OOM -> 2m21s, peak RSS 941MB. all_typerecs_simple is restated so its typerec case is selected by a boolean test on the head name (reducible at a variable name), and slightly strengthened. partial_eval_wf_in_no_typerec_lang gains the missing all_typerecs_simple hypothesis (the old statement was false) and a Qed corollary compiled_partial_eval_wf; it and partial_eval_preserves_equality stay Admitted, now for structural rather than resource reasons (see STATUS.md, stage H). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
…boundary compiler equations Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
…erec redesign Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
…dary equations SimpleMultilangCompiler.v, PolyBoundaries.v and TyperecPartialEval.v now all build against the value-level `typerec` / `boundary_cases` redesign, with no breakage in the compiler definitions, the case-wf lemmas or the equation statements. The redesign closes the two `#"exp_subst"` boundary equations in each of the two compilers (the three boundary cases are now the constants `bstar` / `bbool` / `bfunc`, whose substitution rules are one-step rewrites), taking both stages from 7 of 13 equations to 9 of 13. The four equations that need `"typerec func"` still time out at 900s. Root cause, newly diagnosed: `"typerec func"` instantiates the function case by a *type* substitution, and `boundary_cases` has no (and can have no) `"ty_subst bfunc"` rule that absorbs an instantiating type substitution, so the e-graph must unfold `"bfunc def"` and push `#"val_ty_subst"` through the whole `bfunc_body`. Both whole-compiler theorems therefore stay `Admitted`. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
…tions
TrecTerms.v: [#"bfunc"] now takes its instantiation as explicit arguments
(bfunc t1 t2 c1 c2 : val D G (P (-> t1 t2))) instead of living at
ty_ext (ty_ext D) with two bound type variables. New "ty_subst bfunc" rule
and a plain (non-g_lift) "val_subst bfunc"; "bfunc def" uses c1/c2 weakened
under the three intervening binders. [type_casing] is unchanged.
SimpleMultilangCompiler.v / PolyBoundaries.v: by_reduction_checked now uses a
forward-only reversibility filter. Together with the bfunc change this closes
"dtt uT mismatch" and "dtt uF mismatch" (~56s each) and makes every other
equation cheaper ("exp_subst dtt" 101s, controls 48s). 11 of the 13 boundary
equations are Qed in both files; "dtt func" / "ttd func" still do not saturate
(forward-only, TIMEOUT 1500s) and stay Admitted, so the two whole-compiler
theorems stay Admitted.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
"dtt func" / "ttd func" were not a shape mismatch: the e-graph's reduce-and-restart loop (egraph_reducing_equal) restarts saturation from the smallest extracted representative, and the rewrite these two equations need first, "typerec func", strictly grows the term, so it was discarded at every restart. Each equation is now eq_term_trans of two by_reduction_checked hops through an explicit intermediate (I1/J1, PI1/PJ1) in which the typerec at #"->" "A" "B" is already unfolded to #"bfunc" "A" "B" TREC[A] TREC[B]. All 13 boundary equations are Qed in both SimpleMultilangCompiler.v and PolyBoundaries.v, and simple_multilang_compiler_preserving / poly_multilang_compiler_preserving are assembled from them and Qed, both closed under the global context. Assembling also required fixing the order of the two compiler entries (the term rules of boundaries are dtt-before-ttd) and restating preserving_compiler_term with map fst c = cargs as an explicit premise (pct/ppct), since the constructor as stated cannot be applied. TyperecPartialEval.v rebuilt unchanged; eq_sort_sml_implies_eq_sort_tml is now closed under the global context, and compiled_partial_eval_wf depends only on the still-open partial_eval_wf_in_no_typerec_lang. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
Close partial_eval_preserves_equality (axiom-free) by proving the general target-language statement elim_typerec_eq, and fix two bugs in the partial evaluator that made the old statement false: meta_typerec dropped "sigma" (so elim_typerec of a closed term had a free variable), and its arrow case used a separately-elaborated copy of the "typerec func" RHS whose implicit environment arguments differ from the rule's, so no instance of the rule ever matched it. The arrow template is now read off the rule itself. is_simple_type is now indexed by the type environment (simple_type_at D mu), which the "typerec func" instance needs and which no sort-injectivity principle could recover. partial_eval_wf_in_no_typerec_lang remains Admitted; the sanctioned weakening partial_eval_wf_in_target is Qed. See STATUS.md for the residual goal (a conservativity statement for the conversion case). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
…ed conservativity
New Theory/Conservativity.v: general lemma eq_conservative_check, proved with
CutFreeInd.cut_ind — if a sublanguage keeps every rule of a language at a
closed stratum of sort names (decided by vm_compute), sort equality transfers
to the sublanguage for all sorts and term equality at stratum sorts.
Instantiated at {ty_env, env, ty, ty_sub} for target_multilanguage vs
target_multilanguage_without_typerec; together with typerec-freeness of the
partial evaluator's output this closes the last Admitted in the folder.
All theorems in Multilanguages are now Qed and closed under the global context.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
- Remove all Time/Timeout wrappers from proofs. - Replace by_reduction_checked/ctw_checked (e-graph run at tactic time and again at Qed) with by_reduction_fwd: standard Automation.by_reduction' with the forward-only rule filter, side goals by compute_term_wf; shared between SimpleMultilangCompiler and PolyBoundaries. Build times: SimpleMultilangCompiler 64 -> 41 min, PolyBoundaries 70 -> 47 min. - Delete dead code in TyperecPartialEval (superseded Derive block, unused Ltac cluster, commented-out old theorem, duplicate Utils lemma). - Rewrite session-diary comments as design documentation; add file headers. - Replace PLAN.md/STATUS.md session logs with README.md. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015rWXLHFoeqaD5qG7XtHm7A
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.
The LLM claims to have finished the multilanguage boundaries work. This PR needs human review.