The Coq mailing list

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

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?

Here is the example code:

<<<
Require Import Program.

Definition decidable P := {P}+{~P}.
Definition decidable2 P := {b:bool | if b then P else ~P}.
Definition sumbool_of_sigbool A (b : decidable2 A) : decidable A :=
  match b with
    | exist true H => left H
    | exist false H => right H
  end.
Definition sigbool_of_sumbool A (s : decidable A) : decidable2 A :=
  match s with
    | left H => exist (fun b : bool => if b then A else ~A) true H
    | right H => exist _ false H
  end.
Coercion sumbool_of_sigbool : decidable2 >-> decidable.
(*Coercion sigbool_of_sumbool : decidable >-> decidable2.*)

Program Fixpoint eq_nat_dec m n : decidable (m=n) :=
  match m,n with
    | 0, 0 => true
    | S p, S q => eq_nat_dec p q
    | _, _ => false
  end.

(* ==> ERROR : The term "true" has type "bool" while it is expected to
have type "decidable (0 = 0)". *)

>>>

Thanks in advance,
        -m