Update the proofs of add_open_term_sound and related functions#22
Open
DIJamner wants to merge 42 commits into
Open
Update the proofs of add_open_term_sound and related functions#22DIJamner wants to merge 42 commits into
DIJamner wants to merge 42 commits into
Conversation
…ph_ok style Delete ~1500 lines of dead commented proofs in Tools/EGraph/Theorems.v that were phrased against the now-removed state_sound_for_model predicate and the missing primitive helpers (hash_entry_sound, alloc_opaque_sound, update_entry_sound, ssm_bind, etc.). Replace them with new vc-based statements using egraph_ok + egraph_sound_for_interpretation, matching the shape of rebuild_sound and force_equiv_sound. Add admitted Layer A primitive sound lemmas next to union_sound in Utils/EGraph/Semantics.v: alloc_opaque_sound, hash_entry_sound, update_entry_sound. These are what the new high-level statements depend on. Layer C status in Theorems.v: - add_open_sort_sound, add_open_term_sound: proven (delegations). - add_open_sound, add_open_sort'_sound, add_ctx_sound: admitted with proof sketches pointing at WfCutElim.wf_cut_ind, fuel induction, and wf_subst induction respectively. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Required for any proof of the freshness clauses (map.get i (fst res) = None and ~Sep.has_key (fst res) (parent (equiv e_in))). Derivation: from union_find_ok's next_upper_bound (lt k next for any key k), applied at k = next, gives lt next next; asymmetry then contradicts this for any hypothetical Sep.has_key next pa_in. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds a self-referencing fresh root to a forest: forest_extend: map.get r x = None -> forest l r -> forest (x :: l) (map.put r x x). Needed by the (still-pending) proof of alloc_opaque_sound to extend union_find_ok's forest invariant after UnionFind.alloc adds (next, next) to the parent map. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Discharge most of alloc_opaque_sound by: - Building union_find_ok for the extended forest via forest_extend + field-by-field forwarding (forest_closed for the rank_increasing case where pa_in ki = Some nx_in would force nx_in into pa_in's domain). - Preserving egraph_sound_for_interpretation's wf/exact/atom fields (db unchanged, parent only extended). - Discharging the trailing equality conjuncts and the new key facts. Remaining 4 admits inside the proof: - worklist_ok preservation (PER monotonicity for union_repair entries) - parents_ok preservation (PER monotonicity for atom_canonical_equiv) - atom_in_egraph_up_to_equiv preservation for args/ret - rel_interpretation (no new PER edges other than nx_in ~ nx_in, which is vacuously sound since map.get i nx_in = None) Also add (Hlts : forall x, lt x (idx_succ x)) and (Hltt : Transitive lt) preconditions for next_upper_bound and the rank/has_key monotonicity arguments. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Discharge all 4 of the inner admits in alloc_opaque_sound, completing its proof: - worklist_ok, parents_ok args, parents_ok ret: monotonicity of uf_rel_PER under the new singleton self-loop, via a new uf_rel_PER_alloc_monotone helper (any old PER edge transfers because the underlying parent_rel edge references map.get pa i = Some j with i in pa, hence i != nx, so the map.put doesn't shadow). - rel_interpretation: via a new uf_rel_PER_alloc_reflect helper that reflects the new PER back to either (nx, nx) or an old PER edge (using forest closure: pa cannot map any key to nx since nx isn't a key of pa). The (nx, nx) case is sound via the new Hdd precondition; the old case lifts the original soundness, using has_key facts to show neither i1 nor i2 is nx. Statement change: take (d : domain m) plus (domain_wf d, domain_eq d d) preconditions. The fresh id is interpreted as d. Callers (e.g. add_ctx_sound) pick d to match the intended Pyrosome variable. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add a structured TODO sketch inside the Admitted proof body. Discharging fully requires either a new db_set_sound primitive (for the None branch) or extracting from the existing update_entry_canonicalized_denote_iff. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
vc_bind db_lookup_pure to split the cases; structural intros to set up the Some r (union) and None (db_set) branches as separate admits with proof sketches. The full proof requires either a db_set_sound primitive or extraction from db_set_after_canonicalize_denote_iff. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Discharge the structural part of the fuel induction: - base (fuel=0) via Lia.lia on the vacuous length precondition - step: inversion Hsort gives In (n, sort_rule c' args) l1; lift to l via Hincl; rewrite the named_list_lookup match; apply add_open_sound's proj2 with (add_open_sort' fuel) as the inner sort handler and IHfuel (suitably composed via incl_tran + Lia.lia) as its soundness. Only the final hash_entry step remains admitted - needs hash_entry_sound (itself admitted) applied with out_d := inr (scon n s_t[/sub/]) and the interprets_to witness from interprets_to_sort + eq_sort_refl on the substituted sort. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Discharge the base case of the wf_subst induction (empty subst + ctx): list_Mfoldr ... [] [] reduces to ret [], so ctx_post holds with i_out := i_in (identity extension). Cons case still admitted - requires chaining four vc_binds over add_open_sort_sound, alloc_opaque_sound, hash_entry_sound, union_sound plus constructing the extended ctx_post. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Set up wf_cut_ind for the mutual induction. Discharge: - eq_sort conversion case: postcondition is independent of the sort, so the IH for any t applies to t'. - nil args case: list_Mmap on [] reduces to ret []; trivial. - partial var case: structurally produce the extending_sound envelope with i_out := i_in. Remaining inner admits: - con case: needs hash_entry_sound (admitted) + add_open_sort_inner_sound for the with_sorts=true branch + update_entry_sound (admitted). - var case completion: extract the interpretation of the lookup result via args_in_instance_in. - cons args case: vc_bind chain over IH_term and IH_args, then args_in_instance_cons. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… needed Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Discharge the var case inner admit by: - proving all_fresh of c, r, (with_names_from c s) from wf_ctx_all_fresh + NoDup_fresh + Hmaps + map_fst_with_names_from - using args_in_instance_in to recover the interpretation - proving the two named_list_lookup-from-In lemmas inline via induction + all_fresh (no suitable existing lemma) Two inner admits remain in add_open_sound: con case (with_sorts branch needs hash_entry_sound + update_entry_sound + add_open_sort_inner_sound) and cons args case (vc_bind chain + args_in_instance_cons). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Set up the cons args case with vc_bind through IH_term (head) and IH_args (tail). Two inner admits remain: the IH_args call needs the interpretation extended by the head step (requires args_in_instance_monotone-like reasoning), and the final ret needs to combine the two extending_sound envelopes + use args_in_instance_cons. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Discharge the cons args inner admit: - Apply IH_term to get i_head with extending_sound i e_in i_head and result interp v_head -> inl e_arg[/sub/]. - Apply IH_args under i_head (using args_in_instance_monotone to lift Hai). - Compose the two extending_sound envelopes (manual map.extends chaining + key-set monotonicity composition). - Use args_in_instance_cons for the final list extension. - Note: discharging the head's interpretation under i_final uses Hexti_final on the underlying map.get rather than option_relation. One inner admit remains in add_open_sound (the con case), plus the outer Admitted. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Inversion-via-wf_cut_ind gives (In (name, term_rule c' args t) l1, wf_args). Lift In to l via Hl1, derive lookup_err = Some, rewrite the match. Inner vc chain (list_Mmap via IH, hash_entry, optional sort_of annotation) still admitted - needs hash_entry_sound + update_entry_sound. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Move hash_entry_sound and update_entry_sound to after db_set_after_canonicalize_denote_iff so they can use the helpers get_analyses_preserves_fields etc. that are defined later in the file. Add db_set_sound stub: fresh-insertion variant of db_set_after_canonicalize_denote_iff with simpler preconditions (atom_sound_for_model, has_key on args/ret, no existing entry). Body has structured TODO sketch. Theorems.v builds clean (the imports are unchanged; only positions moved). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Decompose db_set into get_analyses + update_analyses + db_set'; extract field-preservation equalities at each step: - get_analyses preserves db, equiv, parents (via get_analyses_preserves_fields) - update_analyses preserves db, equiv, parents (only changes analyses) - db_set' preserves equiv, epoch, worklist Net result: equiv unchanged throughout (Heq_post_e_in), enabling trivial has_key preservation and PER lifting. db is updated only by db_set' insertion of the new atom. Remaining 'admit' covers the egraph_ok + sound conjuncts. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Has_key preservation is trivial since equiv is unchanged through the get_analyses + update_analyses + db_set' chain (Heq_post_e_in). Egraph_ok and egraph_sound conjuncts remain admitted with detailed sketches for each sub-field (equiv_ok, worklist_ok, parents_ok, db_idxs_in_equiv, idx_interpretation_wf, interpretation_exact, atom_interpretation, rel_interpretation). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ation Use Heq_post_e_in (equiv unchanged) to immediately discharge: - egraph_ok.equiv_ok (exists same roots from Hok) - egraph_sound.interpretation_exact (lift via rewrite) - egraph_sound.rel_interpretation (lift via rewrite) idx_interpretation_wf trivial from Hsound (i unchanged). Remaining 3 admits: worklist_ok (analysis_repair prefix + lifted entries), parents_ok (new atom in db + db preservation for old parents), atom_interpretation (new atom sound by precondition + old atoms preserved), db_idxs_in_equiv (new atom args/ret have has_key + old preserved). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
e_post.worklist = e_u.worklist = e_g.worklist; e_g.worklist = (analysis_repair entries) ++ e_in.worklist via get_analyses_worklist_extends. Each prefix entry is analysis_repair (trivially worklist_entry_ok), each lifted e_in entry is ok via Heq_post_e_in (equiv unchanged). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ation Establish: - Hkargs_post / Hkret_post: has_key facts for args/ret in e_post - Hain_a_post: the new atom is in e_post.db (via map.get_put_same) - Hain_post_split: every atom in e_post.db is either the new atom or an old e_u.db atom at a different key - Hain_a_uptopost: atom_in_egraph_up_to_equiv a e_post (reflexive) - Hlift: lift atom_in_egraph_up_to_equiv from e_in to e_post (inner admit on the case-split, to be filled) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three more sub-conjuncts proven, leaving only the inner Hlift case-split. parents_ok: use fold_left_cons_map_update_get to case-split each parent list entry into (v = a) or (v in old parents). First case uses Hain_a_uptopost; second uses Hparok + Hlift. db_idxs_in_equiv: case-split via Hain_post_split. New atom: args/ret has_key via Hkargs_post / Hkret_post. Old atom: Hdbkok + Hkeys. atom_interpretation: case-split. New atom is sound by Hatom_sound; old atoms preserved via Hi_atom. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
All 8 sub-conjuncts discharged: - egraph_ok: equiv_ok (Heq_post_e_in), worklist_ok (get_analyses_worklist_extends + Heq_post_e_in), parents_ok (fold_left_cons_map_update_get + Hain_a_uptopost + Hlift), db_idxs_in_equiv (Hain_post_split + Hkeys). - egraph_sound_for_interpretation: idx_interpretation_wf (i unchanged), interpretation_exact (Heq_post_e_in), atom_interpretation (Hain_post_split + Hatom_sound | Hi_atom), rel_interpretation (PER via Heq_post_e_in). - has_key preservation (Heq_post_e_in trivial). Key helper assertions: - Hain_a_post: the new atom is in e_post.db - Hain_post_split: every atom in e_post.db is either the new atom or an old atom from e_u.db at a different key - Hain_a_uptopost: atom_in_egraph_up_to_equiv a e_post (PER reflexive via parent_rel base + sym + trans on has_key keys) - Hlift: atom_in_egraph_up_to_equiv lifts e_in -> e_post (case-split on whether bb's key matches the new atom's key; contradiction via Hno_can in the match case) Now unlocks the path to hash_entry_sound + update_entry_sound, which in turn unlocks the 3 Layer C inner admits. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The None case (no existing entry for (a.fn, a.args)) reduces directly to db_set_sound: extract the no-existing-entry precondition from Hnone (db_lookup_pure's None postcondition gives this), apply db_set_sound. Some branch (union r (atom_ret a)) remains admitted. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Apply union_sound, decompose its postcondition into: - Hdb_eq: db preserved - Hroots: new union_find_ok - Hper: new PER = union_closure (old PER, (r, atom_ret a)) - Hpar_eq: parents preserved - Hwl_rel: union_worklist_rel - Hper_xr: r ~PER~ v_u in new equiv Prove Hkey_pres (parent map domain preserved by union via PER closure + uf_rel_PER_has_key + PER reflexivity on has_key keys). egraph_ok + egraph_sound on e_u' still admitted. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Both branches proven:
- None branch: directly applies db_set_sound (no existing entry).
- Some branch: applies union_sound; lifts to egraph_ok + sound:
* Hkey_pres: parent map domain preserved (PER reflexivity + uf_rel_PER_has_key).
* Hr_eq: eq_sound_for_model m i r (atom_ret a) via atom_sound_eq_ret
(using domain_wf = domain_eq d d to discharge all2 self-reflexivity).
* Hrel_new: PER induction over union_closure to lift soundness;
base cases for old PER (Hi_rel) and the new edge (Hr_eq); PER trans
and sym preserved via eq_sound_for_model_trans/Symmetric.
* Worklist preservation handles both same-worklist and new-union_repair
branches; the new entry's old_idx ~PER~ new_idx via v_old ~ r ~ atom_ret a ~ v_new.
* Parents preserved (db unchanged, PER monotone via Hper_lift).
* Db idxs in equiv preserved via Hkey_pres on args/ret.
Only hash_entry_sound remains Admitted in Semantics.v.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
vc_bind through list_Mmap_find_preserves_fields_strong (canonicalize args) then vc_bind through db_lookup_pure (look up f/args'). Case-split on the optional result: Some r (return r) vs None (alloc + db_set). Both cases admitted - structured TODO sketches for each step in place. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds two helper lemmas (fields_preserved_egraph_ok, fields_preserved_sound_for_interpretation) and one new primitive (alloc_sound, modeled on alloc_opaque_sound but without the analyses write). hash_entry_sound is now Qed: the Some branch uses atom_interpretation + interprets_to_functional to lift the canonicalized atom's recorded return to domain_eq with the supplied out_d; the None branch composes alloc_sound (fresh r) with db_set_sound (insert (f, args', r)) using i' := map.put i r out_d. Removes Semantics.v's last admit (Admitted on hash_entry_sound) and enables the three blocked inner admits in Theorems.v to be discharged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The three remaining inner admits in Theorems.v (add_open_sound con case, add_open_sort'_sound hash_entry step, add_ctx_sound cons case) are now unblocked: hash_entry_sound, db_set_sound, update_entry_sound, alloc_sound, alloc_opaque_sound, and union_sound are all Qed in Semantics.v. The comments reflect what the remaining work entails (vc_bind plumbing, interprets_to construction from rule witnesses, args_in_instance threading) and rough size estimates. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The proof skeleton (intros, args_in_instance extraction via iss_case, all2_lang_model_eq_inl' for the inl-list refinement, hash_entry_sound application, interprets_to_sort witness via sort_con_congruence) is now documented in the admit comment so subsequent work has a concrete 8-step recipe to follow. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Discharges the hash_entry step inner admit in add_open_sort'_sound by applying hash_entry_sound on (n, a_out), building the interprets_to witness via interprets_to_sort + sort_con_congruence + all2_model_eq_eq_args, and threading the resulting i' extension into the open_sort_post envelope. Key tactical details: - iss_case extracts dl from args_in_instance Hai_out - all2_lang_model_eq_inl' refines dl to map inl dl' - explicit section args needed for hash_entry_sound across the V/lang_model instantiation - explicit Eqb_ok V_Eqb position needed for sort_con_congruence and wf_args_subst_monotonicity - core_model_ok Hwf provides the Pyrosome-level Model_ok for eq_args_sym - lang_model_eq_PER l Hwf provides Symmetric for the all2 reversal Theorems.v admit count: 3 -> 2 (add_open_sound con case, add_ctx_sound cons case remain). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The con case's main obstacle is the with_sorts conditional inside add_open_term': for with_sorts=false the proof mirrors add_open_sort'_sound (now Qed); for with_sorts=true it must also discharge add_open_sort_inner_sound + update_entry_sound on the sort_of(x) atom. The comment documents the full recipe so the proof can be carried out as a follow-up. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Establishes the full hash_entry_sound chain (interprets_to_term via term_con_congruence, args_in_instance lift via all2_lang_model_eq_inl', key-set discharge via interpretation_exact, wf-ctx/wf-args lifts via the *_lang_monotonicity lemmas). The with_sorts=true branch is split out as a remaining inner admit; it composes add_open_sort_inner_sound with update_entry_sound on the sort_of(x_res) atom. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Interactively walked through the full primitive chain via rocq_check: add_open_sort_sound on t -> alloc_opaque_sound with d := inl e -> hash_entry_sound on sort_of [x'] with interprets_to_sort_of from H0 -> union_sound on (t_v, tx'). All hypothesis bookkeeping checks out (Hkey_tv_he via interpretation_exact, the wfd witness for inl e via eq_term_refl, etc.). Remaining work documented in comment: the post-union egraph_ok/sound bookkeeping (~150 lines), pattern from update_entry_sound's Some branch. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Discharges the final non-with_sorts admit in Theorems.v by completing the full primitive chain in the cons case of the wf_subst induction: 1. IHHsubst gives base' with map fst base' = map fst c' and args_in_instance for the tail. 2. add_open_sort_sound on t with sub=base' gives t_v with map.get i_sort t_v ≈ inr t[/with_names_from c' (map snd s)/]. 3. alloc_opaque_sound with d:=inl e produces fresh x' interpreted as inl e (wfd via eq_term_refl on H0). 4. hash_entry_sound on (sort_of, [x']) gives tx' with map.get i_he tx' ≈ inr t[/s/], using interprets_to_sort_of H0. 5. union_sound on (t_v, tx'). 6. Post-union bookkeeping: egraph_ok preservation across union via worklist/parents/db_idxs lifts using Hper_lift; sound_for_ interpretation via Heqs_tv_tx derived from both t_v and tx' interpreting to inr t[/s/] (with_names_from c' (map snd s) = s when map fst c' = map fst s, from wf_subst_dom_eq). 7. extending_sound chain: i ⊑ i_tail ⊑ i_sort ⊑ map.put i_sort x' (inl e) ⊑ i_he, with has_key preservation similarly. 8. args_in_instance via args_in_instance_cons: x' maps to (inl e) via the put, base' tail lifted via monotone. Theorems.v: 2 admits -> 1 admit (with_sorts=true branch of con case). add_open_sort_sound, add_open_term_sound, add_ctx_sound — all top-level lemmas fully Qed for with_sorts=false. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The with_sorts=true branch of add_open_sound's con case requires applying add_open_sort_inner_sound recursively on the rule's t_rule. The strict-decreasing-language precondition (length l2 < length l1) needs constructing l2 as a proper prefix of l1 where t_rule is wf — which requires a wf_lang_ext_split lemma not currently in the codebase. Document this blocker and the proof sketch in the admit comment. All other major lemmas are Qed: - Layer A (Semantics.v): 100% Qed - Layer C (Theorems.v): add_open_sort'_sound, add_open_sort_sound, add_open_term_sound, add_ctx_sound, plus add_open_sound (mutual) for var, cons args, nil args, eq_sort, con-with_sorts=false cases. Remaining: 1 inner admit (con-with_sorts=true), 1 outer Admitted (add_open_sound, mutual lemma) blocked on the inner admit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
wf_lang_ext_split: from In (n, r) l1 and wf_lang l1, extracts a smaller well-formed lpost (the tail-suffix of l1 after where the rule appears, length strictly less, with wf_rule lpost r and incl lpost l1). This unblocks the strict-decreasing-language precondition of add_open_sort_inner_sound when called recursively on a rule's body. Interactive verification of the with_sorts=true branch confirmed end-to-end that the chain works: wf_lang_ext_split extracts l_small, inversion gives wf_ctx l_small c'_rule + wf_sort l_small c'_rule t_rule, then add_open_sort_inner_sound applies cleanly to produce (t_v, e_sort) with map.get i_sort t_v ≈ inr t_rule[/subst/]. Then update_entry_sound for the sort_of(x_res) atom requires atom_sound_for_model with the witness constructor interprets_to_sort_of on a wf_term derivation — derived via (con name s'[/sub/]) being wf via wf_term_by + wf_term_subst_monotonicity chain, with eq_term_conv and term_sorts_eq handling sort coercion. The final closure of the with_sorts=true case is partially-written and working interactively up to the substitution composition step ((con name s')[/sub/] reduces to con name (s'[/sub/])). Documented as the sole remaining blocker. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Prove the with_sorts=true branch of the con case in add_open_sound by using wf_lang_ext_split to obtain a strictly-smaller language for add_open_sort_inner_sound, then chaining the sort sub-call with update_entry_sound on (sort_of, [x_res], t_v). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Extract reusable helpers (extending_sound_refl, extending_sound_trans, list_Mmap_get_has_some, args_in_instance_has_keys, option_relation_get_extends) and rewrite the three sound proofs to use them. Replaces 4-step nested extending_sound destructures with conjunctive intro patterns, collapses hand-written "all args have keys" induction into the helper, and chains extension layers via extending_sound_trans. Net: 151 lines removed, 123 added (~28 line reduction); add_open_sound 395 -> 343, add_open_sort'_sound 126 -> 97, add_ctx_sound 270 -> 263. Co-Authored-By: Claude Opus 4.7 (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.
Update the proofs of add_open_term_sound and related functions that add Pyrosome constructs to egraphs for the sake of rule compilation.