The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Birgit Fruth wrote:
> Hallo!
>
> I try to expand the examples of Coq'Art chapter 13. So I tried to 
> build a lemma which says, that a special automaton-tree fulfills a 
> property. (There is already one for LLists.)
> It works only for empty trees. So I think there is a type-confict with 
> s0. What can I do? The lemma is called satisfies_p.
>
> Could you please help me?
> Thank you!
>
> Birgit
> --Erstellt mit Operas revolutionärem E-Mail-Modul: 
> http://www.opera.com/mail/
Dear Birgit,

In your example, there is no type conflict, but for a reason that I did 
not have time to explore yet,
the system does not see see s0 indeed has type (states A0).  You can 
make some progress by instantiating
the arguments to the theorem Atomic_tree_intro.  In my case, I was able 
to make one step of progress
in your proof by typing

"apply (Atomic_tree_intro A0)."

instead of "apply Atomic_tree_intro."  as you did.

Cheers,

Yves