The Coq mailing list

[Roberto Zunino <roberto.zunino AT unitn.it>]

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.