The Coq mailing list

[CHA Reeseo <reeseo AT formal.korea.ac.kr>]

2009/12/24 Babak Moazzez 
<babakmoazzez AT yahoo.com>:
> 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.

Assuming both p and q have a specific type T, one of simple ways is
constructing an equality test function of type "T -> T -> bool" and using
it instead of eq (=).

Or, any proof of "forall (x y:T), {x = y}+{x <> y}" can also be used as a
test function with IF-THEN-ELSE, guaranteeing that it cannot go wrong.
Coq theories constain various theorems named "*_eq_dec" or something.

If you want a polymorphic union function of type "forall T, list T ->
list T -> list T", you may also need a polymorphic equality test function
of type "forall T, T -> T -> bool" or "forall T, forall (x y:T),
{x = y}+{x <> y}".  AFAIK, the latter cannot be proven (in intuitionistic
setting).  The former type is inhabited (e.g., fun _ _ _ => true) but will
not meet your requirement.

-- 
CHA Reeseo
http://www.reeseo.net/