标签: proof

嗨,大家好我想比较2个算法,并认为我可以尝试为他们写一个证明!(我的数学很糟糕因此问题)

通常在去年的数学课上我们会遇到类似的问题

证明:(2r + 3)= n(n + 4)

那么我会做所需的4个阶段并在最后得到答案

我被困的地方是证明prims和Kruskals - 我怎样才能将这些算法变成上面的数学形式所以我可以继续证明

注意:我不是要求别人为我回答 - 只是帮我把它放到一个我可以自己去的地方

谢谢

在之前的一个问题中,我展示了(希望是正确的)f(n)= O(g(n))意味着具有充分条件的lg(f(n))= O(lg(g(n)))(例如,lg) (g(n))> = 1,f(n)> = 1,并且n)足够大.

现在,我需要证明OR反驳f(n)= O(g(n))暗示2 ^(f(n))= O(2 ^ g(n))).直观地说,这是有道理的,所以我想我可以在前一个定理的帮助下证明它.我注意到f(n)可以重写为lg(2 ^ f(n))而g(n)只是lg(2 ^ g(n)),这让我很兴奋...这是记录日志我希望证明的两边的基础2,它简化了很多事情!

但我很确定这不起作用.仅仅因为lg(2 ^ f(n))= O(lg(2 ^ g(n)))并不一定意味着2 ^ f(n)= O(2 ^ g(n))...那是向后的从前面的定理(说"暗示",而不是"当且仅当").

我是否需要以另一种方式尝试这种证据,或者我能否真正摆脱我所拥有的(至少作为首发)？

**说到其他方式,也许我可以争论如何将2增加到某个g(n),这个数字"高于"f(n)仍会保持更高？这几乎感觉像一个常识论点,但也许我错过了一些重要的东西..

**哦,哎呀!我忘了补充说f(n)和g(n)是渐近正的.通过我们的教科书定义,这意味着它们"对所有足够大的n都是正面的".

我有一个Isabelle证据结构如下:

proof (cases "n = 0")
  case True
  (* lots of stuff here *)
  show ?thesis sorry
next
  case False
  (* lots of stuff here too *)
  show ?thesis sorry
qed

第一种情况实际上是几页长,所以在阅读第二种情况时,对于一个随意的读者,甚至对我自己来说,它False所指的不再是清楚的.(嗯,它实际上是,但不是来自阅读,只能在交互式环境中:例如,如果在Isabelle/jEdit中,您将光标置于其后case False,您将n ? 0在"输出"面板中的"this"下看到.)

那么是否有一种语法允许假设"假"情况明确,这样读者既不必与IDE交互,也不必向上滚动到proof关键字,但是可以正确看待假设？

我只是开始玩idris和定理证明一般.我可以在互联网上关注大多数基本事实证据的例子,所以我想尝试一些我自己的任意事物.所以,我想为map的以下基本属性编写一个证明术语:

map : (a -> b) -> List a -> List b
prf : map id = id

直觉上,我可以想象证明应该如何工作:获取任意列表l并分析map id l的可能性.如果l是空的,那很明显; 当l非空时,它基于函数应用程序保持相等的概念.所以,我可以这样做:

prf' : (l : List a) -> map id l = id l

这就像一个所有声明.如何将其转化为所涉及功能相等的证明？

我们在Haskell平台上获得的所有Haskell应用类型类的实例是否都被证明满足所有的适用法律？如果是,我们在哪里找到这些证明？

Control.Applicative的源代码似乎不包含任何证据证明各种实例的适用法律确实存在.它只是提到了

-- | A functor with application.
--
--Instances should satisfy the following laws:

然后它只是在评论中陈述法律.

我发现了其他类型类(Alternative和Monad)实例的类似案例.

这些图书馆的用户是否应该自己验证这些法律？

但我想知道这些法律的严格证明是否已由开发商在其他地方提供过？

同样,我知道IO Monad的Applicate(或Monad)法律的严格证明,一般涉及与外界交谈,可能非常复杂.

谢谢.

众所周知,Monad实例应该遵循Monad法则.可能不太为人所知,Functor实例应遵循Functor法则.尽管如此,我仍然对编写优化的GHC重写规则感到相当自信fmap id == id.

还有哪些标准类有隐含法则？是否(==)有一个真正的等价关系？是否Ord必须形成部分订单？总订单？我们至少可以假设它是可传递的吗？反对称？

这些最后几个似乎没有在Haskell 2010报告中指定,也不会有信心编写利用它们的重写规则.但是,有没有共同的图书馆？一个实例的病理如何可以自信地写出来？

最后,假设这样一个实例可能存在一个边界,那么每种类型实例必须遵守的法律是否有一个标准的综合资源？

举个例子,我要定义多少麻烦

newtype Doh = Doh Bool
instance Eq Doh where a == (Doh b) = b

它只是难以理解或编译器在任何地方都不正确地优化？

我有点难以理解如何证明免费monad的法律Functor和Monad法律.首先,让我提出我正在使用的定义:

data Free f a = Pure a | Free (f (Free f a))

instance Functor f => Functor (Free f) where
    fmap f (Pure a) = Pure (f a)
    fmap f (Free fa) = Free (fmap (fmap f) fa)

instance Functor f => Monad (Free f) where
    return = Pure
    Pure a >>= f = f a
    Free fa >>= f = Free (fmap (>>=f) fa)

{-

Functor laws:
(1) fmap id x == x …

我想forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.在Coq中证明或伪造.这是我的方法.

Inductive True2 : Prop :=
 | One : True2
 | Two : True2.

Lemma True_has_one : forall (t0 t1 : True), t0 = t1.
Proof.
  intros.
  destruct t0. destruct t1.
  reflexivity.
Qed.

Lemma not_True2_has_one : (forall (t0 t1 : True2), t0 = t1) -> False.
Proof.
  intros.
  specialize (H One Two).
  inversion H.

但是,inversion H什么都不做.我想也许是因为coq的证明独立性(我不是英语母语,我不知道确切的词,请原谅我的无知),而且coq使得无法证明One = Two - > False.但是,如果是这样,为什么必须消除证据的内容？ …

我怎样才能让伊德里斯自动证明两个值不相等？

p : Not (Int = String)
p = \Refl impossible

如何让Idris自动生成此证明？auto似乎不能证明涉及的陈述Not.我的最终目标是让Idris自动证明矢量中的所有元素都是唯一的,并且两个矢量是不相交的.

namespace IsSet
    data IsSet : List t -> Type where
        Nil : IsSet []
        (::) : All (\a => Not (a = x)) xs -> IsSet xs -> IsSet (x :: xs)

namespace Disjoint
    data Disjoint : List t -> List t -> Type where
        Nil : Disjoint [] ys
        (::) : All (\a => Not (a = x)) ys -> Disjoint xs ys …

我的目标是证明霍纳法则是正确的。为此，我将 Horner 当前计算的值与“实数”多项式的值进行比较。
所以我做了这段代码：

package body Poly with SPARK_Mode is
   function Horner (X : Integer; A : Vector) return Integer is
      Y : Integer := 0;
      Z : Integer := 0 with Ghost;
   begin
      for I in reverse A'First .. A'Last loop
         pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);
         Y := A(I) + Y * X;
         Z := Z + A(I) * (X ** (I - A'First));
      end loop;
      pragma Assert (Y = Z); …