您如何查找CoQ证明策略的定义或实施？
我正在查看this： Theorem eq_add_1 : forall n m, n + m == 1 -> n == 1 / m == 0 / n == 0 / m == 1. Proof. intros n m. rewrite one_succ. intro H. assert (H1 : exists p, n + m == S p) by now exists 0. appl
..
proof相关内容
如何证明这个不变量?
我的目标是证明霍纳法则是正确的.为此，我将霍纳当前计算的值与“真实"的值进行比较.多项式. 所以我做了这段代码: 带有 SPARK_Mode 的包体 Poly 是函数 Horner (X : Integer; A : Vector) return Integer isY : 整数 := 0;Z : 整数 := 0 与 Ghost;开始对于我在反向 A'First .. A'Last 循环pra
..
使用 SPARK 证明 Select Sort 算法
我试图证明我在 Ada 中实现的 Select Sort 是正确的.我尝试了一些循环不变量，但使用 gnatprove 只能证明内循环的不变量: 使用 SPARK_Mode 的包体选择是过程排序(A : in out Arr)是I: 整数 := A'First;J:整数；Min_Idx:整数；Tmp:整数；开始当我
..
证明时间复杂度
我正在尝试确定这两个函数的复杂度，其中 D 是一个整数，而 list 是一个整数列表: def solve(D, list):对于列表中的元素:doFunc(元素，D，列表)def doFunc(元素, D, 列表):数量 x = 0如果(D > 0):对于列表中的其他元素:如果 otherElement == 元素:数量 x += 1返回数量 x + (doFunc ((element+1),
..
在 agda 中使用计算函数的值进行证明
我仍在尝试围绕 agda 进行思考，所以我写了一个小井字游戏类型 data Game : Player ->维克广场 9 ->设置在哪里开始:游戏 x ( - ∷ - ∷ - ∷- ∷ - ∷ - ∷- ∷ - ∷ - ∷ [] )xturn : {gs : Vec Square 9} ->(n: ℕ) ->游戏 x gs ->≤(#ofMoves gs) ->游戏 o (makeMove gs
..
外行人的抽水引理是什么?
我看到了这个问题，并且很好奇泵引理是什么(维基百科a> 没有多大帮助). 我知道这基本上是一个理论证明，必须是真实的，才能使语言属于某个类别，但除此之外，我真的不明白. 有人愿意尝试以非数学家/comp sci 博士可以理解的方式在相当细粒度的水平上解释它吗? 解决方案 抽水引理是一个简单的证明，表明一种语言不是正则的，这意味着无法为其构建有限状态机.规范示例是语言 (a^n)
..
上下文无关语言问题(Pumping Lemma)
我知道这与编程没有直接关系，但我想知道是否有人知道如何将泵引理应用于以下证明: 证明 L={(a^n)(b^n)(c^m) : n!=m} 不是上下文无关语言 我对应用抽水引理非常有信心，但这真的让我很恼火.你怎么看? 解决方案 编辑:我完全把你引向了错误的轨道.这就是当我自己还没有完全解决问题时尝试提供帮助时会发生的情况. 奥格登引理 假设 L 是上下文无关的.根
..
我如何证明这种类型的Haskell定理?
关于清单1 ，我将如何证明类型级别的公理 (t a)=(t(getUI(t a))) 持有? 列出1 数据连续a =连续a派生(Show，Eq)类UI在哪里-...实例UI Int其中-...类别tgetUI ::(UI a)=>(t a)->一种实例类别连续哪里getUI(continuant a)=一个-公理(t a)=(t(getUI(t a)))是否适用于给定类型?测试
..
唯一的最小生成树充分必要的条件
给出图G，这是充分必要的条件，因此该图具有唯一的最小生成树?此外，如何证明这些条件? 到目前为止，我发现这些条件是: 1)对于将V(G)分为两个子集的每个分区，每个子集中具有一个端点的最小权重边是唯一的. 2)在G的任何循环中，最大重量边都是唯一的. 但是我不确定这是否正确.即使万一是正确的，我也无法证明其正确性. 解决方案 实际上，唯一的MST有必要的充分条件.在
..
如何删除Isabelle中所有出现的子多重集?
因此，我想定义一个函数(我们称其为 applied )，该函数将消除另一个多重集中所有子多重集的所有出现，并用单个元素替换每次出现.例如， 应用了{#a，a，c，a，a，c#}({#a，a，c#}，f)= {#f，f#} 所以起初我尝试了一个定义: 定义的应用:: :: [['a multiset，('a multiset×'a)]⇒'a multiset';在哪里“应用的ms t
..
如何处理"false = true"；证明定理中的命题
我不熟悉coq并试图证明这个定理 归纳表达式:类型:=|Var(n:nat)..定理variable_equality:forall x:nat，forall n:nat，((等于x n)= true)->(Var x = Var n). 这是对等的定义 固定点等于(n1:nat)(n2:nat):=匹配(n1，n2)与|(O，O)＝>真的|(O，S n)＝>错误的|(S n，O)＝>错误
..
证明定理时循环
在用Debruijn指数形式化Lambda演算并在Coq中进行替换之后，我试图证明以下定理. 定理atom_equality:forall e:expression，forall x:nat，(beta_reduction(Var x)e)->(e = Var x). 这些是表达和减少beta的定义 归纳表达式:类型:=|Var(n:nat)|抽象(e:表达式)|应用程序(e1:表达式)(
..
有按位算子定律吗?
从代数定律的角度考虑，我想知道在位操作领域中是否存在与代数类似的任何官方指南. 代数示例 a-b =/= b-a 让 a = 7 和 b = 5 a-b = 2 b-a = -2 让 a = 10 和 b = 3 a-b = 7 b-a = -7 因此如果>b ， b-a 等于 a-b 的负值.因此，我们可以说 | a-b |= | b-a |
..
如何证明C语句-x，〜x + 1和〜(x-1)产生相同的结果?
我想知道这句话背后的逻辑，即证明.对于任何x，C表达式-x，〜x + 1和〜(x-1)都产生相同的结果.对于特定示例，我可以证明这是正确的.我认为证明这一点的方式与二进制补码的性质有关.有任何想法吗? 解决方案 请考虑将数字按位补码时所得到的结果.n位整数x的按位补码在所有x都为0的地方都为1，反之亦然.因此很明显可以看到: x +〜x = 0b11 ... 11(全1的n位值)
..
用Prop代替bool的常见策略
coq中是否有一个证明策略，该表达式将表达式中的所有布尔运算(andb，orb，implb等)都用命题连接词(和，或impl)替换，并将布尔变量x封装在Is_true(x)? 如果没有，我该怎么写? 解决方案 您可以使用重写数据库，例如: 需要导入Setoid.需要导入布尔.引理和b_prop_iff x y:Is_true(x& y)Is_true x/\ Is_true
..
排列数字以形成最大数字-算法证明
存在已知的算法问题，并给出了数组数量，例如 [1、20、3、14] 排列数字的方式应使它们形成最大的数字，在这种情况下为 320141 . 使用以下算法，SO和其他站点上有很多解决方案: String [] strs = new String [nums.length];for(int i = 0; i
..
(N–1)+(N–2)+(N–3)+ ... + 1 = N *(N–1)/2的证明是什么
我从气泡排序算法的一本数据结构书中得到了这个公式. 我知道我们是(n-1)*(n次)，但是为什么要除以2? 任何人都可以向我解释一下或提供详细的证明. 谢谢 解决方案 请参见三角形数字.
..
将fold泛化，使其变得足以定义任何有限递归?
因此，有一种被称为“折叠的通用属性"的东西，具体说明如下: g [] = i; g (x:xs) = f x (g xs) g = fold f i 但是，就像您现在所看到的那样，有一些罕见的情况，例如dropWhile，除非您将其概括化，否则无法将其重新定义为fold f i . 最简单但显而易见的概括方法是重新定义通用属性: g' y [] = j y; g'
..
将假设应用于变量
假设我在证明中，而我有这样的假设： a：nat b：nat c：nat H：somePred ab 及其定义of somePred说： 定义somePred（p：nat）（q：nat）：属性：= forall（x：nat） ，P（x，p，q）。 如何将 H 应用于 c 并获得 P（c，a，b）？ 解决方案 答案是： 用c特
..
如何从明显矛盾的假设中证明错误
假设我要证明以下定理： 定理succ_neq_zero：forall n m：nat，S n = m-> 0 = m->假。 这很简单，因为 m 不能假定为后继和零。但是我发现要证明它非常棘手，而且我不知道如何在没有辅助引理的情况下做到这一点： 引理succ_neq_zero_lemma：全部n：nat，O = S n->假。 证明。 前奏。 倒置H. 问。
..