Algebraic universes and variances#21603
Draft
mattam82 wants to merge 47 commits intorocq-prover:masterfrom
Draft
Algebraic universes and variances#21603mattam82 wants to merge 47 commits intorocq-prover:masterfrom
mattam82 wants to merge 47 commits intorocq-prover:masterfrom
Conversation
coqbot-app
bot
added
the
needs: full CI
github-actions
bot
added
the
needs: rebase
mattam82
force-pushed
the
universes-and-variances
branch
2 times, most recently
from
90af0a6 to
f1b122f
Compare
Add stdlib overlay
Use ";" instead of "|" to separate sort and univ binders, resolving ambiguities in univ decls
Fix an issue in univMinim considering already defined flexible
Remove debug output from test-suite file
Fix cumulative attribute passing
Revert test-suite file
Fix various bugs after rebase
Problem in inferCumulativity
Fix wrong custom defs of whd_decompose
Fix after rebase
Fix template universes handling (conclusion is already flex, but all Set/0 <= u constraints disappear after minimization now)
Support ";" delimiter instead of "|" in sorts and instances to separate qualities from universe levels
Fix test-suite files (new syntax for variances)
Remove debug cmds from test-suite file
Change printing of level `0+n` to `n`
Revert test-suite file
Clean test-suite file, still to investigate different minimization
Fix universe binders handling
Remove debug cmd
Fix back test-suite file
Updated test-suite files
Real output differences (to be discussed)
New warning for deprecated | syntax (tbd)
Finally allow to simplify `max(0+n,u1+k1,..,un+kn)` to `max(u1+k1,..un+kn)` when `n <= k1 /\ ... /\ n <= kn`
Restore printing of `<` constraints in source paths
Fix scheme generation to infer variances, minor cleanups
Fix computation of variance in sections
Allow to solve all flexibles during minimization when strict univ declarations are used
Start canonizing at unifications
Eager substitution of equalities in loop_checking, simplifying the implementation and allowing a more efficient `set` operation
Adapt to the new API
Fix substitution code in loop_checking
Add comments for tricky substitution functions
Fix various issues introduced after rebase
Updated output tests
Fix after rebase
Universe level Set -> 0 renaming
Collapse to 0 only if minimization to Set is allowed
Remove unnecessary module ApplicationVariances
Extending variance info to account for toplevel fix binders
WIP
Add topfix_binders information to variance occurrences and
use it to more finely compute variances for fixpoints
Remove application_variances
Add variance for typing in term
Properly separate cumulativity checking and type inference variance information
TODO fix variance ascription: it should check what?
Minor bugs
Fix forcing of variances
Fix test-suite issues
Fix printing of inferred variances
Fix inference of projections variances (primitive or not)
Add tests
Fix cumulativity test (no -indices-matter here)
Fix test-suite file relying on previously too strong minimization
Fix issues with *non*-cumulative inductives, and correctly compute variance at cases
Fix test-suite, usually relying on arbitrary minimizations
Debug and normalize properly
WIP removing the duplicated constraints and substitution in ustate
Finish removing duplicate state in ustate (UnivFlex and constraints)
Let X := Type. minimizes to 0 now
Simplify ustate to avoid the `local` record and work directly with UState.t
Add support for rigid flag (heuristic) in graph
Fix side-effect handling
Clearer minimization test for allowed instantiation by 0/Set
Fix back NumberNotations test-suite
Fix output and a bad bug in inferCumul due to missing universe subst
Improve explanations
Fixed output tests
Fix a bad bug in ClauseOf.subsumes
Fix elimscheme weakening
Use presence in binders to determine minimization status
Allow minization to set in solve_flexibles mode
Use "Conv" cumul_pb for assumptions
Fix variances annotations in test-suite
Refine elimschemes fix
Better debug msg in univMinim
Improve EConstr.eq_constr_universes
Fix UnivProblem.Set compare bug
Fix bug in canonical structure resolution in unification.ml in presence of univ poly
Fix econstr eq_universes to take unfoldability of constants into account
Fix evarutil compare_cumulative_instances: take unfoldability into account.
Change API to declare a fixed universe context and force solving of flexibles respecting it
Use fixed compare_cumul functions in reductionops
Prevent destroying typeclass abstractions in solve_evar_evar
Fixes a bug in HoTT where ?le ~= ?le' : Le ?A constraints where turned into ?A -> ?A -> Type evars, and hence became unresolvable
Revert change of interpretation in do_assumptions for Parameters in polymorphic mode, as this breaks TC resolution among the parameters.
Fix evarconv using an incorrect eq_constr_universes
Fixed syntactic equality check up to cumulativity
Non-extensible constraints are checked earlier now
Proper fix for issue in bug_10669 (polymorphic parameters).
We should probably just prohibit multiple Polymorphic (Global) parameters in a single command, as we already restrict to one univ decl on the first assumption.
Fix handling of side-effects in ustate
Fixes after rebase
Fix printing of univ and instance
Fix output tests
Rewrule test (? for extensible constraints)
Revert ? for ext change, fix parsing of + for extensibility of cstrs.
Improve printing of constraints (use <)
Make normalize resiliient to undeclared universes
Keep constraints on demoted globals in UState.context_set
Remove debugging code from loop_checking.ml
Minor optim in loop_checking
More compact printing of constraints
Fix refman syntax
Minor fixes and comments
Ensure that i + 1 >= j + 1 implies i >= j by enabling the clause during checking, starting back from the minimal model values for premises.
Fix output test
Check that injectivity of +1 is handled correctly.
Fix output test
Debug in comInductive, fix comment
Add a test-suite file
WIP Fixes
compiles but fails at Logic.v
Fix passing and handling of sort_poly flag (can be moved before univs)
Fix after merge, we don't store the local universe constraints in ustate.local anymore, only local elimination constraints
Use 𝒰 for sort polymorphism, Type remains the fixed Type sort, unless for pseudo-sort-poly inductives (using unconstrained_sorts flag).
fix: Thread sort poly flag more correctly
It was being passed as unconstrained_sorts in some cases.
fix minimize univ rebasing in prepare proof
Remove Sort Poly flag (quickfix)
refactor: Replace sort_poly by poly
Revert Corelib changes
Fixes in comInductive w.r.t. elaboration of template-poly/sort-poly
Fix sort_poly argument passing
Forgotten parsing rule for Type@{s;u}
Printing flags changes
Renaming in declare.ml
Fix compile error (to merge with univpoly)
New eliminator code to univpoly
fix: Properly remove levels from extra constraints upon restriction
Fix parsing issues after rebase (to merge with univs)
Introduce SortPolyFlags to gather flags for polymorphic defs
Adapt the whole code base to using this instead of the multiple
poly/sort_poly/cumulative flags.
poly_flags -> poly
Fix test-suite files
Cleanup bugs (reverting changes of notation for flexible/rigid)
By default we don't reduce lets during cumulativity inference, to avoid potential blowups
mattam82
force-pushed
the
universes-and-variances
branch
from
f1b122f to
8578b07
Compare
coqbot-app
bot
removed
the
needs: rebase
This completely changes the semantics of `Axiom A : Type@{i} -> Prop` for
example, with `i` becoming cumulative.
Type.1 was previously generated by the (monomorphic) ssr_congr_arrow definition which talks about equality of types.
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.
This follows up from #19537 and previous PRs.
Rebased on master, minimizing API friction so further rebases should be lightweight.
At this point (Feb 7th 2026) equations, hott, stdlib and elpi work, hb should follow soon.
There are a few commits that can move move directly to master, I will do that. This will probably stay a draft, but people can play with it and report feedback here at least.
Fixes / closes #????
make doc_gram_rsts.