The Coq mailing list

[Matthias Puech <puech AT cs.unibo.it>]

Hi Matthieu,
Thanks for your advises! You are right, it is more natural to use (left
_) and (right _) in this case.
bye,
        -m

Matthieu Sozeau wrote:
> 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