The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hello Everyone,

I sometimes use "Local Notation" to hide arguments that remain constant
throughout a section. A contrived minimal example would look as follows:

Require Import ssreflect.

Definition U {T} (s : list T) := app s s.

Section Foo.
  Variables (T:Type) (x : T).
  Local Notation U := (U (cons x nil)).

  Lemma foo : length U = 1 -> False.

As a preprocessing step before calling an automation tactic, I want to
unfold all occurrences of U. However, using "unfold U in *" fails.
Ssreflect's "rewrite /U" succeeds in unfolding U, but requires explicit
naming of all hypothesis, which I'm trying to avoid.

  Lemma foo : length U = 1 -> False.
  Proof.
    intros H.
    (* unfold U in *. *)
    (* Error: U is bound to a notation that does not denote a reference. *)
    (* rewrite /U in * *)
    (* Error: assumptions should be named explicitly *)
    rewrite /U in H. (* unfolds (U (cons x nil)) *)
  Abort.

I tried using the following piece of Ltac:

Ltac unfold_U :=
(repeat progress match goal with
                  | [H : context[U] |- _] => rewrite /U in H
                 end); rewrite /U.

This works for the particular U defined above. If I try to abstract "U",
I get the same error as when calling "unfold U in *"

Is there anything else I can do? (This is on Coq 8.4)

-- 
Regards
Christian