以下示例来自《软件基础》一书的 Poly 章节。
Definition fold_length {X : Type} (l : list X) : nat :=
fold (fun _ n => S n) l 0.
Theorem fold_length_correct : forall X (l : list X),
fold_length l = length l.
Proof.
intros.
induction l.
- simpl. reflexivity.
- simpl.
1 subgoal
X : Type
x : X
l : list X
IHl : fold_length l = length l
______________________________________(1/1)
fold_length (x :: l) = S (length l)
我希望它能简化左侧的步骤。当然应该可以。
Theorem fold_length_correct : forall …我知道apply f in H可以用来将假设应用于函数，并且我知道apply f with a b c可以用来提供在直接应用时无法自行推断的参数f。
是否可以以某种方式结合使用两者？
现在，我要从软件基础中继续前进，在软件基础中，一切都放在盘子上，我很难弄清楚如何建立自己的项目。那里有一些说明，但由于我刚刚开始，在尝试设置 hello world 程序时我发现这太复杂了。我还有其他一些问题。
hello.v
我成功编译空文件的方法hello.v是将以上内容放入_CoqProject文件中，然后运行...
coq_makefile -o Makefile.coq -f _CoqProject
这会生成 makefile。
make -f Makefile.coq
这会编译项目，但我无法make hello仅使用它，而 Proof General 在编译单个文件时恰好使用它。
make hello.vo
make: *** No rule to make target 'hello.vo'. Stop.
以上是我尝试从 Proof General 进行编译时得到的结果。
我应该在这里做什么？使用空文件设置项目以与 Proof General + Emacs 一起使用的最简单的方法是什么？
-Q . VFA
另外，为什么《科幻小说》第 3 卷尽管文件内容不多，但仍然有效_CoqProject？它只有以上这些。
Coq 8.10.1 的 VST（验证软件工具链）2.5v 库遇到问题：
VST 的最新工作提交出现错误，即“不支持内部结构复制”。最小的例子：
struct foo {unsigned int a;};
struct foo f() {
struct foo q;
return q; }
启动证明时出现错误：
错误：策略失败：表达式 (_q)%expr 包含内部结构复制，这是可验证 C（级别 97）当前不支持的 C 功能。
这是由于floyd/forward.vcheck_normalized中的：
Fixpoint check_norm_expr (e: expr) : diagnose_expr :=
match e with
| Evar _ ty => diagnose_this_expr (access_mode ty) e
...
所以，问题是：
1) 存在哪些建议的解决方法？
2）这个限制的原因是什么？
3) 从哪里可以获得不支持的功能列表？
换句话说：如果我们分别删除归纳和共归纳数据类型使用的终止检查和防护条件，归纳/共归纳和修复/共归纳之间是否不再有根本区别？
\n我所说的“根本差异”是指 Coq\xe2\x80\x93 核心演算的差异，而不是语法和证明搜索等方面的差异。
\n这似乎最终归结为一个关于构造微积分的问题。
\n注意：我知道一个定理证明者跳过了递归/核心递归的终止检查/防护可以证明False\xe2\x80\x93so，如果有帮助，请将其视为有关非完全编程的问题而不是证明。
由于Coq有强大的类型推断算法，我想知道我们是否可以根据Notation的变量“重载”不同的重写符号。
作为一个例子，我将借用我在 Coq 中形式化类型化语言语义的一篇作品。在这种形式化中，我有类型对和表达式对，并且我想对它们各自的构造函数使用相同的符号：{ _ , _ }。
Inductive type: Type := ... | tpair: type -> type -> type | ...
Inductive expr: Type := ... | epair: expr -> expr -> expr | ...
Notation "{ t1 , t2 }" := tpair t1 t2
Notation "{ e1 , e2 }" := epair e1 e2
我知道最后一个语句会引发错误，因为符号已经定义；如果有人考虑过围绕它进行欺骗，或者是否有另一种“官方”方式来做到这一点，我将不胜感激。
手动或由计算机代数系统执行的符号计算可能是错误的或仅在某些假设下成立。一个经典的例子是sqrt(x^2) == x，一般情况下，这不是真的，但如果x是实数且非负，则它确实成立。
是否有使用证明助手/检查器（例如 Coq、Isabelle、HOL、Metamath 或其他）来证明符号计算的正确性的示例？我特别对微积分和线性代数示例感兴趣，例如求解定积分或不定积分、微分方程和矩阵方程。
更新： 更具体地说，了解是否有微积分和线性代数方面的本科作业示例可以正式解决（可能在证明助理的帮助下），以便解决方案可以通过自动验证证明检查器。这里有一个非常简单的精益作业示例。
我想在 Coq 证明脚本中编写中间引理，例如，在 SCRIPTProof. SCRIPT Qed.本身中 - 类似于在 Isar 中的做法。在 Coq 中如何做到这一点？例如：
have Lemma using Lemma1, Lemma2 by auto.
我知道这个exact陈述，想知道是否就是这样……但我也想得到这个陈述的证据，就像在伊萨尔我们有have by auto或using Proof. LEMMA_PROOF Qed.
为了使其具体化，我试图做这些非常简单的证明：
Module small_example.
Theorem add_easy_induct_1:
forall n:nat,
n + 0 = n.
Proof.
intros.
induction n as [| n' IH].
- simpl. reflexivity.
- simpl. rewrite -> IH. reflexivity.
Qed.
Theorem plus_n_Sm :
forall n m : nat,
S (n + m) = n + (S m).
Proof. …Theorem law_of_contradiction : forall (P Q : Prop),\n P /\\ ~P -> Q.\nProof.\n intros P Q P_and_not_P.\n destruct P_and_not_P as [P_holds not_P].\n我正在尝试真正理解这个intros关键字。假设我们想证明P /\\ ~P -> Q。好的，以某种方式intros P Q介绍P和Q。但是这是什么意思？它能识别出P要Q证明的事物吗？关于什么P_and_not_P？它是什么？为什么P和Q使用相同的名称，而is却P_and_not_P定义了一个名称？
更新：
\n看起来它是逐项匹配的：
\nTheorem modus_tollens: forall (P Q : Prop),\n (P -> Q) -> ~Q -> ~P.\nProof.\nintro P.\nintro Q.\nintro P_implies_Q.\nintro not_q.\nintro not_p.\n给出
\nP Q \xe2\x84\x99\nP_implies_Q P \xe2\x86\x92 …我有以下感应类型和测试功能：
Inductive parameter : Type :=
| Nop
| OneP : forall A, A -> parameter
| TwoP : forall (A : Type) (r : nat) (b : A), parameter
.
Check (TwoP nat 1 5).
Definition test (p : parameter) : option (nat * nat) :=
match p with
| TwoP nat x y => Some (x, y)
| _ => None
end.
测试功能失败并出现错误：
术语“Some (x, y)”的类型为“option (Datatypes.nat * nat)”，而预期的类型为“option (Datatypes.nat * Datatypes.nat)”。
我不明白为什么我的定义不起作用。nat 和 Datataypes.nat 之间有区别吗？
任何帮助，将不胜感激。谢谢！
coq ×10
isabelle ×2
c ×1
codata ×1
coinduction ×1
coq-tactic ×1
coqide ×1
corecursion ×1
gallina ×1
hol ×1
isar ×1
notation ×1
overloading ×1
verifiable-c ×1