The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 09 Jul 2012 09:09:24 -0400,
Adam Chlipala 
<adamc AT csail.mit.edu>
 a écrit :

> On 07/09/2012 09:03 AM, Denis Cousineau wrote:
> > I've found that the tactic subst  only works with equations in
> > contexts that concern variables that were quantified in the goal,
> > and not global parameters. 
> 
> I imagine this issue hasn't bothered others because use of global 
> parameters is strongly discouraged; it's really against the spirit of 
> constructive logic!
> 
> But, you can easily get [subst] to behave as you wish for parameter
> [x] by running:
>      generalize dependent x; intros; subst.
> 

I have reported a similar bug here (not with subst/rewrite, but some
hacky stuff I had to do to destruct a parameter…)
https://coq.inria.fr/bugs/show_bug.cgi?id=2243

Personnaly, I do not discourage use of global parameters. It is often
useful when you have many of them and do not want to collect them in
some artificial record, and do not want to pass them explicitely in
each definition you pose.

Furthermore, in case of closures, I am not sure what is the most
readable between:
(*1*)
Section Map.
Variable A B : Type.
Variable f : A → B.

Fixpoint map (l : list A) : list B :=
  match l with
  | nil => nil
  | a::l => (f a)::(map l)
  end.
End Map.

and:
(*2*)
Definition map {A B : Type} (f : A → B) :=
  fix map (l : list A) : list B :=
  match l with
  | nil => nil
  | a::l => (f a)::(map l)
  end.

I tend to use (*2*), but don't discourage use of (*1*)
and prefer both of them to:

Fixpoint map {A B : Type} (f : A → B) (l : list A) : list B :=
  match l with
  | nil => nil
  | a::l => (f a) :: (map f l)
  end.

Furthermore, there is this funny bug, where I do not know how to deal
without Section or removing implicit flag:
https://coq.inria.fr/bugs/show_bug.cgi?id=2838