The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Michael, 

  what you propose is a version of the definitional version of UIP (also know as the K axiom), you 

might want to read Adam Chlipala's chapter about it in CPDT. I believe 

http://adam.chlipala.net/cpdt/html/Cpdt.Equality.html turns around this subject.

Best,

-- Matthieu

On Wed, Sep 7, 2016 at 3:39 PM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Guillaume,

thanks a lot, your example gives some interesting insight into how match works. So if I have nat = bool, I can convince match to accept 1 as a bool:

Definition foo2 (H : nat = bool) : bool :=
  match H in (_ = t) return t with
  | eq_refl => 1
  end.

But I wonder how this really works. I can see that an "in" clause is used to bind a variable to a part of the match argument type and this is used in a "return" clause. But how does Coq know that it should use the equality to relate this to the actual return type? Is there a rule that if the match argument is an equality of types, it can be used to unify the declared and actual return type?

Coming back to my issues with computations with dependent types: how about reducing such matches, in case the types are unifiable, as in the example I have shown where the types are "t bool (0+1)" and "t bool 1". This should be quite common in computations with concrete values of dependent types, e.g. vectors of known length.

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