Implemented rewrite Pr [...] for mu_ge0 and mu_le1#2
Merged
Conversation
rewrite Pr [...] for mu_ge0 and mu_le1, corresponding to lemma ge0_mu (d : 'a distr) p : 0%r <= mu d p. lemma le1_mu (d : 'a distr) p : mu d p <= 1%r. from Distr.ec
Gustavo2622
added a commit
that referenced
this pull request
Oct 25, 2025
strub
added a commit
that referenced
this pull request
Apr 30, 2026
…hange) Splits the existing TcCtt resolution logic into three named local helpers — strat_tvar_via_tvtc, strat_abs_via_decl, strat_infer_by_carrier — corresponding to catalog modes #5, #6, and #1/#2 in doc/typeclasses-inference.md. Behavior is identical: same dispatch order, same failures, same pickup of [Tvar a]/[Tconstr p] cases, same parking of univar carriers. The refactor exists so Phase 3 can drop a By-args strategy in without disturbing the existing logic.
strub
added a commit
that referenced
this pull request
May 6, 2026
Companion to the previous commit (bug #2: per-path synthesis + tci_parents lookup). With multi-flavor inheritance, a single carrier may have multiple synthesised instances of the same TC (e.g. a comring on int has both an addmonoid- and a mulmonoid-derived monoid instance). When applying a polymorphic monoid lemma to a goal whose operator carries a SPECIFIC witness via an abbrev (e.g. [bigM] or the [( * )] alias), the unifier was committing arbitrarily to one of the candidates via [strat_infer_by_carrier], then failing later when the goal's [TcTw] equation pinned the other view. Fix: detect ambiguity at strategy-resolution time. When [infer_all] returns more than one candidate witness for [(carrier, tc)], DEFER — leave the witness univar unresolved instead of committing. A subsequent [TcTw] equation from the surrounding goal will bind the univar to the concrete witness via [bind_uni], picking the correct view from context. The dispatch in [select_op] gains a fourth case alongside (resolved / park-on-arg-deps / failure): if no resolution AND ambiguity detected, hold the constraint live without failing. If unification later doesn't narrow it, the resulting unbound univar surfaces as the usual "type-ambiguous" error elsewhere. Adds [EcTypeClass.infer_all : env -> ty -> typeclass -> tcwitness list] (companion to [infer]). Effect: with both bug fixes in place, [apply big_cat] (on [monoid]) discharges goals stated with [bigA] / [bigM] wrappers at concrete carriers — previously failing because the unifier picked the wrong view. The full multi-flavor factory pattern (e.g. [comring <: addgroup & (mulmonoid with idm = oner, (+) = ( * ))]) now works end-to-end: [\sum] and [\prod]-style notations both fold correctly, and lemmas on [monoid] apply to either flavor without needing per-flavor restatements. Regression: all existing TC examples build clean under --profile=ci.
strub
added a commit
that referenced
this pull request
May 6, 2026
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.
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
2 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.
Implemented rewrite Pr [...] for mu_ge0 and mu_le1, corresponding to the Distr.ec lemmas
lemma ge0_mu (d : 'a distr) p : 0%r <= mu d p.
lemma le1_mu (d : 'a distr) p : mu d p <= 1%r.