IndProp:证明 Prop 不可证明
IndProp: prove that Prop is not provable
任务。
假设我们给 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.
以下哪些命题是可以证明的?
我证明了 3 个中的 2 个。
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. ?
not A
是 A -> False
。你应该在上面引入荒谬的假设和推理(见倒置策略)。
您可以编写一个函数,从 nat
参数(我们称之为 gen
)生成列表并证明 R2 n l -> l = gen n
。由此,您可以通过证明 l <> gen n
.
来证明您的命题
您必须在 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
策略来极大地减少这个证明,它取代了中间的 inversion
y 部分。
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 _ _.
这是一个使用目标泛化技术的简单证明。
首先,我们证明了一个比我们实际提出的更普遍的 属性。
From Coq Require Import Lia.
Lemma R2_len n l : R2 n l -> n <= length l.
Proof. induction 1; simpl; lia. Qed.
现在我们的例子是更一般的属性.
的简单具体实例
Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof. intros H%R2_len; simpl in H; lia. Qed.
这等同于@HTNW 的证明
Lemma R2_head' {a n l}: R2 a (n::l) -> a <= S n.
intros H; dependent induction H;
try pose proof (IHR2 _ _ eq_refl); lia.
Qed.
Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof. intros C; pose proof (R2_head' C); lia. Qed.
任务。
假设我们给 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.
以下哪些命题是可以证明的?
我证明了 3 个中的 2 个。
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. ?
not A
是 A -> False
。你应该在上面引入荒谬的假设和推理(见倒置策略)。
您可以编写一个函数,从 nat
参数(我们称之为 gen
)生成列表并证明 R2 n l -> l = gen n
。由此,您可以通过证明 l <> gen n
.
您必须在 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
策略来极大地减少这个证明,它取代了中间的 inversion
y 部分。
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 _ _.
这是一个使用目标泛化技术的简单证明。
首先,我们证明了一个比我们实际提出的更普遍的 属性。
From Coq Require Import Lia.
Lemma R2_len n l : R2 n l -> n <= length l.
Proof. induction 1; simpl; lia. Qed.
现在我们的例子是更一般的属性.
的简单具体实例Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof. intros H%R2_len; simpl in H; lia. Qed.
这等同于@HTNW 的证明
Lemma R2_head' {a n l}: R2 a (n::l) -> a <= S n.
intros H; dependent induction H;
try pose proof (IHR2 _ _ eq_refl); lia.
Qed.
Example Example_R23 : not (R2 6 [3;2;1;0]).
Proof. intros C; pose proof (R2_head' C); lia. Qed.