The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Actually, the current state of Ltac vs. symbol definedness is weaker 
than what I wrote below.  For instance, while this works:

Goal True.
try let x := uconstr:(JMeq) in idtac.

This does not:

Ltac detect := try let x := uconstr:(JMeq) in idtac.

So, it doesn't seem possible to have a tactic detect any kind of symbol 
definedness in its dynamic (calling) environment.:-(


I will file an enhancement request in bugzilla....

-- Jonathan

On 07/06/2016 02:01 PM, Jonathan Leivent wrote:
> ...
> For the "using JMeq" case when not all indexes are decidable - this 
> leads to an interesting general question.  Some tactics are able to 
> conditionally use something, like JMeq, only if it was previously 
> Required, and do something else instead if not - but those are 
> probably all using plugins to accomplish this choice. How would this 
> be done in pure Ltac?
>
> AFAICT, the only non-plugin mechanism(s) that could be used for such 
> "do things one way if X is not Required, else another way if X is 
> Required" would be based on typeclasses, canonical structures, or 
> hints - but these all require some amount of declaration to exist 
> already in X to set up the search.
>
> Would it make sense to have a way for Ltac to attempt to determine if 
> some things are Required or not, without relying on particular 
> declarations (instances or hints)?  For example, the following does 
> not work:
>
> Goal True.
> Fail try let x := uconstr:(JMeq.JMeq) in idtac.
>
> because Coq complains very early that JMeq.JMeq isn't in the current 
> environment - earlier than uconstr formation, evidently. It does work 
> for just an unqualified "JMeq" alone, however:
>
> Goal True.
> try let x := uconstr:(JMeq) in idtac.
>
> so it is the lookup of id qualifiers that is happening too soon for 
> uconstr - and it thus is possible to conditionalize on Require Import, 
> just not on Require alone.
>
> Would it make sense if uconstrs were allowed to refer to undefined 
> qualified symbols, with the requirement that their qualifications be 
> defined deferred just as is done for unqualified symbols? Should there 
> be some kind of "moral equivalence" between the use of an unqualified 
> symbol and a qualified one when both are undefined?
>
> Or, would it be better to have another form that does this environment 
> querying?
>
> -- Jonathan