I am working on a verification problem in Coq that requires extensive use of the standard vector library Coq.Vectors. There are many useful definitions, but I don't see some desired properties being proved.
I need to operate on the last element in a vector. I think shiftin and last-shiftout form an inverse on the non-empty vector. But I failed to prove the following.
From Coq Require Import Vector.
Lemma shiftin_last_shiftout:
forall A (n:nat) (x: t A (S n)),
x = shiftin (last x) (shiftout x).
This lemma can be proven rather straightforwardly by first proving a helper lemma. Specifically, if we know that shiftin (last t0) (shiftout t0) = t0, then the rest quickly follows. Proving that helper lemma requires a trick:
From Coq Require Import Vector.
Lemma vec_shiftin_eq' A n (t0 : t A n) :
match n as n' return t A n' -> Prop with 0 => fun _ => True | S nn =>
fun t0 => shiftin (last t0) (shiftout t0) = t0 end t0.
Proof.
induction t0 as [|el1 n t0' IH]; [easy|].
destruct t0' as [|el2 n t0']; [easy|].
simpl in IH|-*. rewrite IH. easy.
Qed.
Lemma vec_shiftin_eq A n (t0 t1 : t A (S n)) :
t0 = t1 <-> shiftin (last t0) (shiftout t0) = shiftin (last t1) (shiftout t1).
Proof. now rewrite !(vec_shiftin_eq' A (S n)). Qed.
Print Assumptions vec_shiftin_eq.
(* Closed under the global context *)
We want to prove our helper lemma by induction on the vector. But induction on the vector always requires that the n indicating its length is unconstrained, i.e. that it is a free variable. Doing induction where it is S n does not work. To work around this, we are forced to generalize the induction statement to something that works for all n, which requires saying what should hold at n=0. We say that nothing interesting is happening at n=0, i.e. True. With this, the induction goes through without a hinch.