theorem-proving_编程技术问答社区_程序员问答知识库

以下是关于 theorem-proving 的编程技术问答

当我写算法时，我通常会在评论中写下不变性. 例如，一个函数可能会返回有序列表，另一个函数期望订购列表. 我知道定理掠夺者存在，但是我没有使用它们的经验. 我也相信智能编译器[sic！]可以利用它们来优化程序. 因此，是否可以写下不变性并使编译器检查它们? 解决方案好吧，答案是肯定的.没有办法只编写与类型分开的不变性并进行检查.但是，在Haskell的研究叉中实施了这一实施，但是:您还有其他各种选择.首先，您可以使用:然后，使用适当的标志，您可以关闭这些主张以进行生产. 更一般而言，您可以在类型中编码不变性.我打算在这里添加更多，但Dons将我击败了. 另一个例子是红色树木的非常好的编码:其他解决方案以下是一个特技，但这是一个安全的特技，所以请在家尝试一下.它使用一些有趣的新玩具将 order orders 烘烤到Mergesort中. {-# LANGUAGE GADTs, PolyKinds, KindSignatures, MultiP

2 2023-10-30 编程技术问答社区 haskell types invariants theorem-proving

Isabelle中的" Arith"和" Presburger"有什么区别?

到目前为止，我在Isabelle中遇到的每个目标也可以通过arith解决，也可以通过presburger来解决，反之亦然，例如 lemma "odd (n::nat) ⟹ Suc (2 * (n div 2)) = n" by presburger (* or arith *) 两个求解器之间有什么区别?一个人可以解决的目标示例，但另一个不能很好. 编辑:我设法提出了arith证明presburger无法处理的引理.似乎这与实数有关: lemma "max i (i + 1) > (i::nat)" by arith -- ✔ lemma "max i (i + 1) > (i::nat)" by presburger -- ✔ lemma "max i (i + 1) > (i::real)" by arith -- ✔ lemma "max i (i + 1) > (i::real)" by presburger -- ✘ 解决方案

20 2023-09-06 编程技术问答社区 solver isabelle theorem-proving

定理使用与HOL推理规则的SML从第一原则证明

我试图使用带有HOL推理规则的SML证明定理 [] |- p /\ q q /\ p :thm .这是SML代码: val thm1 = ASSUME ``p:bool /\ q:bool``; val thm2 = ASSUME ``p:bool``; val thm3 = ASSUME ``q:bool``; val thm4 = CONJ thm2 thm3; val thm5 = CONJ thm3 thm2; val thm6 = DISCH ``(q:bool/\p:bool)`` thm4; val thm7 = DISCH ``(p:bool/\q:bool)`` thm5; val thm8 = IMP_ANTISYM_RULE thm6 thm7; 上述代码的结果是: val thm8 = [(p :bool), (q :bool)] |- (q :bool) /\ (p :bool) p /\ q: thm 我在做什么错?

8 2023-09-05 编程技术问答社区 sml theorem-proving hol

Isabelle：通过类型构造函数 "Set.set "不支持数据类型的递归出现

问题我想知道是否有自然的编码方式这样: type_synonym Var = string datatype Value = VInt int | ... datatype Cmd = Skip | NonDeterministicChoice "Cmd set" | ... 动机是给定义一些规范命令就非确定性选择而言，例如: Magic == NonDeterministicChoice {} Rely c r z = Defined using set compreehension and NonDeterministicChoice isabelle抱怨" cmd set"中的" cmd"类型的递归发生，即: 通过类型的" cmd"类型的不支持的递归发生构造函数" set.set"在类型表达式" cmd set"中.使用" BNF" 命令注册" set.set"为有限的天然函数以允许通过它嵌套(CO)递归查看isabell

2 2023-08-15 编程技术问答社区 recursion isabelle theorem-proving

用pytorch验证卷积定理

基本上该定理如下: f(f*g)= f(f)xf(g) 我知道这个定理，但我只是无法通过使用pytorch来重现结果. 以下是可再现的代码: import torch import torch.nn.functional as F # calculate f*g f = torch.ones((1,1,5,5)) g = torch.tensor(list(range(9))).view(1,1,3,3).float() conv = F.conv2d(f, g, bias=None, padding=2) # calculate F(f*g) F_fg = torch.rfft(conv, signal_ndim=2, onesided=False) # calculate F x G f = f.squeeze() g = g.squeeze() # need to pad into at least [w1+w2-1, h1+h2-1], which

4 2023-07-16 编程技术问答社区 pytorch fft convolution theorem-proving

使用序言显示布尔逻辑失败的原因

假设我有以下布尔逻辑: Z = (A or B) and (A or C) 是否可以使用Prolog(可能与某些库一起使用)来弄清楚为什么Z是错误的，并以以下格式返回答案: z是错误的，因为A或(B和C)是False 如果我替换了一些已知值(或全部)(c = true)，它会说:z是错误的，因为a是false 它可以告诉我哪个规则或规则的哪一部分导致了此问题:z是错误的，因为a在" z =(a或b)和(a或b)和(a或c)的(a或b)中是错误的? 再次对z = true的问题再次相同. 或这些问题不适合Prolog，我应该看一些SAT求解器或其他问题? 我的目标是分析程序的数据流，并回答类似的问题.我希望这是真的/错，但事实并非如此? 解决方案我必须说这是一个很酷的问题. 我看到了两种基本方法，其中一种使用Prolog's read_term/2以及该术语中使用的变量名称获得一个术语，看起来像这样: ?- read_term(T

12 2023-07-14 编程技术问答社区 prolog theorem-proving

证明一个可逆列表在Coq中是一个调色板

这是我对pelindromes的归纳定义: 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] ). 和我想证明的定理，从软件基础: Theorem rev_eq_pal : forall ( X : Type ) ( l : list X ), l = rev l -> pal l. 我对证明的非正式大纲如下: 假设l0是一个任意列表，因此l0 = rev l0.然后必须持有以下三个案件之一. l0有: (a)零元素，在这种情况下，它是定义上的回文. (b)一个元素，在这种情况下，它也是定义上的回文. (c)两个或更多元素，在这种情况下，对于某些

20 2023-05-16 编程技术问答社区 coq palindrome theorem-proving logical-foundations

哈斯喀尔定理证明策略作为索引漏斗和单体

我试图跟随此博客文章在Haskell中制作一个简单的直觉定理.范·巴克尔(Van Bakel)先生建议使用索引的单子进行证明国家操纵.这是索引单元的建筑物(相当于Control.Monad.Indexed的定义): class IFunctor f where imap :: (a -> b) -> f j k a -> f j k b class IFunctor m => IPointed m where ipure :: a -> m i i a class IPointed m => IApplicative m where iap :: m i j (a -> b) -> m j k a -> m i k b class IApplicative m => IMonad m where ibind :: (a -> m j k b) -> m i j a -> m i k b ijoin :: IMonad m => m i j (m j k a)

40 2023-05-16 编程技术问答社区 haskell monads theorem-proving

在证明一个定理时进行循环

我试图在用debruijn索引和替换中形式化lambda conculus后，试图证明以下定理. Theorem atom_equality : forall e : expression , forall x : nat, (beta_reduction (Var x) e) -> (e = Var x). 这些是表达和β降低的定义 Inductive expression : Type := | Var (n : nat) | Abstraction (e : expression) | Application (e1 : expression) (e2 : expression). . . Inductive beta_reduction : expression -> expression -> Prop := | beta_1step (x y : expression) : beta_1reduction x y -> beta_red

26 2023-03-31 编程技术问答社区 coq proof lambda-calculus theorem-proving

Coq：生活在Set中的非列表数据结构？

如果我有以下行: Definition Foo : Set := list nat. 然后我没有问题. 但是，假设我想对Coq.Lists.ListSet进行相同的操作，一个代表有限集的库为列表: (*Section first_definitions. Variable A : Type. Definition listset := list A.*) Definition Bar : Set := listset nat. 我收到以下错误: The term "listset nat" has type "Type" while it is expected to have type "Set" (universe inconsistency). 有没有办法"铸造" listset，以便它生活在Set而不是Type中?即，如果我知道我将使用listset与类型Set的参数使用，是否有一种方法可以使它生存在Set的继承结构中? 为什么发生错误的

34 2023-03-31 编程技术问答社区 functional-programming coq dependent-type theorem-proving

担保人：承认错误

有没有办法在coq中宣称? 假设我有这样的定理: Theorem test : forall m n : nat, m * n = n * m. Proof. intros n m. assert (H1: m + m * n = m * S n). { Admitted. } Abort. 上面的断言似乎对我不起作用. 我收到的错误是: Error: No focused proof (No proof-editing in progress). 我想要的是Haskell中的undefined.从赛赛上，我稍后再回到这一点，并证明这一点. Coq中有类似的东西可以实现吗? 解决方案一般而言，策略admit(低案例的首字母)承认当前的子目标.因此，assert . admit.在您的情况下应起作用. 或以下完整的荣耀. Theorem test : forall m n : nat,

58 2023-03-31 编程技术问答社区 coq theorem-proving

我怎样才能读懂Coq'的proj1_sig的定义？

在coq中，sig定义为 Inductive sig (A:Type) (P:A -> Prop) : Type := exist : forall x:A, P x -> sig P. 我读为 " A SIG P是一种类型，其中P是一个函数，占用A并返回Prop.定义了类型，以使A型A类型A的元素X属于SIG P型，如果P X持有." proj1_sig定义为 Definition proj1_sig (e:sig P) := match e with | exist _ a b => a end. 我不确定该怎么做.有人可以提供更直观的理解吗? 解决方案非依赖对与sig 定义了类型，使得A类型的元素x是sig P type sig P如果P x保持. 这不是完全正确的:我们不能说x

20 2023-03-31 编程技术问答社区 coq theorem-proving

Coq简化程序Fixpoint

是否有策略simpl for Program Fixpoint s? 特别是一个人如何证明以下微不足道的陈述? 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，但是我在更复杂的环境中面临着同样的问题，我需要

18 2023-03-31 编程技术问答社区 coq theorem-proving totality

Z3Py：从方程组中生成抽象公式

我的示例:方程系统伪代码约束基础 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约束系统中检索此信息? 谢谢. - 如果有什么不清楚的话，请评论出什么问题. 解决方案 Z3不是提

18 2023-03-28 编程技术问答社区 math constraints z3 proof theorem-proving

Isabelle：对包括常数因子的矩阵进行转置

在我的isabelle理论中，我有一个具有恒定因素的矩阵: ... k :: 'n and c :: 'a (χ i j. if j = k then c * (A $ i $ j) else A $ i $ j) 我可以计算转置矩阵: (transpose (χ i j. if j = k then c * (A $ i $ j) else A $ i $ j)) 在我眼中，后者应该等于 (χ i j. if i = k then c * (A $ j $ i) else A $ j $ i)) 按transpose的定义.但是这是错误的.我在这里的错误是什么? 顺便说一句，转移的定义是: definition transpose where "(transpose::'a^'n^'m ⇒ 'a^'m^'n) A = (χ i j. ((A$j)$i))" 解决方案我不确定您的意思是:，但这不是正确的.您期望的是真实的，可以在I

26 2023-03-22 编程技术问答社区 matrix isabelle theorem-proving

Z3: 执行矩阵操作

我的情况我正在从事一个需要: 的项目证明找到一个带有未知矩阵条目值的模型. 我的问题使用矩阵操作表达公式的最佳方法是什么他们可以通过z3解决吗? ( z3py的sudoku 示例不是非常优雅，似乎不适合更复杂的矩阵操作.) 谢谢. - 如果有的话，请留下问题评论. 解决方案 Z3不支持这样的矩阵，因此编码它们的最佳方法是编码它们代表的公式.这与Sudoku示例如何编码事物大致相同.这是一个简单的示例，例如2x2真实矩阵(z3py链接: http://rise4fun.com/z3py/mynb ): # nonlinear version, constants a_ij, b_i are variables # x_1, x_2, a_11, a_12, a_21, a_22, b_1, b_2 = Reals('x_1 x_2 a_11 a_12 a_21 a_22 b_1 b_2') # linear version (all

14 2023-03-22 编程技术问答社区 matrix z3 theorem-proving

如何证明大O记号

在我的算法课中，我们正在讨论大o符号，我被困在证明这个示例问题: 证明f(n) = 3n lg n + 10n + lg n + 20 = O(n lg n) 细节将不胜感激. 解决方案 Big O符号是渐近符号，这全是关于案例的近似(最坏，最佳和中部). 在您的示例中，nlgn的增长速度比n和lgn都快，而且常数值无关，并且可以在这样的近似值中忽略. 因此，复杂性为O(nlgn). 其他解决方案您需要证明的只是某些M和X0: m n lg n> = 3n lg n + 10n + lg n + 20，大于x0 4对于M 很容易我确定您可以计算上述不等式所持的一些X0，然后很容易地表明，对于所有N大于x0 在4到中替换后，它有助于简化上述 (n-1)lg n> = 10n + 20 一旦任何n都足够大，应该很明显lg n> 1，因此，n的增加，超出该n的右侧增加了1，而左侧则增加了1. .

10 2023-03-20 编程技术问答社区 c++ algorithm math theorem-proving

Z3定理验证器。勾股定理 (非线性算术)

为什么? 我的问题发生的用户酶上下文我定义了三角形的3个随机项目. Microsoft Z3应该输出: 约束是满意的还是有无效的输入值? 所有其他三角项目的模型，将所有变量分配给具体值. 为了限制我需要 assert 三角形平等的项目 - 我想从毕达哥拉斯定理开始((h_c² + p² = b²) ^ (h_c² + q² = a²)). 问题我知道Microsoft Z3仅具有解决非线性算术问题的功能有限.但是，即使是某些手工计算器也能够求解一个非常简化的版本这样: (set-option :print-success true) (set-option :produce-proofs true) (declare-const a Real) (declare-const b Real) (assert (= a 1.0)) (assert (= b 1.0)) (assert (exists ((c Real))

110 2023-03-13 编程技术问答社区 logic z3 smt constraint-programming theorem-proving

有没有办法用Djinn在Emacs中自动生成Haskell代码？

标题几乎说明了一切.我正在寻找这样的东西: f :: Int -> Bool -> Int f = _body djinn可以使用定理证明通过证明该类型居住的函数来生成代码. 我想知道，是否有一种现有方法可以从emacs内获得此功能?因此，我没有在代码中编写TemplateHaskell，而只是在代码上运行一个命令，然后插入生成的代码? 我已经安装了GHC-MOD，但我对此并不熟悉. 解决方案引用serras的相关部分 emacs指南: 这很好，但是在某些情况下，GHC-Mod可以为您做更多的事情:它可以写出您的整个表达！它通过利用 Djinn.例如，让我们回到Maybemap之后的定义分裂: maybemap没什么f = _maybemap_body maybemap(仅x)f = _maybemap_body 如果在每个孔中按C-C C-A，则有几个选项将显示的代码将显示，包括第一个案例，什么都没有，只有x在第二种情况下

12 2022-10-30 编程技术问答社区 haskell emacs ghc theorem-proving ghc-mod

应该如何理解 "lemma "函数的一般类型？

也许这是一个愚蠢的问题.这是解决此问题的一种方法是编码引理，由参数化方程，以及Haskell函数.通常，这样的引理可以编码为类型的函数: ∀ x1 ... xn. Natty x1 → ... → Natty xn → ((l ~ r) ⇒ t) → t 我以为我理解了RankNTypes，但是我无法理解该命题的最后一部分.我正在非正式地阅读它，为"给定术语l ~ r，返回该术语".我敢肯定这种解释是错误的，因为它似乎导致了一个循环:我们不知道l ~ r直到证明本身的结论，所以我如何期望将其作为证明的假设一个术语需要吗? 我本来希望平等证明具有更多类型: Natty x1 → ... → Natty xn → l :~: r 非正式地，"给定一堆Natty s，返回l和r相等的命题的证明"(使用GHC的 data.type.equality ).这对我来说更有意义，并且似乎与您在其他相关类型的系统中所说的话保持一致.我猜这等同于纸上的版本，但是我正在努力

14 2022-10-29 编程技术问答社区 haskell theorem-proving dependent-type higher-rank-types

首页
<
1
>
尾页