coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?

From: Gabriel Scherer <gabriel.scherer AT gmail.com>
To: Eduardo León <abc.deaf.xyz AT gmail.com>
Cc: Adam Chlipala <adamc AT csail.mit.edu>, Kristopher Micinski <krismicinski AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?
Date: Sat, 29 Dec 2012 22:38:02 +0100

In Coq, pattern matching (in fact elimination of inductive types) is a
primitive concept, and the equality type is a derived concept, defined
as an inductive datatype. Pattern matching do not generate equalities,
it's the other way around: to use an equality witness, you must
pattern match on it. For further details, see the chapter of Adam's
book.

On Sat, Dec 29, 2012 at 9:56 PM, Eduardo León
<abc.deaf.xyz AT gmail.com>
wrote:
> e head of a length-indexed list guaranteed to contain at least one element?
> I understand why the auxiliary function trick works, but it looks to me like
> a hack, in the sense that `hd' Nil` has no obvious interpretation - it
> solely exists for the purpose of

[Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, abc.deaf.xyz, 12/29/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Adam Chlipala, 12/29/2012
  - Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Eduardo León, 12/29/2012
    - Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Gabriel Scherer, 12/29/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Kristopher Micinski, 12/29/2012
- Re: [Coq-Club] Inside a branch of a match block, how do I use the assertion that the matched expression is equal to the branch's data constructor expression?, Matthieu Sozeau, 12/30/2012