A Coercion from vectors of length 2 to ordered pairs
First Question
Consider the following definitions:
Require Import Bvector.
Implicit Arguments Vcons [A n].
Implicit Arguments Vnil [A].
Implicit Arguments Vhead [A n].
Implicit Arguments Vtail [A n].
Definition vec2 (A:Type) := vector A 2.
Definition vcons2 (A:Type)(a b:A): vec2 A := Vcons a (Vcons b Vnil).
Implicit Arguments vcons2 [A].
Define a coercion from vec2 to the class prod of cartesian
products.
The following commands should work properly:
Check (fst (vcons2 3 4)).
Eval compute in (snd (vcons2 3 4)).
A (more difficult) question
Prove the following theorem:
Lemma V2 : forall A (v:vec2 A), v= vcons2 (fst v) (snd v).
Hint
The solution of the second question may use dependent elimination.
Please refer to
The tutorial on [Co]-Inductive Types in Coq (Section 6).
Solution
Look at this file .
Going home