Avoid implicit arguments of Fixpoint from becoming explicit in proof mode

user_7013880 0
Viewed 79

Is there a way to enforce Fixpoint implicit arguments to remain implicit in proof mode?

Example:

Fixpoint foo {a : Set} (l : list a) : nat :=
  match l with
  | nil => 1
  | _ :: xs => ltac:(exact (1 + foo _ xs))
                                   ^^^  
end.

But I would like to write

Fixpoint foo {a : Set} (l : list a) : nat :=
  match l with
  | nil => 1
  | _ :: xs => ltac:(exact (1 + foo xs))
  end.
coq
1 Answers

As people have been saying I don't think it will be implemented but in some cases I believe you can circumvent the issue using sections.

From Coq Require Import List.
Import ListNotations.

Section Foo.

  Context {a : Set}.

  Fixpoint foo (l : list a) : nat :=
    match l with
    | nil => 1
    | _ :: xs => ltac:(exact (1 + foo xs))
    end.

End Foo.

Note that this is equivalent (in that it produces the same definition) as:

Definition foo' {a : Set} :=
  fix foo' (l : list a) : nat :=
    match l with
    | nil => 1
    | _ :: xs => ltac:(exact (1 + foo' xs))
    end.

Here the trick is more explicit, you take the argument a : Set before doing a fixed-point.

Of course this only works when the implicit argument in question is uniform in the definition.

user_12759750
Related