[Why3-club] Coq driver

Guillaume Melquiond guillaume.melquiond at inria.fr
Tue Mar 18 06:17:38 CET 2014


On 18/03/2014 02:49, Jean-Jacques Levy wrote:

> 2- I do not get the point [you meant that you cannot use a type previously defined in a new one ??!!]. But now it works.

No, it is a bit more complicated; it happens when the definition of an 
inductive type crosses another inductive type. (Otherwise we would 
hopefully have encountered the bug much earlier.)

When you have "type t 'a = ...", the corresponding Coq inductive type 
requires a proof that 'a is not empty. So, when you have "type u = ... 
(t u)", Coq asks you to build a proof that u is not empty. But since you 
are in the process of defining u, you cannot prove yet that it is not 
empty. Hence the bug you encountered.

A possible fix is to move the type constraints from the polymorphic type 
definitions to the polymorphic function definitions. That would fix the 
issue above, but I don't know yet if that won't break something else.

Best regards,

Guillaume



More information about the Why3-club mailing list