The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

> Quoting Babak Moazzez 
>Â <babakmoazzez AT yahoo.com>:
> 
> > Hi.
> >
> > I am trying to define a function in Coq that adds two lists  
> > together. for this purpose , I need to use a structure which is
> > very familiar in any programming language:
> >
> > if (p=q) then do ....
> >
> > but in Coq I cannot use this since (p=q) is not a boolean value
> > but just a proposition which needs to be proved if it is true.
> >
> > Can anybody tell me what to do?

For these purpouse, I think coq lacks some meta-programming features:
it would be very nice to have meta-types:
boolean_equality: forall (T: fully-computationnal-type), T -> T -> bool
boolean_equality_to_eq
: forall (T: fully-computationnal-type) (a b: T),
  if boolean_equality a b then a = b else a <> b

But it is way too complicate to implement (if implementable), for that
there is also an alternative using Type Classes; I am not very
familiar to them and I use to implement them manually (as they are
done in practice):

Record decidable_type (T: Type): Type :=
Dec_Type
{ beq: T -> T -> Type;
  beq_to_eq: forall (a b: T), beq a b = true -> a = b;
  beq_to_neq: forall (a b: T), beq a b = false -> a <> b;
  beq_reflexive: forall (a: T), beq a a = true;
  beq_symmetric: forall (a b: T), beq a b = beq b a;
        ...
}.

and then use some kind of functor:
Lemma make_decidable: forall (T: Type) (f: T -> T -> bool),
 (forall (a b: T), if f a b then a = b else a <> b) ->
 decidable_type T.
Proof.
...
end.

As an alternative, you can use modules:
Module Type decidable.
 Parameter T: Type.
 Parameter beq: T -> T -> bool.
 Parameter beq_to_eq ...
 ...
 Ltac rw := repeat
        match goal with
        | [H : beq ?x ?y = true |- _] =>
                (clear H x y) ||
                (clear H x) ||
                (clear H y) ||
                (rewrite (beq_to_eq H) in *; clear H x) ||
                (rewrite <- (beq_to_eq H) in *; clear H y) ||
                (rewrite (beq_to_eq H) in *) ||
                (rewrite <- (beq_to_eq H) in *) ||
                idtac
        end.
 Ltac refl := repeat rewrite beq_reflexive in *.
End decidable.

Module Type decidable_kernel.
 Parameter T: Type.
 Parameter beq: T -> T -> bool.
 Parameter beq_to_eq ...
End decidable_kernel.


and a functor:
Module make_decidable (M: decidable_kernel): decidable
       with Definition T := M.T.
...
End make_decidable.

Record vs Modules:
Records can be generalized in types, and built "à la volée", wheras
        modules can't.
Module Types can contain tactics
 (which in fact are some "meta-functions"), which cannot belong to
 inductive types (yet), and should be faster.

So use one or the other is a matter of choice, depending of your use of
polymorphism and tactics.

---------------------------------------------------------------
go back to the main thread:

There are some cases of interest:
* you want to extract your program in a programming language
-> you can consider adding the following lines:
Axiom beq : forall {T : Type}, T -> T -> bool.
Extract Constant beq => (=).

Do not take care of the warning as beq can be inhabited (see Resseo
reply).

But if you want specification on this function, you may introduce
inconsistency, as you cannot prove anything on it, and have to rely
only on axioms you give.

* you use your function with only one type and don't bother with
  polymorphism, furthermore, you need some specification on it
  and like to use a boolean equality only here
-> follow the other replies; note that SSreflect uses a variant of
   {x=y}+{x<>y}, which I think can be slightly more interesting:
 Inductive eq_reflect (t1 t2 : t) : bool -> Set :=
 | reflect_true : (t1 = t2) -> eq_reflect t1 t2 true
 | reflect_false : (t1 <> t2) -> eq_reflect t1 t2 false.
   Some practice is required to use any of these versions and choose
   the best.

* you want some polymorphism, or use boolean equalities in many
  functions, so you don't want to pass your equality function and
  its specification everywhere
-> refer to the first part of this mail
 
> >
> > Thanks.
> >  Babak Moazzez
> > School of Mathematics and Statistics
> > Carleton University
> >
> > Address:
> > Room 4356, Herzberg Building
> > Carleton University
> > 1125 Colonel By Drive
> > Ottawa, ON K1S 5B6
> > Canada
> >
> > Web: www.math.carleton.ca/~bmoazzez
> >