7
$\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 @.

Improve this question
$\endgroup$
6
  • $\begingroup$ Can you share any concrete example where the problem occurs? $\endgroup$
    – Bubbler
    Commented Mar 10, 2022 at 4:23
  • $\begingroup$ Updated the question. Thanks @Bubbler $\endgroup$
    – lyfeng
    Commented Mar 10, 2022 at 14:04
  • 1
    $\begingroup$ Let abt := @abt 𝒳.? $\endgroup$
    – Mike Shulman
    Commented Mar 11, 2022 at 1:46
  • 1
    $\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
    Commented Mar 12, 2022 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$
    – Mike Shulman
    Commented Mar 13, 2022 at 16:41

1 Answer 1

Reset to default
3
$\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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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