标签: theorem-proving

手动或由计算机代数系统执行的符号计算可能是错误的或仅在某些假设下成立。一个经典的例子是sqrt(x^2) == x，一般情况下，这不是真的，但如果x是实数且非负，则它确实成立。

是否有使用证明助手/检查器（例如 Coq、Isabelle、HOL、Metamath 或其他）来证明符号计算的正确性的示例？我特别对微积分和线性代数示例感兴趣，例如求解定积分或不定积分、微分方程和矩阵方程。

更新： 更具体地说，了解是否有微积分和线性代数方面的本科作业示例可以正式解决（可能在证明助理的帮助下），以便解决方案可以通过自动验证证明检查器。这里有一个非常简单的精益作业示例。

我正在使用 TPTP 语法测试一些定理证明器（例如 Z3、Alt-Ergo、Vampire 等）的归纳能力。令我惊讶的是，他们都没有能够证明以下简单的猜想：

tff(t1, type, (fun: $int > $int )).

tff(ax1, axiom, ( 
    ! [A: $int] : (
        $less(A, 1) => (fun(A) = 123)
    )
)).

tff(ax2, axiom, ( 
    ! [A: $int] : (
        $greatereq(A, 1) => (fun(A) = fun($difference(A, 1))) 
    )
)).

tff(conj1, conjecture, ! [A: $int] : ($greatereq(A, 1) => (fun(A) = 123))).

% END OF SYSTEM OUTPUT
% RESULT: SOT_EWCr1V - Z3---4.8.9.0 says Timeout - CPU = 60.09 WC = 35.47 
% OUTPUT: SOT_EWCr1V - …

我的例子:方程组

  a = b+c
? e = a*c

? a = +2     ; some replaceable concrete values
? c = +18

  b = -16
? e = -32

我想要的信息

在一个方程组中,我希望得到以下知识:

我可以用来从给定值(在约束基础中)计算变量值(解决方案)的抽象公式.

(就像在高中,老师不仅希望看到结果,而且还有这样一个转化的抽象公式.)

  b = a-c     ; is an equivalent transformation from `a = b+c`
? e = (a-c)*c ; is an term replacement `b ? a-c` of `e = a*c`

我的问题

如何使用Z3Py从Z3约束方程组中检索此信息？

谢谢. - 如果有什么不清楚的地方,请评论一下是什么问题.

我正在尝试对依赖函数进行证明,而且我遇到了障碍.

所以我们假设我们有一个f-相等的定理

f-equal : ? {A B} {f : A ? B} {x y : A} ? x ? y ? f x ? f y
f-equal refl = refl

我试图证明一个关于依赖函数的平等保存的更普遍的概念,并遇到障碍.即,类型

?-equal : ? {A} {B : A ? Set} {f : {a : A} ? B a} {x y : A} ?
            x ? y ? f x ? f y

让编译器不高兴,因为它无法弄清楚fx和fy属于同一类型.这似乎是一个可以修复的问题.是吗？

注意; 使用的等价关系定义如下:

data _?_ {A : Set}(x : A) : A ? Set where
  refl : x …

我想在精益定理证明器中证明这个定理。首先，我需要定义部分有序集合之类的东西，以便我可以定义 infimum/supremum。这在精益中是如何完成的？本教程提到了 setoids，它们是具有关联等价关系的类型。但我不清楚这有什么帮助。

在使用Idris的类型驱动开发的第9章中,我们将介绍Elem带有构造函数的谓词,Here并There证明元素是向量的成员.例如

oneInVector : Elem 1 [1, 2, 3]
oneInVector = Here

twoInVector : Elem 2 [1, 2, 3]
twoInVector = There Here

我想知道如何显示元素不在向量中.它应该是通过提供这种类型的解决方案:

notThere : Elem 4 [1, 2, 3] -> Void
notThere = ?rhs

在这种情况下,表达/证明搜索没有得出答案,给出:

notThere : Elem 4 [1,2,3] -> Void
notThere = \__pi_arg => ?rhs1

扫描库Data.Vect,这些定义看起来很有用(但我不知道如何连接点):

||| Nothing can be in an empty Vect
noEmptyElem : {x : a} -> Elem x [] …

我可能遗漏了一些基本的东西.

我可以证明以下"身份":

Theorem identity_simple : forall a : Prop, a -> a.

随着intro. intro. assumption..

但是,我似乎无法证明:

Theorem identity : forall a : Prop, a.

我当然能做到intro,但这让我:

a : Prop
_________(1/1)
a

我不知道该怎么做.
第一种形式似乎是多余的,表明对所有人而言a,a意味着a.

我理解使用这种inversion策略的防爆原理:

Theorem ex_falso_quodlibet : forall (P:Prop),
  False -> P.
Proof.
  intros P contra.
  inversion contra.  Qed.

但是,我不明白Coq为了做同样的证明所采取的步骤,而是使用destruct而不是inversion:

Theorem ex_falso_quodlibet' : forall (P:Prop),
  False -> P.
Proof.
  intros P contra.
  destruct contra.  Qed.

False归纳如何被破坏？它如何影响目标并完成证明？

我不知道在哪种情况下应该使用Theorem过度Lemma或相反的用法。两者之间有什么区别（尽管在语法上）

Theorem l : 2 = 2.
  trivial.
Qed.

和这个

Lemma l : 2 = 2.
  trivial.
Qed.

？

我想not A通过假设A和发现来证明False。将目标not A转化为最短，最通用的方法是A -> False什么？

我尝试过exfalso，但是并没有增加A我的假设...

外延公理说，如果两个函数在域的每个参数上的动作相等，则它们是相等的。

Axiom func_ext_dep : forall (A : Type) (B : A -> Type) (f g : forall x, B x),
  (forall x, f x = g x) -> f = g.

平等=的定理声明的两侧是命题平等（具有单个数据类型eq_refl构造函数）。使用这个公理可以证明f = a + b和g = b + a在命题上是相等的。

但是f和g显然不等于数据结构。

你能解释一下我在这里遗漏了什么吗？可能函数对象没有正常形式？

我想在我的C++程序中使用z3 API.我想知道要包含哪些头文件以及如何运行包含z3函数等的程序.

我看到了example.cppz3源代码附带的文件,为了运行这个文件,我不得不make examples在内部执行命令的build目录中运行

g++ -o cpp_example  -I../src/api -I../src/api/c++ 
    ../examples/c++/example.cpp libz3.so -lpthread -fopenmp -lrt

现在,如果我创建任何程序,../src/api每次需要编译程序时,是否需要像这样编译它(包含和链接lib文件)？

请帮帮我,我之前从未使用过z3.任何帮助是极大的赞赏.:)