The Atelier Focal

Show Task #

Task #206 Erreur de typage Ã Coq.

Opened by François Pessaux (francois) - 28 May 2009
Last edited by François Pessaux (francois) - 28 May 2009

Task Type	Bug Report
Category	Compiler
Status	Unconfirmed
Assigned To	François Pessaux (francois)
Operating System	All

Severity	High
Reported Version	Current
Due in Version	Undecided
Percent Complete

Details

(Initialement trouvÃ© par LiÃªn)

Avec le fichier joint en attachement, Coq raconte:
Error while reading ./automata_3_bug.v :
File "./automata_3_bug.v", line 485, characters 37-49
Error:
In environment
A_T : Set
...
...
The term "rf_verify_e1" has type
"forall a a1 : A_T,
Is_true (rf_is_e1 a a1) ->
Is_true (_p_P_is_in_trace (_p_P_trace _p_P_origin _p_P_present_state) a1)"
while it is expected to have type "Prop"

Comment by François Pessaux - Thursday, 28 May 2009, 12:42pm

Ceci n'est pas Ã proprement parler un bug. En fait, le compilo devrait rÃ¢ler plutÃ´t que de laisser passer Ã§a et que ce soit Coq qui rÃ¢le. Donc il va falloir trouver un moyen de faire lever une erreur.

L'histoire est la suivante:
property verify_e1 : all a a1 in A,
is_e1(a, a1) ->
P!is_in_trace(P!trace(P!origin, P!present_state), a1) ;

property verify_e2 : all a a2 in A,
is_e2(a, a2) ->
~(P!is_in_trace(P!trace(P!origin, P!present_state), a2)) ;

property verify_nlim : all a a1 a2 a3 in A,
(~(!verify_e1) \/ ~(!verify_e2)) ;

verify_e1 et verify_e2 sont des propriÃ©tÃ©s. Ce sont des FAITS que l'on doit prouver. Il ne peuvent donc Ãªtre utilisÃ©s que pour faire DES PREUVES et non dans des ENONCES ! C'est un peu comme si on disait truc_reflexive => truc_symetric.
D'ailleurs, dans l'Ã©noncÃ© de verify_nlim qui est celui qui ne passe pas, on voit bien que l'on binde a a1 a2 a3 et que l'on ne s'en sert pas !
Si on autorisait ce genre de chose, la forme du truc obtenu serait quelque chose comme:
(all x in X, truc (x, x)) => (all a b in X, truc (a, b) => truc (b, a))

J'ai fait exprÃ¨s de mettre a et b dans le second membre pour montrer qu'il n'y a aucun rapport entre x et a.

Ce que voulait l'utilisateur est certainement de dÃ©finir des logical let pour verify_e1 et verify_e2.

Bon, maintenant, le compilo doit rÃ¢ler sur ce truc qui passe car le type ML d'une property est bool, donc Ã§a passe Ã la trappe sans faire d'erreur d'unification.