Conversation
Update the inline comment in TcRing.ec to reflect investigation findings: bugs #1 and #2 are fixed for concrete-carrier use cases (e.g. [bigA] / [bigM] on [int]), but section-internal proofs with a Tvar carrier and multi-parent inheritance hit a [TCIAbstract.lift] representation limit — the [lift] field is a single integer that can't disambiguate among multiple parent walks of different lengths to the same target ancestor TC. Practical effect: declaring a class as [comring <: addgroup & (mulmonoid with ...)] would WORK for [bigA]/[bigM] on concrete carriers but not for proofs of generic comring lemmas inside a section. Until the witness representation supports multi-parent walks (path-encoded lift), [comring] stays single-parent with multiplicative axioms re-stated.
Five framework pieces, fixing what the multi-parent factory port of
[Ring.ec] was hitting at every step, plus the resulting tcalgebra port.
[1] [tcwitness.lift : int list] (was [int])
Multi-parent inheritance reaches the same ancestor TC via different
parent walks; collapsing the path to a step count (single int) loses
which parent edge was taken at each step. [lift] is now a list of
parent-edge indices through the DAG. [resolve_lifted] in [ecEnv]
walks [tci_parents] step-by-step; [bind_uni] / [strip_lift] in the
unifier handle path suffixes (since [bump_lift] appends).
[2] Matcher η-reduction
[apply addmA] for [associative ((*)<:t>)] was failing with
[IncompleteInference] because the abbrev expansion of [(*)] gives
the goal as [Fquant(λ x y, (+) x y)] while the lemma is
[Fop((+))] — these match only via [is_conv], which silently
ignores etyargs on [Fapp] heads. Added [try_etared] in the
matcher's strategy list: when matching a bare [Fop p] against
[fun x y. h x y], η-reduce the lambda before recursing, restoring
structural [unify_etyarg] (which binds witnesses).
[3] Op-name-aware path filtering
[(+)<:comring>] where [comring <: addgroup & (mulmonoid with (+) =
(*))]: two paths reach [monoid], but only the addgroup walk leaves
[(+)] unrenamed. [with_lift] in [ecUnify] now returns paths paired
with the cumulative ancestor→child renaming; the op-typing site
(after [opentvi]) calls [disambiguate_op_witnesses], which filters
candidate paths by [op_preserved] on the op name and pins the
unique survivor. With this, the [comring] class declaration
(multi-parent factory) accepts [mulrDl : left_distributive (*)
(+)<:comring>] without ambiguity.
[4] Subsumption-based TC/concrete op-resolution filter
Old policy ("always prefer concrete over TC") silently picks
[Int.(+)] for [(+)] in [right_id zero<:t> (+)], causing
downstream type-unification to fail. New policy: drop a TC
candidate iff [tc_reduce] succeeds on the resolved carrier and
yields a head op already among the concrete candidates (the TC is
just an indirection), or if the carrier is concrete with no
applicable instance. Otherwise both candidates survive and the
typer's [MultipleOpMatch] retry uses surrounding context to
disambiguate. One existing test ([monoidtc.ec]) needed three
qualified references — the user-accepted trade-off.
[5] Tydef-witness substitution + chain pre-registration
[sb_tydef p ↦ (params, body)] couldn't carry the witness list for
[p]'s declared TCs, so substituting [`Abs p; offset; lift] just
rewrote the path mechanically — leaving the offset pointing at TC
slots [body] doesn't have. Widened to [(params, body, tcwitness
list)], symmetric with [sb_tyvar : etyarg]. The [`Abs] case of
[subst_tcw] now mirrors the [`Var] case via [bump_lift lift
tcs[offset]].
Then [add_generic_instance]:
- pre-computes all chain instance paths up front so the tydef
bindings can reference them as forward [TCIConcrete] witnesses
(the class body's [`Abs anc.tc_name; offset = 0] is a
self-reference to the to-be-registered instance);
- registers the chain in the env BEFORE [check_tci_axioms], so
the substituted obligation's concrete witnesses resolve
through the freshly-bound [tci_parents];
- auto-skips a chain entry's axioms when a previously-declared
instance for the same (TC name, carrier, op-symbols) triple
already proves them — matched against existing
[TcInstance.get_all] entries, excluding our own
just-registered chain. This lets [instance addmonoid with int]
succeed without re-stating [addmA / addmC / add0m] when
[instance monoid with int] is already on the books, and lets
[instance idomain with int] discharge by [smt()] alone instead
of leaving placeholder [int.\`1^N] obligations.
[tcalgebra port]
[examples/tcalgebra/TcRing.ec]: complete port of [theories/algebra/
Ring.ec]'s abstract hierarchy under TCs:
- addgroup (ZModule) full;
- comring (ComRing) full incl. exp/expr*, intmul × multiplication
(mulrnAl etc.), squaring, lreg/regularity, fracrDE;
- boolring, idomain, field, additive, multiplicative;
- top-level [(^)] abbrev for any comring carrier.
[examples/tcalgebra/TcInt.ec] (new): canonical [int] instance.
Single [instance idomain with int] declaration — synthesises every
ancestor in the chain, all axioms by [smt()] / [smt(@CoreInt)].
Plus the int-specific corollaries [intmul_int], [poddX], [oddX].
[examples/tcalgebra/sandbox.ec] (new): regression for the multi-
parent factory case — Tvar carrier with a factory-renamed
mulmonoid parent, [apply addmA / addmC / add0m] on
[associative (*)<:t>] / [commutative (*)<:t>] /
[left_id one<:t> (*)<:t>].
[Regression]: stdlib + examples — no new failures (the two pre-
existing baseline failures, [DynMatrix.eca] and [qselect.ec],
unchanged).
[Known limitation, not addressed here]: [ecTheoryReplay]'s
[Inline] mode for [type t <: tc] clones still passes [] for the
witness list. Stdlib doesn't trigger it; left as a [FIXME:TC].
The [Inline] mode of clone replay (`ecTheoryReplay`) was passing [] as the witness slot when registering [add_tydef t_path → (params, body)]. This was the FIXME left in the previous commit — symmetric with the hole that [add_generic_instance] needed: when the cloned source is [type t <: tc1 <: tc2 …] and the user substitutes [t <- body], witnesses for [`Abs t_path; offset = i; lift] inside cloned axioms need a [tcwitness] entry per declared TC of [otyd], looked up against [body]'s view in the instance database. Without them the substitution just renames the path and leaves the offset pointing at TC slots [body] doesn't have. [ecTypeClass]: new [witnesses_for_body env body tcs] — calls [infer] per tc; on lookup failure, falls back to a [`Abs body_path] / [`Var a] placeholder, preserving the pre-fix shape for cases that worked by accident before. Non-failing on purpose so the change is backward-compatible. [ecTheoryReplay] (`Inline` arm): when [otyd.tyd_type] is [`Abstract tcs], call [witnesses_for_body env body tcs] and feed the result into [add_tydef]. For non-TC clones (the stdlib case) [tcs = []] and the result is [], so no behavioural change there. Smoke test: cloning [type t <: addgroup] with [t <- int] now resolves inherited lemmas through int's registered addgroup instance — the substitution lands on concrete [int] / [CoreInt.add] / [CoreInt.opp] rather than opaque [int.\`1^N] ghosts. [Regression]: stdlib + examples, no new failures (the two pre-existing baseline failures unchanged).
The [TcMonoid] hierarchy ships generic notation abbrevs like abbrev ( * ) ['a <: mulmonoid] (x y : 'a) = (+)<:'a> x y that, applied at a [comring] carrier, expand to the same [Fop] as [comring]'s own [( * )] TC operator. Inside the defining file's scope, [by_current] drops the abbrev (different prefix); but in external clients the two compete and [select_op] reports [MultipleOpMatch]. Add a new [drop_shadowed_notation] filter: drop OB_nott candidates whose basename matches a TC-op (OB_oper (Some (OP_TC _))) candidate's. Run AFTER [drop_subsumed_tc] so the abbrev survives when the TC candidate has just been eliminated (e.g. concrete carrier with no registered instance — [Int.( <= )] vs the new [tcrealdomain.( <= )]). While here, also dereference the carrier through the candidate's per-call [subue] inside [drop_subsumed_tc]'s [carrier_is_concrete] check — at filter time the [etyargs] field still holds the pre-unification [Tunivar] even after [select_op] bound it to something concrete via [unify env subue top texpected]. [Regression]: stdlib + examples — no new failures.
Mirrors [theories/algebra/Number.ec:RealDomain] as a TC class: [tcrealdomain <: idomain] with the 5 ordering/norm ops ([|.|], [(<=)], [(<)], [minr], [maxr]) and 10 axioms ([ler_norm_add], [addr_gt0], [norm_eq0], [ger_leVge], [normrM], [ler_def], [ltr_def], [real_axiom], [minrE], [maxrE]). The two helper preds [homo2] / [mono2] and the [mono2W] / [monoLR] / [monoRL] lemmas from the [Number.ec] preamble are ported verbatim — they're TC-free. Phase 2 — porting the ~280 [RealDomain] derived lemmas — left as TODO. Initial smoke testing showed the original proof scripts make rewrite-pattern assumptions ([!mulr1] expecting both [_ * oner] and [oner * _] occurrences, etc.) that interact with the TC abstraction differently from the [clone include Ring.IDomain] form. Each batch will need targeted review. [ger0_def], [subr_ge0], [oppr_ge0] are ported as a Phase-2 starter (3-line proofs, no rewrite-pattern surprises).
Framework changes driven by completing the algebra port through [examples/tcalgebra/TcBigalg.ec]: * [src/ecTcCanonical.ml] (new): per-(carrier_tcs) canonical-paths table via BFS-first walk through the parent DAG. Used as the source of truth for abstract-witness canonical encodings. * [src/ecCoreEqTest.ml] for_tcw and [src/ecUnify.ml] unify_tcw's structural fallback canonicalise both sides — the convertibility layer for tcwitnesses, analogous to type-alias unfolding inside for_type. * [src/ecEnv.ml] new tc_reduce_abstract_via_rename: walks a TCIAbstract witness's lift, finds a parent edge that renames the requested op, returns the renamed class op with the truncated witness. Plumbed through tc_reducible / tc_reduce so factory renames fire on abstract carriers (not just concrete instances). * [src/ecMatching.ml] try_delta gains two clauses for tc_reducible ops, calling new doit_tc_reduce — so f_match_core unfolds rename-equivalent heads during apply / pf_form_match. * [src/ecProofTerm.ml] kmatch in pf_find_occurence accepts heads that tc_reduce to the pattern's key path — needed because rewrite's keyed pre-filter would otherwise drop rename-equivalent positions before pf_form_match runs. * [src/ecTyping.ml] carrier_is_concrete refined: Abstract _ → Abstract (_ :: _), so primitive types like int (Abstract []) are classified as concrete and drop_subsumed_tc can dedup TC ops against non-TC alternatives. New drop_tc_bounded_notation filter: drops a notation whose tparams have non-empty TC bounds when a same-basename non-TC-bounded alternative is also a candidate. * [src/ecScope.ml] add_generic_instance gains a diamond coherence check: when an existing instance for the same (anc, ty) is in scope, the new chain entry's symbol map must agree on every op, else hierror with both decl sites. * [src/ecUnify.ml] match_tc_offset returns the canonical (offset, lift) via the new table; bind_uni reverts to plain structural suffix-strip (no class-validation / canonical-bind workarounds needed once paths are canonical). Algebra port: * [examples/tcalgebra/TcRing.ec] adds Additive / Multiplicative morphism predicates and helper sections. * [examples/tcalgebra/TcNumber.ec] tcrealfield as a multi-parent factory class, full RealDomain port, normr0_eq0, canonical int : tcrealdomain instance directly in this file. * [examples/tcalgebra/TcBigop.ec] adds bigiA / bigiM range-indexed flavor abbrevs. * [examples/tcalgebra/TcInt.ec] intmul_int → intmulz. * [examples/tcalgebra/TcBigalg.ec] (new): port of Bigalg.ec — BigZModule, BigComRing.BAdd, BigOrder. 36/37 lemmas with original proofs; only divr_suml deferred (field-only). Test: [tests/tc-ko/diamond-coherence.ec] exercises the instance-time coherence error path.
[divr_suml] is in [BigComRing.BAdd] (the additive view of comring), not field — [(/) (x y : t)] on a comring abbreviates [x * invr y] and is already declared at TcRing.ec:236. Original proof replays verbatim. Bigalg port now lemma-complete (37/37).
[subtype X = { x : T | P x }] declared inside [section. declare type
c <: ...] previously stayed monomorphic at section close — [poly] in
[Subtype]-cloned form was bound with [tyd_params = []], so even
though the cloned auto-axioms ([to_polyN], [of_polyP], etc.) and
the [to_poly]/[of_poly] ops correctly gained a [c] tparam, [poly]
itself didn't. The result was an inconsistent state where the
operations were polymorphic over [c] but returned a single shared
[poly] type for all carriers — a soundness gap flagged by the
[FIXME:SUBTYPE] marker at [add_subtype].
This patch threads the carrier and predicate of the subtype through
the type declaration so [tydecl_fv] picks up their dependency on
section-declared free types, and the existing
[generalize_tydecl] machinery adds the right tparams at close.
[ecDecl.{ml,mli}]: add [tyd_subtype : (ty * form) option] to
[tydecl]. [None] for non-subtype declarations.
[ecScope.ml] [add_subtype]: compute carrier+pred before [bind] and
populate [tyd_subtype = Some (carrier, pred)] on the placeholder.
[ecSection.ml] [tydecl_fv]: union in the carrier+pred fv when the
field is set, so [generalize_tydecl] sees the section-declared
types the subtype depends on. [generalize_tydecl] preserves the
field on the produced [Th_type].
[ecSubst.ml] [subst_tydecl]: substitute through the carrier and
predicate when present.
Other [tydecl] builders ([ecHiInductive], [ecTheoryReplay], the
class-stub builder in [ecScope]) are updated to set the new field
to [None]. After this, [subtype poly = { p : int -> c | ispoly p }]
inside a [section. declare type c <: comring.] generalises to
[type 'c poly] at close, and the cloned ops/axioms type-check
consistently against [poly<:'c>].
Three fixes in [add_generic_instance] that together let [instance C with ['a <: D] (T 'a)] (parametric carrier) coexist with intermediate registrations on the same carrier. 1. [symbols_of_tc] no longer freshens tparams. The ops it returns are later resolved against a unienv seeded with the instance's original tparams, so freshening produced [c_fresh] in the expected type but [c_orig] in the resolved op — printing identically as ['a] but rejected by [EqTest.for_type]. Build the substitution binding each tparam to itself with abstract TC witnesses on the original ident. 2. Proof obligations carry the instance's tparams. [check_tci_axioms] now takes [?tparams], threaded from [add_generic_instance] as [fst ty]; the synthesised [ax] for each axiom inherits them instead of [[]], so the obligation can be discharged in a context where the carrier tparam is in scope. 3. Self-witness etyargs match the registered instance. For a chain entry registered with the user's tparams, the [TCIConcrete] self-witness must re-apply those tparams as etyargs (each carrying abstract TC witnesses) — not [], or [tc_reduce] hits a [tci_params]/[etyargs] length mismatch when the witness is later consulted. 4. Chain-entry reuse. [add_generic_instance] previously allocated a fresh path for every ancestor in the chain, which would silently register a duplicate instance when an intermediate ancestor was already in scope (e.g. registering [comring] on a carrier already bound at [addgroup] would create a second addgroup instance, diverging witnesses and violating one-canonical-instance-per- (class, carrier)). [find_existing_chain_entry] now looks up an existing matching instance ((tc_name, carrier, op-symbols) all agree); if found, the chain entry's path is reused and no re-registration happens. [chain_self_paths] is filtered to freshly-allocated paths so [already_discharged] still recognises the reused instance as the discharger of the corresponding axioms. Validates on the existing tcalgebra suite (TcMonoid/TcRing/TcInt/ TcBigop/TcBigalg/TcNumber/TcPoly) and unblocks parametric polynomial instances over [comring] coefficients.
Port [theories/algebra/Poly.ec:PolyComRing] (lines 1-516) to the TC
framework as a parametric instance over a [comring] coefficient.
Key structural difference from the original: instead of cloning
[Ring.ZModule] then [Ring.ComRing] in two phases (and re-cloning
[Bigop]/[Bigalg] inside each), we declare a single [comring with
['c <: comring] ('c poly)] instance. Once registered, every TcBigA
/ TcBigZModule / TcBigComRing lemma polymorphic over the relevant
class applies at carrier ['c poly] with no further cloning. The
chain-entry reuse fix in [ecScope.ml] makes the explicit Phase-3
[addgroup] declaration coexist with the Phase-5 [comring] one (no
duplicate registration).
[unit] / [invr] follow the [Ring.ec:ComRingDflInv] pattern:
[poly_unit p := exists q, q * p = poly_one] and
[poly_invr p := choiceb (fun q => q * p = poly_one) p]. The three
obligations [mulVr] / [unitP] / [unitout] discharge from
[choicebP] / [choiceb_dfl] alone — no ring axioms needed. The
structural "constant with invertible coefficient" characterisation
only holds when [c : idomain] (deg multiplicativity requires no
zero divisors); that bridge will live in a future idomain phase
as a separate [unitE]/[polyVE] equivalence.
Phases covered:
- Phase 1: [poly] subtype + [deg] / [_.[_]] / [lc].
- Phase 2: [polyC] / [polyXn] / [polyD] / [polyN] / [polyM] / [polyZ]
constructors, [ispoly] closure lemmas, coefficient formulas
([coeffE], [polyME], [polyMXE], [polyZE]), scaling ([scale*p]).
- Phase 3: [addgroup with ['c <: comring] ('c poly)].
- Phase 4: [polyM_mulrA] / [mulrC] / [mul1r] / [mulrDl] / [oner_neq0]
via the standard bigop expansion of [polyM]'s convolution.
- Phase 5: [comring with ['c <: comring] ('c poly)] with choiceb
defaults for [unit]/[invr].
Higher-level theory (mul_lc, deg arithmetic, evaluation, polyXn
exponents — Poly.ec lines 522-847) and the idomain extension
(Poly.ec lines 855+) are deferred to follow-up commits.
Port of [theories/algebra/Poly.ec] lines 296-415 into a fresh section over [c <: comring]: [degC] / [degC_le] / [lcC] / [lc0] / [lc1] / [deg0] / [deg1] / [deg_eq0] / [degX] / [nz_polyX] / [lcX] / [deg_ge1] / [deg_gt0] / [deg_eq1] / [lc_eq0]; [degN] / [lcN] / [degD] / [degB] / [degDl] / [lcDl] / [degDr] / [lcDr]. Most proofs port verbatim. Three places need adaptation: - [lc_eq0] [argmin_min] precondition discharged manually (the [smt()] in the original was opaque to the TC-elaborated form). - [degDr] / [lcDr] use [polyD_addrC<:c>] explicitly, since inferring the [addgroup] witness for [c poly] from a bare [addrC] in this section did not resolve. - [lcDr]'s premise typo in the original ([deg q < deg p] in both the goal and conclusion-by-symmetry) is corrected to [deg p < deg q]; the conclusion becomes [lc q] (mirroring [degDr]).
[EcTypeClass.infer] previously consulted only the registered instance database, so its recursion in [check_tcinstance] (when matching a parametric instance, line 144) could not discharge a tparam constraint whose carrier was a section-declared abstract type. Concretely: section. declare type c <: comring. lemma _ (a b : c) : a + b = b + a. proof. apply (addrC<:c> a b). qed. failed with "type c does not satisfy typeclass constraint addgroup", because [check_constraints]' fallback to [abs_satisfies] is only a yes/no check and is not propagated through the recursive [infer] call inside parametric-instance matching. [EcUnify] handled this case via [strat_abs_via_decl] (Mode #6) in its strategy dispatch, but [EcTypeClass.infer] is called from several other paths (proof-term TVI elaboration, theory-replay, reduction) that don't go through the unifier dispatch. This adds [infer_via_abs_decl] alongside [check_tcinstance] and makes [infer] fall back to it after the instance-database search. The fallback walks [tcs] (the carrier's declared class bounds) looking for one whose ancestor DAG reaches [tc], and produces a [TCIAbstract { support = `Abs p; offset; lift }] witness — same shape as Mode #6 in [EcUnify]. Validates: the suite (TcMonoid/TcRing/TcInt/TcBigop/TcBigalg/ TcNumber/TcPoly) passes unchanged; new test [apply (addrC<:c> a b)] inside [section ; declare type c <: comring] now succeeds. Note: this fix completes constraint resolution for non- parametric Path B uses (e.g. [addrC<:c>]). The parametric case [addrC<:c poly>] now passes constraint resolution but the proof-term and goal witness encodings can still mismatch (the unifier produces a [TCIUni] with [lift] that doesn't always collapse to the goal's resolved form). That's a separate issue, untouched by this commit.
Chain-entry reuse (commit fdb522c) used [EcReduction.EqTest.for_type] to compare carrier types, which requires ident-equality on tparams. But existing parametric-carrier instances have their tparams freshly generated at registration time with new [EcIdent] uids, so a later [instance C with ['c <: D] (T 'c)] declaration whose own [c] has a different uid would fail to match the existing instance — and the chain synth would create a duplicate registration. Concrete failure mode: declaring [instance addgroup with ['c <: comring] ('c poly)] then [instance comring with ['c <: comring] ('c poly)] produced two distinct [addgroup] instances on [poly], because the two ['c]s had different idents. [infer_all] then returned 2 matches, [strat_carrier_is_ambiguous] flagged the resolution as ambiguous, and the [TcCtt] constraint stayed deferred. Fix: compare carriers via [EcTypeClass.ty_match] with the existing instance's tparams as pattern variables. This is alpha-equivalent matching — ['c poly] (existing) matches ['c poly] (new) regardless of the tparam idents. Exports [ty_match] and [NoMatch] from [ecTypeClass] for use here. Validates: tcalgebra suite (TcMonoid/TcRing/TcInt/TcBigop/TcBigalg/ TcNumber/TcPoly) passes; reproducer's [INFER_ALL: tc=addgroup -> 2 match] is now gone. Note: the parametric Path B (e.g. [apply (addrC<:c poly> p q)]) still fails because the unifier's [TcCtt] resolution doesn't reach the proof-term print — the [TCIUni] placeholder is committed in the resolution map but the [tw_assubst] used by [concretize_env] doesn't seem to follow it. That's a separate, deeper issue.
Port [theories/algebra/Poly.ec] lines 522-589 (multiplicative degree on poly): [mul_lc] / [degM_le] / [degM_proper] / [lcM_proper] / [degZ_le] / [degZ_lreg] / [lcZ_lreg]. Most proofs port verbatim. Adaptations: - [mul_lc]'s [poly0] base cases use the structural [polyM_mul0r] / [polyM_mulrC] / [poly0E] chain instead of the original's [!(mul0r, poly0E)] (which relied on the polyComRing clone having [poly] under the comring [( * )] so [mul0r] applied at the poly carrier — Path B in the TC port, currently routed through structural lemmas). - [degM_proper] proof restructured to derive the lower bound via forward [have] reasoning instead of the original's [eqz_leq + split + bracket-or].
Port [Poly.ec] lines 600-669: [polyCX] / [degXn_le] / [degXn_proper] / [lcXn_proper] / [deg_polyXn] / [lc_polyXn] / [deg_polyXnDC] / [lc_polyXnDC] / [polyXnE] / [lreg_lc]. These lemmas use [exp p i] at carrier [c poly] (via the comring instance), exercising the parametric-Path-B path in the elaborator. With the [infer-via-abs-decl] (commit 0dd7d21) and chain-reuse alpha-match (commit c182895) fixes, lemma statements typecheck; proof bodies rely on structural lemmas ([polyM_mulrC] in [polyXnE] instead of original's [PolyComRing.mulrC]) where Path-B-via-class-lemma would fail. [degXn_le]'s [(IntID.addrC 1)] in the original uses the integer [addrC] from the cloned [IntID]; the TC port uses [addzC 1] (the TcInt analogue) directly.
Port [Poly.ec] lines 681-720 (the [BigPoly] block contents): [polysumE] / [polyE] / [polywE] / [deg_sum]. The original had [theory BigPoly. clone include BigComRing with theory CR <- PolyComRing. ... end BigPoly] re-exporting BigA/BigM on poly under names PCA/PCM. The TC port skips that scaffolding — [bigA<:c poly>] resolves directly through the registered comring instance. Replaces [PCA.big] -> [bigA] / [bigi] throughout. Single workaround: [polywE]'s tail [rewrite addr0] hits the parametric Path-B (addr0 = [forall 't <: addmonoid (x : 't), x + idm = x] applied at carrier [c poly]); replaced with explicit [apply/poly_eqP] + coefficient-level [poly0E]/[addr0] (the latter on coefficient [c], non-parametric Path B works).
Port [Poly.ec] lines 726-779: [peval] / [root] / [prepolyL] / [isprepolyL] / [polyL] / [polyLE] / [degL_le] / [degL] / [inj_polyL] / [surj_polyL]. Closes the Phase 6 section. Adaptations: - [prepoly] is the Phase-1 section-local subtype's underlying fun-type; outside that section it's parametric in [c]. The Phase 6 section uses the synonym [int -> c] explicitly for [prepolyL]'s codomain rather than spelling out [c prepoly]. - [polyL]'s result type spelled as [c poly] (parametric form) instead of the section-local [poly] (Phase 1's bare alias). Skipped from this chunk: [finite_for_poly_ledeg] / [dpoly]-distribution lemmas (lines 782-844 of original) — these need [is_finite_for] / distribution theory that hasn't been TC-ported, and they're not on the critical path for the rest of the algebra port. Will revisit if downstream needs them.
Port [Poly.ec] lines 850-973 (the [Poly] abstract theory built
over [c : idomain]):
- [degM]: deg(p·q) = deg p + deg q − 1 for non-zero p, q
(multiplicativity of deg, requires no zero divisors).
- [lcM]: lc(p·q) = lc p · lc q.
- [polyM_mulf_eq0]: polynomials over an idomain inherit the
no-zero-divisor property — the [mulf_eq0] axiom one would
feed to a hypothetical [instance idomain with ('c poly)]
registration.
- [unitE]: bridges the choiceb-based [poly_unit] (committed at
Phase 5 over [c : comring]) to the structural form
[deg p = 1 /\ unit p.[0]] available when [c : idomain]. Both
directions proved: (=>) uses [degM] to force both factors of
any inverse pair to have degree 1; (<=) builds the explicit
inverse [polyC (invr a)].
- [polyVE]: structural value of [poly_invr (polyC a)] when
[unit a] — equals [polyC (invr a)] via uniqueness of the left
inverse modulo [polyC a]'s left-regularity (which holds iff
[a] is non-zero, which holds when [a] is a unit in an idomain).
[unitE]/[polyVE] do NOT redefine the registered [poly_unit] /
[poly_invr] (those were committed at Phase 5 and are fixed for
all 'c poly carriers). They expose the structural shape under
the additional [c : idomain] assumption — downstream proofs
rewrite with these to argue structurally about invertibility
without unfolding [choiceb].
Skipped: [degV] (poly's deg of polyV equals deg p) and
[finite_for_poly_ledeg] / [dpoly] distribution lemmas. The
former depends on [polyV]'s structural form which doesn't
match our [poly_invr] (poly_invr is choiceb-based, not the
[if deg p = 1 then polyC (IDCoeff.invr p.[0]) else p] form);
the latter need finite/distribution scaffolding not TC-ported.
Smoke test exercising the parametric polynomial library at carrier [int] (which is registered as [idomain] via TcInt). Confirms each phase of TcPoly resolves correctly through the chain of TC instances ([int : idomain : comring : addgroup : addmonoid : monoid] plus the [int poly : comring]-via-Phase-5 chain) at a concrete carrier: - Phase 1-2: [polyCE] / [polyXE] coefficient formulas. - Phase 4: [polyM_mulrA] / [polyM_mulrC] structural lemmas. - Phase 6a: [degC] / [deg0] / [deg1] / [degX] degree arithmetic. - Phase 6c: [deg_polyXn] / [lc_polyXn] X^i theory. - Phase 6e: [polyLE] polyL constructor. - Phase 7: [degM] / [lcM] / [polyM_mulf_eq0] idomain extension. - Concrete: [polyM (X+1) (X−1) .[0] = -1] computes through the polyM convolution. Caveat: tests use [polyM]/[polyD]-spelled forms instead of the [+]/ [*] abbrevs — the abbrev resolution at carrier [int poly] hits the parametric-Path-B witness encoding gap (recorded in memory). The underlying lemmas all apply correctly via structural names. Once that gap is closed, the abbrev forms will work too.
Closes the parametric-Path-B witness encoding gap that left class- lemma applications at parametric carriers ([apply (addrC<:c poly>)] inside [section ; declare type c <: comring]) unusable. **The bug.** [opentvi] creates a [TCIUni] for each opened tparam's TC bound and posts a [`TcCtt] problem, but doesn't itself drain the queue. The TCIUni stays parked in [tcenv.problems] until something else triggers [unify_core]. Meanwhile a proof-term carrying [(+)<:c poly[TCIUni #a [0;0]]>] arrives at the matcher's [try_delta], which tries [Op.tc_reducible env (+) tys] — and [tc_core_reduce] raises [NotReducible] on TCIUni witnesses, since it can only walk [TCIConcrete]/[TCIAbstract] forms. So [try_delta] falls through to [default]'s [is_conv], which doesn't TC-reduce either; matching fails, [pf_form_match] raises MatchFailure, [t_apply] reports "the given proof-term proves: ... it does not apply to the goal". **The fix.** Two changes: 1. [EcUnify.UniEnv.flush_tc_problems env ue] (new): runs [Unify.unify_core] on a trivial-true [`TyUni] problem, which re-pushes every parked [`TcCtt] in [tcenv.problems] and lets the strategy dispatcher resolve them. After the call, the resolution map contains a witness for every [TCIUni] that any strategy (Modes #1..#6) could pin. 2. In [EcMatching.f_match_core]'s [try_delta]: before destructuring the heads, call [flush_tc_problems env ue] and re-normalise both sides via [norm]. The substitution machinery in [tcw_subst] (ecCoreSubst.ml:209) dereferences resolved TCIUnis through [fs_tw_uni], so after [norm] both forms carry the concrete witness; [tc_reducible] then succeeds and [doit_tc_reduce] produces the renamed structural op (e.g. [polyD] for poly's addgroup-via-class-(+)), which conv'ing against the goal succeeds. Combined with the earlier framework fixes [0dd7d21] (infer-via- abs-decl) and [c182895] (alpha-equivalent chain reuse), this lets [apply (addrC<:c poly> p q)] and [apply (mulrA<:c poly> p q r)] inside a [c <: comring] section discharge directly, without requiring users to fall back to the underlying [polyD_addrC<:c>] / [polyM_mulrA] structural lemmas. The TcPoly port's structural-form workaround in Phase 6 / Phase 7 / smoke test stays as-is for the already-written code, but new code can use the natural class form. Validates: tcalgebra suite (TcMonoid/TcRing/TcInt/TcBigop/TcBigalg/ TcNumber/TcPoly/TcPolySmokeTest) all pass; the parametric Path B reproducer at /tmp/repro_pathb.ec now closes [test_path_b] via [apply (addrC<:c poly>)] without admit.
…c carrier Add [test_addrC_at_int_poly] / [test_addrA_at_int_poly] / [test_mulrC_at_int_poly] using [apply (addrC<:int poly>)] etc. With the [try_delta] flush fix (commit 5e04bf6), these now work directly — the TCIUni parked at [opentvi] gets resolved before [tc_reducible] is checked. [*] at carrier [int poly] still has a parser-level ambiguity (both the section-local abbrev [Top.TcPoly.*] and the comring class [Top.TcMonoid.*] match). Test uses [polyM] explicitly there. That ambiguity is orthogonal to TC inference — it'd want a disambiguation policy at the parser level.
[gen_select_op]'s [drop_subsumed_tc] classifies candidates by the
[op_kind] of their declared path — but after typing, abbrev
candidates are inlined and their bodies' heads are what actually
appear in the elaborated term. So an abbrev whose body is itself a
TC-op invocation escapes the filter even when, post-inline, it's a
TC-op-headed term that reduces to the same head as another candidate.
Concrete trigger: writing [p * q] with [p, q : int poly] yielded
[MultipleOpMatch] because three [*] candidates survived:
- [Top.TcPoly.*] (abbrev → body head [polyM], non-TC)
- [Top.TcMonoid.*] (abbrev → body head [(+)], TC op of monoid)
- [Top.TcRing.*] (TC class op → reduces to [polyM])
[drop_subsumed_tc] correctly drops [Top.TcRing.*] (TC op subsumed by
[polyM] in concrete_paths), but it leaves [Top.TcMonoid.*] alive
because its declared kind is [OB_nott] (abbrev), not [OB_oper(OP_TC)].
The body's head [(+)] is a TC op, but the filter never inspects it.
Compare to [+] at the same carrier: only two candidates, the second
being the [Top.TcMonoid.+] class op directly. [drop_subsumed_tc] sees
its declared kind as [OB_oper(OP_TC)], runs [tc_reduce], drops it.
The asymmetry is just that TcMonoid ships an [abbrev (*) ['a <:
mulmonoid] = (+)<:'a>] but no analogous abbrev for [+].
Fix: add [drop_subsumed_by_post_inline_head], a sibling of
[drop_subsumed_tc] that operates on the post-inline body head rather
than the declared op_kind. For each candidate with a body, force the
[sbody] lazy and extract the body's head op. Collect the non-TC heads
as [concrete_heads]. Then drop any candidate whose post-inline head
is a TC op that [tc_reduce]s to a head already in [concrete_heads].
Run after [drop_tc_bounded_notation] so the existing pre-inline
filters dedupe what they can first.
After the fix, [p * q] at carrier [int poly]:
- [Top.TcPoly.*] body head [polyM] — kept
- [Top.TcMonoid.*] body head [(+)] (TC) — tc_reduce → [polyM] in
concrete_heads → dropped
- [Top.TcRing.*] already dropped by [drop_subsumed_tc]
=> single candidate, parses cleanly. [apply (mulrC<:int poly>)] now
discharges directly. Smoke test ([test_mulrC_at_int_poly],
[test_mulrA_at_int_poly]) covers both.
Validates: tcalgebra suite (TcMonoid/TcRing/TcInt/TcBigop/TcBigalg/
TcNumber/TcPoly/TcPolySmokeTest) all still pass; [+]/[-]/[**] paths
unaffected (their candidate sets don't trigger the new pass).
With the post-inline subsumption filter (commit c47657a), [p * q] at carrier [int poly] resolves uniquely without needing the [polyM] disambiguation. Replace the [polyM]-based test with the natural class-form, and add [test_mulrA_at_int_poly] to cover associativity. The mulmonoid [*] abbrev that previously caused the [MultipleOpMatch] ambiguity is now dropped post-inline, because its body head [(+)] [tc_reduce]s to [polyM] which is already represented (concretely) by the section-local [Top.TcPoly.*] abbrev's body.
[pf_find_occurence]'s key extraction takes the pattern's literal head op-path. For a pattern like [addrC<:int poly> p q] proving [(+)<:int poly[wit]> p q = (+)<:int poly[wit]> q p], the key would be [(+)] — but the goal, after abbrev expansion at [int poly], usually has [polyD] (the realisation). Different keys → keyed filtering rejects every position → "nothing to rewrite" even though the goal *does* contain a position equivalent to the pattern under TC reduction. Fix: when the pattern's head [Fop p tys] is a TC op that [tc_reduce]s at the supplied [tys] to a concrete op, key on the *reduced* head instead of the literal one. Matches how the keycheck-side already handles the symmetric case (goal's head being a TC op that reduces to the pattern's key). Apply already worked for class-form lemmas at parametric carriers after the [try_delta] flush fix (commit 5e04bf6). This commit extends parity to [rewrite]. [examples/tcalgebra/TcPoly.ec] simplifications enabled: - [degDr] / [lcDr]: [polyD_addrC<:c>] → [addrC<:c poly>] (rewrite at parametric carrier). - [polyXnE]: [polyM_mulrC] → [mulrC<:c poly>]. Other structural-name uses ([polyM_mul0r] in [mul_lc] base cases, the instance-obligation proofs) remain — those reach into goals where the rewrite-engine's pattern would need to match e.g. [zero<:c poly>] against [polyC zero<:c>] (poly0's abbrev expansion), and the head-bridge alone doesn't span that distance. Path-B for *apply* is solid; *rewrite* through deeper structural re-encoding is more delicate.
Two printer fixes that make TC-elaborated goals readable: 1. [pp_tyvarannot] uses [pp_tyvar_ctt] instead of dropping the TC constraint list. So [print poly0] now shows [abbrev poly0 ['c <: comring] : 'c poly = polyC idm<:'c[...]>.] instead of [abbrev poly0 ['c] : ...] (which hid the comring bound). The sibling [pp_tyvar_ctt] already knew how to format ['c <: comring]; [pp_tyvarannot] just wasn't using it. 2. [try_pp_notations] chases the abbrev's tparam univars through the matched unienv, using [ov.args] (the [etyarg list] from [opentvi], which carries both the type univar AND any TC-witness univar) plus [f_op_tc] (etyarg-aware) instead of bare tvars + [f_op] (which built empty witnesses). Effect: a goal like [p = poly0] inside [section ; declare type c <: comring] now prints as [p = poly0<:c[c.`1]>] with the carrier and TC witness visible, instead of [p = poly0<:#a>] where [#a] was a stale univar reference left behind because [ov.subst] (the fresh-univars map from [opentvi]) was applied without then chasing through the matched unienv's substitution. Without these, the user typing [have h: p = poly0] inside a comring section would see a goal carrying a fresh-univar [#a] that looked like an unresolved type, even though the matcher had already pinned it to the section's [c]. The univar was a print-side ghost — the underlying form was fully ground.
[pf_find_occurence]'s [kmatch] keyed filter previously only accepted goal positions whose head matched the pattern's head literally (or [tc_reduce]d to it). For a TC-op pattern like [mul0r<:int poly>] with [( * )<:int poly[wit]>] applied, the goal's [polyM] head (which is the registered structural realisation) was rejected by the keyed filter, even though it's the carrier-specific structural form of the same op. This commit adds the reverse direction: when the pattern's key is a TC class op [tcop] and the goal's head [op'] is a registered realisation of [tcop] in some instance's symbol map, accept the position. The actual unification still has to bridge the heads downstream — typically by [tc_reduce] firing once the pattern's witness is resolved (Path-B fix paths handle this). Adds [EcEnv.Op.tc_op_realised_by env tcop concrete] as the syntactic check, used by [ecProofTerm]'s [kmatch]. Effect: rewrite patterns with class-form heads (e.g. [( * )<:c>]) no longer get filtered out at goal positions whose head is the structural realisation. Doesn't on its own fix the bare-rewrite case ([rewrite mul0r] without TVI still fails because the unification can't pin the pattern's univar carrier; see followup notes), but it's a strict improvement on the keyed-filter side and unblocks several positions that were silently rejected.
Mirror [Poly.ec:degXn_le]'s [(IntID.addrC 1)] disambiguation step with the TC equivalent [(addrC<:int> 1)]. Both proofs invoke a *qualified* commutativity at the int level to pin the rewrite to the integer ring (vs the polynomial ring whose [addrC] is also in scope at this point). Poly.ec qualifies via the cloned-module path [IntID.addrC]; the TC port qualifies via TVI [addrC<:int>] — direct semantic translation. The earlier port used [addzC] (an int-specific lemma in TcInt's module) as the disambiguator; replacing it with [addrC<:int>] (a) brings the proof closer to [Poly.ec]'s structure, and (b) demonstrates that TVI-based qualification is the principled way to disambiguate class lemmas in TC — same role as [Module.lemma] in clone-based theories.
When the pattern head is a TC class op (e.g. [*]<:comring>) with the carrier still a univar and the goal head is a registered concrete realisation of that class op (e.g. CoreInt.mul), force unification of the carriers so the TC resolver can pin down the witness. Without this, [rewrite mul0r] on a goal at a parametric or concrete carrier could not find a position whose head was the realisation rather than the class op.
Add a [reducible] modifier on [instance] declarations. Reducible-marked instances participate in strict TC reduction: when [/=] (cbv) hits a TC class op whose witness resolves through such an instance, it folds the op to its concrete realisation. Non-reducible instances (e.g. polynomial instances over an abstract carrier) stay opaque so users keep reasoning through algebraic lemmas. Matcher and [is_conv] are unaffected — both look through any concrete witness regardless of the flag, so unification and convertibility stay maximal. Strict mode is opt-in via [Op.tc_reducible ~strict:true] / [Op.tc_reduce ~strict:true]. Plumbing: - [tcinstance.tci_reducible] field; threaded through manual and synthesised-along-the-class-chain instance declarations. - [REDUCIBLE] keyword in the [instance] grammar. - [Op.tc_core_reduce] gains [?strict]; raises [NotReducible] when the resolving instance is not marked reducible. Abstract-rename folding also gated by strict. - [EcCallbyValue.reduce_user_delta] op-step calls [Op.tc_reduce ~strict:true] and recurses on the result. - [EcReduction.fold_reducible_tc] normalises a form by folding every reducible-marked TC op recursively. Called by [t_rewrite] after position substitution so the post-rewrite goal carries underlying core ops rather than verbose [op<:T[Conc(...)]>] heads. Standard-library usage: - TcInt: [instance idomain with int reducible]. - TcBigop: drop legacy [import Ring.IntID] (was a workaround for the missing fold; the int instance now folds at [/=]). - TcPoly: drop [(addrC<:int> 1)] TVI workaround in [degXn_le].
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.