6
$\begingroup$

If I had a module declared as follows in file A.v:

Section A.
  Context {𝒳 : Set}.
  Inductive abt := Abt_leaf (x : 𝒳) | Abt_node.
End A.

And in another file, B.v, I had:

Require Import A.
Definition 𝒳 := nat.
Inductive typ := Tpe_num | Typ_str.
Definition typ_to_abt (t : typ) : abt (* @abt 𝒳 *) := Abt_node.

The implicit arguments in abt when defining typ_of_abt can't be inferred.
How could I let Coq know I always want abt to be @abt 𝒳 in B.v? The intent is to avoid explicitly specifying them using @.

$\endgroup$
6
  • $\begingroup$ Can you share any concrete example where the problem occurs? $\endgroup$
    – Bubbler
    Mar 10 at 4:23
  • $\begingroup$ Updated the question. Thanks @Bubbler $\endgroup$
    – lyfeng
    Mar 10 at 14:04
  • 1
    $\begingroup$ Let abt := @abt 𝒳.? $\endgroup$ Mar 11 at 1:46
  • $\begingroup$ @MikeShulman It is a solution. I think Notation also works. But both need to be repeated for every definition such as abt (when there are many) in A.v. I wonder if there's a more concise solution. $\endgroup$
    – lyfeng
    Mar 12 at 1:26
  • $\begingroup$ Ah. I don't know a better solution in Coq -- I think in Agda you can do that by passing a parameter to a module. You could conceivably do that in Coq too, but Coq's modules are more heavyweight, and you might run into issues with generativity. $\endgroup$ Mar 13 at 16:41

1 Answer 1

2
$\begingroup$

Not sure how robust that is, but you can do something quite nice using typeclasses.

Section A.
  Class leaf_type := X : Type.
  Context `{L : leaf_type}.
  Inductive abt := Abt_leaf (x : X) | Abt_node.

End A.

Section B.
  #[local] Instance nat_leaf : leaf_type := nat.

  Inductive typ := Tpe_num | Typ_str.
  Definition typ_to_abt (t : typ) : abt := Abt_node.

End B.

To elaborate on what is happening here, we are first declaring a class leaf_type, that Coq will try to infer on its own automatically whenever it can, and abt makes use of that typeclass. In section B, we put this to work: we declare nat as a #[local] instance, so that whenever an implicit argument of type leaf_type is encountered in that section, Coq will find the local instance nat and be happy with it. Once you close the section, the instance is gone and you can declare another one later on.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.