Search code examples
coqdependent-typetheorem-proving

Coq vector: equality of shiftin

I am using the standard vector type in Coq.Vectors. I want to prove the following property regarding shiftin.

Lemma vec_shiftin_eq:
  forall A (n:nat) (a0 a1: A) (t0 t1: t A n),
  shiftin a0 t0 = shiftin a1 t1 <-> a0 = a1 /\ t0 = t1.

<- is straightforward. -> a0 = a1 is ok. But I have no idea about -> t0 = t1.

Part 2 (added):
Edit: this part is now stated as a separate question: shiftin, shiftout, and last

Meanwhile, would it be possible to show that last and shiftout are valid inversion of shiftin if vector length is at least 1?

Lemma shiftin_last_shiftout:
  forall A (n:nat) (x: t A (S n)),
  x = shiftin (last x) (shiftout x).
Solution

  • There are several answers already, however, all of these rely on additional axioms, in particular these two:

    Axioms:
proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2
Eqdep.Eq_rect_eq.eq_rect_eq :
  forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), x = eq_rect p Q x p h

    These axioms are generated when using dependent induction. These axioms are, however, not required for proving your goal. To instead prove it without axioms, one needs to know a bit more about the theory of index-inductive datatypes, and in particular how to work with inductive equality and exploit uniqueness of identity proofs. Luckily, we don't actually need this for this proof, since we can plug together a few lemmas from the Vec library that already did the heavy lifting for us:

    From Coq Require Import Vector.

Lemma vec_shiftin_eq A n a0 a1 (t0 t1 : t A n) :
    shiftin a0 t0 = shiftin a1 t1 <->
    a0 = a1 /\ t0 = t1.
Proof.
  split; [|now intros [-> ->]].
  induction t0 as [|n te t0' IH] in t1|-*.
  - pose proof (nil_spec t1) as ->. simpl.
    intros [=]. easy.
  - pose proof (eta t1) as ->. simpl.
    intros [-> [-> ->]%IH]%cons_inj.
    split; [easy|].
    now rewrite <-eta.
Qed.

    This proof is now Closed under the global context 🎉

    If you want to learn how to work with index-inductive datatypes like Vec.t in Coq, then looking at the proofs of eta, cons_inj, or nil_spec might be instructive. They might also be incomprehensible if you're not already familiar with the theory.

    Note that using e.g. injection instead of the lemma cons_inj does not work since the tactic would need to reason about uniqueness of identity proofs on nat, which injection can not do on its own since it is rather tricky.