The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/07/2016 10:13 AM, Soegtrop, Michael wrote:
> Dear Guillaume,
>
> > Coq just checks that this is true for all the branches  of the "match"; if so, it 
> > assumes that it is also true for the "match" itself.
> Sorry, I don't get it. That is what I assumed Coq does until I saw your example, but how does Coq 
> check that (in my example below ) the branch term "1" has type "bool"?
>
> Definition foo2 (H : nat = bool) : bool :=
>    match H in (_ = t) return t with
>    | eq_refl => 1
>    end.

Here's a non-type-theorists view of what is happening: matches on 
equalities can only reduce when the equality is exactly eq_refl because 
otherwise the equality might be hypothetical - as in your nat = bool 
case.  Even assuming UIP, when there can only be one proof of the 
equality, there can also be no proof of it.  Hence, what the match above 
says is : in the imaginary world where we can prove nat = bool, 1 is a 
bool because it is a nat.

IMHO, the more interesting "feature" about Coq's logic is that it 
doesn't have universal UIP - hence it can't even assume an actual proof 
of x = x is always eq_refl, even though eq_refl is the only way to 
construct x = x.  And, other constructive-logic-based dependently-typed 
languages out there, such as Agda and Idris, do have UIP built in (via 
K, which is equivalent).  Coq seems to act in confusing ways when 
dealing with x = x.  Sometimes, when that x = x is alone, it can reduce 
it to eq_refl.  Other times, when there are multiple instances of x = x 
in a goal, it can only reduce one to eq_refl.  Also, other 
one-constructor fieldless Props are irrelevant  - as long as they don't 
have a type index.

For instance, one can prove forall (x:True), x = I, but not:

Inductive Foo : unit -> Prop := foo : Foo tt.

Goal forall (f : Foo tt), f = foo.


-- Jonathan