The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Aurore Collomb wrote:
Bonsoir,

 As-tu les définitions préalables ?

 une première question :
  Ne serait-ce pas "Coinductive" qu'il faudrait mettre ?

  ton type inductif à un seul constructeur récursif me parait bien vide :
 on pourrait même prouver que
  bisim m c m1 c1 -> False


  Ensuite, une preuve comme celle que tu voudrais faire est une preuve
par coinduction (avec la tactique cofix)

  Une bonne source d'info est le tutorial d'Eduardo Gimenez.
  Pourrais-tu envoyer les déclarations préalables à la définition de
bisim.

  Sur http://www.labri.fr/Perso/~casteran/CoqArt/co-inductifs/index.html
  Il y a aussi toute une série d'exemples


Pierre



> 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



--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran