The Coq mailing list

["Birgit Fruth" <birgit AT fruth.org>]

Thank you both. This helped a lot.

But is there a possibility to give a value to a matching construct like I  
use in "autotree", too? I'd like to use it for Lemma "always_q_autotree".
Or have you a suggestion how I can get rid of these dependencies in the  
arguments?
I' ve search already in the Coq'Art book, but I couldn't find something.

I have to do this at university and I really want to learn Coq but there's  
no one here, who has experience with Coq (but some who'd like to have). So  
I would be grateful if you could help me again. Thanks for your help!

Birgit


Am 06.02.2008, 18:03 Uhr, schrieb Stephane Glondu 
<steph AT glondu.net>:

> Birgit Fruth a écrit :
> > 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.
>
> Let me remind the problematic subgoal:
>
>    t : LTree (states A0)
>    t' : LTree (states A0)
>    ============================
>     Atomic_tree A0 p (LBin s0 t t')
>
> and the type of Atomic_tree_intro is:
>
> forall (A : automaton) (P : Prop) (a : states A)
> (t1 t2 : LTree (states A)),
> (ref A a -> P) -> Atomic_tree A P (LBin a t1 t2)
>
> and the problem is "apply Atomic_tree_intro" fails with the error:
>
> Error: Impossible to unify "Atomic_tree ?5875 ?5876 (LBin ?5877 ?5878  
> ?5879)" with "Atomic_tree A0 p (LBin s0 t t')"
>
> However, "apply (Atomic_tree_intro A0)" succeeds. I suspect the  
> unification fails because of the dependance in A in the types of the  
> arguments.
>
> Cheers,



--
Erstellt mit Operas revolutionärem E-Mail-Modul: http://www.opera.com/mail/

Attachment: uebung.v
Description: Binary data