The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jonathan,

> 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.

Thanks for sharing your insights - it is not that easy to get deeper into Coq 
after 40 years of using traditional programming languages having the semi 
mathematical education of a physicist.

Let's see how this applies to my original case:

    match plus_n_O 1 in (_ = y) return (t bool y) with
      | eq_refl => cons bool false 0 (nil bool)
    end : t bool (1 + 0)

The match term is:

    Check (plus_n_O 1).
    (* plus_n_O (S O) : @eq nat (S O) (Nat.add (S O) O) *)

If I understand you right, the match would reduce if this would be @eq nat x 
x for some x.
My point is that Nat.add is computing, e.g.
 
    Eval compute in (Nat.add (S O) O = (S O)).
    (* @eq nat (S O) (S O) : Prop *)

But it does NOT compute in the type part of a term:

    Eval compute in (plus_n_O 1).
    (* plus_n_O (S O) : @eq nat (S O) (Nat.add (S O) O) *)

If Coq would reduce the type part, it would reduce the match.

I wonder why this is. As far as I know Coq does reduction in type terms to 
check if they are equal, so there shouldn't be general conflicts with this.

So the question boils down to why doesn't Coq do reductions of types of terms 
to check if a match could be reduced? Shouldn't Eval compute compute in type 
terms as well?

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928