标签: proof

我正在尝试使用异构相等来证明涉及此索引数据类型的语句:

data Counter : ? ? Set where
  cut : (i j : ?) ? Counter (suc i + j)

我能够使用Relation.Binary.HeterogenousEquality.≅-Reasoning编写我的证明,但只能假设以下同余属性:

Counter-cong : ? {n n?} {k : Counter n} {k? : Counter n?} ?
               {A : ? ? Set} ? (f : ?{n} ? Counter n ? A n) ?
               k ? k? ? f k ? f k?
Counter-cong f k?k? = {!!}

然而,我不能模式匹配Relation.Binary.HeterogenousEquality.?-Reasoning是k?k?没有得到从类型检查以下错误消息:

Refuse to solve heterogeneous constraint 
    k : Counter n =?= …

我希望在网页中以自然演绎的方式显示证明树.我将从JSON文件中获取数据.

什么是显示这样的东西的最佳方式？它只能用css吗？或者有一个库可以做这样的事情吗？渲染为图像是不可能的,因为最终它应该是交互式的.我还应该提到这棵树可以变得相当大.

例:

更新:最终结果的最佳示例:

我在想我们可以证明一个程序有错误.我们可以对其进行测试,以评估它是否或多或少具有抗虫性.

但有没有办法(甚至在理论上)证明程序没有错误？

对于简单的程序,例如"Hello World",我想我们应该能够做到.但是大型项目呢？

有时<statement> solve_direct（我通常通过调用<statement> try）列出一些库定理并说“当前的目标可以直接解决：……”。

设<theorem>一个搜索结果solve_direct，然后在大多数情况下我可以证明<statement> by (rule theorem)。

然而，有时这样的证明不被接受，导致错误信息“应用初始证明方法失败”。

是否有一种通用的、不同的技术来重用由 找到的定理solve_direct？

还是要看个人情况？我可以尝试找出一个最小的例子并将其附加到这个问题上。

我注意到,在与Isabelle/HOL Isar合作时,有几种方法可以处理通用量化问题.我正在尝试以适合本科生理解和复制的风格写出一些证据(这就是我使用Isar的原因!)而且我对如何以一种很好的方式表达普遍量化感到困惑.

例如,在Coq中,我可以写forall x, P(x),然后我可以说"感应x",它将根据相应的归纳原理自动生成目标.然而,在Isabelle/HOL Isar中,如果我想直接应用归纳原理,我必须在没有任何量化的情况下陈述该定理,如下所示:

lemma foo: P(x)
proof (induct x)

这样可以正常工作,因为x被视为一个原理图变量,就像它被普遍量化一样.但是,它在声明中缺乏普遍的量化,而这种量化并不是很有教育意义.我资助的另一种方式是使用\<And>和\<forall>.但是,如果我以这种方式陈述引理,我不能直接应用归纳原理,我必须首先修复普遍量化的变量......从教育的角度来看,这似乎很不方便:

lemma foo: \<And>x. P(x)
proof -
fix x
show "P(x)"
proof (induct x)

什么是表达通用量化的一个很好的证明模式,不需要我在归纳之前明确地修复变量？

如果阿格达两个值,或一些其他的依赖性类型的语言,可以证明v?不是不等于v?,你能证明v?等号v?？

比如,有类型的功能((v? ? v? ? ?) ? ?) ? v? ? v?吗？

如果无法证明,这似乎可以安全地添加为公理,因为最多可以有一个值v? ? v?.

这个有趣的原因是双重否定((a ? ?) ? ?)形成了一个单子.通常你不能从它中提取值,但是你可以?从某些值中获取它们(如果你在经典逻辑monad中得出一个矛盾,你就会有矛盾).我想知道平等是否是可以提取的东西.

我们foldl可以实现foldr这一点.这在关于折叠的普遍性和表现力的教程中有详细解释.在论文中指出:

相反,它是不可能重新定义fold来讲foldl,由于这样的事实,foldl在其列表参数的尾部严格,但fold并非如此.

不过,我看不出这构成了对定义的不可能性证明foldr来讲foldl(注意,在原纸上fold是一个代名词foldr).我很困惑,试图理解严格性在这里发挥作用.有人可以扩展这个解释吗？

我正在阅读Jeremy Gibbons关于折纸编程的文章,我坚持练习3.7,要求读者证明列表的融合法展开:

unfoldL p f g . h = unfoldL p' f' g'

Run Code Online (Sandbox Code Playgroud)

如果

p . h = p'
f . h = f'
g . h = h . g'

Run Code Online (Sandbox Code Playgroud)

unfoldL列表展开的功能定义如下:

unfoldL :: (b -> Bool) -> (b -> a) -> (b -> b) -> b -> List a
unfoldL p f g b = if p b then Nil else Cons (f b) (unfoldL p f g (g b))

这是我目前尝试的证据:

(unfoldL p f …

如何显示在Scala中没有构造函数的类型的值有什么变化？我想对值进行模式匹配，并让Scala告诉我没有模式可以匹配，但是我愿意接受其他建议。这是一个为什么有用的简短示例。

证明负面

在Scala中，可以在类型级别上定义自然数，例如使用Peano编码。

sealed trait Nat
sealed trait Zero extends Nat
sealed trait Succ[N <: Nat] extends Nat

由此我们可以定义数字等于偶数的含义。零是偶数，比偶数多2的任何数字也是偶数。

sealed trait Even[N <: Nat]
sealed case class Base() extends Even[Zero]
sealed case class Step[N <: Nat](evenN: Even[N]) extends Even[Succ[Succ[N]]]

由此我们可以证明例如两个是偶数：

val `two is even`: Even[Succ[Succ[Zero]]] = Step(Base())

但是，即使编译器可以告诉我该类型Base也Step不能居住于该类型，但我无法证明它不是偶数。

def `one is odd`(impossible: Even[Succ[Zero]]): Nothing = impossible match {
  case _: Base => ???
  case _: Step[_] => ???
}

编译器会很高兴地告诉我，我给出的所有情况都不可能与错误有关pattern type is incompatible with expected …

这个问题是参考或解释的请求.主要思想是:如果我从Coq的标准库中添加每个公理怎么办？它会引起矛盾还是相互调整好？除了标准的Coq库之外,还有哪些关于Coq的可靠信息来源.(我看过九十年代,八十年代的一堆论文.显然有很多类型理论的变体.哪一个适用于当代的Coq？或者我应该认为"所有已知的东西都可以在https://coq.inria.fr找到/ refman /,在https://sympa.inria.fr/sympa/arc/coq-club/199​​3-12/和标准库中.")

(A)您是否知道纸张或其他来源,证明某些公理可以正确添加到Coq？这里适当地意味着扩展系统将是以前OR的保守扩展将被认为是安全加强.

(B)就个人而言,我对这些公理感兴趣:

0)ex2sig(它是否一致？)

Axiom ex2sig : forall (A:Type) (P:A->Prop), @ex A P -> @sig A P.

1)LEM

2)功能扩展性

Axiom functional_extensionality_dep : forall {A} {B : A -> Type},
  forall (f g : forall x : A, B x),
  (forall x, f x = g x) -> f = g.

3)选择

Theorem choice :
 forall (A B : Type) (R : A->B->Prop),
   (forall x : A, exists y : B, R x …