The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Je m'aperçois que mon message précédent n'était pas clair
(erreurs due à Mozilla et à ma fatigue de fin de semaine/année).

Une définition inductive ne contenant que des constructeurs récursifs
définit un type vide. Ce qu'on fait pour définir des bisimulations
est de prendre des types co-inductifs (on peut donc imaginer une
preuve de bisimulation comme une preuve infinie). La techno des types
co-inductifs est assez déroutante au départ, mais très amusante.

Il faudrait voir le tutorial d'Eduardo en premier, et les exemples
de  notre bouquin 
http://www.labri.fr/Perso/~casteran/CoqArt/co-inductifs/index.html

après (types de listes ou d'arbres finis ou infinis, définitions et 
preuves sur la bisimulation).

Pour le reste, il faudrait voir tes déclarations de types, et ta 
définition de semcom pour voir quels lemmes peuvent être prouvés
par ta relation de bisimulation, au moins que c'est une relation
d'équivalence.




Bon week end,
Pierre





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