Implicit arguments propagation

0
votes

Is it possible in Coq to implicitly propagate implicit arguments?

Class C := { n : nat }.

Section Sec.
  Context {c : C}.
  Definition f := fun x => x + n.
End Sec.

Fail Lemma f_inc : forall x, f x >= x.

For example here, after the end of section Sec, c is implicit argument of f but it is not automatically inserted as implicit argument of f_inc, which uses f.

I know this can be achieved by inserting Context {c : C}. before the lemma but it would make c an axiom and I still need the possibility to instantiate it later. I could also open a new section with context c but I don't want to put the whole project inside sections because of scoping issues.

1
coq

1 Answers

1
votes

Every argument must be explicitly declared somewhere. This declaration can either appear in a section (as you did for f), or in the header of a definition, lemma statement, etc. You have a few options here:

  1. Bring f_inc inside the section where f is declared.

  2. Put f_inc inside its own section, where c : C is also in the context.

  3. Add c : C as an argument, implicitly or explicitly:

     Lemma f_inc {c : C} : forall x, f x >= x.

    You can also avoid having to name this argument explicitly, which is particularly useful when typeclasses are involved:

     Lemma f_inc `{C} : forall x, f x >= x.