COQ向量：Shiftin

Question

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.

<-

很简单。

-> a0 = a1

还可以。但是我不知道

-> t0 = t1

。
    

您需要策略

dependent destruction

（我要进口

Program

Answer 1

From Coq Require Import Vector.
From Coq Require Import Program.

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.
Proof.
  intros A n a0 a1.
  dependent induction t0;
  dependent destruction t1.
  all: split; intros H.
  all: cbn in *.
  - split.
    + inversion H.
      reflexivity.
    + reflexivity.
  - destruct H as [-> _].
    reflexivity.
  - split.
    + inversion H; subst h0.
      apply inj_pair2 in H2.
      apply IHt0 in H2 as [-> _].
      reflexivity.
    + inversion H; subst h0.
      apply inj_pair2 in H2.
      f_equal.
      apply IHt0 in H2 as [_ ->].
      reflexivity.
  - f_equal.
    + inversion H.
      inversion H1; subst h0.
      reflexivity.
    + apply IHt0.
      inversion H; subst a0.
      inversion H1; subst h0.
      apply inj_pair2 in H3.
      subst t0.
      split; reflexivity.
Qed.