Coq: adding implicit variables

Question

Suppose that I have a set of functions, each of which can depend on one or two implicit variables A B: Type. How can I specify this? I.e. add these variables to their variable list and set them as implicit.

The most obvious way is to add {A B: Type} to their definitions. However, in real life and moderately complicated developments such shared lists of implicits can easily be 6-10 entries long and include complicated types, thus making function definitions hard to read and even harder to understand their similarity or make change to mentioned types. Thus this solution is not applicable.

I could include all functions in a section or module and write Variables (A B: Type) etc in the beginning, but that would not make variables implicit and I would have to manually set arguments for all functions at the end of section. Even worse, that would make all variables shared. I.e. if I declare

Section sect.
  Variable A B: Type.

  Definition f (t: A -> Type) := (..).

  Definition g (t: A -> Type) (s: B -> Type) := G (f t) (f s).
End sect.

(G is some two-variable function) then g would not be accepted, since s is not in A -> Type, even though essentially f requires only an arbitrary type family.

I could make a section and declare Context {A B: Type}. That would make those variables implicit for all functions, but the sharing problem like in previous case would still remain. Thus I would have to arbitrarily split my functions into several sections so that I could call functions from Sect.1 with different values of their implicit arguments. This works, but is ugly, and I can easily imagine a situation where each section would have to be 2-3 functions long just so that I could call them properly.

Is there a better solution?

I'm not sure I understand the sharing problem. What would be the problem with using Context {A : Type} and declaring both f and g to take a A -> Type parameter? — Arthur Azevedo De Amorim
I am sorry, but I'm still confused. Couldn't you have changed the definition of G so that it also took types parameterized over A instead of B? — Arthur Azevedo De Amorim

John Wiegley John Wiegley · Accepted Answer · 2015-08-06T17:51:38

There are two things you can do that are less difficult:

Generalizable All Variables.

Definition g `(t: A -> Type) `(s: B -> Type) := G (f t) (f s).

Now you can use backtick, and it will automatically insert the implicit variables you need to make the definition valid. This is the most common way that I introduce implicits.

The other way is to follow your section with:

Arguments g : default implicits.

You'll need to repeat this for every defined term, but at least you don't need to name all of the arguments.

Coq: adding implicit variables

1 Answers