The Coq mailing list

[Aurore Collomb <aurorecollomb AT chez.com>]

Bonjour,

Encore une question idiote.
Ayant terminer de definir la semantique de mon langage, je veux 
maintenant verifier qq proprietes, notamment que quelques actions de mon 
langage sont bisimilaires.

semcom definit ma relation de transition entre les etats et je declare 
une propriete bisim de la facon suivante :

Inductive bisim :  memory -> com  -> memory -> com -> Prop :=
   est_bisim :
       (c, c1, c',c1': com) (la : label)(m, m', m1, m1' : memory)
   (semcom m c la m' c') ->
   (semcom m1 c1 la m1' c1') ->
   (bisim m' c' m1' c1')
   -> (bisim  m c  m1 c1).

ou je suppose que si mes deux etats peuvent faire une transition 
etiquete par le meme label, et les etats atteints sont bisimilaires 
alors le tout est bisimilaire.

Puis je cherche a demontrer ma 1ere bisimulation :
Lemma bisim_null_A : (m:memory) (c2: com) (bisim m (seq null c2)  m c2).

Et en essayant d'appliquer "est_bisim" Apply est_bisim. Coq ne veut pas 
,  il ne veut pas prendre des valeurs pour les variables c' la m'...

Voila j'espere avoir ete claire...

Merci

Aurore Collomb

--
INRIA - VASY
655 av. de l'Europe
F-38330 Montbonnot Saint-Martin
Tel : 04.76.61.53.37
http://www.inrialpes.fr/vasy/people/Aurore.Collomb/