标签: coq

我正在阅读关于Coq的教程.它构造一个bool类型如下:

Coq < Inductive bool :  Set := true | false.
bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined

然后它显示了这些东西正在使用"检查".

Coq < Check bool_ind.
bool_ind
     : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b

Coq < Check bool_rec.
bool_rec
     : forall P : bool -> Set, P true -> P false -> forall b : bool, P b

Coq < Check bool_rect.
bool_rect
     : …

我理解像Coq和Idris这样的语言如何用于证明用这些语言编写的程序的属性(根据我在该主题中的一点经验来判断.)但是我想知道是否有一种平易近人的方式在外部做同样的事情,在现有的代码库.

有没有办法使用像Coq或其他专业工具这样的工具来证明用C++编写的算法的正确性？如果是这样,这样做有什么要求？

是否可以切换当前目标或子目标以在Coq中证明？

例如,我有一个这样的目标(来自eexists):

______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)

我想要做的是首先split证明合适的合并.我认为这将给出存在变量的值?s,而左合并应该只是一个简化.

但split默认情况下,将左合并设置?s > 0为当前目标.

______________________________________(1/2)
?s > 0
______________________________________(2/2)
r1 * (r1 + s1) + ?s = r3 * (r3 + s2)

我知道我可以在战术2:上加上第二个子目标的操作,但这很尴尬因为

1)我看不到目标#2和.的假设

2)如果它处于不同的上下文中,目标#2可能是第三个或第k个目标.证明不可移植.

这就是为什么我想把第二个目标设定为当前目标.

顺便说一下,我正在使用CoqIDE(8.5).

我怎么能在coq中证明一个函数f接受bool true|false并返回一个bool true|false(如下所示),当对一个bool应用两次时true|false总会返回相同的值true|false:

(f:bool -> bool)

例如函数f只能做4件事,让我们调用函数的输入b:

• 永远回来 true
• 永远回来 false
• 返回b(即如果b为真则返回true,反之亦然)
• 返回not b(即如果b为真,则返回false,副)

因此,如果函数始终返回true:

f (f bool) = f true = true

如果函数总是返回false,我们会得到:

f (f bool) = f false = false

对于其他情况,让我们假设函数返回 not b

f (f true) = f false = true
f (f false) = f true = false

在两种可能的输入情况下,我们总是最终得到原始输入.如果我们假设函数返回,则同样成立b.

那么你如何在coq中证明这一点？

Goal forall (f:bool -> bool) (b:bool), f (f b) …

我试图(经典地)证明

~ (forall t : U, phi) -> exists t: U, ~phi

在Coq.我想要做的是证明它是相反的:

1. Assume there is no such t (so ~(exists t: U, ~phi))

2. Choose arbitrary t0:U

3. If ~phi[t/t0], then contradiction with (1)

4. Therefore, phi[t/t0]

5. Conclude (forall t:U, phi)

我的问题是第(2)和(5)行.我无法弄清楚如何选择U的任意元素,证明它的一些东西,并得出一个结论.

任何建议(我不承诺使用对立面)？

这是一个递归函数all_zero,用于检查自然数列表中的所有成员是否为零:

Require Import Lists.List.
Require Import Basics.

Fixpoint all_zero ( l : list nat ) : bool :=
  match l with
  | nil => true
  | n :: l' => andb ( beq_nat n 0 ) ( all_zero l' )
  end.

现在,假设我有以下目标

true = all_zero (n :: l')

我想用这个unfold策略将其转化为

true = andb ( beq_nat n 0 ) ( all_zero l' )

不幸的是,我不能用一个简单的方法来做,unfold all_zero因为战术会急切地找到并替换所有的实例all_zero,包括一次展开形式的实例,它变成一团糟.有没有办法避免这种情况并只展开一次递归函数？

我知道我可以通过证明临时等价来获得相同的结果assert (...) as X,但效率很低.我想知道是否有一种简单的方法可以做到这一点unfold.

在交互式定理证明器Coq的,任何交互证明或定义可与被终止Qed或Defined.有一些"不透明"的概念Qed强制执行但Defined不强制执行.例如,Adam Chlipala 撰写的" 依赖类型认证编程 "一书指出:

我们用" Defined而不是"结束"证据" Qed,以便我们构建的定义仍然可见.这与结束证明的情况形成对比Qed,其中证据的细节随后被隐藏.(更正式地,Defined将标识符标记为透明,允许它展开;同时Qed将标识符标记为不透明,防止展开.)

但是,我不太确定这在实践中意味着什么.有一个后来的例子,Defined由于需要Fix检查某个证据的结构,有必要使用,但我不明白这个"检查"的确切含义,或者为什么如果Qed使用它会失败.(看看定义Fix也不完全具有启发性).

从表面上看,很难说Qed实际上在做什么.例如,如果我写:

Definition x : bool.
exact false.
Qed.

我仍然可以x通过执行命令看到值.Print x. 此外,我以后允许在"不透明"值上进行模式匹配x:

Definition not_x : bool :=
  match x with
    | true => false
    | false => true
  end.

因此,我似乎能够使用正常的价值x.Chlipala教授在这里"展开"是什么意思？不透明和透明差异究竟有什么区别？最重要的是,这有什么特别之处Fix …

我注意到在Coq对有理数的定义中,零的倒数被定义为零.(通常,除以零没有明确定义/合法/允许.)

Require Import QArith.
Lemma inv_zero_is_zero: (/ 0) == 0. 
Proof. unfold Qeq. reflexivity. Qed.

为什么会这样？

它可能会导致有理数的计算出现问题,还是安全的？

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

Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
    (a <> [] \/ b <> []) -> a ++ b <> [].

现在我当前的策略是破坏一个,在打破分离之后,理想情况下我可以说,如果一个<> []那么a ++ b也必须<> [] ......这就是计划,但我似乎无法通过类似于第一个"a ++ b <> []"的子目标,即使我的上下文明确指出"b <> []".有什么建议？

我还查看了很多已有的列表定理,并没有找到任何特别有用的东西(减去app_nil_l和app_nil_r,对于某些子目标).

假设我在上下文中有两个假设,a_b : A -> B并且a : A.我应该能够申请a_b到a获得进一步的假设,b : B.

也就是说,给定以下状态:

1 subgoal
A : Prop
B : Prop
C : Prop
a_b : A -> B
a : A
______________________________________(1/1)
C

应该有一些策略,foo (a_b a)将其转换为以下状态:

1 subgoal
A : Prop
B : Prop
C : Prop
a_b : A -> B
a : A
b : B
______________________________________(1/1)
C

但我不知道是什么foo.

我能做的一件事是:

 assert B as b.
 apply a_b. …