The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Tue, Jul 29, 2014 at 10:54:15AM +0200, Cedric Auger wrote:
> Now for the how to fix it, there are multiple solutions:
> - the local one: change the terms to be syntactically the same.
>   Useful tactics: change, fold, unfold (and probably others); these tactics
> often allow to target a specific location («at» keyword) of a specific
> hypothesis («in» keyword)
>   Examples: «unfold sf in H7; rewrite H7.», «fold sf; rewrite H7.», «change
> (list (sum non_terminal terminal)) with sf; rewrite H7.»
> - avoid use of type aliases (like sf). This is generally a bad idea, as you
> will have to be quite verbose, and the terms will be big (this is likely to
> degrade performances).
> - monomorphize your code (ie. use specialized functions). Thus a
> "Definition sf_last : list sf -> sf := fun (l:list sf) => @last sf l []."
> and then use "sf_last l" in your lemma would probably have solved your
> problem.
> 
> In practice, I most often use the 1st proposed solution. It is the more
> practical. 2nd solution is a bad one from my point of view, and 3rd
> solution can be used for some functions, when you think that the use of
> your first solution arise way too often.

Let me add that there is no good reason for the tactic to fail here.
If "list ..." and "sf" are convertible then they are the very same term.

In the implementation of the rewrite tactic that is part of ssreflect
the conversion relation is taken into account.  If this annoyance is
very recurrent in your scripts it may be worth giving it a try.

Best,
-- 
Enrico Tassi