Stream: MetaCoq

Topic: Reification of operations on Z

Chantal Keller (Aug 31 2022 at 09:53):

Hello
When executing:

Require Import String.
From MetaCoq.Template Require Import utils All.
MetaCoq Run (tmQuote BinInt.Z.add >>= tmPrint).

it is quoted as BinIntDef.Z.add. As far as I understand the Include command, BinIntDef.Z.add is however syntactically different from BinInt.Z.add, isn't it?
This is tested with Coq 8.13 and Metacoq 1.0~beta2+8.13.
Thanks!

Yannick Forster (Aug 31 2022 at 10:08):

My understanding also is that they are syntactically different, for instance Check BinInt.Z.add = BinIntDef.Z.add. yields not the exactly same printout on the left and right side. However, the two are convertible, and this even holds for inductive types obtained through Include. I guess that MetaCoq somewhere does a little bit too much unfolding when quoting, the bug also seems present in more up-to-date versions. @Tan Yee Jian is currently revamping all of the quoting of modules, we can probably resolve this issue as part of the re-design

Gaëtan Gilbert (Aug 31 2022 at 10:13):

they are syntactically equal

Require Import String.

Goal False.
  constr_eq BinInt.Z.add BinIntDef.Z.add. (* succeeds *)

Janno (Aug 31 2022 at 10:16):

Locate can also help to figure these things out: Locate BinInt.Z.add yields:

Constant Coq.ZArith.BinInt.Z.add (shorter name to refer to it in current context is Z.add) (alias of BinIntDef.Z.add)

Chantal Keller (Aug 31 2022 at 11:11):

So Include does not create a copy, but an alias?
How do we recognize such aliases in MetaCoq? And in OCaml?

Gaëtan Gilbert (Aug 31 2022 at 11:13):

in ocaml it is the difference between Constant.canonical and Constant.user

Chantal Keller (Aug 31 2022 at 11:20):

How can I check that two econstr are equal in the sense of the tactic constr_eq?

Gaëtan Gilbert (Aug 31 2022 at 11:29):

Tactics.constr_eq ~strict:false

Yannick Forster (Aug 31 2022 at 11:48):

I guess you want to do it in MetaCoq @Chantal Keller ? Then you might be able to use the technique described here, just simplified a little: https://github.com/MetaCoq/metacoq/wiki/Calling-Ltac-from-the-TemplateMonad

Yannick Forster (Aug 31 2022 at 11:52):

From MetaCoq.Template Require Import All.
From MetaCoq Require Import bytestring.
Require Import List.
Import MCMonadNotation ListNotations.
Open Scope bs.

(* Definitions that can be outsourced to a central file *)

MetaCoq Run (tmCurrentModPath tt >>= tmDefinition "solve_ltac_mp").

Definition solve_ltac (tac : string) {args : Type} (a : args) (Goal : Type) := Goal.
Existing Class solve_ltac.

Definition tmDef name {A} a := @tmDefinitionRed name (Some (unfold (solve_ltac_mp, "solve_ltac"))) A a.

(* Local definition adding a new tactic *)

Hint Extern 0 (solve_ltac "tauto" tt _) => unfold solve_ltac; tauto : typeclass_instances.

Hint Extern 0 (solve_ltac "constr_eq" (?x, ?y) _) => constr_eq x y; exact tt : typeclass_instances.

(* Calling this tactic from the monad *)

Require Import String.
From MetaCoq.Template Require Import utils All.
MetaCoq Run (tmQuote BinInt.Z.add >>= tmPrint).

MetaCoq Run (res <- tmInferInstance None (solve_ltac "constr_eq" (BinInt.Z.add, BinIntDef.Z.add) unit) ;;
             match res with
             | my_Some _ => tmPrint "equal!"
             | my_None => tmFail "not equal"
             end).

Fail MetaCoq Run (res <- tmInferInstance None (solve_ltac "constr_eq" (fun x : nat => S x, fun x : nat => x + 1) unit) ;;
             match res with
             | my_Some _ => tmPrint "equal!"
             | my_None => tmFail "not equal"
             end).

Matthieu Sozeau (Aug 31 2022 at 15:20):

Right now MetaCoq does not consider the aliasing status: I think it only produces entries/references to canonical names

Chantal Keller (Aug 31 2022 at 15:41):

Thanks to all of you, that is very clear now :-)

Last updated: May 31 2023 at 02:31 UTC