proof

5热度

1回答

作为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 i

1热度

1回答

级联的民主基金和列表是民主基金 - 证明哈斯克尔

一个人怎么能证明下面的每个列表XS是真的： undefined ++ xs = undefined

0热度

1回答

如何证明（R - > P）[Coq证明助理]？

如何证明（R-> P）在Coq中。我是这方面的初学者，并且不太了解这个工具。这是我写的： Require Import Classical. Theorem intro_neg : forall P Q : Prop,(P -> Q /\ ~Q) -> ~P. Proof. intros P Q H. intro HP. apply H in HP. inversion HP. a

3热度

1回答

似乎矛盾typechecks在Idris

我有以下定义向量谓词，如果一个是一个集合（没有重复的元素）或不。我定义的成员与一个类型级布尔： import Data.Vect %default total data ElemBool : Eq t => t -> Vect n t -> Bool -> Type where ElemBoolNil : Eq t => ElemBool {t=t} a [] False

0热度

1回答

如何证明X + Y - Z = X +（Y - Z）在勒柯克

我要证明这一点： 1 subgoals x : nat y : nat z : nat ______________________________________(1/1) x + y - z = x + (y - z) 它看起来微不足道，但它让我困惑了很多，我需要它另一个证明。谢谢。

4热度

3回答

如何证明b = c if（andb b c = orb b c）in coq？

我是新来的辅酶Q，我试图证明这一点...... Theorem andb_eq_orb : forall (b c : bool), (andb b c = orb b c) -> (b = c). 这是我的证明，但我碰到困难时，我得到的目标（假=真 - >假=真）。 Proof. intros b c. induction c. destruct b. refle

0热度

1回答

我如何证明有复发？

我有以下的谐波序列： h(n) = 1 + 1/2 + 1/3 + 1/4 +...+ 1/n 我还想证明，有一个与 h(n) (less than or equal to) h(lowerbound(n/2)) + 1

0热度

1回答

是否从未声明证明线性时间逻辑公式？

我有一个LTL式，这是自动地从节目我用生成： (((a))&&F((((b))&&F((c))))) 其内容 a && F(b && Fc) 我然后用于从这里下载的ltl2BA-win.exe后程序： LTL 2 BA并得到了一个从未声称作为输出。该网站还可以为LTL公式生成一个Büchi自动机（在使用本网站时，我没有选中“使用自旋语法”和“使用自旋4.3.0”选项）。我的问题是： 1.

2热度

1回答

向Agda证明我们正在谈论同样的事

我试图证明一个矛盾，但我遇到了一个问题，试图向Agda证明由<>-wt-inv返回的西格玛域类型与所看到的相同西格玛在证明之前。我希望uniq型证明能够帮助我，但我无法将它们放在一起。我希望下面的代码中的注释给出足够的上下文。 -- given a type for (f ⟨⟩), we can derive that f is a function type -- and we can p

3热度

2回答

伊德里斯证明顾名思义

我可以写函数 powApply : Nat -> (a -> a) -> a -> a powApply Z f = id powApply (S k) f = f . powApply k f ，并证明平凡： powApplyZero : (f : _) -> (x : _) -> powApp Z f x = x powApplyZero f x = Refl 到目前为止，一切都