手动或由计算机代数系统执行的符号计算可能是错误的或仅在某些假设下成立。一个经典的例子是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. …这个问题涉及使用Isabelle/HOL定理证明器生成代码.
当我导出distinct列表上的函数的代码时
export_code distinct in Scala file -
我得到以下代码
def member[A : HOL.equal](x0: List[A], y: A): Boolean = (x0, y) match {
case (Nil, y) => false
case (x :: xs, y) => HOL.eq[A](x, y) || member[A](xs, y)
}
def distinct[A : HOL.equal](x0: List[A]): Boolean = x0 match {
case Nil => true
case x :: xs => ! (member[A](xs, x)) && distinct[A](xs)
}
此代码具有二次运行时.有更快的版本吗？我想到了"~~/src/HOL/Library/Code_Char"在我的理论开头导入字符串并建立列表的高效代码生成之类的东西.更好的实现distinct方法是在O(n log n)中对列表进行排序,并迭代列表一次.但我猜一个人可以做得更好吗？
无论如何,是否有更快的实现distinct和可能的其他功能Main？
遵循如何使用 - 持久堆 - 图像 - 使理论加载 - 更快 - 在isabelle和另一个建议我为Nominal Isabelle创建了一个图像:
isabelle build -v -b -d . Nominal2
堆映像是在〜/ .isabelle下创建的:
.isabelle/Isabelle2013-2/heaps/polyml-5.5.1_x86-linux/Nominal2
然后我开始了
isabelle jedit -d /path/to/Nominal-distribution -l Nominal2
我希望系统能够快速加载一个导入名义部分的理论,但这花了差不多一分钟.这是通常的吗？
我试图证明一个存在定理
\n\nlemma "\xe2\x88\x83 x. x * (t :: nat) = t"\nproof\n obtain y where "y * t = t" by (auto)\n但我无法完成证明。所以我有了必要的东西y，但我怎样才能将其纳入最初的目标呢？
我是伊莎贝尔的新手并试图证明以下简单的不等式:
lemma ineq:
"(a::real) > 0 ? a < 1 ? (b::real) > 0 ? b < 1 ? (a + b - a * b) > 0"
proof
have "1/a + 1/b > 1" by auto
qed
我试图用上面的线条显示它,但它显然不是那么容易,无论我尝试什么(show,have,from的几种组合),isabelle节目Illegal application of proof command in 'prove' mode.我不知道这是什么意思.有人可以说明如何继续吗？
〜(P /\ Q) |- Q -> 〜P
我不知道从哪里开始。否定让我困惑。
我必须在 Isabelle（一个程序）中解决这个问题，但是如果有人解释如何使用自然演绎来解决这个问题，那将有足够的帮助。
免责声明:我是伊莎贝尔的初学者.
我正在尝试使用"sqrt"将"sqrt"函数或函数和定义导出到Haskell.我的第一次尝试只是:
theory Scratch
imports Complex_Main
begin
definition val :: "real" where "val = sqrt 4"
export_code val in Haskell
end
这导致以下错误:
Wellsortedness error
(in code equation root ?n ?x ?
if equal_nat_inst.equal_nat ?n zero_nat_inst.zero_nat then zero_real_inst.zero_real
else the_inv_into top_set_inst.top_set
(?y. times_real_inst.times_real (sgn_real_inst.sgn_real y)
(abs_real_inst.abs_real y ^ ?n))
?x,
with dependency "val" -> "sqrt" -> "root"):
Type real not of sort {enum,equal}
No type arity real :: enum
所以我试图用Haskell的"Prelude.sqrt"替换"sqrt":
code_printing
constant sqrt ? (Haskell) "Prelude.sqrt _"
export_code val in Haskell …证明助手的主要功能是什么？
我只是想知道证明检查的内部逻辑。例如，有关此类助手的图形用户界面的主题使我不感兴趣。
对于编译器，我也提出了类似的问题：https : //softwareengineering.stackexchange.com/questions/165543/how-to-write-a-very-basic-compiler
我的担心是一样的，但对于校对系统。
我知道伊莎贝尔可以通过构造函数（例如列表）进行案例分析，但是
\n有没有办法根据条件是真还是假来划分案例？
\n例如，在证明以下引理时，我的逻辑（如以下无效语法中的无效证明所示）是，如果条件“x \xe2\x88\x88 A”为真，则证明会简化为微不足道的东西；当条件为假时（即“x \xe2\x88\x89 A”），它也会简化：
\nlemma "(x \xe2\x88\x88 A \xe2\x88\xa8 x \xe2\x88\x88 B) \xe2\x88\xa7 (x \xe2\x88\x88 A \xe2\x88\xa8 x \xe2\x88\x88 C) \xe2\x9f\xb9 x \xe2\x88\x88 A \xe2\x88\xa8 (x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C)"\nproof (case "x \xe2\x88\x88 A")\n (* ... case true *)\n show "x \xe2\x88\x88 A \xe2\x88\xa8 (x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C)" by (rule disjI1)\nnext (* ... case false *)\n have "x \xe2\x88\x88 B \xe2\x88\xa7 x \xe2\x88\x88 C" by simp\n show "x \xe2\x88\x88 …关于列表的证据是归纳的
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
by (induct xs) auto
但是,关于Nats的证据是
lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
by (rule add_assoc)
为什么我不需要nat_add_assoc证据上的归纳？是因为在自然数上发生了一些自动化吗？