我有一个功能max：
Fixpoint max (n : nat) (m : nat) : nat :=
match n, m with
| O, O => O
| O, S x => S x
| S x, O => S x
| S x, S y => S (max x y)
end.
以及交换律的证明max如下：
Theorem max_comm :
forall n m : nat, max n m = max m n.
Proof.
intros n m.
induction n as [|n'];
induction m as [|m'];
simpl; trivial. …如何才能看到 Coq 中内置策略的具体实现？更具体地说，是否有替代方法Print Ltac <user-defined-tactics>可以在 Coq 中查找内置策略的确切定义？
我试图理解@at 符号在 Coq 中在所有情况下的作用。我看到这个的背景是我正在 Coq 中尝试打印和删除符号（或尽可能多）。特别是，我用 . 打印 (Gallina) 术语Set Printing All。我定义了自己的加法和 nat，当我这样做时得到了这个
my_add_eq =
fun x y : my_nat => @eq_refl my_nat (my_add x y)
: forall x y : my_nat, @eq my_nat (my_add x y) (my_add x y)
但我不确定这个@标志是什么意思。这是什么意思？
请注意，我在 Coq 8.5pl1 中看到了这个问题 Refine 和 @ (at) 符号，但它们似乎@在证明的上下文中使用，而我在不同的上下文中看到它（我正在打印 Gallina 术语）。老实说，我并不完全理解这个问题的答案。也许这与我的问题有关，但我不能说。也许通过更仔细地阅读，我可能需要隐含的论据才能真正理解什么@意思？令我惊讶的是，What does the at sign @ in coq do除了我发布的那个问题之外，谷歌搜索并没有得到太多结果。对 coq 手册/文档的参考将是理想的选择（我确实尝试在文档中搜索at sign，@ …
我试图证明 Coq 中最简单的事情：
Require Import Coq.Structures.OrdersFacts.
Require Import Coq.Structures.Orders.
Lemma easy: forall a b : nat, (a = b) -> (a <= b).
Proof.
intros.
apply le_lteq. (* doesn't work *)
apply LeIsLtEq.le_lteq. (* doesn't work *)
但我收到以下错误：
The reference le_lteq
was not found in the current
environment.
这有点奇怪，因为我确实在Coq.Structures.Orders中看到了它
经过多次失败后，我发现 Coq 做了一件我不明白的奇怪事情。抱歉涉及的代码，我无法隔离一个更简单的示例。我有一个包含trident三个变量的公式p，q, r。a <-> b然后，我简单地用in place of p、ain place ofq和bin place of写出该公式的一个实例r，并尝试证明一个引理，表明结果相当于trident上面的代入。当试图证明我被第一个子目标困住时，它写着
a, b : Prop
H : b
============================
a \/ (a <-> b)
这显然是无法证明的：如果b假设为真，那么就a \/ (a <-> b)变为正义a，并且没有理由它为真。
这是完整的代码：
From Coq Require Import Setoid.
Definition denseover (p q : Prop) := (p -> q) -> q.
Definition trident (p q r …我目前正在关注《软件基础》一书，目前正在阅读“列表”章节。 然而，我很难理解模式匹配的具体情况，并且由于是 Coq 的初学者，我不确定如何找到这个问题的答案。
因此，练习是创建一个来计算列表（更具体地说是一个包）中有Fixpoint多少 nat 。vs
我决定为此使用模式匹配，但如果我尝试定义这样的函数：
Fixpoint count' (v: nat) (s: bag) : nat :=
match s with
| nil => O
| h :: t => match h with
| v => S (count' v t)
end
end.
并尝试将此功能应用于，比方说，
Example test_count1: count' 1 [1;2;3;1;4;1] = 3.
我最终会得到6 = 3。我的理解是，匹配h始终v是“true”，因此它最终会计算列表中的每个元素。
但为什么会发生这种情况呢？h我们如何使用模式匹配来比较和的值v？
PS：我已经使用比较 ifh和vequal 的辅助函数解决了这个练习，但我想知道这是否只能使用内置模式匹配来实现。
我试图用勒柯克的listSet创建set的nats.但是,在向集合添加成员时遇到问题.
这是我正在运行的代码.
Require Import ListSet Nat.
Axiom eq_dec : forall x y : nat, {x = y} + {x <> y}.
Compute (set_add eq_dec 0 (set_add eq_dec 0 nil)).
运行时,输出为
=如果eq_dec 0 0则(0 :: nil)%list else(0 :: 0 :: nil)%list:set nat
现在,我知道为什么我if-else在输出中得到语句.这是因为我只告诉Coq,平等nats是可判定的,但没有评估平等.我也知道如何比较两个nats.代码如下.
Fixpoint nats_equal (m n : nat) : bool :=
match m, n with
| 0, 0 => true
| 0, _ => …用于确定集合是否是另一个集合的子集的函数:
Fixpoint subset (s1:bag) (s2:bag) : bool :=
match s1 with
| nil => true
| h :: t => match (beq_nat (count h s1) (count h s2)) with
| true => subset (remove_all h t) (remove_all h s2)
| false => false
end
end.
为清楚起见
beq_nat 确定两个自然数的相等性count 计算给定自然数出现在集合中的次数remove_all 从集合中删除给定自然数的每个实例CoqIDE"不能猜测减少修正的论点." 鉴于递归是在t(尾部s1)的子集上完成的,为什么不能保证终止？
注意:此问题来自此网站,其作者要求解决方案不公开发布.此外,我已经解决了这个问题,因此不需要解决方案.解释为什么coq不能确定终止将非常感激.
我想证明一个小于Int.max_unsigned的Z类型值.
引理测试:10%Z <Int.max_unsigned.证明.?? 如何证明上述测试引理？
我想证明不包含0的自然数。因此，我对属性P的基本情况应为P 1而不是P 0。
我正在考虑使用n> = 0作为目标假设，但是在Coq中还有另一种方法可以做到这一点吗？