The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

The error message is misleading. As in your previous question, the
problem here is that you are trying to use v in the second branch, and
Coq is not smart enough to understand that its length is OK. When this
kind of error happens, it is often the case that the problem is not
where the error message is pointing at.

The solution is annotate the return type of the match and write the
second case slightly differently:

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

Notice the "as v'" in the second branch of the pattern match. The
problem with your original version was that, when type-checking a
pattern-matching branch, Coq doesn't keep track of any connection
between the thing you matched on and what you're returning on that
branch. In particular, it doesn't know that len = 0 on the second
branch. Because it doesn't know this, trying to return v directly will
result in an error, since it will be trying to unify (S 0) (which is
the length you should be returning on that branch) with (S len) (which
is the length of v).

2014-04-12 12:45 GMT+02:00 Ö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



-- 
Arthur Azevedo de Amorim