我在Coq玩,试图创建一个排序列表.我只是想要一个带有列表的函数,[1,2,3,2,4]并返回类似的东西Sorted [1,2,3,4]- 即取出坏的部分,但实际上并没有对整个列表进行排序.
我想我会先定义一个lesseq类型的函数(m n : nat) -> option (m <= n),然后我可以非常轻松地模拟匹配.也许这是一个坏主意.
我现在遇到的问题的症结在于(片段,底部的整个功能)
Fixpoint lesseq (m n : nat) : option (m <= n) :=
match m with
| 0 => match n with
| 0 => Some (le_n 0)
...
不是类型的; 它说它期待一个option (m <= n),但它Some (le_n 0)有类型option (0 <= 0).我不明白,因为很明显,两者m并n在这方面零,但我不知道如何告诉勒柯克说.
整个功能是:
Fixpoint lesseq (m n : nat) : option (m <= …Coq的文档带有一般警告,不依赖于内置命名机制,而是选择自己的名称,以免命名机制中的更改过去证明无效.
在考虑表单的表达式时remember Expr as v,我们将变量v设置为表达式Expr.但是假设的名称是自动选择的,就像这样Heqv,我们有:
Heqv: v = Expr
我怎样才能选择自己的名字而不是Heqv？我总是可以使用rename命令将它重命名为我喜欢的任何内容,但这并不能保证我的证明不依赖于Coq中内置命名机制的假设未来变化.
在coq中,该destruct策略有一个变体接受"连接析取引入模式",允许用户为引入的变量分配名称,即使在解包复杂的归纳类型时也是如此.
coq中的Ltac语言允许用户编写自定义策略.我想写(实际上,维持)一种策略,在将控制权交给之前做一些事情destruct.
我希望我的自定义策略允许(或要求,更容易)用户提供我的策略可以提供的介绍模式destruct.
Ltac语法实现了什么？
以下定理在Coq中可证明吗？如果没有,有没有办法证明它不可证明？
Theorem not_for_all_is_exists:
forall (X : Set) (P : X -> Prop), ~(forall x : X, ~ P x) -> (exists x: X, P x).
我知道这种相关关系是真的:
Theorem forall_is_not_exists : (forall (X : Set) (P : X -> Prop), (forall x, ~(P x)) -> ~(exists x, P x)).
Proof.
(* This could probably be shortened, but I'm just starting out. *)
intros X P.
intros forall_x_not_Px.
unfold not.
intros exists_x_Px.
destruct exists_x_Px as [ witness proof_of_Pwitness].
pose (not_Pwitness := forall_x_not_Px witness). …我正在尝试编写一个函数,它接受一个自然数列表并返回其中不同元素的数量作为输出.例如,如果我有列表[1,2,2,4,1],我的函数DifElem应该输出"3".我尝试了很多东西,我得到的最接近的是:
Fixpoint DifElem (l : list nat) : nat :=
match l with
| [] => 0
| m::tm =>
let n := listWidth tm in
if (~ In m tm) then S n else n
end.
我的逻辑是:如果m不在列表的尾部,那么将一个添加到计数器.如果是,不要添加到计数器,所以我只计算一次:它是最后一次出现.我收到错误:
Error: The term "~ In m tm" has type "Prop"
which is not a (co-)inductive type.
In是Coq列表标准库的一部分Coq.Lists.List.它定义为:
Fixpoint In (a:A) (l:list A) : Prop :=
match l with
| [] => False
| b :: m => b = a …我很好奇discriminate战术背后的策略是如何运作的.因此我做了一些实验.
首先是一个简单的归纳定义:
Inductive AB:=A|B.
然后是一个简单的引理,可以通过discriminate策略证明:
Lemma l1: A=B -> False.
intro.
discriminate.
Defined.
让我们看看证明的样子:
Print l1.
l1 =
fun H : A = B =>
(fun H0 : False => False_ind False H0)
(eq_ind A
(fun e : AB => match e with
| A => True
| B => False
end) I B H)
: A = B -> False
这看起来相当复杂,我不明白这里发生了什么.因此,我试图更明确地证明相同的引理:
Lemma l2: A=B -> False.
apply (fun e:(A=B) => match e with end).
Defined. …我有点困惑在自然数上定义的后继函数的单射性是否Coq是一个公理？根据维基百科/皮亚诺公理，它是一个公理（7）。当我查看Coq.Init.Peano手册页时，我看到以下内容：
定义 eq_add_S nm (H: S n = S m): n = m := f_equal pred H。
提示立即 eq_add_S: core.
它看起来像一个公理（？），但令我困惑的是，在该页面的顶部它说：
它陈述了有关自然数的各种引理和定理，包括皮亚诺算术公理（在 Coq 中，这些是可证明的）
这句话是不是有点歧义？
我想看一个 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 …
感谢软件基金会的电子书，我目前正在学习 coq 。我成功地添加了如下内容：
Definition cnat := forall X : Type, (X -> X) -> X -> X.
Definition plus (n m : cnat) : cnat :=
fun (X : Type) (f : X -> X) (x : X) => n X f (m X f x).
但由于以下错误，我坚持使用 exp：
Definition exp (n m : cnat) : cnat :=
m cnat (mult n) n.
(*
In environment
n : cnat
m : cnat
The term "cnat" has type "Type@{cnat.u0+1}"
while …我发现我自己（有点）重复代码，因为我希望在目标和假设匹配时采用相同的策略。例如：
match goal with
| H : PATTERN |- _ => simpl in H; rewrite X in H; ... ; other_tactic in H
| |- PATTERN => simpl ; rewrite ; ... ; other_tactic
end.
如果匹配案例中的策略变得很长，我基本上会重复它，并in添加一些子句，这看起来很不令人满意，特别是如果我有很多匹配子句，这样我就会重复很多代码。
有时并不是因为我匹配，而只是因为我定义了自定义策略，但根据上下文，我想将其应用于目标或命名假设。例如：
Ltac my_tac H := simpl in H; rewrite X in H; ... ; other_tactic in H.
Ltac my_tac_goal := simpl ; rewrite X ; ... ; other_tactic.
然后我再次“复制”代码。
有什么方法可以避免这种重复吗？
在某些时候，我想知道目标是否有一个名称，例如GOAL假设，因此simpl in GOAL相当于simpl，但我怀疑情况并非如此。在这种情况下，我可以删除 的定义my_tac_goal，然后直接调用 …