当我用来Function在Coq中定义非结构递归函数时,在询问特定计算时,结果对象的行为很奇怪.实际上,Eval compute in ...指令不是直接给出结果,而是返回相当长的(通常为170 000行)表达式.似乎Coq无法评估所有内容,因此返回一个简化(但很长)的表达式而不仅仅是一个值.
这个问题似乎来自我证明所产生义务的方式Function.首先,我认为问题来自我使用的不透明术语,并且我将所有的引理转换为透明常量.那么,有没有办法列出一个术语中出现的不透明术语？或者任何其他方式将不透明的引理变成透明的引理？
然后我说,问题来自于所使用的订单有充分根据的证据.但我得到了奇怪的结果.
例如,我log2通过重复应用来定义自然数div2.这是定义:
Function log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| n => S (log2 (Nat.div2 n))
end.
我有两个证明义务.第一个检查n尊重lt递归调用中的关系,并且可以很容易地证明.
forall n n0 n1 : nat, n0 = S n1 -> n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1)
intros. apply Nat.lt_div2. apply le_n_S. apply …我面临一种情况，记录被赋予弱多态类型，但我不确定为什么。
这是一个最小化的例子
module type S = sig
type 'a t
val default : 'a t
end
module F (M : S) = struct
type 'a record = { x : 'a M.t; n : int }
let f = { x = M.default; n = (fun x -> x) 3 }
end
这里f给出了类型'_weak1 record。
有（至少）两种方法可以解决该问题。
let n = (fun x -> x) 3
let f = { x = M.default; n }
t …我想使用集合,为此尝试使用MSets库.但我需要将函数从一种类型的集合写入另一种类型的集合,并且它与Coq的模块系统交互不良.
这是我面临的一个问题的例子.我想要一套类型T和套T*T.我加入投影功能proj1和proj2从一组对,和功能的获得一组值add_l并add_r创建从一个值组对和一组值.
我实例化我的模块nat.我创建了一组nat并调用add_l,但Coq并不知道这一点SNat.t并且S.S1.t是相同的.在这里,我可以直接创建一组类型S.S1.t,但如果它必须与更复杂的环境进行交互将会更加困难.
有可能让Coq理解SNat.t并且S.S1.t是一样的吗？或者我的问题有另一种解决方案吗？
Require Import MSets.
Module DecidablePair (DT1:DecidableType) (DT2:DecidableType) <: DecidableType.
Definition t : Type := DT1.t * DT2.t.
Definition eq x y := DT1.eq (fst x) (fst y) /\ DT2.eq (snd x) (snd y).
Lemma eq_equiv : Equivalence eq.
Proof.
split.
- split; reflexivity.
- split; symmetry; apply H. …我刚刚发现了最大和非最大参数的存在(参见https://coq.inria.fr/refman/Reference-Manual004.html#sec109).
但是有一些动机使用一个而不是另一个吗？一个比另一个更近？仅需要{}创建最大隐式参数,而必须使用Arguments或Implicit Arguments指定非最大参数.是否应该首选最大隐式参数？
我有重写引理的基础。其中一些由类型类参数化。当应用引理时，重要的是当 Coq 无法自动解析类型类时重写会失败。我发现获得这种行为的唯一方法是隐式声明大多数参数。
Class T (t:Type) : Type.
Instance T1 : T nat.
Instance T2 : forall {A1 A2:Type} {t1:T A1} {t2:T A2}, T (A1*A2).
Definition f {A:Type} (x:A) := x.
Lemma f_eq : forall {A:Type} (t:T A) (x:A), f x = x.
Proof.
reflexivity.
Qed.
Lemma test1 : f (0,1) = (0,1).
Proof.
rewrite f_eq.
(* a subgoal T (nat * nat) is generated,
which should have been resolved directly *)
Abort.
Lemma test2 : f (0,true) = (0,true). …Coq允许编写复杂的模式匹配，但随后将它们分解，以便其内核可以处理它们。
例如，让我们考虑以下代码。
Require Import List. Import ListNotations.
Inductive bar := A | B | C.
Definition f (l : list bar) :=
match l with
| _ :: A :: _ => 1
| _ => 2
end.
我们在列表和第二个元素上都进行模式匹配。打印f显示Coq存储了它的更复杂的版本。
Print f.
(* f = fun l : list bar => match l with
| [] => 2
| [_] => 2
| _ :: A :: _ => 1
| _ :: B :: _ => 2
| …