Trocq Interface Rework

[MysaaJava]

This Issue is here to discuss a rework of the interface of Trocq, so as to allow better control by the user.
Here are the things we would like to add:

• Access the parametricity relation from Rocq i.e. use Trocq to compute X @ T ~ X' because XR, and allow the user to register X' and XR to the global context
• A notion of Trocq databases in which Trocq translations are registered. The user can create and populate their own databases, and they can decide which ones to use when using trocq.
• Add a way of directly opening a goal for the parametricity witness when one gives two grefs G and G' and a level at which they should be translated (see Trocq command opening goals #26)
• Adding a etrocq tactic that open new goals for missing translations instead of failing (see this comment on Trocq command opening goals #26)

This issue aims at discussing the API syntax, which we want to be stable across Trocq updates.
Here is the latest syntax proposition:

(* Adds translations to a database*)
Trocq Register A B C. (* By default, core database is selected *)
Trocq Register A B C : mydb. (* Create or add to database mydb *)
Trocq Register D E : mydb mydb2. (* Adds the two translatinos to mydb and mydb2, which creates database mydb2 *)

Trocq Register G @ T ~ G' because GR (* This would add GR to the database and it would make sure it is understood correctly *)

#[unsafe]  Trocq Register D : mydb. (* Disables warning when D is registered to mydb *)

(* Database inclusion *)
Trocq Register DB mydbA mydbB : mydb1 mydb2. (* Links mydbA and mydbB to be included in mydb1 and mydb2 *)

(* Prove directly *)
Trocq Prove A at T ~ B. (* Opens a proof goal for [[T]] A B. Creates a Gref and adds it to database core *)
Trocq Prove A at T. (* Opens two proof goals for B : tr(T) and [[T]] A B. *)
#[because=truc_R] Trocq Prove A at T ~ B. (* Same as above, the created Gref has name truc_R *)
Trocq Prove A at T ~ B : mydb. (* Same as above, but we add the gref to the database mydb *)
Trocq Prove A at T ~ B : . (* Same as above, but we don't add the gref to any database *)

(* Registering axioms *)
Trocq Axiom axiom. (* Trocq should detect what kind has this axiom (whether it is univalence or funext) *)

(* Calling the `trocq` tactic in proof mode *)
trocq. (* By default, trocq with core *)
trocq with *. (* Emits warning: Which db actually used *)
trocq with mydb.
trocq using RNat. (* like Register + with but locally *)
trocq using *. (* Later ? Register all in local context *)
trocq to term.
etrocq. (* Same syntax as above, adds every remaining evar that cannot be computed as a goal. For example, when Trocq has a gref with no translation, or if the gref has a translation which is not strong enough. *)

(* Calling the full parametricity translation *)
(* This hooks the `derive` vernac that already exists in coq-elpi *)
(* That's why we can't change the interface as we want *)
#[with=(mydb)] derive truc.
#[using=(RNat)] derive truc.
#[to=blabla] derive truc.
#[at=aterm] derive truc. (* Or list of classes *)
#[as=truc'] derive truc.
#[because=truc_R] derive truc.
#[db= "mydb"] derive truc.

(* Activate coercion hooks *)
Trocq Coercion On. (* Activates the hook with database core *)
Trocq Coercion On with db1 db2. (* Activates the hook with databases db1 and db2 *) 

(* Prints *)
Trocq Print Translations. (* Prints translations in core *)
Trocq Print Translations A. (* Prints translations in core for gref A *)
Trocq Print Translations A with mydb. (* Prints translations in mydb for gref A *)
Trocq Print Translations with mydb. (* Prints all translations in mydb *)
Trocq Print Translations with *. (* Print all translations in every db -- This may be overkill *)
Trocq Print DB. (* Prints the name of every databases with their inclusion graph *)

(* Logging *)
Trocq Logging off. (* Trocq is silent except for Rocq warnings/errors and printing *)
Trocq Logging a b. (* Activates logging for modules a and b *)
Trocq Logging a -b. (* Activates logging for a and disables logging for module b *)

(* Help Message*)
Trocq Usage.

Questions:

• Should databases be identified by string or by grefs ?
• Should core be excluded when not specified, or should we add a special argument no-core ? Or maybe a special database ?
• The questions i raised in this message have not been answered

(Personal references about how to implement the things above in Elpi)

The following code sample show an example on how to do it in Elpi and how we could use it.

From elpi Require elpi.

Elpi Tactic trocq.param44.
Elpi Accumulate lp:{{

solve (goal Ctx _ G Statement [trm From, trm To]) [] :-
  if (var G) (G = {{ Type}}) true,
  Statement = {{ True }}.

}}.
Elpi Export trocq.param44.

Lemma foo : trocq.param44 bool nat.
Check param44.

nat bool.

(this example is wrong, we should use trocq.param [44] 44 list array for example)

For creating a goal directly, here's the API, using api in this example, which is documented in README of coq-elpi

[MysaaJava]

There should also be a vernac that runs trocq on the body of any gref.
This is a possible interface.

Definition double : nat -> nat := fun x => x + x.

Trocq Derive double.

(*
    What trocq does: 

    Fetch gref ctx -> double : T_double := t_double
    We annotate T_double at raw -> AT_double
    param t_double @ AT_double ~ t_double' because t_double_R

    Definition double' «: tr(AT_double)» := t_double'
    Definition double_R : [[AT_double]] double double' := t_double_R

    -> double' : N -> N
    -> double_R : forall x : nat, forall x' : N,
        forall xR : RN x x' -> RN (double x) (double x')
*)

Trocq Derive double at [04].
(*
    We annotate T_double with [04] instead of raw
    If we translate something that has `Type` in its type

    <!> Should we give Classes,OutClass, or just AllClasses ?
*)

Trocq Derive double to t_double'.
(* 
    We use t_double' as given, possibly with evars 
    t_double' is a term
*)

Trocq Derive double as double' because doubleR.
(*
    Gives the names of the two grefs that will be created.

    <!> `as` should be mandatory. Should `because` ?
*)

Trocq Derive double with A B C.
(*
    Same as `trocq with`
*)

[CohenCyril]

We should be reusing the generic derive hook system. With attribute for renamings eg #[as="double'", because="doubleR"].

[MysaaJava]

Yes for hooking the derive system, but isn't it weird that by default, we don't give explicitly the name of the objects we add to the global environment ? Doesn't seem very stable.
It seems that Rocq constructs do that, but it seems weird and error-prone to have automatic generation of names.

This would be the interface ?

derive double.
derive N_rect at [04].
derive double to t_double'.
derive double with A B.
#[as="double'", because="doubleR"] derive double.

Should we use derive like this, and keep Trocq Derive with as and because mandatory ? This way we have an «old» interface that can create things in the global environment, and a «new» interface that would avoid doing such things.

[MysaaJava]

#[db = "core"] Trocq Register A B C. (* By default, db=core *)
#[db = "mydb"] Trocq Register A B C. (* Create or add to database mydb *)
#[db = "mydb"] Trocq Register D E. (* Adds them to the database *)

trocq. (* By default, trocq with core *)
trocq with *. (* Emits warning: Which db actually used *)
trocq with mydb.
trocq using RNat. (* like Register + with but locally *)
trocq using *. (* Later ? Register all in local context *)
trocq to term.

#[with=(mydb)] derive truc.
#[using=(RNat)] derive truc.
#[to=blabla] derive truc.
#[at=aterm] derive truc. (* Or list of classes *)
#[as=truc'] derive truc.
#[because=truc_R] derive truc.
#[db= "mydb"] derive truc.

Here's what could be the interface

[MysaaJava]

We could add something like #[db = "otherdb"] Trocq RegisterDB mydb to add every translation in mydb to otherdb.

[CohenCyril]

We could add something like #[db = "otherdb"] Trocq RegisterDB mydb to add every translation in mydb to otherdb.

Or to be generic and compositional, factoring in Trocq Register in one command and reusing the semantics of with and using:
#[db="mydb"] Trocq using A B C with mydb1 mydb2...

[MysaaJava]

I am not sure that it's clear that this with adds all translations of the databases into mydb.
Also it makes unclear where is the limit between using and with (if you have a GRef named with)

[MysaaJava]

Assia proposed a Trocq Coercion vernac, where someone could register simple "functions" translations.
We could make it so that Trocq Coercion recognized terms types like A -> B or forall A B, (A -> B) -> (L A -> L' B).
Some issues :

• What should the second one be translated to ? Box^10 -> box^10 ? Box^10->box^40 ? Box^40->box^40 ? All of them ?
• There is no error message when coercion fails. Then this "user friendly" interface has hidden output which defies the point.
• This could just be handeled by Trocq Register

This feature can be useful for demonstrations of the coercion feature

[bousmahawassel]

For my PR on the rework of databases, this is what I've implemented:

Trocq Register DB gref. (* gref is now registered as a database in Trocq *)
Trocq DB Include gref1 gref2 Into gref.
(* gref1 and gref2 are now included into gref ; when using `trocq with gref`,
 it will also pull all translations registered in gref1 and gref2. 
This *does not* create a snapshot of gref1 and gref2 ; in particular, 
modifying gref1 may change the behavior of gref *)
Trocq Use Witness1 Witness2 : gref1 gref2. 
(* Add both witnesses to both databases. This should emit 4 warnings, since
we modify 4 times a database already included into another database, which
could get affected as a side effect *)
(* This syntax resembles the one of `Hint Resolve`, since it's a parallel we already
have between `trocq with` and `auto`/`eauto` *)

Trocq Coercion On with gref1 gref2. (* activates coercion, using databases gref1 and gref2 *)

There should be an attribute to add to Trocq Use to silence the warnings, but I don't know what shape to give to it.