Patrick Nicodemus (Apr 12 2023 at 15:03): Patrick Nicodemus (Apr 12 2023 at 15:03):I would like it to be possible to use Ltac2 without importing Coq.Init.
I am interested in formalizing mathematics and there are various type theories I think would be interesting to use and perhaps make formalization a little bit easier, such as observational type theory, cubical type theory, homotopy type theory, etc. (I am aware observational type theory / cubical type theory in Coq is only a distant goal right now.)
In many of these cases there are various parts of the Coq.Init lib that would be irrelevant/orthogonal because of the very different foundations. In the case of homotopy type theory the univalence axiom is incompatible with propositional erasure and the coq-HoTT and Unimath libraries go to great pains to avoid having Prop pop up anywhere.
If one is operating outside the standard library Ltac is much weakened because one cannot use many standard powerful automation tactics which were developed with Prop/the stdlib in mind. You must write your own. So we are only left with vanilla Ltac as a language, and not the existing library of Ltac tactics. Therefore it becomes even more desirable to have a good and scalable language for writing automation.
I will tag @Enrico Tassi as these comments apply equally well to Elpi, which is a desirable tool and all the more desirable to have outside the stdlib.
If importing the Coq.init is unavoidable, it would be at least highly helpful to deal with the conflict https://github.com/coq/coq/issues/16934 we discussed a few months ago. Suppose I have a large development which in general does not rely on the stdlib but does declare a typeclass_instances database in the root file of the project. If I want to use Ltac2 (or Elpi) in a single file to write a single tactic, in any file which imports it (even transitively) we must carefully orchestrate the order of file imports so that we do not have any file which adds a hint to the typeclass_instances db before the stdlib typeclass_instances library is created, otherwise all these hints will be wiped away when the new empty database is created on top of it.
Enrico Tassi (Apr 12 2023 at 15:39):I'm fine separating https://github.com/LPCIC/coq-elpi/blob/master/theories/elpi.v so that what is after line 12 goes a file which depends to the stdlib, and have another version of that for UM or HoTT. Some parts of that file are also useless these days.
I've no clue about the Require Ltac, I don't even know if it is necessary.
Ali Caglayan (Apr 12 2023 at 15:40):It's possible to separate but a little tricky. @Pierre-Marie Pédrot and I had a go some time ago. Unfortunately there was some reuse of the ltac mlg for ltac2 which means some code will have to be duplicated (probably for the better).
Ali Caglayan (Apr 12 2023 at 15:41):Then there are these ltac2 bindings for ltac1 tactics that use the stdlib. They will have to be separated.
Ali Caglayan (Apr 12 2023 at 15:43):This was an attempt: https://github.com/coq/coq/pull/15632
Ali Caglayan (Apr 12 2023 at 15:44):Here is some related work making rewrite tactics stdlib agnostic by declaring more constants as registerable https://github.com/coq/coq/pull/16907
Ali Caglayan (Apr 12 2023 at 15:44):I gave up on that because I wasn't motivated enough to see it through.
Patrick Nicodemus (Apr 12 2023 at 16:08):Ok, cool. Thank you!
Last updated: Nov 29 2023 at 21:01 UTC