The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/08/2016 05:25 AM, Soegtrop, Michael wrote:
> 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.

I've only got 38 years of traditional programming languages, and I 
switched my major from physics to comp-sci.  But I think I feel your pain.

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

Not quite...

Actually, I think there are three separate points here.  One is that 
match doesn't determine the discriminee value from its type, regardless 
of how simple it is, even if the type of the discriminee indicates that 
there is only one possible value.  Hence:

Variable u : unit.
Compute (match u with tt => 1 end).

is still a match, not 1.

The second point is: why doesn't plus_n_0 1 reduce to eq_refl. That's 
because it is opaque, as was mentioned.

The third point is: why can't one just directly replace any proof of @eq 
A x x with eq_refl, since it is the only constructor?  That's because of 
the lack of a built-in UIP (or K) in Coq - and something similar occurs 
with type indexes on other types as well as eq.  But, one can use 
Eqdep_dec.UIP_refl_nat in this case.  However, Coq, doesn't allow one to 
rewrite in values, only in types.  There is actually a rewrite tactic 
syntax "rewrite R in (value of H)", but I have never seen it work (see 
bugs 4075, 2911).

-- Jonathan