标签: theorem-proving

有没有人尝试用Z3本身证明Z3？

甚至可以使用Z3证明Z3是正确的吗？

更理论化,是否有可能使用X本身来证明工具X是正确的？

我试图在Coq中证明以下引理:

Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
    (a <> [] \/ b <> []) -> a ++ b <> [].

现在我当前的策略是破坏一个,在打破分离之后,理想情况下我可以说,如果一个<> []那么a ++ b也必须<> [] ......这就是计划,但我似乎无法通过类似于第一个"a ++ b <> []"的子目标,即使我的上下文明确指出"b <> []".有什么建议？

我还查看了很多已有的列表定理,并没有找到任何特别有用的东西(减去app_nil_l和app_nil_r,对于某些子目标).

我正在寻找一个工具(首选GUI但CLI可以工作),它允许我输入数学表达式,然后执行它们的操作,但限制我只有数学上有效的操作.此外,该工具必须能够保存会话,然后证明给定的已保存操作集是有效的.

注意:我不是在寻找一个生成校样的系统,只是检查我手动指定的步骤是否有效.

我已经使用ACL2进行类似的操作,并且它在某些情况下表现很好但是很难用于其他所有情况.

这个小项目是我的动力.它是一种D模板类型,允许求解方程.鉴于这个等式:

(A * B) = C + D / F;

可以将任何一个符号设置为未知,并评估该表达式将导致对该变量的赋值.它的工作原理是将表达式树构建到类型中,然后使用重写规则将其转换为可以针对未知类型进行事件处理的事物.

我需要的是一些验证重写规则的方法.可以通过测试给定某种关系为真的断言来验证它们,另一种也是.

通常我有问题sledgehammer找到证据,但是当我插入它时,它不会终止.我猜sledgehammer是Isabelle最重要的部分之一,但如果证据失败则会变得很烦人.

在Sledgehammer教程中,有一个小章节"为什么Metis无法重建证明？".

它列出:

1. 尝试isar_proofs选项以获得逐步的Isar证明,其中每个步骤都是正确的metis.由于步骤相当小, metis因此更有可能重播它们.
2. 尝试使用smt证明方法而不是metis.它通常更强大,但您需要使用Z3重放证明,信任SMT求解器或使用证书.
3. 尝试blast或者auto证明方法,通过传递必要的事实unfolding,using,intro:,elim:,dest:,或simp:适当.

问题是第一个选项使证明更加冗长,并且还涉及手动干预.第二种选择很少有效.

那么第三种选择呢？我可以使用任何易于遵循的启发式方法吗？

unfolding和之间有什么区别using？也有关于如何使用的最佳做法intro:,elim:以及dest:从失败的metis证明吗？

部分例子

proof- 
  have "(det (?lm)) = (det (transpose ?lm))" by (smt det_transpose) 
  then have "(det (?lm)) = [...][not shown]"
    unfolding det_transpose transpose_mat_factor_col by auto
  then show ?thesis [...][not …

这是我对回文的归纳定义:

Inductive pal { X : Type } : list X -> Prop :=
  | pal0 : pal []
  | pal1 : forall ( x : X ), pal [x]
  | pal2 : forall ( x : X ) ( l : list X ), pal l -> pal ( x :: l ++ [x] ).

我想从Software Foundations中证明这个定理:

Theorem rev_eq_pal : forall ( X : Type ) ( l : list X ),
  l = rev l -> …

我正在尝试compile_correct从依赖类型的认证编程的第一章做一个修改过的证明.在我的版本中,我试图利用progDenote折叠的事实,并在证明主要引理的证据中使用较弱的归纳假设compile_correct.

与本书相同的代码是:

Require Import Bool Arith List.
Set Implicit Arguments.

Inductive binop : Set := Plus | Times.

Inductive exp : Set :=
  | Const : nat -> exp
  | Binop : binop -> exp -> exp -> exp.

Definition binopDenote (b : binop) : nat -> nat -> nat :=
  match b with
    | Plus => plus
    | Times => mult
  end.

Fixpoint expDenote (e : exp) : nat :=
  match …

有喜欢的战术什么simpl的Program FixpointS'

特别是,如何证明以下琐碎的陈述？

Program Fixpoint bla (n:nat) {measure n} :=
match n with
| 0 => 0
| S n' => S (bla n')
end.

Lemma obvious: forall n, bla n = n. 
induction n. reflexivity.
(* I'm stuck here. For a normal fixpoint, I could for instance use 
simpl. rewrite IHn. reflexivity. But here, I couldn't find a tactic 
transforming bla (S n) to S (bla n).*)

显然,Program Fixpoint这个玩具示例没有必要,但我在一个更复杂的设置中面临同样的问题,我需要证明Program Fixpoint手动终止.

我试图在Agda中证明一个简单的引理,我认为这是真的.

如果一个向量有两个以上的元素,那么采取head以下方法就init可以head立即采用它.

我的表述如下:

lem-headInit : ?{l} (xs : Vec ? (suc (suc l)))
                    -> head (init xs) ? head xs
lem-headInit (x ? xs) = ?

哪个给了我;

.l : ?
x  : ?
xs : Vec ? (suc .l)
------------------------------
Goal: head (init (x ? xs) | (initLast (x ? xs) | initLast xs)) ? x

作为回应.

我不完全了解如何阅读该(init (x ? xs) | (initLast (x ? xs) | initLast xs))组件.我想我的问题是; 是否有可能,该术语的含义和含义是什么.

非常感谢.

我正在试验Z3,在那里我结合了算术,量词和平等的理论.这似乎不是非常有效,事实上,在可能的情况下用所有实例化的地面实例替换量词似乎更有效.考虑下面的示例,其中我为一个函数编码了唯一名称公理,该函数f接受两个排序参数Obj并返回一个解释排序S.这个公理说明每个唯一的参数列表f返回一个唯一的对象:

(declare-datatypes () ((Obj o1 o2 o3 o4 o5 o6 o7 o8)))
(declare-sort S 0)

(declare-fun f (Obj Obj) S)
(assert (forall ((o11 Obj) (o12 Obj) (o21 Obj) (o22 Obj))
    (=> 
        (not (and (= o11 o21) (= o12 o22)))
        (not (= (f o11 o12) (f o21 o22))))))

虽然这是在逻辑中定义这样一个公理的标准方法,但是像这样实现它在计算上非常昂贵.它包含4个量化变量,每个变量可以有8个值.这意味着这导致了8^4 = 4096平等.需要Z3 0.69s和2016量词实例来证明这一点.当我编写一个生成此公式实例的简单脚本时:

(assert (distinct (f o1 o1) (f o1 o2) .... (f o8 o7) (f o8 o8)))

生成这些公理需要0.002s,而在Z3中需要0.01s(或更少).当我们增加域中的对象或函数的参数数量时,f这种差异会迅速增加,并且量化的情况很快变得不可行.

这让我想知道:当我们有一个有界域时,为什么我们首先在Z3中使用量词？我知道SMT使用启发式方法来寻找解决方案,但我感觉它仍然无法与一个简单的特定于域的地面实施竞争,后者将基础实例提供给SMT,这仅仅是SAT解决方案.我的直觉是否正确？

我试图通过 Isabelle（定理证明者）的 Isar 章节，第一个陈述是：

lemma "¬ surj(f :: 'a ? 'a set)"

我想了解常数surj是什么。我知道查找定理很容易：

thm notI

显示：

(?P ? False) ? ¬ ?P

我试过谷歌搜索，surj但没有任何有用的东西出现。

我去了文档（https://isabelle.in.tum.de/documentation.html），但我找不到一种简单的方法来搜索它（例如使用搜索栏）。

人们在做证明时如何搜索定义或一般内容？你如何以有效的方式为伊莎贝尔查找东西，而不必求助于 SO 等琐碎的东西（我应该能够自己查找）？像man命令或-help标志等？

我意识到底部有一个查询框，所以我试了一下。但它向我展示了 38 个定理。这是一个很好的进步，但我觉得这是因为当我说我的引理时，伊莎贝尔确切地知道它在使用哪个。有没有办法强制 Isabelle 透露它使用的定义（因为它显然必须知道它使用的是什么）。

我刚刚注意到：

thm surj_def

显示：

surj ?f = (?y. ?x. y = ?f x)

确实显示了一些东西...这个问题是值得的，因为我发现了查询框，但无论如何人们在 Isabelle 中的发展方式仍然很棒。

编辑：

如果它与解释他们做了什么或类似的事情的战术文档相关联，那也会很好......