问题标签 [theorem-proving]

Isabelle 中的“商类型模式”是什么？

我在互联网上找不到任何解释。

我正在尝试在 OCaml 中开发 Coq 策略，我在其中构建了一个constr术语，现在想用这个术语在目标中实例化一个存在变量。我正在尝试调用该Evar_tactic.instantiate策略；但它需要一个类型的参数 Tacinterp.interp_sign * Glob_term.glob_constr。反正有没有转换constr成这种类型？或者我可以从 OCaml 级别实例化 evas 的任何其他方式？

其次，在 Coq 中有一种叫做setand的策略。pose我找不到它们的定义位置。如果我想从 OCaml 使用它们，我应该怎么做？

我只是用 Coq 证明定理的初学者，我坚持这个目标：

任何人都可以为我做这件事吗？

有人可以帮助了解如何在 Z3 中正确使用“for all”吗？我一直在查看文档，但找不到信息。我想做的是

在“foo”中，我需要在 Z3 中说一些相当于

“让（u，r）在{（断言（（u，r）在用户中）（断言（r，t）在角色中）}中可运行（t）”

我不知道如何将 runnable 中的第一个元素断言在用户中，然后将第二个元素断言在角色中。

(declare-sort Task) (declare-sort Role) (declare-sort User) (declare-fun runnable (Task) (User Role)) (declare-fun perm (Role Task) Bool) (declare-fun users (User Role) ) 布尔)

(assert (forall (t Task)) (foo))

(check-sat) (get-model)

据我所知，我可以声明一个返回多个元素的函数。假设我有一个函数 x，它接收一个排序 T 并返回一个排序 U 和一个排序 R

(declare-sort T) (declare-sort R) (declare-sort U)

（声明乐趣 x (T) (UR)）

那么，当调用函数 x 返回元素时，我该如何访问......可以说我需要断言将 U 传递给一个函数，将 R 传递给另一个函数.. 可以这样做吗？

我创建了 4 种（任务、角色、用户和运行），最后一个接收 2 个参数，然后我为它们中的每一个声明一个乐趣，包括一个用于 Run ，调用 P 接收 2 个参数以创建 Run 的“实例” . 然后我创建了两个数组，一个包含用户角色“关系”（Privs），另一个包含角色任务“关系”（角色）。我使用这两个数组来断言当查看用户 u 时，它是否在 Privs 中具有角色 r，如果在查看角色 r 中的角色时，它是否具有任务 t。到目前为止，我设法在单独的行中做到这一点，如下所示：

但是现在我试图取笑它接收一个 Run (User,Role 对) 并且在函数内部断言相同但对于 P 中的所有用户及其所有角色。这可以通过将运行排序变量传递给函数来完成吗？？用于访问其内部的元素（用户、角色）？

I'm running some Lattice proofs through Prover9/Mace4. I'm using a non-standard axiomatization of the lattice join operation, from which it is not immediately obvious that the join is commutative, associative and idempotent. (I can get Prover9 to prove that it is -- eventually.)

I know that Prover9 looks for those properties to help it search faster. I've tried putting those properties in the Additional Input section (I'm running the GUI version 0.5), with

Q1: Is this the way to get it to look at hints?

Q2: Is there a good place to look for help on speeding up proofs/tips and tricks? (If I can get this to work, there are further operators I'd like to give hints for.)

For ref, my axioms are (bi-lattice with only one primitive operation):

(EDIT after DougS's answer posted.)

Wow! Thank you. Orders-of-magnitude speed-up.

Some follow-on q's if I might ...

Q3: The generated hints seem to include all of the initial axioms plus the goal -- is that what I should expect? (Presumably hence your comment about not needing all of the hints. I've certainly experienced that removing axioms makes a proof go faster.)

Q4: What if I add hints that (as it turns out) aren't justified by the axioms? Are they ignored?

Q5: What if I add hints that contradict the axioms? (From a few trials, this doesn't make Prover9 mis-infer.)

Q6: For a proof (attempt) that times out, is there any way to retrieve the formulas inferred so far and recycle them for hints to speed up the next attempt? (I have a feeling in my waters that this would drag in some sort of fallacy, despite what I've seen re Q3 and Q4.)

在Isabelle/HOL 的编程和证明中，练习 2.4 建议在简单的算术表达式上使用“algebra_simps”，表示为“数据类型 exp”。有人可以举一个例子，如何使用 algebra_simps 证明这些表达式的一些简单属性？例如'Mult ab = Mult b a'？

一般来说，我试图证明以类似形式表示的简单算术表达式的等价性（使用有限的运算符集）。

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

我想证明的定理来自软件基础：

我对证明的非正式概述如下：

假设l0是一个任意列表，使得l0 = rev l0. 那么以下三种情况之一必须成立。l0有：

(a) 零元素，在这种情况下，根据定义它是回文。

(b) 一个元素，在这种情况下，根据定义，它也是一个回文。

(c) 两个或更多元素，在这种情况下l0 = x :: l1 ++ [x]，对于一些元素x和一些列表l1，使得l1 = rev l1.

现在，既然l1 = rev l1，以下三种情况之一必须成立......

递归案例分析将终止任何有限列表l0，因为分析的列表的长度通过每次迭代减少 2。如果它终止于任何 list ln，则它的所有外部列表l0也是回文，因为通过在回文的任一端附加两个相同元素构造的列表也是回文。

我认为推理是合理的，但我不确定如何将其正式化。它可以在 Coq 中变成证明吗？对所使用的策略如何起作用的一些解释将特别有帮助。

我正在 Idris 中编写一个基本的单子解析器，以适应 Haskell 的语法和差异。我有基本的工作正常，但我坚持尝试为解析器创建 VerifiedSemigroup 和 VerifiedMonoid 实例。

事不宜迟，这里是解析器类型、Semigroup 和 Monoid 实例，以及 VerifiedSemigroup 实例的开始。

我基本上被困在之后intros，具有以下证明者状态：

看起来我应该能够以某种方式rewrite一起使用appendAssociative，但我不知道如何“进入” lambda \s。

无论如何，我被困在练习的定理证明部分——而且我似乎找不到太多以 Idris 为中心的定理证明文档。我想也许我需要开始查看 Agda 教程（尽管 Idris 是我确信我想学习的依赖类型语言！）。