The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Hi all,

In case you're about to answer this question as "read CPDT", I want to
say that I'm already reading it and but I couldn't find anything
relevant yet and I don't want to wait until I finish the entire book
because it will probably take long time. (if you know which particular
page I need to read, I can of course jump to that page :-) )

Anyway, I'm trying to implement some certified algorithms/data
structures and I came across this problem several times: I can't tell
Coq that tail of discriminee(the value that we're pattern matching on)
is one shorter than the discriminee. An example function:

  Fixpoint pt_aux (h : nat) len (v : Vector.t nat (S len)) : Vector.t
nat (S len) :=
    match v with
    | Vector.nil => admit
    | Vector.cons h' 0 _ => v
    | Vector.cons h' (S len') t' =>
        Vector.cons nat (h + h') _ (pt_aux h' _ t')
    end.

Here, Coq fails with

  The term "Vector.cons nat (h + h') (S len') (pt_aux h' len' t'0)" has type
   "Vector.t nat (S (S len'))" while it is expected to have type
   "Vector.t nat (S len)".

How can I tell Coq that (S (S len') = S len) ?

I first though that maybe I need a pattern matching function with type:

  match_vec : n -> forall A, Vector.t A n -> option {Vector.t A (S n')
| S n' = n}

obviously this doesn't work, because I need to somehow apply this
function n'. I tried using `exists` like this `option (exists n',
{Vector.t A (S n') | S n' = n})` but no luck... Maybe what I'm trying
to do does not even make sense.

(I had asked a similar question here, I was trying to tell Coq that n
= S n' in successor case of pattern matching on natural number n, I
tried using similar techniques for solving this problem but couldn't
do anything useful)

Thanks..

---
Ömer Sinan Ağacan
http://osa1.net