主页 / coding / 问题 / 79434830
Accepted
KingsAlpaca
Asked: 2025-02-13 08:54:05 +0800 CST

Coq 向量：移位的平等性

  • 772

我在 中使用标准向量类型Coq.Vectors。我想证明关于 的以下属性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。

第 2 部分 （已添加）：
编辑：此部分现在作为单独的问题提出： shiftin、shiftout 和 last

同时，如果向量长度至少为 1，是否有可能证明last和shiftout是的有效反转？shiftin

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

3 个回答

  1. dependent destruction您可以使用我正在导入的策略Program，那么证明就相对容易了。

    这是我的看法，我能够inj_pair2找到Search existT.：

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

    已经有几个答案，但是，所有这些都依赖于额外的公理，特别是这两个：

    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

    这些公理是使用时生成的dependent induction。但是，这些公理对于证明您的目标并不是必需的。为了在没有公理的情况下证明它，需要更多地了解索引归纳数据类型的理论，特别是如何使用归纳相等并利用身份证明的唯一性。幸运的是，我们实际上不需要这个来证明，因为我们可以Vec从已经为我们完成繁重工作的库中插入一些引理：

    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.

    这个证明现在是Closed under the global context🎉

    如果您想学习如何使用像 Coq 中的索引归纳数据类型，那么查看、或的Vec.t证明可能会有所帮助。如果您还不熟悉该理论，它们可能也难以理解。etacons_injnil_spec

    请注意，使用例如injection代替引理cons_inj是行不通的，因为该策略需要推断上的身份证明的唯一性nat，而这injection本身是无法做到的，因为它相当棘手。

    • 2

  3. 如果你Search shiftin发现cons_inj引理在你进行依赖归纳时很有用。

    Proof.
    dependent induction v0;
      dependent destruction v1.
    - apply cons_inj.
    - intros H; simpl in H.
      destruct (cons_inj H) as [H1 H2].
      destruct (IHv0 _ H2) as [H3 H4].
      rewrite H1, H3, H4. 
      split; reflexivity.
Qed.
    • -1

相关问题