coq - Coq:证明 < 和 ≤ 之间的关系
问题描述
我现在正在学习 Coq,在一个更大的证明中,我被以下子证明难住了:
Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.
或者,一旦展开:
Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → S n ≤ m.
这里,“n ≤ m”归纳定义如下:
Inductive le : nat → nat → Prop :=
| le_n : ∀ n : nat, le n n
| le_S : ∀ n m : nat, (le n m) → (le n (S m)).
我还没有走得很远,但我的尝试看起来像这样:
Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.
Proof.
unfold lt.
intro n.
induction n.
- induction m.
+ intros. exfalso. contradiction.
+ admit.
- admit.
Admitted.
在第一个归纳步骤(由第一个承认标记)中,归纳假设显示以下内容:
1 subgoal
m : nat
IHm : 0 ≤ m → 0 ≠ m → 1 ≤ m
______________________________________(1/1)
0 ≤ S m → 0 ≠ S m → 1 ≤ S m
我不确定如何利用这个假设来证明子目标。我将不胜感激任何正确方向的指导。
解决方案
由于le
被定义为归纳谓词,因此对其进行归纳而不是n
. le
没有引用0
甚至S n
(它确实有S m
),所以归纳n
可能不是要走的路。感应m
可能会起作用,但它可能比必要的更难。
在开始正式证明之前,考虑如何非正式地证明这一点通常会很有帮助(尽管仍然使用相同的定义)。如果你假设n ≤ m
,那么根据 的归纳定义lt
,这意味着n
和m
相同,或者m
是某个数的后继m'
并且n
小于或等于m'
(你能明白为什么 的定义lt
暗示了这一点吗?)。在第一种情况下,我们将不得不使用额外的假设n ≠ m
来得出矛盾。在第二种情况下,我们甚至不需要它。n ≤ m'
意味着S n ≤ S m'
, 所以因为m = S m'
, S n ≤ m
, 即n < m
.
对于形式化,我们必须证明在最后一行n ≤ m
暗示的假设S n ≤ S m
。您应该尝试类似的非正式分析来证明这一点。除此之外,非正式证明应该可以直接形式化。案例分析就H: n ≤ m
只是destruct H.
。
还有一件事。这不是必需的,但从长远来看通常会有所帮助。在定义一个归纳类型(或谓词)时,如果您可以分解出在每个构造函数中使用相同方式的参数,它可以使归纳原理更加强大。le
使用,的方式n
是普遍量化的,并且对两个构造函数都使用相同的方式。的每个实例都le
以le n
.
Inductive le : nat → nat → Prop :=
| le_n : ∀ n : nat, le n n
| le_S : ∀ n m : nat, (le n m) → (le n (S m)).
这意味着我们可以将该索引分解为参数。
Inductive le' (n: nat) : nat → Prop :=
| le_n' : le' n n
| le_S' : ∀ m : nat, (le' n m) → (le' n (S m)).
这为您提供了一个稍微简单/更好的归纳原理。
le'_ind
: forall (n : nat) (P : nat -> Prop),
P n ->
(forall m : nat, le' n m -> P m -> P (S m)) ->
forall n0 : nat, le' n n0 -> P n0
将此与le_ind
.
le_ind
: forall P : nat -> nat -> Prop,
(forall n : nat, P n n) ->
(forall n m : nat, le n m -> P n m -> P n (S m)) ->
forall n n0 : nat, le n n0 -> P n n0
基本上这里发生的是le_ind
,你必须为每个n
. 使用le'_ind
,您只需要为n
您正在使用的特定证明它。这有时可以简化证明,尽管它不是证明你的定理所必需的。证明这两个谓词等价是一个很好的练习。
推荐阅读
- sql - PostgreSQL - 如何按一组重复的相同字段值排序
- java - 如何在Android中一行显示TextView和EditText?
- regex - 其他字符串之间的字符串中的字符
- reactjs - React 使用 Redux-form , post 方法
- watson-assistant - IBM Watson 工作区编排
- javascript - 当事件附加到文档时,获取 elem 的 id
- python - 运行 Python 程序时出错(新手)
- python - django,以可视形式将对象从数据库获取到模板
- java - log4j 文件随机进入桌面
- javascript - 使用 USB 数据线从 Beacon 读取/写入数据