The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 11/02/2013 21:31, J. Ian Johnson wrote:
> IMO, the semantics of if in Coq is terrible. You want to use match
> just about anywhere.

There is no difference between an « if » and a « match » construct. The
former is syntactic sugar for the latter. More precisely,

if e return T then u else v

is nothing more than:

match e return T with
| c1 x1 ... xm => u
| c2 y1 ... yn => v
end

where c1 and c2 are the two constructors of the type of e.

On 11/02/2013 21:23, Patricia Peratto wrote:
> Is it possible to define an if expression that gives values of
> different types in cases true and false?

Maxime has answered to this: you need to use the return clause of a 
match, or use the bool_rect predicate, which is an instance of it.

Definition bool_rect
  (P : bool -> Type) (u : P true) (v : P false) (b : bool) :=
match b return P b with
| true => u
| false => v
end.

It is quite difficult to grasp the typing rule of the dependent match, 
but the idea is that you in each branch, b is unified with the 
corresponding constructor. Maybe Chlipala's book is a good thing to 
start with.

> Definition type1 (b:bool) : Set :=
> _ifT Set b nat bool.

It is a bad practice to explicitely use the « Set » universe, unless you 
know what you're actually doing. Just use « Type », or better, don't 
specify it at all.

> But I get the error message Error: In environment b : bool The term
> "0" has type "nat" while it is expected to have type "type1 b". The
> question is how can I define function1 (using if).

Here O is the constructor of the unary integers, so it is not the type 
of a type, hence your construction does not type check.

I would write:

Definition _ifT (A B : Type) (b : bool)
  (e1 : A) (e2 : B) : if b then A else B
:= bool_rect (fun (b : bool) => if b then A else B) e1 e2 b.

and use it like:

Definition function1 (b:bool) := _ifT bool nat b true 0.

Hope it helps,
PMP