Conversation
When `case` or `elim` search for a redex, allows the reduction to unfold non-transparent operators. This does not affect tactics that does case/elim internally (e.g., />). fix #132
Second site of the bug fixed in f7bdd89: [find_existing_chain_entry] inside [add_generic_instance] compared chain-entry symbol maps by op-path head only. With a literal realisation ([op oner = 1]), [head_path (Fint 1) = None] caused it to falsely report "differs from the existing instance", so the chain re-registered a duplicate ancestor (e.g. [comring with int]). The duplicate broke downstream TC op resolution on the carrier. Fall back to [EcReduction.is_alpha_eq] when either side has no head path, mirroring the fix in [already_discharged].
Now that the [find_existing_chain_entry] regression is fixed (parent commit), [op idm = 0] and [op oner = 1] in [TcInt]'s [idomain] instance no longer break chain-instance reuse. Flip both bindings to the bare literals. Drop the trailing [!(mul0r, mulr0, addr0, mul1r, add0r)] from [test_polyM_at_0]: with literal realisations the [/=] simplifier fully reduces the coefficient computation to [true], so the explicit ring-lemma chain is no longer needed (and would fail on the closed goal).
Same cleanup as the TcInt flip in 94a9f43: now that the [same_symbols] chain-reuse bug is fixed at both sites, the real-carrier [idomain] instance can bind [idm] and [oner] to the bare literals [0%r] and [1%r] directly, dropping the [CoreReal.zero] / [CoreReal.one] indirection.
[tci_parents] holds the synthesised parent-instance paths (one per ancestor edge, used by the chain machinery to walk inheritance at witness-resolve time). The substitution that rebuilds a [tcinstance] during theory replay was substituting [tci_type], [tci_instance], and [tci_params] but leaving [tci_parents] alone — so a [clone include] of a theory that registered a TC chain instance produced cloned-in instances whose [tci_parents] still pointed at the source theory's local paths (e.g. [Top.ZModRing.addgroup_NNN]). Subsequent users (e.g. the field-instance refinement in TcZModP) then dereferenced those paths and failed with "unknown symbol". Map [forpath] over [tci_parents] like the other path fields.
Port of [theories/algebra/ZModP.ec] under the TC framework. The legacy file's three layers of redundancy collapse: - the private [theory ZModule] / [theory ComRing] (proved by hand) and the [clone Ring.ComRing as ZModpRing] + 12 [realize]s - the [clone Bigalg.BigComRing as BigZMod] - the AlgTactic [instance ring with zmod] all fold into a single [instance comring with zmod reducible] block backed by direct lemmas at top level of [ZModRing]. [ZModField] does [clone include ZModRing] for the [prime p] case and refines the carrier to [idomain] with one extra axiom ([mulf_eq0]). The [instance field with zmod] refinement step is deferred — it hits an EC infrastructure issue around chain symbol-map keying after theory-replay-introduced parent instances. The [idomain] level is enough for downstream consumers that don't need [invr]/[unitfP] beyond what comring's [choiceb]-backed inverse provides. Smoke test [TcZModPSmokeTest.ec] instantiates ZModRing at p := 5 and exercises [zmod_addrA], [zmod_mulrC], and [inzmod] coercion lemmas.
[Scope.add_instance] dispatches on the unqualified TC name. Three strings — [ring], [field], [bring] — were hardwired to the legacy [AlgTactic] handlers ([addring], [addfield]). With the tcalgebra port declaring [type class ring] and [type class field], those names collide: a user writing [instance field with zmod reducible proof unitfP by …] would be routed to [addfield], which then complains about the legacy AlgTactic op slots ([rzero], [rone], [add], [mul], [opp], [inv]) being missing. Resolve the ambiguity by checking whether the name in the [instance] declaration resolves to a typeclass in scope: if yes, dispatch to [add_generic_instance]; otherwise fall back to the legacy AlgTactic handler. This preserves the legacy code path for users of stdlib [Ring]/[Field] while letting the TC framework's own classes shadow the keywords when imported.
With the [add_instance] dispatcher fix in the parent commit, [instance field with zmod reducible proof unitfP by exact: unitE] is now correctly routed through [add_generic_instance] instead of the legacy [addfield] handler. Drop the TODO note and add a [ZModField] smoke-test slice that clones at [p := 5] and exercises [unitE].
Adds a comring-level lemma stating: if [unit x] and [x ^ k = oner], then [x ^ n = x ^ (n %% k)]. This is the natural setting for the result — it depends only on commutative-ring [exp] (with negative exponents handled via [invr] under [unit]) and on integer division, not on any specific carrier. The result was previously available only as a [zmod]-specific lemma inside the legacy [theories/algebra/ZModP.ec], proved via the zmod-only [exp_inzmod] coercion. Lifting it to comring lets every downstream consumer (notably TcZModField's Fermat-flavoured corollaries) inherit it without reproof. Adds [IntDiv] to the imports for [%%] and [divz_eq].
Ports the field-specific tail of legacy [theories/algebra/ZModP.ec] (lines 372–467): - [exp_mod]: zmod-flavour of the comring [exp_mod_unit] (precondition becomes [x <> zmod_zero] via [unitE]). - [exp_sub_p_1]: Fermat's little theorem at zmod — every unit raised to [p - 1] is one. - [exp_p]: Frobenius — [x ^ p = x] for every element (including 0). - [inv_exp_sub_p_2]: [invr x = x ^ (p - 2)] for units. Extends the smoke test with [test_exp_p_minus_1] and [test_exp_p] clones-at-[p := 5] checks. Notably, the proof of [exp_sub_p_1] still needs the [inzmod]-coercion trick (lift to [int]'s [exp], apply legacy [IntDiv.Fermat_little]) — that part is genuinely zmod-specific. But [exp_mod_unit] from TcRing lets [exp_mod] become a one-line corollary.
… realisation
Two matcher gaps surfaced by porting the legacy [theories/algebra/ZModP.ec]
[exp_p] / [inv_exp_sub_p_2] proofs:
1. [kmatch]'s alt-head check accepted only [EcPath.p_equal p p'] between
the pattern's key and the goal-head's TC-reduced path. In the
multi-parent-factory case where the goal's head is itself a TC op
reached via a renaming edge (e.g. [(+)<:zmod via mulmonoid>]
playing the role of comring's [( * )]), [tc_reduce] yields the same
concrete realisation as the pattern's class op would. Accept the
match when [tc_op_realised_by pat-key reduced-head] holds.
2. In [f_match_core]'s [try_delta] dispatcher, the delta-unfolding
branches for [Op.reducible] fired BEFORE the mathcomp-style branch
that would force-unify the carriers of a TC-op-vs-realisation pair.
This eagerly unfolded e.g. [zmod_mul] into [inzmod (asint x * asint y)]
and lost the chance to match the pattern's [(* )<:?t>] against the
concrete realisation. Reorder so mathcomp-style fires first, and
after carrier unification, also run [tc_reduce] on the pattern-side
so its now-pinned TC op call lines up with the goal's concrete op.
These let [rewrite mul1r] / [mulr1] / etc. succeed on goals like
[zmod_one * x = x] without the user adding manual [have ->] workarounds.
TcZModP's Fermat-flavoured corollaries are simplified accordingly.
TcRing's [exp_mod_unit] proof is also tightened (uses [{1}h] to limit
the divz_eq rewrite to the LHS).
With the matcher fix in the parent commit, [rewrite mul1r] / [mulr1]
fire correctly on goals like [zmod_one * x = x] (where [zmod_one] is
the reducible-folded realisation of [oner<:zmod>]). The TcZModP
Fermat-flavoured proofs that previously needed [have ->] workarounds
collapse to one-liners mirroring the legacy [theories/algebra/ZModP.ec]:
- [exp_p]: was 8 lines, now 5 (legacy: 4).
- [inv_exp_sub_p_2]: was 10 lines, now 5 (legacy: 6).
Also tightens [TcRing.exp_mod_unit]'s [divz_eq] rewrite to use [{1}h]
so only the LHS occurrence of [n] is decomposed.
…1] literals With Path A Phase 4 supporting arbitrary [sform] on instance op RHSs, the named anchors [zmod_zero = inzmod 0] and [zmod_one = inzmod 1] are redundant — bind the class slots [idm]/[oner] directly to [(inzmod 0)] / [(inzmod 1)] and state the structural lemmas (and consumers) in terms of those literals. Saves two [op] declarations and conceptually one layer of indirection; proofs are unchanged otherwise. The [zmod_zeroE] / [zmod_oneE] lemmas become [inzmod0E] / [inzmod1E] (renamed to reflect the absence of the intermediate named op).
[reducible] biases the printer toward the carrier-level realisation (e.g. [zmod_add x y] instead of [x + y]) and triggers aggressive unfolding under [/=]. For an abstract algebraic carrier like [zmod] the class notation is what users want to read; concrete unfolding should only happen on demand (via explicit [/idm], [/zmod_add], or named-lemma rewrites). Compare TcInt / TcReal where [reducible] makes sense because the carrier IS the concrete realisation ([idm = 0] is already what the user thinks of). [zmod] is one indirection away ([idm = inzmod 0]), and exposing that under [/=] is undesirable. The matcher still folds concrete <-> class via [tc_op_realised_by] so rewrites by class lemmas keep working.
Without these, [x + y] at [zmod] is ambiguous: zmod has two monoid instances (the addmonoid and mulmonoid-renamed views inherited via comring's multi-parent factory) and the resolver can't disambiguate the bare class op without surrounding op-name context. [Int.ec] and [Real.ec] solve this the same way — each declares its own [abbrev ( + ) = CoreInt.add] / [CoreReal.add] which shadows the class-level [+] for that carrier. Apply the same pattern at [zmod]: abbrev ( + ) (x y : zmod) : zmod = zmod_add x y. abbrev ( * ) (x y : zmod) : zmod = zmod_mul x y. abbrev [-] (x : zmod) : zmod = zmod_opp x. Smoke test extended with [test_addrC_infix] / [test_mulrC_infix] to confirm bare infix notation now resolves.
…ain synth)
Records the cumulative ancestor->leaf op renaming on each
chain-synthesised intermediate instance produced by
[add_generic_instance]'s chain loop. [None] for manually-declared
instances (legacy AlgTactic [addring]/[addfield], user-declared roots).
This is preparatory for the resolver fix: the field is populated at
registration time but not yet consulted by the resolver. Behaviour is
unchanged at this commit.
The field is environment-independent (just [(symbol * symbol) list]),
so [EcSubst.subst_tcinstance] and [EcTheoryReplay.replay_instance]
both propagate it unchanged. The latter uses [{ tci with ... }] which
already carries it through implicitly.
Follow-ups (deferred):
- The resolver's [strat_carrier_is_ambiguous] Tconstr-concrete branch
will filter [infer_all] candidates by [op_preserved] on this field
(next commit).
- The matcher's [kmatch_alt_head + tc_op_realised_by] approach
(commit a8bba55) and this new resolver path could be unified for
readability.
… tci_chain_rename The Tconstr-concrete branch of [strat_carrier_is_ambiguous] previously counted [infer_all] candidates blindly and declared >1 as ambiguous. For comring-derived concrete carriers this spuriously fires because [comring]'s multi-parent factory creates two [monoid] instances on the carrier — one via [addmonoid] (identity rename) and one via [mulmonoid] with rename [(+) := ( * ), idm := oner]. Both candidates match a query like [int : monoid], so the resolver gave up and deferred forever. Use the new [tci_chain_rename] field on each chain-synthesised intermediate to filter candidates: when the resolver knows the op name being queried ([pb_op]), drop any candidate whose chain rename clobbers that name. The mulmonoid-path monoid has rename [(+) -> ( * )] and is dropped for [pb_op = "+"]. Only the addmonoid view survives, ambiguity disappears, [strat_infer_by_carrier] commits a witness. [strat_infer_by_carrier] also rewired to take the first op-preserving candidate (instead of [EcTypeClass.infer]'s first-match) so the chosen witness agrees with the disambiguation. Effect: bare [x + y] at zmod and [idm<:zmod>] both resolve cleanly without needing carrier-specific abbrevs. The abbrevs are kept in TcZModP.ec anyway for parity with Int.ec/Real.ec, faster elaboration, and explicit printer behaviour, but they're now an optimisation/style choice rather than a correctness requirement. Tests added in TcZModPSmokeTest: [test_addrC_infix] / [test_mulrC_infix] exercise the bare class-op notation [x + y] / [x * y] at zmod with [apply addrC] / [apply mulrC]. Both rely on the resolver fix being correct even with the abbrevs present (the abbrev shadows [+] but not all uses).
Class declarations like [comring <: addgroup & (mulmonoid with idm = oner, (+) = ( * ))] no longer require redeclaring [oner] and [( * )] in the body. They are auto-imported from the renamed parent edge and promoted to first-class entries of [comring.tc_ops], producing the external [OP_TC] global at the current class's path. Body axioms elaborate against shared idents that the env-bind machinery rewrites to the global [Fop] reference. Non-renamed inherited ops are NOT promoted (they already exist globally under the ancestor's path and are reachable via the chain walk); they are also not bound as body-locals, so axioms reference them directly through the global namespace. New [tc_decl.tc_ops_origin] field tracks the canonical source [(ancestor_path, original_op_name)] for each [tc_ops] entry. Downstream classes consult it during auto-import to dedupe ops reached through multiple inheritance paths in the DAG (e.g. [boolring <: comring] seeing [oner] both via [comring.tc_ops] and via the direct [mulmonoid → monoid.idm] walk — same origin, silent merge). Different origins under the same local name = genuine collision, rejected with a request for an explicit rename. Cleanup: removed the now-redundant explicit [op oner] / [op ( * )] declarations from [comring] in examples/tcalgebra/TcRing.ec.
Extends [type class C <: P with ...] syntax to accept an optional [as Label] qualifier on each parent edge. Default label = bare class name. Threads the label through [tc_decl.tc_prts], [tcinstance]'s new [tci_chain_labels] field, and [EcTypeClass.ancestors_with_labels] (a label-aware variant of [ancestors_with_renaming]). No semantic change yet: the chain machinery records labels but the obligation collector still uses name-only dedup. Subsequent commits will use the label path to fix the dedup bug where two distinct obligations reaching the same name (e.g. [mopA] from addmonoid vs mulmonoid views) get silently merged. Uniqueness of labels at the same level is enforced at class-decl time (duplicate labels => error, force explicit [as] disambiguation). 13/13 tcalgebra files still pass.
Obligation collector (in [add_generic_instance]) now emits per (name, label-path) triples instead of name-only entries. Dedup across multiple paths happens only when the underlying form is alpha-equivalent (genuine diamond), not when names happen to collide (the latent bug where [mopA] of addmonoid view and [mopA] of mulmonoid view used to be silently merged). User proof syntax: [proof X<:L1/L2/...> by tac] qualifies the target obligation by a sub-path of the label chain. Bare [proof X by tac] still works when [X] is unambiguous by name; otherwise the user must disambiguate. Ambiguity = hard error. check_tci_axioms's input shape changes from (name, form) list to (name, labels, form) list and the user's [pti_axs] gains an optional label-qualifier list. 13/13 tcalgebra files still pass (no existing file relies on label disambiguation yet — the legacy machinery dedupes by name, which is still correct for current axiom-naming conventions).
[proof X<:L> by tac] should match any obligation whose path contains [L] as a contiguous subsequence (single-label = anywhere in the path), not just whose path ends with [L]. The suffix-only match was too restrictive for the common case where the user writes a single inner label like [<:addmonoid>] against an obligation reached via [["addgroup"; "addmonoid"; "monoid"]].
Two follow-ups to the labels-on-edges feature: 1. Parser: [as Label] now accepts lident (lowercase) labels, not only uident. This matches the default label convention (bare class name, which is lident-cased). 2. Revert the per-entry [subst] for obligation collection. The change to overlay per-chain-entry Flocal bindings was the right structural fix for the latent name-collision bug, but it changes semantics of bare [proof X by tac] clauses in ways that require the full TcMonoid neutralization migration to absorb. Without that migration in place, the per-entry subst makes existing tcalgebra instances ambiguous on [addmA] / [mulrA]. Restored the global [subst] with name-only dedup, plus a comment flagging the known unsoundness. The labels machinery (Phases 1-6) remains in place as the foundation for a future migration that moves all monoid lemma names to neutral forms.
Replaces three parallel parser rules for class bounds (in class declarations, type declarations, and op/lemma tparam signatures) with a single [tc_bound] rule that uniformly accepts: Class (Class as Label) (Class with X = Y, ...) (Class as Label with X = Y, ...) Adds a new [ptcbound] type in the parsetree and updates [ptyparam] and [PTYD_Abstract] to use it. Labels and renames on tparam bounds are parsed and stored but DROPPED at the typing layer for now (Phase A.1 will plumb them through into the tparam's recorded bounds). Adds a uniqueness check on bound labels for tparams (mirroring the class-declaration-level check): default label is the bare class name; duplicate labels at the same level are rejected with a request for an explicit [as Label] clause. Labels (both in tparam-bound [as Lbl] and proof-clause [<:Lbl>]) now accept any ident casing, not just lident.
Extends [tvars_app] type-arg-instantiation syntax to accept a trailing witness selector on each entry: X<:T> (* unchanged: no selector *) X<:T /Lbl1/Lbl2> (* label-based *) X<:T via Some.Path> (* path-based *) X<:T /Lbl via Path> (* combined (typer rejects irrelevant) *) Parsetree carries [pwitness_selector] per tvi entry; both unnamed/named forms support it. The typer currently drops the selector (Phase B will plumb it into [tcwitness] construction). New keyword [via] added to the lexer. All 12 existing tcalgebra files still pass.
[petyarg] gains a third field [witness_selector] carrying the user's [/Lbl+] / [via P] selector from the parsetree. [transtvi] translates parsetree selectors (resolving [via P] paths against the env) into [EcUnify.witness_selector] records. [opentvi]'s pattern-match destructures the new field but currently drops it (selectors have no semantic effect yet). The actual resolution of selectors to [tcwitness] values will land in a subsequent commit. 13/13 tcalgebra files still pass (sandbox.ec is pre-existing).
[UniEnv.opentvi] gains an optional [?env] parameter and a new [resolve_witness_selector] helper. When a tparam carries a non- empty selector, the helper picks a [TCIConcrete] witness: - [via P]: looks up instance P, verifies class and carrier match, returns the witness. - [/Lbl+]: enumerates env-level instances, filters by class ([tc.tc_name]), carrier ([ty_equal]), and label-path containment ([tci_chain_labels] contains the user's labels as a contiguous subsequence). Unique match required. - combined: requires both to agree on the same path. V1 limitations: - Concrete carriers only (uses [ty_equal], not unification). Parametric carriers ([Tvar 'a]) not yet handled. - Tparams with multiple bounds error out (per-bound selector syntax is future work). - Ring/Field instances rejected ([general] only). Errors raised as [UniEnv.InvalidSelector of string]; caller in [ecProofTerm] catches and re-raises as a [tc_error]. Verified end-to-end: at carrier [int] (which has both addmonoid and mulmonoid views of [monoid]), `apply (addmC<:int /addmonoid>)` and `apply (addmC<:int /mulmonoid>)` both work, with the latter correctly providing commutativity of ( * ) (proving [x*y = y*x]) instead of the additive default. All 12 working tcalgebra files still pass.
Extends [resolve_witness_selector] to handle abstract carriers:
- [Tvar id]: a type variable bound in the unienv (lookup via
[(!ue).ue_uc.tvtc]).
- [Tconstr p, _] where [p]'s tydecl is [\`Abstract tcs]: a
declared-abstract type (e.g. [declare type t <: comring]).
For both, the resolver BFS-walks the carrier's declared bounds
through their class chains, tracking (offset, lift_rev, label_path).
A match is an entry whose class equals [tc.tc_name] AND whose
label path contains the user's labels as a contiguous subsequence.
Unique match yields [TCIAbstract { support = `Var/`Abs; offset; lift }].
End-to-end verified:
section.
declare type t <: comring.
lemma p1 (x y : t) : x + y = y + x. proof. apply (addmC<:t /addmonoid>). qed.
lemma p2 (x y : t) : x * y = y * x. proof. apply (addmC<:t /mulmonoid>). qed.
end section.
[via P] still rejected on abstract carriers (paths only resolve to
concrete-carrier instances). [via]-on-abstract could be added later
if a use case arises.
Two refinements to the witness-selector resolver: 1. [select] in [select_op] catches [InvalidSelector] from [opentvi] and treats it as a candidate-rejection signal (raises [E.Failure]) rather than letting the anomaly bubble out. The error surfaces as a normal "no matching operator" if no candidate accepts the selector. 2. Concrete vs abstract dispatch: previously any [Tconstr p] with [tyd_type = `Abstract _] went to the abstract-search branch. But primitive types like [int] are declared abstract with an EMPTY bound list — they should be treated as concrete carriers. Fixed by requiring at least one bound to take the abstract path; empty-bound abstract types fall through to env-level instance lookup. Verified: selectors work on [int] (concrete), on [t <: comring] (declared-abstract with bounds), and (transitively) on type variables in op signatures.
Renames monoid's op to neutral [mop] and axioms to [mopA]/[mopC]/[mop0]. Section lemmas use [m] suffix ([mop0m], [mopCAm], etc.). [addmonoid] and [mulmonoid] rename ops via [(monoid with idm = zero, mop = (+))] and [(monoid with idm = oner, mop = ( * ))], with re-export section lemmas [addm*]/[mulm*] specialized to those subclasses. [comring] drops body axioms [mulrA]/[mulrC]/[mul1r]. They come for free through the [mulmonoid] chain; the comring section re-exports them under conventional names via [apply: mulm*]. Instance files (TcInt, TcReal, TcZModP, TcPoly) use labeled proof obligations: [proof mopA<:addmonoid> by ...] and [proof mopA<:mulmonoid> by ...]. Discharges both views distinctly. [src/ecScope.ml]: restore the per-entry obligation substitution fix (reverted in 03cb8f4). Now safe to land because the user can disambiguate via labels. [TcBigop]: parametric over [t <: monoid] using neutral [mop]. [local abbrev (+) = mop<:t>] (as a direct alias, NOT [fun x y => mop x y]) so partial applications [(+) x] keep their curried shape without introducing a [fun y => ...] lambda that would defeat rewrites. Status: 9/13 tcalgebra files pass. Four downstream (TcBigalg, TcBinomial, TcPoly, TcPolySmokeTest) fail with the same root cause: [zero<:t>] (the auto-promoted addmonoid op) and [idm<:t>] (monoid's op) have distinct global paths and the unifier doesn't see through [tc_reduce] when matching them. Manifests as [bigop_endo oppr0 opprD] failing because [oppr0]'s [-zero = zero] doesn't unify with [f idm = idm]. Tracked as follow-up; needs either unifier improvement or a redesign where renamed inherited ops are transparent aliases (like the original [abbrev zero] in TcMonoid) rather than fresh promoted ops. sandbox.ec is pre-existing failure unrelated to this migration.
When the rigid [Fop, Fop] match case encounters paths that differ but resolve to the same canonical TC origin (via [tc_ops_origin]), treat the ops as equivalent. The canonical origin is the path of the class where the op was originally introduced — followed through auto-import [tc_ops_origin] chains. Two ops match when: 1. They share an origin, AND 2. One's declared class is an ancestor (or descendant) of the other's — i.e., they sit on a single inheritance chain. The ancestor constraint distinguishes legitimate aliases ([monoid.idm] ↔ [addmonoid.zero], related by [addmonoid <: monoid] with the [idm = zero] rename) from sibling views that share an origin but are NOT equivalent ([addmonoid.(+)] vs [mulmonoid.( * )] — both auto-imported renamings of [monoid.mop], but [addmonoid] and [mulmonoid] are siblings, not ancestors). When paths differ but the ops are origin-equivalent, only the carrier types of the etyargs are unified (witness univars stay independent, since the tparam constraints differ — [<:monoid>] on one side, [<:addmonoid>] on the other; TC inference will resolve them through the appropriate chain view once carriers are pinned). New helpers in [EcEnv.Op]: - [tc_op_canonical_origin env p]: follows [tc_ops_origin]. - [tc_ops_same_origin env p1 p2]: origin + chain-relation check. Fixes TcBigalg.ec ([sumrN] via [big_endo oppr0 opprD] now works at section [t <: addgroup]: pattern [f idm = idm] matches subject [-zero = zero] because [monoid.idm] and [addmonoid.zero] are recognized as the same canonical op). 10/13 tcalgebra files now pass (was 9). TcPoly / TcBinomial / TcPolySmokeTest still fail on related but different bigop-at-poly issues.
Class declarations like [addmonoid <: (monoid with idm = zero, mop = (+))] no longer auto-import renamed inherited ops as new global OP_TCs. The rename clause is pure metadata; ergonomic local names ((+), zero, ( * ), oner) are wired up at the theory level via manual abbrev declarations that expand at typing time to the parent op (mop / idm). This makes class-decl renames symmetric with type-variable-constraint renames (which can never create ops) and eliminates the [Top.TcMonoid.+] vs [Top.TcMonoid.mop] duality that broke congr in TcBinomial and forced the same-origin scaffolding in the matcher. Resolver/SMT changes: - [match_tc_offsets] single-candidate guard ([ecUnify.ml]): with a single chain path, use it even when the rename clobbers the op name - the parent op is still accessible via that path. Without this [mop<:'a>] at ['a <: addmonoid] doesn't resolve. - [drop_tc_bounded_notation] removed from canonicalize: it preferred unbounded ops by name regardless of type, killing the new TC-bounded abbrevs. Real ambiguities (e.g. legacy Real.ec [(^)] vs TC [(^)]) are resolved at the user-code site (use [exp] in TcBinomial.binomial_r). - [tc_reduce_abstract_via_rename] removed entirely: it folded TC ops through rename edges to produce Fops at the renamed name. With renames now being abbreviations, the produced path resolves to an OB_nott that doesn't survive typing; the resulting Fop leaks an opaque why3 symbol into SMT tasks, breaking proofs like TcRing.expr_pred. - [head_op_after_tc_reduce] and the [tc_ops_same_origin] / [same_op] matcher clause removed (dead with the duality gone). Scope changes: - [inherited_tc_ops], [inherited_origins] always empty; body-local bindings for renamed inherited ops dropped (they'd leave dangling Flocals in axiom bodies otherwise). TcAlgebra changes: - TcMonoid.ec gains four abbrevs ((+) / zero / ( * ) / oner). - TcBinomial.binomial_r uses [exp] explicitly to pick the TC variant past the legacy Real.ec [(^) : real -> int -> real] abbrev. - TcPoly.ec instance proof tactic name updates. Batch: 11/11 examples/tcalgebra, 16/16 tests/tc.
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
3 participants
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.
No description provided.