The Coq mailing list

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

Dear Coq Users

 

I thought about this a bit more. Since the following term type checks:

 

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)

 

Coq knows that (t bool y) and the type of “cons bool false 0 (nil bool)” unify. Also it is obvious that the only possible value of this match is “cons bool false 0 (nil bool)”, the only question is what type it has. But since Coq knows that the type of the result term and the complete match unify (otherwise the match wouldn’t typecheck), I don’t think that one needs “proof irrelevance for equality” to justify that the above term is equal to:

 

cons bool false 0 (nil bool) : t bool 1

 

Can’t one add a rule which reduces matches in the following situation:

 

-          the match has only one pattern

-          the result term does not depend on any pattern bindings

-          the type of the result term and the type of the match unify (should always be the case – otherwise the match wouldn’t type check)

 

Would such a rule be sound? I have the impression that this would solve some of the issues which lead to the statement I hear from time to time: “Yes, Coq is dependently typed – but don’t use it”. This kind of matches which just changes the type of a term, but not the term itself, are quite common when dealing with dependent types and lead to exploding term sizes. E.g. the standard library Vectors.rev function comes with the comment “Caution : There is a lot of rewrite garbage in this definition”, so I guess it is not trivial – if possible at all - to write a rev function for standard library vectors, which doesn’t lead to exploding term sizes when computing with concrete values.

 

I think being unable to give a reasonably well behaved implementation for something as trivial as a vector reversal is problematic. Well I am not sure if it is really not possible, but the comment in the standard library reduced my hopes to find a solution a bit.

 

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