Algorithm for populating Trocq database for inductives by Tvallejos · Pull Request #73 · rocq-community/trocq

Tvallejos · 2026-04-08T12:16:10Z

description todo

MysaaJava · 2026-04-08T16:28:36Z

TODO

rebase
git mv std/algo/theories generic/inductives and change std/_CoqProject and hott/_CoqProject accordingly
git mv std/algo/elpi elpi/inductives and update Elpi Accumulate accordingly
git mv std/algo/tests tests/inductives and update tests/_CoqProject.{std,hott} accordingly
Move most significant examples of std/algo/detailed to docs/inductive-generation, and write some documentation to docs/codebase.md about how the inductive generation works. Remove std/algo/detailed.
rename Umap to Map4
Remove coq.locate and {{ ... }} constructs from inside elpi code
Remove dead code inside Rel40

Todo for myself, after merge:

split utils.elpi content to adequates files if needed
accumulate from inside elpi files directly
Fold generic/Param_xxx into one file generic/Param_inductives.v Move check commands to tests/inductives/check_.....v
Add a failing test with an inductive to Prop. For example with derive False which should generate False_sym when it doesn't. Check Zulip #Trocq users & devs > populating the Trocq database

Issues for later:

There is a duplicated database with trocq.db, derive.param2.db and derive.xxx.db
Can we clean all the databases derive.xxxx.db ?

Tvallejos · 2026-04-17T16:25:58Z

Hi @MysaaJava,
I'm using Trocq definitions in elpi files. Where should I register those definitions?

A few examples are Mapn.Has, eq_Mapn and eq

MysaaJava · 2026-04-17T16:52:50Z

I think you can add them to database.elpi.
You can add a predicate definition here, and accumulate on the clause.
You can see an example in Hierarchy.v which calls a predicate in generation/hierarchy.elpi

Tvallejos · 2026-04-22T13:10:33Z

I've been working on recovering the build for HoTT.
Inductives in HoTT are defined using universe polymorphism, so I need to extend the plugins to not assume global _ terms. In particular, almost all my derivations query derive.param2.db, which currently does not support universe polymorphism issue.

I minimized the dependencies to derive, but there are a couple more that will need such extension. For instance, discriminate and isK in derive.
I'm working on adding support for these plugins before continuing.

Tvallejos · 2026-05-11T13:29:05Z

This PR now depends on LPCIC/coq-elpi#1003.
To fully recover the build for HoTT, derivations isK and ltac.discriminate in elpi's derive have to be adapted to support universe polymorphic definitions PR. I'll be working on those.

Tvallejos · 2026-05-29T20:10:45Z

Depends on LPCIC/coq-elpi#1003 and LPCIC/coq-elpi#1018 , which were merged before the release of rocq-elpi 3.4.0.

Also depends on LPCIC/coq-elpi#1022 and LPCIC/coq-elpi#1030 . The first PR was merged, but not released and the second PR is pending review.

I'll work on cleaning a bit the history before rebasing

Tvallejos · 2026-06-01T08:48:46Z

Hi @MysaaJava, @CohenCyril. Most of the CI is green again.
I'm getting an error building trocq-std-examples, but seems related to the nix setup.

Here is the error I'm getting:

File "./flt3_step.v", line 14, characters 0-50:
Error:
Compiled library mathcomp.algebra.ssralg (in file /nix/store/qgggghxlg3mhwj0wc59rlx9zsnk0xcfa-rocq-core9.1-mathcomp-algebra-2.5.0/lib/coq/9.1/user-contrib/mathcomp/algebra/ssralg.vo) makes inconsistent assumptions over library mathcomp.boot.nmodule

Would you know why is this happening?

Tvallejos · 2026-06-05T16:41:46Z

I removed the detailed examples of derivations from this PR.
The failing CI is due a nix issue I could not reproduce it locally. Here is a Zulip discussion about it.

Tvallejos · 2026-06-05T18:08:59Z

A few comments:
mymap.elpi is derivative of map.elpi from coq-elpi.
The predicate whd-fuel is derivative of coq-elpi's.

Is there something to be done regarding license? both projects, trocq and coq-elpi are GNU LESSER GENERAL PUBLIC LICENSE

MysaaJava

General comments on the code:

~~Remove all coq.locate and relpace them with database predicates~~ POSTPONED
~~Use elpi accumulate system (and this should remove the need for #[superglobal])~~
~~Accumulate headers first, then files, and databases after~~
There is a lot of coq.typecheck ? ? _ is there a reason not to put ok instead of _ ?
~~Why are they main predicates both in elpi and rocq files ?~~

Questions for @CohenCyril

Should we have some "{{:gref ...}}" inside the code ? Why not, after all
Some utilities -> move them to util.elpi ?
Separate «static» database "trocq.consts" and «dynamic» database "trocq.translations" ?
~~What is Unset Universe Minimization ToSet. ?~~
The Trocq file header is not in the added files. How bad is that ?
Are the names of the Rocq files good ? Is From Trocq Require Import Relnm. clear ?

MysaaJava · 2026-06-22T05:37:56Z

+
+pred build-has-of i:map-class, o:gref.
+build-has-of M R :-
+  coq.locate {calc ("Map" ^ {map-class.to_string M} ^ ".BuildHas")} R.


Replace this with a database predicate

CohenCyril · 2026-06-23T07:28:30Z

Should we have some "{{:gref ...}}" inside the code ? Why not, after all

All coq.locate and {{:gref ...}} have basically the same defect and must be removed when located outside .v file: indeed .elpi code is relocatable and importing the same .elpi file in distinct sets of Require Import directive may lead to different results.

algorithm design collecting projectors partially generating the type of the injection lemma partially generating the type of injection lemmas + params deriving injection lemmas type correcting use of is injection terms + definitions adding injection lemmas to the db

…given an inductive implementing mR for unit + bool extending mR for enum containers 0+ constructors with 0+ arguments mR for recursive non parametric inductives Enum + Recursive no TyParam + TyParam no Recursive mR working for recursive inductives with type parameters

deriving type of Rm Rm for non inductive parameters, constructors without arguments Rm for non parametric inductives, constructors with 0+ arguments Rm for non parametric recursive arguments using KR to get arguments for IR_ind Rm for type parameters Rm for type parameters + recursion

fix _Coqproject

injK init refactoring some code wip injK type cleaning refactoring + cleaning moving some functions to utils wip injK adding type conlusion refactoring + generating injK types body of injKij tests for injK

mRRmK of False mRRmK body, many constructors 0 args. Unit, Bool, etc fixing imports + porting to elpi 3

fixing some duplicated files after the rebase

collecting arguments for rewriting injKs mRRmK for inds with multiple constructors + multiple arguments. No recursion No Typaram mRRmK + recusion mRRmK for type parameters + recursion cleaning mRRmK deriving mRRmK

add logical path to generic/inductives add generic to logical path in tests rename rel44 umap + mv tests to tests/inductives removing checks in generic fix tests postpone docs on inductive generation

wip introducing use of coq.env.global to recover HoTT build pruning extra plugins in derive

removing derive.bcongr dependency removing derive.eqk dependency removing some comments

adapt to univ.poly.param2 issue 1003 in rocq-elpi fix some uses of coq.env.global recovers param_empty for HoTT. requires isK and discriminate for pglobal to recover the rest fixes param_bool for hott adapt injections + injK to sortpoly fix injK for inductives with type parameteres fix sym symK non-dep path induction fix option for hott fixes sym and symK fix injections + injK + Rm fixes mRRmK up to sum fixes prod + adds 'iota' for primitive projections fixes lists fix vector fixes hott

recover examples/std fixes examples/hott

update dependencies trocq-std opam temporary hott dep + dev dep update nix temporary nix dependency for hott as discussed in rocq-community#79 and a temporary dependency for coq-elpi update nix, last PR got merged in coq-elpi master

MysaaJava

Remove extra "Extra Dependencies"

Tvallejos force-pushed the prop branch from a3ea760 to 618bffb Compare April 16, 2026 14:27

Tvallejos marked this pull request as draft May 11, 2026 13:29

Tvallejos force-pushed the prop branch 2 times, most recently from a76bced to 652bcff Compare May 30, 2026 10:18

Tvallejos force-pushed the prop branch 4 times, most recently from 456c356 to 2ce27a3 Compare June 5, 2026 15:29

Tvallejos marked this pull request as ready for review June 5, 2026 16:41

MysaaJava requested changes Jun 22, 2026

View reviewed changes

Tvallejos added 10 commits June 24, 2026 17:08

generating maps with relation10 instead of function

d61ecb7

common + change of interface + preparing Rm

01643db

structuring

b86f989

fix _Coqproject

details on injijK

dcc7b2f

injK init refactoring some code wip injK type cleaning refactoring + cleaning moving some functions to utils wip injK adding type conlusion refactoring + generating injK types body of injKij tests for injK

type of mRRmK

9f02a9f

mRRmK of False mRRmK body, many constructors 0 args. Unit, Bool, etc fixing imports + porting to elpi 3

changing structure

db3bd6b

fixing some duplicated files after the rebase

collecting injKs

3ed6bcc

collecting arguments for rewriting injKs mRRmK for inds with multiple constructors + multiple arguments. No recursion No Typaram mRRmK + recusion mRRmK for type parameters + recursion cleaning mRRmK deriving mRRmK

Tvallejos added 13 commits June 24, 2026 17:08

a hott generalizaion

d5bac20

a proof of RmmRK

612c216

wip move theories to generic/inductives + mv elpi to /elpi

fd82c5e

update in structure

03e7e4d

add logical path to generic/inductives add generic to logical path in tests rename rel44 umap + mv tests to tests/inductives removing checks in generic fix tests postpone docs on inductive generation

improving imports

870d3c6

wip introducing use of coq.env.global to recover HoTT build pruning extra plugins in derive

removing elpi.lib dependencies

4245361

removing derive.bcongr dependency removing derive.eqk dependency removing some comments

fix issue with name overlap in coverage

39a7e64

recovers examples

89809de

recover examples/std fixes examples/hott

updates dependencies

9eff89a

update dependencies trocq-std opam temporary hott dep + dev dep update nix temporary nix dependency for hott as discussed in rocq-community#79 and a temporary dependency for coq-elpi update nix, last PR got merged in coq-elpi master

removing elpi warnings

9ad9f4c

coq.typecheck ok

7d98505

rm comments

06b97ef

Tvallejos force-pushed the prop branch 3 times, most recently from f74b49c to fc71038 Compare June 24, 2026 21:49

Tvallejos added 8 commits June 25, 2026 00:01

pi + decl into pi-decl + tail-cut

e7b6084

cleaning outdated files + moving definition of RmmRK

1705dd6

tidying generalization thm 7.2.2

87c5d26

accumulating db headers, then files, then dbs

7275ff5

elpi's accumulate system

4534d4b

add rocq-elpi to nix

61e4672

rm mathcomp ssreflect build inputs nix

64d6e90

update actions

6fde77a

Tvallejos force-pushed the prop branch from fc71038 to 6fde77a Compare June 24, 2026 22:02

Tvallejos added 2 commits June 25, 2026 10:09

rm outdated db

339409a

rm superglobal when possible

26961c2

Tvallejos requested a review from MysaaJava June 25, 2026 13:09

MysaaJava approved these changes Jun 26, 2026

View reviewed changes

rm synterp hooks require

e04a747

Uh oh!

Conversation

Tvallejos commented Apr 8, 2026

Uh oh!

MysaaJava commented Apr 8, 2026

Uh oh!

Tvallejos commented Apr 17, 2026

Uh oh!

MysaaJava commented Apr 17, 2026

Uh oh!

Tvallejos commented Apr 22, 2026

Uh oh!

Tvallejos commented May 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Tvallejos commented May 29, 2026

Uh oh!

Tvallejos commented Jun 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Tvallejos commented Jun 5, 2026

Uh oh!

Tvallejos commented Jun 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MysaaJava left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

MysaaJava Jun 22, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

CohenCyril commented Jun 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MysaaJava left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Tvallejos commented May 11, 2026 •

edited

Loading

Tvallejos commented Jun 1, 2026 •

edited

Loading

Tvallejos commented Jun 5, 2026 •

edited

Loading

MysaaJava left a comment •

edited

Loading

CohenCyril commented Jun 23, 2026 •

edited

Loading