The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

If you are not allergic to writing programs as proofs, here is what you can do (checked with Coq 8.4pl2):

Lemma pt_aux : forall (h : nat) len (v : Vector.t nat (S len)), Vector.t nat (S len).

Proof.

 induction len as [ | hlen recursiveCall ]; intros.

 - exact v.

 - inversion v. apply (Vector.cons _ (h0+h)). apply recursiveCall. exact H0.

Defined.

Remember to end the proof with "Defined" instead of  "Qed".

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sat, Apr 12, 2014 at 11:21 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

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.

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