The Coq mailing list

[Eduardo León <abc.deaf.xyz AT gmail.com>]

Do you mean the `hd` function for taking the 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 being discarded as a possibility in `hd`.

I have noticed that, when you make an Inductive definition `a`, in addition to `a` itself, you get three additional definitions, which serve as "induction principles": `a_rect`, `a_ind`, and `a_rec`. This is of course very clever, and I suppose this is what actually makes things like the `match` construct and the `induction` tactic work.

I want `match` to be similarly clever. Obviously, when I `match blargh with | blerg => ...`, I expect `blargh = blergh` in that branch. Furthermore, it is actually true. So why do I not have an access to an instance of the type `blargh = blergh`? Maybe there is a technical reason why this is not possible... I would like to know!

On Sat, Dec 29, 2012 at 2:51 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 12/29/2012 02:37 PM, abc.deaf.xyz AT gmail.com wrote:

I want to write it as follows:

     Theorem nope n (p : n = O) (q : n <> O) : False.
       contradict q.
       exact p.
     Qed.

     Definition pred2 n (q : n <> O) :=
       match n with
         | S n =>  n
         | O   =>
           let p := _ in
           match nope n p q with end
       end.

My problem is... what do I fill in the hole in the let clause?
   

I actually treat the example of dependently typed predecessor at length in Chapter 6 of CPDT <http://adam.chlipala.net/cpdt/>.  The version you're looking for is one among several that the chapter works its way through.

-- 
Eduardo León