The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 13 Mar 2013 19:08:32 +0100,
Roberto Zunino 
<roberto.zunino AT unitn.it>
 a écrit :

> While playing with Coq, I was surprised to see that the following
> definition type checks:
> 
> Require Import Bool.
> Definition prove_true (b : bool) : option (b = true) :=
>   match b with
>   | true  => Some (eq_refl true)
>   | false => None
>   end
> .
> 
> The above looks strange to me because (eq_refl true) has type
> (true=true) which unifies with (b=true) only under the assumption
> that b unifies with true. That assumption is intuitively provided by
> the match, but how this actually works is not yet clear to me. For
> instance, it would seem possible to rewrite the above code as
> 
> Definition prove2_true (b : bool) : option (b = true) :=
>   match b with
>   | true  => @Some (b = true) (eq_refl true)
>   | false => None
>   end
> .
> 
> But this does NOT type check, as I originally expected:
> 
>    The term "eq_refl true" has type "true = true"
>    while it is expected to have type "b = true".
> 
> I am unable to pass an explicit argument to @Some to make it type
> check.
> 
> Further, I tried the following:
> 
> Definition prove_bool (b : bool) : sum (b = true) (b = false) :=
>   match b with
>   | true  => inl (b = false) (eq_refl true)
>   | false => inr (b = true)  (eq_refl false)
>   end
> .
> 
> This does NOT typecheck too, as expected:
> 
>    The term "inl (b = false) (eq_refl true)" has type
>    "((true = true) + (b = false))%type" while it is expected to have
> type "((?16 = true) + (?17 = false))%type".
> 
> Is there some way to write prove_bool ?
> 
> Thank you,
> Roberto.

That is normal.

Just that Coq is sometimes smart and does not need all the required
stuff.

In the manual, see the pattern matching with "as … in … return …"
clause.

Definition prove_true (b : bool) : option (b = true) :=
  match b with
  | true  => Some (eq_refl true)
  | false => None
  end
.

must be read as:

Definition prove_true (b : bool) : option (b = true) :=
  match b as b0 return option (b0 = true) with
  | true  => @Some (true = true) (@eq_refl bool true)
  | false => @None (false = true)
  end
.

Same remark for your sum type.