我注意到在Coq对有理数的定义中,零的倒数被定义为零.(通常,除以零没有明确定义/合法/允许.)
Require Import QArith.
Lemma inv_zero_is_zero: (/ 0) == 0.
Proof. unfold Qeq. reflexivity. Qed.
为什么会这样？
它可能会导致有理数的计算出现问题,还是安全的？
当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. (* …当我试图证明一个关于递归函数的定理时(见下文),我最终得到了一个可简化的表达式
(fix picksome L H := match A with .... end) L1 H1 = RHS
我想扩大match表达,但Coq拒绝.这样做simpl只是扩大了右侧为不可读的混乱.为什么Coq无法完成证明simpl; reflexivity,以及如何指示Coq精确扩展redex,并完成证明？
该函数是一个递归函数pick,它接受list nat并执行第一个nat调用a,a从列表中删除以下项,并在剩余列表上进行递归.即
pick [2;3;4;0;1;3])=[2; 0; 1]
我试图证明的定理是函数'只对包含零的列表无效'.以下是导致问题的发展:
Require Import Arith.
Require Import List.
Import ListNotations.
Fixpoint drop {T} n (l:list T) :=
match n,l with
| S n', cons _ l' => drop n' l'
| O, _ => l
| _, _ => nil
end.
第一个引理: …
我想看一个 Coq 版本的 Bananas、Lenses 等。它们建立在sumtypeofway 递归方案介绍的优秀系列博客文章中
然而，博客文章是在 Haskell 中，它允许无限的非终止递归，因此完全满足于Y组合器。哪个 Coq 不是。
特别是，定义取决于类型
newtype Term f = In { out :: f (Term f) }
它构建无限类型 f (f (f (f ...)))。 Term f 允许使用 Term 系列类型对 catamorphisms、paramorphisms、anamorphisms 等进行非常漂亮和简洁的定义。
尝试将其移植到 Coq 作为
Inductive Term f : Type := {out:f (Term f)}.
给了我预期的
Error: Non strictly positive occurrence of "Term" in "f (Term f) -> Term f".
问：在 Coq 中将上述 Haskell Term 类型形式化的好方法是什么？
以上f是 type Type->Type …
我正在构建一个match在列表上执行的递归函数l.在cons分支中我需要使用信息l = cons a l'来证明递归函数终止.但是,当我使用match l信息丢失时.
我如何使用match来保存信息？
下面是函数(drop并drop_lemma_le在最后给出,为便于阅读):
Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat.
refine (
match l with
nil => nil
| cons a l' => cons a (picksome (drop a l') _)
end
).
apply H.
assert (l = cons a l') by admit. (* here is where I need the information *)
rewrite …我试图提出一个问题，以便仅重写就足以证明目标。我想避免使用“聪明”的命题，而是使用可以由Coq计算的布尔值。
我定义了一个布尔测试函数member，如果一个元素在列表中，则different返回true；如果两个列表中都没有元素，则返回true。
我想证明我different只能使用重写为表达式member。
Theorem different_member: forall xs ys y,
different xs ys = ((negb (member y ys)) || negb (member y xs)).
（(negb X || Y)形式是布尔值）。
作为热身和现实检查，我想证明
Theorem diff_mem:
forall xs ys,
different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.
进行的方式是通过在xs上进行归纳，但是我一直在搞弄最后一步。
非常感谢这两个定理的帮助！这是开发的相关部分。
Require Import Arith.
Require Import List.
Require Import Bool.
Import List.ListNotations.
Open Scope list.
Open Scope …我正在（为我自己）写一篇关于如何在 Coq 中进行有根据的递归的解释。（参见 Coq'Art 书，第 15.2 章）。首先，我创建了一个基于 的示例函数，nat效果很好，但后来我又为 做了一次Z，当我使用Compute它来评估它时，它并没有一直减少到一个Z值。为什么？
这是我的示例（我将文本放在注释中，以便可以将整个内容复制粘贴到编辑器中）：
(* 有根据的递归测试 *)
(* TL;DR: 要进行有根据的递归，首先创建“函数”，然后使用 Acc_iter（用于可访问关系的迭代器）创建递归函数 *)
(* 作为示例，计算从 1 到 n 的级数之和，如下图所示：
修复 fn := （如果 n = 0 则 0 否则 n + f (n-1)）
现在，我们不要对n 使用结构递归。
相反，我们对 n 使用有充分根据的递归，使用小于 ('lt') 关系是有充分根据的。函数 f 终止，因为递归调用是在结构上较小的项（在递减的 Acc 链中）上进行的。*)
(* 首先我们为 nat 做这件事 *)
Require Import Arith.Arith.
Require Import Program.Utils. (* for 'dec' *)
Require Import Wellfounded.
(* 从关系成立的证明中，我们可以得到其域中的特定元素是可访问的证明。
亲爱的读者，这里的 …
甲单胞菌和史诗函数是同构的，因此它有一个逆。我想在 Coq 中证明这一点。
Axiom functional_extensionality: forall A B (f g : A->B), (forall a, f a = g a) -> f = g.
Definition compose {A B C} (f : B->C) (g: A->B) a := f (g a).
Notation "f ? g" := (compose f g) (at level 40).
Definition id {A} (a:A) := a.
Definition monic {A B} (f:A->B) := forall C {h k:C->A}, f ? h = f ? k …我想对带有 clang 3.4 的 ARMv7 使用内联 asm，以便编写访问 CPU 控制寄存器的低级代码。作为测试，我编写了一个程序，它从寄存器中读取数据，有条件地处理一些位，然后写回新值。
然而，当我查看生成的机器代码时，整个比特摆弄都被优化掉了。显然我没有使用正确的 asm 约束来告诉 clang 写入寄存器的结果取决于正在写入的内容。（我只使用了一个简单的“volatile”修饰符）。
我应该如何编写内联 asm 代码，以便 clang 生成正确的 asm？这是代码test.c
typedef unsigned int uint32_t;
// code that reads and writes the ID_PFR1 register
uint32_t read_ID_PFR1() {
uint32_t a;
asm volatile ("mrc p15, 0, %0, c0, c1, 1" : : "r"(a) : );
return a;
}
void write_ID_PFR1(uint32_t a) {
asm volatile ("mcr p15, 0, %0, c0, c1, 1" :"=r"(a) : : );
}
// regular c code that modifies …我试图证明Coq中“Practical Coinduction”中的第一个例子。第一个例子是证明无限整数流上的字典顺序是可传递的。
我无法制定绕过守卫条件的证明
这是我到目前为止的发展。首先只是无限流的通常定义。然后定义字典顺序称为lex。并最终证明了传递性定理的失败。
Require Import Omega.
Section stream.
Variable A:Set.
CoInductive Stream : Set :=
| Cons : A -> Stream -> Stream.
Definition head (s : Stream) :=
match s with Cons a s' => a end.
Definition tail (s : Stream) :=
match s with Cons a s' => s' end.
Lemma cons_ht: forall s, Cons (head s) (tail s) = s.
intros. destruct s. reflexivity. Qed.
End stream.
Implicit Arguments …