Coq: How do I create a bool from a decidable Prop?

Question

I want to structure my program as abstract modules, and write functions that use the abstract types. But I can't use match to destruct the abstract types, so I will have to create an inversion lemma of some sort, but I can't match on it either. I've tried to boil down my problem to this:

First create a Module Type that can be used by decidable types.

Require Import Decidable.

Module Type decType.
  Parameter T : Type.
  Axiom decT : forall (a b:T), decidable (a=b).
End decType.

Here is an example: nat is decidable. But the aim is to write plus etc. only addressing the abstract type. (I have removed the parameters zero, Succ and their requirements to make the example here minimal).

Require Peano_dec.

Module nat_dec <: decType.
  Definition T := nat.
  Definition decT := Peano_dec.dec_eq_nat.
End nat_dec.

Now to my question: I want to write a module parameterized on a decType module with a function that returns true if a=b and false otherwise. Since a and b are of a decType this should be decidable (and therefore computable, or?), but how to I write beq?

Module decBool (M: decType).
  Import M.
  Definition beq (a b:T) : bool :=
    ???
  .

End decBool.

My thinking so far is that I have to add a boolean function to the decType module type, something like this:

Module Type decType.
  Parameter T : Type.
  Axiom decT : forall (a b:T), decidable (a=b).
  Parameter decB : forall (a b:T), {a=b}+{a<>b}.
End decType.

and then define decB in the nat_dec module above.

Is this what one has to do (i.e. define the function decB)? Is it not possible at all to use the abstract fact that the type is decidable, without going through a function that returns bool?

score 4 · Accepted Answer · edited May 23 '17 at 10:34

You cannot write this function, because of the separation of propositions and computational objects in Coq (cf. this answer, for instance).

Notice that adding your decB parameter to your module makes the decidable axiom unnecessary, since you can use {P} + {Q} to derive P \/ Q.

I'd like to add a couple of related notes. First, I would avoid using the Coq module system for doing anything other than namespacing and writing opaque definitions. If you want to write parametric definitions, you are probably better off with dependent records, e.g.

Record eqType := {
  sort :> Type; 
  eqb : sort -> sort -> bool;
  eqbP : forall x y, eqb x y = true <-> x = y
}.

This is essentially the approach taken by Ssreflect. You can use canonical structures (like Ssreflect does) or type classes to make using these dependent records easier.

Second, you can write explicit eliminator functions to avoid having to resort to match. For instance, the nat_rect function allow you to write recursive functions on nat with higher-order arguments:

nat_rect : forall (T : nat -> Type),
             (* value for 0 *)
             T 0 ->
             (* body for recursive call *)
             (forall n, T n -> T (S n)) ->
             forall n, T n.

These functions are automatically defined for every inductive data type. They involve dependent types, but you can use them for doing non-dependently-typed recursion as well. Although that would be a bit inefficient, you can also use them for pattern matching by passing them functions that ignore the values of the recursive calls (in the example above, the T n argument of the second function argument).

Coq: How do I create a bool from a decidable Prop?

1 Answers1