标签: proof

我需要从CLRS算法书中获得这个练习的提示:

证明无论我们在高度-h二进制搜索树中从哪个节点开始,对Tree-Successor的k次连续调用都需要O(k + h)时间.

当refine一个程序,当我的目标是a时,我试图通过inversion一个False假设来结束证明.这是我试图做的证据的简化版本.Type

Lemma strange1: forall T:Type, 0>0 -> T.
  intros T H.
  inversion H.  (* Coq refuses inversion on 'H : 0 > 0' *)

Coq抱怨道

Error: Inversion would require case analysis on sort 
Type which is not allowed for inductive definition le

但是,既然我什么都不做T,那应该没关系,......还是？

我摆脱了T这样的,证据经过:

Lemma ex_falso: forall T:Type, False -> T.
  inversion 1.
Qed.  

Lemma strange2: forall T:Type, 0>0 -> T.
  intros T H.
  apply ex_falso.  (* …

作为Coq中的练习,我试图证明以下函数返回一对长度相等的列表.

Require Import List.

Fixpoint split (A B:Set)(x:list (A*B)) : (list A)*(list B) :=
match x with
|nil => (nil, nil)
|cons (a,b) x1 => let (ta, tb) := split A B x1 in (a::ta, b::tb)
end.

Theorem split_eq_len : forall (A B:Set)(x:list (A*B))(y:list A)(z:list B),(split A B x)=(y,z) -> length y = length z.
Proof.
intros A B x.
elim x.
simpl.
intros y z.
intros H.
injection H.
intros H1 H2.
rewrite <- H1.
rewrite <- H2.
reflexivity. …

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues指出:

其次,到目前为止,目前的实施工作进展有限,因此可能仍然存在一种情况,即它认为功能是总的而不是.不要依赖它来证明你的证明!

这是否意味着不能依赖Idris作为证据,或者是否有办法创建不需要整体检查的证明？

Monadic一阶逻辑，其中所有谓词都恰好采用一个参数，是一阶逻辑的已知可判定片段。测试公式是否可以满足此逻辑是可以确定的，并且存在基于分辨率的方法来确定这一点。

我处于需要测试一些单子一阶逻辑语句的可满足性的情况。我意识到我将达到理论上的复杂性极限，但我希望在常见情况下能够获得合理的性能。

现在，存在大量的定理证明，它们提供了解决一阶逻辑问题的快速方法。其中包括Vampire，SPASS，E，以及Z3和CVC4的量词扩展。但是，由于不确定性，不能保证它们停止运行。

我的问题

在现有的定理证明者中，有谁能保证在给定单子式公式作为输入时停止？还是有一种方法可以使用它们（以某种方式）有效地测试单子公式的可满足性？

我遵循的是Liquid Haskell的官方教程，偶然发现了其中的“ bug”。

本教程中包含以下代码，而Liquid Haskell应该检查它是否安全。

{-@ type TRUE  = {v:Bool | v    } @-}
{-@ type FALSE = {v:Bool | not v} @-}

{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p ==> q)} @-}
False ==> False = True
False ==> True  = True
True  ==> True  = True
True  ==> False = False

{-@ measure f :: Int -> Int @-}

{-@ congruence :: (Int -> Int) …

我很难理解感应如何与一些不变量一起用来证明算法的正确性.也就是说,如何找到不变量,何时使用归纳假设 - 特别是二元搜索？我还没有找到直观的回复,所以我希望有人可以在这里阐述一下这个话题.

我一直在研究JavaScript/JQuery代码,它允许输入框之间的箭头键移动(是的,我知道这打破了标准UI).

它通过循环遍历每个元素并在每个方向(左,右,上和下)找到最接近的方法.

例

P1:(0,0),P2:(1,0),P3:(0,2)

P1有一个指向右侧(P2)和一个点向上(P3).

P2有一个点向左(P1)和一个点向上(P3).
禁止摄影

P3有两个点(P1和P2),但P1更接近.

因此最后的动作是:

Up
  1 -> 3
  2 -> 3
Right
  1 -> 2
Down
  3 -> 1
Left
  2 -> 1

对于此示例:
P1有两个传入和两个传出连接.
P2有一个传入和两个传出连接.
P3有两个传入和一个传出连接.

这让我想到了.
是否有一组点使得一个或多个点不可访问(0个传入连接),或者可以证明没有这样的集合存在？

旁注:
如果忽略向上/向下组件(仅使用左和右垂直分割),则在P1中将P3指向不可访问:(0,0),P2:(2,0),P3:(1,4 ).

这是JavaScript/JQuery代码,如果它可以帮助任何人.

function arrowKeyNavigation(elements) {
    // Get the position of each element.
    var elementOffsets = [];
    elements.each(function(key, element) {
        elementOffsets[key] = $(element).offset();
    });

    // Find the closest point in each direction and store the points in data('keyNav') for later use.
    for (var i = …

有时,当我在写申请风格的证明,我就想办法修改论证方法 foo来

尝试foo第一个目标.如果它解决了目标,那就好; 如果它没有解决它,恢复到原始状态并失败.

这出现在以下代码中:

qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+

在进一步改变之后,调用simp将不再完全解决目标,然后这将循环.如果我可以指定类似的东西

qed (solve_goal(subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail))+

或(替代建议的synatx)

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)!)+

或者(甚至更好的语法)

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+

它会停止在这个脚本无法解决的第一个目标上.

我设法将目标减少到了

(fun x0 : PSR => me (x x0)) = x

我知道这reflexivity会有效,但出于教学原因,我宁愿继续减少它.

me是一个身份功能,所以unfold me简化它

(fun x0 : PSR => x x0) = x

这只是一个将函数应用于x虚拟变量的匿名函数x0,所以你可以说两边都只是函数x.如果可能的话,我想在双方达成相同的表达方式.