coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Error: U is bound to a notation that does not denote a reference.
Chronological Thread
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Error: U is bound to a notation that does not denote a reference.
- Date: Fri, 5 Jun 2015 13:37:34 -0400
Have you tried defining [Local Ltac unfold_U := unfold U in *.] above your [Local Notation U := ...]?
Another thing you could do is make an [unhold_head] tactic that strips off arguments:
Ltac unfold_head T :=
idtac;
lazymatch T with
| ?f ?x => unfold_head f
| _ => unfold T in *
end.
-Jason
On Jun 5, 2015 8:08 AM, "Christian Doczkal" <doczkal AT ps.uni-saarland.de> wrote:
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
- [Coq-Club] Error: U is bound to a notation that does not denote a reference., Christian Doczkal, 06/03/2015
- Re: [Coq-Club] Error: U is bound to a notation that does not denote a reference., Jason Gross, 06/05/2015
Archive powered by MHonArc 2.6.18.