考虑以下部分证明：
Theorem test : forall (n m : nat),
n = m -> S n = S m.
Proof.
intros n m H.
执行到这一点给我以下内容：
1 subgoal
n, m : nat
H : n = m
______________________________________(1/1)
S n = S m
我想S从目标中删除s ，获得目标n = m。有没有一种策略可以做到这一点？
在问题中Coq中有一套最小的完整策略吗？,提到的答案exact足以证明所有目标.有人可以解释一下吗？例如,A \/ B -> B \/ AA,B作为Prop 的目标如何仅通过一堆来证明exact？如果您有其他更好的例子,请不要犹豫,也请回答.关键是要对这个问题给出一些解释并给出一个非常重要的例子.
在Coq教程 1.3.1和1.3.2节中，有两个elim应用程序：第一个应用程序：
1 subgoal
A : Prop
B : Prop
C : Prop
H : A /\ B
============================
B /\ A
申请后elim H，
Coq < elim H.
1 subgoal
A : Prop
B : Prop
C : Prop
H : A /\ B
============================
A -> B -> B /\ A
第二个：
1 subgoal
H : A \/ B
============================
B \/ A
申请后elim H，
Coq < elim H.
2 subgoals
H …如何才能看到 Coq 中内置策略的具体实现？更具体地说，是否有替代方法Print Ltac <user-defined-tactics>可以在 Coq 中查找内置策略的确切定义？
我理解使用这种inversion策略的防爆原理:
Theorem ex_falso_quodlibet : forall (P:Prop),
False -> P.
Proof.
intros P contra.
inversion contra. Qed.
但是,我不明白Coq为了做同样的证明所采取的步骤,而是使用destruct而不是inversion:
Theorem ex_falso_quodlibet' : forall (P:Prop),
False -> P.
Proof.
intros P contra.
destruct contra. Qed.
False归纳如何被破坏？它如何影响目标并完成证明？
试图理解@keep_learning的答案，我一步一步地浏览了这段代码：
Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).
Example test_nostutter_4: not (nostutter [3;1;1;4]).
Proof.
intro.
inversion_clear H.
inversion_clear H0.
unfold not in H2.
(* We are here *)
specialize (H2 eq_refl).
apply H2.
Qed.
这是我们在执行 specialize 之前所拥有的
H1 : 3 …构造函数策略允许您通过自动应用构造函数来实现归纳数据类型的目标。然而，定义相等在 Coq 中不是归纳产品。那么为什么 Coq 接受这个证明呢？
Example zeqz : 0 = 0. constructor.
经过多次失败后，我发现 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,并试图证明一些看似相当简单的东西:如果列表包含x,那么该列表中x的实例数将> 0.
我已经定义了contains和count函数,如下所示:
Fixpoint contains (n: nat) (l: list nat) : Prop :=
match l with
| nil => False
| h :: t => if beq_nat h n then True else contains n t
end.
Fixpoint count (n acc: nat) (l: list nat) : nat :=
match l with
| nil => acc
| h :: t => if beq_nat h n then count n (acc + 1) t else count n acc t
end.
我试图证明:
Lemma contains_count_ge1 : …有人可以解释一下如何完成这个证明吗？（请不要给出实际答案，只是一些指导:)
练习来自 SF 第 1 卷，如标题所示，内容如下：
(** **** Exercise: 3 stars, standard (injection_ex3) *)
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
j = z :: l ->
x = y.
现在，我在介绍所有术语后尝试通过injectionon来解决这个问题H0。injection经过重写后H2，我最终得到了以下目标，但我不知道如何前进。
1 subgoal (ID 174)
X : Type
x, y, z : X
l, j : list X
H2 : x = …