The Coq mailing list

[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,

--
Stéphane