The Coq mailing list

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

2014-04-13 5:21 GMT+02:00 Ömer Sinan Ağacan 
<omeragacan AT gmail.com>:
> Thanks for your answer, it worked! I don't understand how can this
> code work, though. Because pattern matching has different return type
> than the function.
>

They do look different superficially, but they are actually the same.
Remember that len' is actually S len. Thus, if you substitute S len
for len' in the return type of the match, you get

match S len with
| 0 => unit
| S len => Vector.t nat (S len)
end

which reduces to

Vector.t nat (S len)

allowing Coq to type-check the definition.

In a nutshell, this confusing return type arises because when Coq
type-checks a match, it requires you to generalize over the indices of
your scrutinee (in this case, the length of the vector). This is what
the "as" part of the declaration means. When this happens, Coq
"forgets" that len' is actually S len, and you need to write something
that makes sense for any possible natural number, not just S len. This
is the reason why we need the "0 => unit" branch on the return clause.

Only after accepting the match will Coq use the actual length of your
vector (in this case, S len) to type-check the rest of the definition.
Then, it performs the above substitution and realizes everything is
OK.

> Also, I tried replacing `v'` with `_` and using `refine` tactic, but I
> didn't get `Vector h' 0 someFreshVar = v'` as hypothesis while filling
> the case with `as v'`. Why I never get this types of equalities in
> pattern matching?
>
> Thanks again.
>
> ---
> Ömer Sinan Ağacan
> http://osa1.net



-- 
Arthur Azevedo de Amorim