我和Coq鬼混.具体来说,我试图实现mergesort,然后证明它的工作原理.
我尝试实施的是:
Fixpoint sort ls :=
match ls with
| nil => nil
| cons x nil => cons x nil
| xs =>
let (left, right) := split xs nil nil
in merge (sort left) (sort right)
end.
我得到的错误是:
Error:
Recursive definition of sort is ill-formed.
In environment
sort : list nat -> list nat
ls : list nat
x : nat
l : list nat
y : nat
l0 : list nat
left : list nat
right : …是否有一个完善的Coq图库用于证明简单定理？
我想学习如何证明简单的东西:"G1,G2是同构的,当且仅当它们的补语是同构的"时.
是否有相关/类似的示例或教程？
我有一个库来编写索引类型,而不必显式地索引索引.这通过隐藏不相关的管道导致更清洁的顶级类型.它是这样的:
Section Indexed.
Local Open Scope type.
Context {I : Type} (T : Type) (A B : I -> Type).
Definition IArrow : I -> Type :=
fun i => A i -> B i.
Definition IForall : Type :=
forall {i}, A i.
End Indexed.
Notation "A :-> B" := (IArrow A B) (at level 20, right associativity).
Notation "[ A ]" := (IForall A) (at level 70).
然而,Coq忽略了我的要求,使IForall隐式引入的通用量词如下所示:
Fail Definition id {A : nat -> Type} …Coq是证明助手,而Agda/Idris是编程语言(尽管它们可以称为证明助手).
我正在探索这些语言,我想知道Agda/Idris是否足以完成Coq可以做的所有事情.
那么,是否有一些[证明/管理代码/ IDE(Emacs)功能/其他东西的方式] Coq可以做到而Agda/Idris无法做到？
我正在尝试定义一个名为的函数byteWidth,它捕获有关"获取特定原子类型的字节宽度"的用法.
我的第一次试用:
byteWidth : Type -> Int
byteWidth Int = 8
byteWidth Char = 1
并且Idris编译器抱怨:"当检查byteWidth的左侧时:左侧没有显式类型:Int"
我的第二次试验:
interface BW a where
byteWidth : a -> Int
implementation BW Int where
byteWidth _ = 8
implementation BW Char where
byteWidth _ = 1
在这种情况下,我只能使用byteWidth,byteWidth 'a'但不能byteWidth Char.
这可能是非常微不足道的，但我找不到任何关于 ':>' 符号在 Coq 中含义的信息。U : Type 和 W :> Type 之间有什么区别？
可在此处找到的Coq标准库文件Coq.Init.Logic 包含该语句
Notation "A -> B" := (forall (_ : A), B) : type_scope.
鉴于符号->已经具有内置含义,我不明白这是如何可能的.被这->覆盖了吗？
如果我输入A -> B,Coq如何知道我的意思A -> B或forall (x : A), B？
是的,我知道这两个命题在逻辑上是等价的,但这不应该是一个定理而不是一个符号吗？
你可以说,我对Coq没有多少经验,但我想了解细节.
在Coq(CPDT样式)证明中编写高度自动化的证明时,在广泛使用的基础上eauto N,我必须经常修改我的引理语句以便eauto容易地使用它们.特别是,我必须用形式(2)替换形式(1)forall vars, P (f args)...(在P论文或假设中出现)的陈述forall x args, x = f args -> P x -> ....使用表单(2),eauto可以x根据需要实例化适当的表达式e(通过统一找到),并e = f args通过其通常的证明搜索单独证明.相反,由于形式(1)有必要重写与e = f args证明,一些IIUC期间eauto不会做(除非使用专用Hint Extern).
是否有更好的现有策略来实现相同的结果,这种风格可能是自动化的？我所看到的最接近的是applys_eq软件基础的LibTactics中的策略,它允许在形式(1)中应用引理,但e = f args作为单独的目标; 但是,这种策略需要完全手动规范.
我明白我的要求可能太难或太慢; 知道这是一种合理的方法将有助于停止寻找并继续下去.我听说至少有一位经验丰富的Coq用户描述了同样的问题和相同的方法.
我试图了解证明在Coq提取中的作用。我被两个取自有地板整数除法下面的例子在这里。我第一次尝试使用Admitted关键字：
(*********************)
(* div_2_even_number *)
(*********************)
Definition div_2_even_number: forall n,
(Nat.Even n) -> {p:nat | n=p+p}.
Proof.
Admitted.
(*************)
(* test_even *)
(*************)
Definition test_even: forall n,
{Nat.Even n}+{Nat.Even (pred n)}.
Proof.
Admitted.
(********************)
(* div_2_any_number *)
(********************)
Definition div_2_any_number (n:nat):
{p:nat | n = p+p}+{p:nat | (pred n) = p+p} :=
match (test_even n) with
| left h => inl _ (div_2_even_number n h)
| right h' => inr _ (div_2_even_number (pred n) h')
end. …我一直致力于 Coq 中流程演算的形式化（此处为存储库），并且不断发现自己尝试应用一个因等效但语法不同的子术语而失败的函数。这种情况经常是由于de Bruijn 变量的操纵而发生的。当统一失败时，我通常会事先明确替换行为不当的子项，然后应用我需要的函数。一个简单的代码作为我的意思的例子：
Require Import Lia.
Goal
forall P: nat -> Prop,
(forall a b c, P (a + (b + c))) ->
forall a b c, P (b + c + a).
Proof.
intros.
(* Unification fails here. *)
Fail apply H.
(* Replace misbehaving subterms explictly. *)
replace (b + c + a) with (a + (b + c)).
- (* Now application succeeds. *)
apply H.
- (* Show now they …