logic - 如何在 Coq 中证明 forall n :nat, ~n

转载 作者：行者123 更新时间：2023-12-03 23:57:24 30 4

我已经困惑了几个小时，我不知道如何证明

forall n:nat, ~n<n

在 Coq 中。我真的需要你的帮助。有什么建议吗？

最佳答案

这个引理在标准库中:

Require Import Arith.
Lemma not_lt_refl : forall n:nat, ~n<n.
Print Hint.

结果中有lt_irrefl .实现这一点的更直接的方法是

info auto with arith.

这证明了目标并展示了如何:

intro n; simple apply lt_irrefl.

既然您知道在哪里可以找到证明，我将仅从基本原理(我想这是您作业的重点)给出如何做到这一点的提示。

首先，您需要证明一个否定。这几乎意味着你推 n<n作为一个假设并证明你可以推断出一个矛盾。然后，推理 n<n , 展开它的定义。

intros h H.
red in H.   (* or `unfold lt in H` *)

现在你需要证明 S n <= n不可能发生。要从第一原则做到这一点，此时您有两个选择:您可以尝试在 n 上进行感应。 , 或者你可以尝试在 <= 上感应. <=谓词是由归纳定义的，在这些情况下，您通常需要对其进行归纳——也就是说，通过对假设的证明进行归纳来推理。但是，在这里，您最终需要对 n 进行推理。 , 以表明 n不能是 S n 的第 m^th 个继任者，您可以在 n 上开始感应马上。

在 induction n 之后，你需要证明基本情况:你有假设 1 <= 0 ，并且您需要证明这是不可能的(目标是 False )。通常，要将归纳假设分解为案例，您可以使用 induction战术或其变体之一。这种策略在假设上构建了一个相当复杂的相关案例分析。查看正在发生的事情的一种方法是调用simple inversion。 ，这给您留下了两个子目标:假设的证明 1 <= 0使用 le_n构造函数，它要求 1 = 0 ，或者该证明使用 le_S构造函数，它要求 S m = 0 .在这两种情况下，该要求显然与 S 的定义相矛盾。 ，所以战术discriminate证明子目标。而不是 simple inversion H , 你可以使用 inversion H ，在这种特殊情况下直接证明了目标(不可能的假设情况非常常见，它已融入成熟的 inversion 策略)。

现在，我们转向归纳案例，我们很快就来到了要证明 S n <= n 的地方。来自 S (S n) <= S n .我建议您将其声明为一个单独的引理(首先要证明)，可以概括为:forall n m, S n <= S m -> n <= m .

关于logic - 如何在 Coq 中证明 forall n :nat, ~n<n？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/8103226/

30 4 0

• c - `#define LT(n) n, n, n, n, n, n, n, n, n, n, n, n, n, n, n, n`在这里做什么？

  我看到以下宏 here . static const char LogTable256[256] = { #define LT(n) n, n, n, n, n, n, n, n, n, n, n,

• ruby - 另一个与 "diff.*\n.*\n.*\n.*\n.*\n "相同的正则表达式

  这个问题不太可能帮助任何 future 的访问者；它只与一个小的地理区域、一个特定的时间点或一个非常狭窄的情况有关，这些情况并不普遍适用于互联网的全局受众。为了帮助使这个问题更广泛地适用，visit

• algorithm - n+n/2+n/3+...+n/n 之和的公式

  所以我得到了这个算法我需要计算它的时间复杂度 这样的 for i=1 to n do k=i while (k<=n) do FLIP(A[k]) k

• algorithm - N 次幂 n i-e n^n 是否是多项式？ n^2 和 n^n 之间是否存在多项式差异？

  n 的 n 次方(即 n^n)是多项式吗？ T(n) = 2T(n/2) + n^n 可以用master方法求解吗？ 最佳答案 它不仅不是多项式，而且比阶乘还差。 O(n^n) 支配 O(n!)。同样

• java - 从 Unicode 字符中删除变音符号 (ń ǹ ň ñ ṅ ņ ṇ ṋ ṉ ̈ ɲ ƞ ᶇ ɳ ȵ)

  我正在研究一种算法，它可以在带有变音符号的字符(tilde、circumflex、caret、umlaut、caron)及其“简单”字符之间进行映射。 例如: ń ǹ ň ñ ṅ ņ ṇ

• fibonacci - 如何使用运算符(或其他东西)编写 N N N .... N？

  嗯..我从昨天开始学习APL。我正在观看 YouTube 视频，从基础开始学习各种符号，我正在使用 NARS2000。 我想要的是打印斐波那契数列。我知道有好几种代码，但是因为我没有研究过高深的东西，

• math - 求解递推关系 T(n) = √n T(√n) + n

  已关闭。这个问题是 off-topic 。目前不接受答案。 想要改进这个问题吗？ Update the question所以它是on-topic用于堆栈溢出。 已关闭12 年前。 Improve th

• python - 从 N*N*N 到 N 的双射函数

  谁能帮我从 N * N * N → N 中找到一个双射数学函数，它接受三个参数 x、y 和 z 并返​​回数字 n？ 我想知道函数 f 及其反函数 f'，如果我有 n，我将能够通过应用 f'(n) 来

• regex - 如何在同一等式中搜索/替换所有 "n("-> "n*("和 ")n"-> ")*n"？

  场景: 用户可以在字符串格式的方程式中输入任意数量的括号对。但是，我需要检查以确保所有括号 ( 或 ) 都有一个相邻的乘数符号 *。因此 3( 应该是 3*( 和 )3 应该是 )*3。 我需要将所有

• java - 为什么 n+++n 有效而 n++++n 无效？

  在 Java 中，表达式: n+++n 似乎评估为等同于: n++ + n 尽管 +n 是一个有效的一元运算符，其优先级高于 n + n 中的算术 + 运算符。因此编译器似乎假设运算符不能是一元运算符

• c - n = 0 和 n = n - n 之间的区别

  当我阅读 this 问题我记得有人曾经告诉我(很多年前)，从汇编程序的角度来看，这两个操作非常不同: n = 0; n = n - n; 这是真的吗？如果是，为什么会这样？ 编辑: 正如一些回复所指出

• javascript - ^\n\n\n 的含义

  我正在尝试在reveal.js 中加载外部markdown 文件，该文件已编写为遵守数据分隔符语法: You can write your content as a separate file and

• javascript - 使用 JavaScript，如何按照这些参数/规则生成随机 11 个字符字符串？ (L,L,L,L/N,L/N,N,N,N,N,N,N)

  我试图弄清楚如何使用 Javascript 生成一个随机 11 个字符串，该字符串需要特定的字母/数字序列，以及位置。 ----------------------------------------

• algorithm - 使用主方法求解 T(n) = 2T(n/2) + n/log n 和 T(n) = 4T(n/2) + n/log n 之间的区别

  我最近偶然发现了一个资源，其中 2T(n/2) + n/log n 类型 的递归被 MM 宣布为无法解决。 直到今天，当另一种资源被证明是矛盾的(在某种意义上)时，我才接受它作为引理。 根据资源(下面

• python - 用十进制数 64165 位的 `n ** n` 计算 `n`(n 乘以 n)需要多长时间？

  关闭。此题需要details or clarity 。目前不接受答案。 想要改进这个问题吗？通过 editing this post 添加详细信息并澄清问题. 已关闭 8 年前。 Improve th

• algorithm - O(n) + O(n log n) 是否等于 O(n log n)？

  我完成的一个代码遵循这个模式: for (i = 0; i < N; i++){ // O(N) //do some processing... } sort(array, array + N

• algorithm - 是否有可能证明 f(n) + g(n) = theta(n^2) for f(n) = theta(n^2) & g(n) = O(n^2)

  有没有办法证明 f(n) + g(n) = theta(n^2) 还是不可能？假设 f(n) = theta(n^2) & g(n) = O(n^2) 我尝试了以下方法:f(n) = O(n^2) &

• python - 仅当另一个 n*n 的值具有特定值时才显示 n*n 矩阵的值 (Python)

  所以我目前正在尝试计算我拥有的一些数据的 Pearson R 和 p 值。这是通过以下代码完成的: import numpy as np from scipy.stats import pearson

• postgresql - 如何从 n.n.n.n 格式的 ltree 中选择并在每个级别按数字排序？

  ltree 列的默认排序为文本。示例:我的表 id、parentid 和 wbs 中有 3 列。 ltree 列 - wbs 将 1.1.12, 1.1.1, 1.1.2 存储在不同的行中。按 wbs

• python - 为什么 while(n) n = n>>1 循环不以负数 n 终止

  我的目标是编写一个程序来计算在 python 中表示数字所需的位数，如果我选择 number = -1 或任何负数，程序不会终止，这是我的代码: number = -1 cnt = 0 while(n