The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 16 mars 10 à 14:24, Matthias Puech a écrit :

> Dear Coquists (Coqists?),
>
> I'm trying to use Program to prove the decidability of some  
> predicates,
> stated with [sumbool] but implemented in [bool]. Program doesn't like
> this, so I define a coercion from {b : bool | if b then A else ~A} to
> {A}+{~A}. And the other way around to be sure I'm not mistaken. Still,
> Program doesn't seem to see my [sumbool] as a [sig]! Is it a known
> issue? Or do I get it totally wrong (the most probable)?
> I know, with the coercions I could define the function with type [sig]
> and then use it as a [sumbool], but I was thinking it would be nice to
> have one canonical representative of the (multiple way to define the)
> "decidable" predicates, and coercions to it from the others. Is this
> concern futile? Is there another, beautiful way?

Dear Matthias,

The reason this does not work is that Program does not handle coercions
as you seem to expect. [eq_nat_dec] typechecks if you give it the type
[decidable2 (m=n)] as it can find a subset coercion from [bool] to
[{b:bool|...}] but when you try to coerce [bool] to [decidable] it is
unable to infer that there is a subset coercion path from [bool] to  
[decidable2]
and then a regular coercion from [decidable2] to [decidable]. The two
coercion systems simply do not work together that way and this would
require a substantial change to the existing coercion system. However,
you can force this transitive coercion using casts:

Program Fixpoint eq_nat_dec m n : decidable (m=n) :=
 match m,n with
   | 0, 0 => (true : decidable2 (0=0))
   | S p, S q => if eq_nat_dec p q then left _ else right _
   | x, y => (false : decidable2 (x=y))
 end.

The casts from [bool] to [decidable2] are handled by Program coercions
and the resulting [decidable2] values are coerced to [decidable] using
the declared [sumbool_of_sigbool] coercion. I would suggest sticking
to one representation when programming. If you chose [sumbool] you could
also write:

Program Fixpoint eq_nat_dec m n : decidable (m=n) :=
 match m,n with
   | 0, 0 => left _
   | S p, S q => if eq_nat_dec p q then left _ else right _
   | x, y => right _
 end.

Hope this helps,
-- Matthieu