coq - IndProp : prove that Prop is not provable

Question

任务。

假设我们给 Coq 如下定义:

Inductive R2 : nat -> list nat -> Prop :=
| c1 : R2 0 []
| c2 : forall n l, R2 n l -> R2 (S n) (n :: l)
| c3 : forall n l, R2 (S n) l -> R2 n l.

以下哪些命题是可以证明的？

我证明了三分之二。

Example Example_R21 : R2 2 [1;0].
Proof.
  apply c2. apply c2. apply c1.
Qed.

Example Example_R22 : R2 1 [1;2;1;0].
Proof.
  repeat constructor.
Qed.

3-rd不可证，因为c3只会增加n，永远不会等于表头+1。但是如何形式化地证明它不可证呢？

Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof.

Qed.

更新 1

Fixpoint gen (n: nat) : list nat :=
  match n with
  | 0 => []
  | S n' => (n' :: gen n')
  end.

Lemma R2_gen : forall (n : nat) (l : list nat), R2 n l -> l = gen n.
Proof.
  intros n l H. induction H.
  - simpl. reflexivity.
  - simpl. rewrite IHR2. reflexivity.
  - simpl in IHR2. ?

Answer 1

您必须在 R2 上进行归纳。基本上，如果您有 R2 6 (3::_)，那么它必须是一个 c3(没有其他构造函数适合)，因此它包含一个 R2 7 (3::_)，也一定是c3，其中包含R2 8 (3::_)等，这个链是无限的，所以你永远不会到达尽头。因此，您可以使用 False 作为归纳的目标，您将永远不会达到 实际上 必须生成 False 的基本情况。仅仅使用 inversion 是不够的。反转实际上只是所需归纳的一个步骤，对上下文中的任何其他事物进行归纳都无济于事。

在归纳过程中，第一个参数会发生变化。具体来说，它总是大于 S 3(这就是让我们排除其他构造函数的原因)，因此我们需要对 k 进行概括，其中第一个参数是总是 5 + k(对于我们有 6 的情况，从 k = 1 开始)。

Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof.
  set (xs := [2; 1; 0]).
  change 6 with (5 + 1).
  set (x := 3). (* sets are not strictly needed, but help clean things up *)
  generalize 1 as k.
  intros k.
  (* Everything up to here is just generalizing over k *)
  remember (S (S x) + k) as n eqn:prf_n.
  remember (x :: xs) as l eqn:prf_l.
  intros no.
  revert k prf_n prf_l.
  induction no as [ | n' l' _ _ | n' l' _ rec_no]
  ; intros k prf_n prf_l.
  - discriminate.
  - injection prf_l as -> ->.
    discriminate.
  - subst.
    (* Everything up to here is combined inversion and induction *)
    eapply rec_no.
    + apply plus_n_Sm.
    + reflexivity.
Defined.

我们可以通过使用实验性的 dependent induction 策略极大地减少这个证明，它取代了中间的 inversiony 部分。

Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof.
  set (xs := [2; 1; 0]).
  change 6 with (5 + 1).
  set (x := 3).
  generalize 1 as k.
  intros k no.
  dependent induction no generalizing k.
  eapply IHno.
  - apply plus_n_Sm.
  - reflexivity.
Defined.

另一种清理形式是将广义证明提取到引理中:

Lemma R2_head x k xs : ~R2 (S (S x) + k) (x :: xs).
Proof.
  intros no.
  dependent induction no generalizing k.
  - clear no IHno. (* Another "infinite chain" contradiction *)
    rename x into prf_x, x0 into x.
    induction x as [ | x rec_x].
    + discriminate.
    + injection prf_x.
      apply rec_x.
  - eapply IHno.
    + apply plus_n_Sm.
    + reflexivity.
Defined.
Example Example_R232 : not (R2 6 [3;2;1;0]) := R2_head 3 _ _.