标签: proof

如果语言 L1,...,Ln 是正则的，那么它们的并集也是正则的吗？

我们知道两种正则语言的并集就是正则语言。如何证明多个正则语言的并集也是正则的？

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

Lemma not_eq_S2: forall m n, S m <> S n -> m <> n.

这似乎很容易，但我不知道如何完成证明。有人可以帮我吗？

谢谢你。

据说CRC（循环冗余校验和）可以检测到小于r +1位的突发错误，其中r是多项式的次数。此外，以1 – 2 ^-r的概率检测到长度大于r + 1位的突发。

有人可以指导我提供相同的证明吗？

我正在尝试学习 Agda。任何人都可以完成这个证明（如果它在正确的轨道上）或指向我现有的文章？我进行了广泛的搜索。

sum : ? ? ?
sum 0 = 0
sum (suc a) = (suc a) + sum a

prove2*Sumn=n*sucn : (n : ?) ? ((sum n) * 2) ? (n * (suc n))
prove2*Sumn=n*sucn zero = refl
prove2*Sumn=n*sucn (suc a) = {! !}

我最近不得不看一看 Dijkstra 算法，它就是证明。

算法的证明在我能找到的所有来源中终止，所有顶点的数量和访问的所有顶点的数量相等（例如 R=V 或 S=V）。此外，当 Q（以图的所有顶点开始）为空时，该算法的 while 循环终止，因此必须访问所有顶点。

我不明白为什么必须如此。是否存在算法不必访问所有顶点的图，例如：起始顶点直接连接到权重为 1 的“查找”顶点和权重为 10 的其他顶点。

我希望你能解决我在这里遇到的问题。

编辑：这是我从 Cormen 使用的伪代码：

我的例子:方程组

  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约束方程组中检索此信息？

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

我想澄清一下agda中的双重否定.

即使

z?z : 0 ? 0
z?z = refl 

我无法弄清楚如何证明:

¬¬z?z : (0 ? 0 ? ?) ? ?
¬¬z?z ?

这是长期的¬ (0 ? 0).也许我错过了一路上的agda成语.理想我想要一个最小参考标准库的解释.

我有充分理解如何证明以下某些陈述的问题.

例如,我有一个声明:n^2logn = O(n^2).纠正我,如果我错了,但这个规定,n^2是bigO的n^2logn.意味着n^2增长得快于n^2logn.现在我们将如何证明这一点？我假设我需要使用感应证明,我试图使用但是在这个过程中卡住了.我可以重写这句话n^2logn <= n^2吗？

是否有可能使用归纳法反驳某些东西？例如,反驳n!=O(n^n).或者通过简单地表明任意值(例如大于2)不满足该陈述来反驳该陈述是否有效？

最后为了清楚起见,bigTheta声明方程式在增长正确时是等价的？

我正在做Typeclassopedia的练习; 在Applicative节中,我写ZipList的pure功能,并检查它是否遵循Applicative法律.

我检查过:

• 身份法
• 交换法
• 组成法

但是当我试图检查"同态"定律时,我发现GHCi没有得到结果MZipList.

我想这是因为我错过了指定pure我的Applicative类型课程.如何立即运行pure没有<*>它的功能Applicative？

这是MZipList定义和类实例:

newtype MZipList a = MZipList { getZipList :: [a] }
    deriving (Show)

instance Functor MZipList where
  fmap gs x = pure gs <*> x

instance Applicative MZipList where
  pure a= MZipList (repeat a)
  (MZipList gs) <*> (MZipList xs) = MZipList (zipWith ($) gs xs)

当我检查"交换"法时,例如:

*Main> (MZipList …

我理解使用这种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归纳如何被破坏？它如何影响目标并完成证明？