Thanks to Adam
Chlipala for teaching me how to prove
vec2list2vec. It means that converting a dependently
typed vector to an ordinary list and back yields the same vector
intact. But surely there is a simpler way?
Require Import List.
Require String.
Open Scope string_scope.
Ltac move_to_top x :=
match reverse goal with
| H : _ |- _ => try move x after H
end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move_to_top x
| assert_eq x name; move_to_top x
| fail 1 "because we are working on a different case" ].
Ltac Case name := Case_aux Case name.
Ltac SCase name := Case_aux SCase name.
Inductive vec (X: Type): nat -> Type :=
| vnil: vec X 0
| vcons: forall n: nat, X -> vec X n -> vec X (S n).
Implicit Arguments vnil [ [X] ].
Implicit Arguments vcons [ [X] [n] ].
Check (vcons 4 (vcons 2 (vcons 7 vnil))).
Fixpoint vec2list {X: Type} {n: nat} (v: vec X n): list X :=
match v with
| vnil => nil
| vcons _ h t => cons h (vec2list t)
end.
Fixpoint list2vec {X: Type} (l: list X): vec X (length l) :=
match l with
| nil => vnil
| cons h t => vcons h (list2vec t)
end.
Theorem vec2list_length: forall (X: Type) (n: nat) (v: vec X n),
length (vec2list v) = n.
Proof.
intros X n v. induction v as [| n' h t].
Case "vnil". reflexivity.
Case "vcons". simpl. rewrite -> IHt. reflexivity.
Qed.
Theorem list2vec2list: forall (X: Type) (l: list X),
vec2list (list2vec l) = l.
Proof.
intros X l. induction l as [| h t].
Case "nil". reflexivity.
Case "cons". simpl. rewrite -> IHt. reflexivity.
Qed.
Require Import Eqdep.
Lemma vec2list2vec': forall (X: Type) (l: list X) (n: nat) (v: vec X n),
forall (EQ: length l = n), l = vec2list v ->
v = match EQ in (_ = n) return vec _ n with
| refl_equal => list2vec l
end.
Proof.
intros X l.
induction l as [| h t]; simpl;
intros n v EQ H; destruct v; inversion EQ as [EQ'].
Case "nil". rewrite (UIP_refl _ _ EQ). reflexivity.
Case "cons". inversion H. rewrite (IHt _ v EQ' H2). clear.
generalize (list2vec t) EQ EQ'.
rewrite EQ'. intros v EQ1 EQ2.
rewrite (UIP_refl _ _ EQ1).
rewrite (UIP_refl _ _ EQ2).
reflexivity.
Qed.
Theorem vec2list2vec: forall (X: Type) (n: nat) (v: vec X n),
v = match (vec2list_length X n v) in (_ = n) return vec _ n with
| refl_equal => list2vec (vec2list v)
end.
Proof.
intros. apply vec2list2vec'. reflexivity.
Qed.