coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Roberto Zunino <roberto.zunino AT unitn.it>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Peculiar type checking
- Date: Wed, 13 Mar 2013 19:08:32 +0100
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.
- [Coq-Club] Peculiar type checking, Roberto Zunino, 03/13/2013
- Re: [Coq-Club] Peculiar type checking, AUGER Cédric, 03/13/2013
Archive powered by MHonArc 2.6.18.