Conversation
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].
Move the [fold_reducible_tc] hook from [t_rewrite]'s post-substitute
step to two upstream points so the rule "concrete iff reducible"
applies uniformly to every tactic that consumes a polymorphic-lemma
type, not just rewrite:
1. [EcProofTerm.cpt_subst_form]: substitution + fold. Used by
[concretize_e_form], [concretize_e_form_gen], [concretize_e_arg]
and friends — covers [apply], [exact], [have], [pose], elimination,
and everywhere else that goes through [concretize].
2. [EcLowGoal.LowApply.check]: fold the type returned by [check_]
(the result of [Ax.instanciate] at concrete etyargs). Covers
[rewrite], where [t_rewrite] destructures the [ax] directly
without going through [concretize].
Previously only [t_rewrite] folded its post-substituted goal, which
left [apply] / [exact] producing goals carrying [op<:T[Conc(...)]>]
heads at reducible carriers — inconsistent with rewrite's behaviour.
[cptenv = CPTEnv of f_subst * env] — extended to carry the env so
[fold_reducible_tc] can consult [tci_reducible] flags. Two outside
callers in [ecUserMessages] and [ecHiGoal] updated for the new shape.
The Why3 translation strips the witness slot of every [etyarg] (only
the type is kept — see [trans_app] line 715), so a TC class op like
[-]<:addgroup[Conc(int_inst)]> becomes a polymorphic Why3 function
[op_minus_addgroup : 'a -> 'a]. SMT then has no way to relate it to
the underlying [CoreInt.opp] when 'a is instantiated to [int]: the
abstract polymorphic function has no defining axiom in the Why3 task.
Symptom: a polymorphic axiom over [addgroup] (e.g. [mulrNz : intmul x
(-n) = -(intmul x n)] with [-] = [-]<:addgroup>) cannot be combined
with a concrete int goal that uses [CoreInt.opp]. SMT closes
[Ring.ec]'s identical proof because the [IntID] clone rebinds [-] to
[CoreInt.opp] directly — there's no abstract [-] to bridge.
For each [tci_reducible] instance in the env, emit one Why3 axiom per
(class_op, concrete_realisation) entry in the instance's symbol map:
forall args, class_op<:carrier[Conc(inst)]> args = concrete args
After Why3 stripping the witness, this becomes the bridge that lets
SMT relate [op_minus_addgroup int x] to [CoreInt.opp x]. Polymorphic
axioms over [addgroup] then combine with concrete-int goals as
expected.
Closes the regressions in [TcInt.ec:60] (intmulz) and [TcBigalg.ec:289]
(prodr_ge0_seq) that surfaced after the merge with origin/main and
were the blockers for Phase 3 testing of the [reducible]-flag work.
Tests at concrete reducible carrier (int): - apply / rewrite of TC class lemmas (addrC, addr0, opprK, chained forms) — Phase A folds the proof-term type at concretization time. - SMT calls with TC-class-lemma hints (mulr2z, mulrNz, opprK chained through mulrNz) — Why3 bridge axioms relate the abstract heads to the concrete int realisations. The chained SMT case [test_smt_bridge_chained] mirrors TcInt.ec:60 (intmulz) byte-for-byte; this fails without the bridge axioms. Tests at abstract carrier (declare type c <: comring): - apply of the same TC class lemmas — abstract heads are preserved (no reducible instance to fold through, by design). Each test exercises the rule end-to-end with the standard tactics through which a proof-term gets concretized.
Short-name resolution for binary class ops like [Top.TcRing.*] often finds two candidates — the class op itself and an abbreviation in [Top.TcMonoid] (e.g. [( * ) ['a <: mulmonoid] = (+)<:'a>]) that projects the multiplicative monoid view. Both unify with the same target etyargs and dom, so [op_symb] couldn't pick a unique short form and fell back to the qualified [Top.TcRing.*] form. The downstream [pp_opapp] check ([List.is_empty nm]) then forced prefix display ([Top.TcRing.( * ) p q] instead of [p * q]). Filter out abbreviations from the candidate list (when at least one non-abbreviation candidate exists) so the class op wins, the short form resolves, and infix display fires. Verified zero prefix-fallback events on TcPoly after the fix (was hundreds before).
The elaborator (typing-time op resolution) and the printer (op_symb, deciding the shortest unambiguous qualifier) both need to dedup [select_op]'s output via the same rules: drop TC-ops subsumed by a non-TC candidate, drop notation/abbrev candidates shadowed by a TC-op of the same basename, etc. Previously these four filters lived inline in [ecTyping.gen_select_op] and the printer had only [by_current] plus an ad-hoc "prefer non-abbreviation" hack. Move the four filters drop_subsumed_tc drop_shadowed_notation drop_subsumed_by_post_inline_head drop_tc_bounded_notation to [EcUnify], expose them, and add a [canonicalize] composition that runs them in the established order with the [keep-all-on-empty] safeguard. [ecTyping] now calls [EcUnify.canonicalize] (replacing the inline chain). [ecPrinting.PPEnv.op_symb] does the same (replacing the local "filter abbreviations" hack from the previous commit). A goal printed by the system now resolves the same way the elaborator would parse it back: identical filter chain on both sides.
The check (introduced in [bcaa810]) decides whether to elide the [<:T>] type-instantiation annotation by looking at whether the type parameters of the op appear in the types of the consumed arguments. For nullary ops like [zero ['a]: 'a] applied with no args, no [dom] is consumed and the only place ['a] occurs is the codomain — so the check used to fail, and the annotation was always shown. Extend [covered] to include the residual type at the use site (the unconsumed-dom suffix plus the codomain). The user always sees this type in context — it's the type of the residual term — so any tparam that appears in it is recoverable. Effect: [zero], [oner], [idm] applied bare at a parametric carrier [c <: comring] now print as [zero], [oner], [idm] instead of [zero<:c[c.`1^2]>] etc. The lift-annotation cruft only ever showed up because the residual type wasn't part of the dominated check. Independent of TC: same logic applies to any op with a tparam that only appears in the codomain.
Tier 1 of the [project_tcalgebra_port_next] plan. Three deliverables:
1. [examples/tcalgebra/TcReal.ec] (new): canonical [real] instance
for the TC hierarchy. Mirrors [theories/datatypes/Real.ec:RField]
(a [Ring.Field] clone) plus [theories/algebra/StdOrder.ec:RealOrder].
Three nested instances:
- [idomain with real reducible]: comring/idomain ops + axioms.
- [tcrealdomain with real reducible]: order ops [`|_|], (<=), (<),
minr, maxr + the order axioms (ler_norm_add, addr_gt0, etc.).
- [tcrealfield with real reducible]: closes the field structure
(just unitfP).
All three marked [reducible] so [/=] folds the abstract ops to
their CoreReal realisations and SMT bridges work at concrete real.
2. [examples/tcalgebra/TcNumber.ec]: existing [tcrealdomain with int]
instance gains the [reducible] marker — was missing, now consistent
with the [idomain with int] in TcInt.ec. Real arithmetic SMT bridges
for int's order operators now generated.
3. StdBigop is subsumed: [bigA / bigM / bigiA / bigiM] in TcBigop.ec
already dispatch on the carrier's monoid view. No new file needed
for the legacy [BIA / BIM / BRA / BRM] theories.
Verified: tcalgebra/* + tests/* + theories/algebra/Ring.ec + smoke test
exercising bigops at int and real all compile clean.
Port of [theories/algebra/Binomial.ec] to TC. Three pieces: 1. Concrete int operations [fact / bin1 / bin] and their lemmas, ported verbatim modulo proof-script tweaks where the matcher couldn't bridge concrete-int operators against TC class ops. In a few spots [/#] and [smt(...)] replaced legacy proof chains that relied on direct rewrite matches against [Int.( * )] / [Int.max] / etc. — the witness-slot mismatch between TC class ops and their concrete realisations isn't fully bridged by the matcher in arbitrary positions. Functionally equivalent. 2. Binomial theorem [lemma binomial] over a [comring] carrier, in a single [section. declare type t <: comring.] block. The legacy [BinomialCoeffs] abstract theory + [clone Bigalg.BigComRing as BCR with ...] dance is gone — TC inheritance synthesises the bigop machinery automatically. [bigiA] explicitly chosen as the addmonoid view (the body sums an additive intmul) so the elaborator doesn't see free TC variables. 3. Specialisation at real [lemma binomial_r]. The legacy [BCR.binomial] came from a clone of [BinomialCoeffs] at real; here it's a direct instantiation [binomial<:real>]. A small [intmulr_real] helper replaces the legacy [RField.intmulr] (which lives inside the legacy [Real.ec:RField] clone, not extracted as a standalone lemma). Uses [rewrite (_ : ...)] to dodge a witness-mismatch in the direct rewrite-with-hypothesis path. Side fix to [TcNumber.ec]: the [int_norm / int_le / int_lt / int_min / int_max] wrapper ops in the [tcrealdomain with int] instance are inlined to [CoreInt.absz / CoreInt.le / CoreInt.lt / Int.min / Int.max]. The wrappers broke [tc_op_realised_by] lookups: the matcher hook recognises a concrete realisation registered in the symbol map by *exact path*, and goal-side occurrences of [CoreInt.lt] (via the [Int.(<)] abbrev) failed to bridge to the wrapped [int_lt]. With the direct registration the bridge works, matching how [TcInt.ec]'s [idomain with int] already binds [CoreInt.add / CoreInt.mul] directly.
Pivot for letting [instance] op-bindings be arbitrary forms (not just
named ops). Storage change only — user-visible syntax unchanged.
[ecTheory.{ml,mli}] [tcibody.General]: the symbol map value type
changes from [(path * etyarg list)] to [EcCoreFol.form]. Each entry
is now the form that realises the corresponding class op on the
carrier; for existing instances it's [f_op_tc concrete_path
concrete_etyargs ty], i.e. the same content wrapped in [Fop].
Cascade through all consumers:
- [ecScope.check_tci_operators]: wraps the resolved [(path, etyargs,
ty)] into a form via [f_op_tc] at registration time.
- [ecScope] coherence checks ([same_symbols], [head_path]) extract
the path from the form's [Fop] / [Fapp(Fop,...)] head.
- [ecScope] generalisation-chain subst: substitutes the form
directly through [EcSubst.subst_form] instead of rebuilding
[f_op_tc] from a stored path.
- [ecEnv.Op.tc_reduce]: returns the substituted form directly;
carrier-tparams substitution is now a [subst_form] step instead of
a manual [Tvar.subst] on a recomputed op type.
- [ecEnv.Op.tc_op_realised_by]: matches against the form's head op.
- [ecSubst.subst_tcibody]: maps [subst_form] over the symbol values.
- [ecSection.on_instance]: walks the symbol values via [on_form].
- [ecSmt.trans_reducible_instance_bridges]: bridge axiom RHS is the
symbol value directly; no path/etyargs reassembly.
- [ecTheoryReplay]: maps [subst_form] over the symbol values during
cloning.
- [ecScope.get_ring_field_op] (legacy ring/field): destructures the
form's [Fop] head to recover the op path.
Phase 2 (parser accepts arbitrary forms on the RHS), Phase 3
(simplify [tc_core_reduce]'s return type accordingly), and Phase 4
(drop dead [(path, etyargs)] paths and let users write literals)
follow on top — each phase keeps CI green.
Verified: all tcalgebra/* + tests/* + core theories compile clean.
User-visible: [op X = BODY] in an [instance] declaration now accepts
an arbitrary [sform] on the RHS, not just a [pqsymbol]. Existing
instances stay green because a bare qsymbol is a degenerate form.
New capability: [op idm = 0] and [op oner = 1] now parse — a literal
on the RHS no longer has to round-trip through a named [CoreInt.zero]
/ [CoreInt.one].
[ecParsetree.ml] [ptycinstance.pti_ops]: type changes from
[(psymbol * (pty list * pqsymbol)) list] to [(psymbol * pformula) list].
The [pty list] TVI annotation that the old syntax accepted on the
qsymbol is gone — any disambiguation now happens inside the form.
[ecParser.mly] [tyci_op]: single rule [OP x=oident EQ body=sform].
[REDUCIBLE] keyword and the surrounding [tycinstance] grammar
unchanged.
[ecScope.check_tci_operators]: replaces the [select_op]-driven path
resolution with [EcTyping.trans_form] at the expected type. Closed-
ness check on the body's univars (which surfaces as a sensible
"contains free type variables" error if the body is incompletely
specified). The resulting form is added to the symbol map directly,
no [f_op_tc] wrapping required.
Verified: all tcalgebra/* + tests/* + core theories compile clean.
A smoke test [op idm = 0] in a synthetic [instance idomain with int
reducible] parses and elaborates; the bridge axioms (Phase A SMT
work) tie the literal to the abstract class op as expected.
Phase 3 (simplify tc_core_reduce now that symbols carry forms
directly) and Phase 4 (switch stdlib instances to use literals)
follow on top. Phase 4 exposes a downstream regression in
TcNumber consumers ("end-of-file while processing proof TcNumber")
when TcInt switches to [op idm = 0]; needs investigation before
the stdlib flip.
…h A) Internal cleanup. With the symbol map carrying forms (Phase 1) and op-bindings parsed as forms (Phase 2), [tc_core_reduce] no longer needs to return the [(opname, tciargs, tciparams, symbols)] tuple for the caller to rebuild a substitution and look up the body. Move the look-up + carrier substitution into a [finalise] helper inside [tc_core_reduce] itself; return the substituted form. The [tc_reduce] wrapper collapses to a one-liner over the abstract-rename fallback. No user-visible change. tc_reducible / tc_op_realised_by / the SMT bridge generator all already work on form values; the only consumer of the old tuple shape was [tc_reduce] itself.
[ecScope.already_discharged]'s [same_symbols] check decides whether an existing instance of a TC ancestor on the same carrier "matches" what the user is declaring (so that ancestor's axiom obligations don't need to be reproven). It compared values by their head op-path — which covers the common [Fop concrete] case but breaks when Path A's form-valued symbol map carries a non-Fop form (e.g. a literal [Fint 1] from [op oner = 1]). Fix: fall back to [EcReduction.is_alpha_eq] when at least one side isn't an [Fop] / [Fapp (Fop, …)]. This handles [Fint] / [Fdecimal] / lambda / etc. uniformly. Path A Phase 4 (switching stdlib instances to literal RHSs) is still blocked by a separate issue: binding [op idm = 0] / [op oner = 1] makes the elaborator's [select_op] see the literal as a polymorphic op candidate, so plain user code like [if k = 0 then a else 0] fails with "the formula contains free type-class variables". That elaboration-time ambiguity is independent of [same_symbols] and needs its own fix before stdlib instances can flip.
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].
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.