在问题Is there a minimal complete set of tactics in Coq?中，回答提到exact就足以证明所有目标。有人可以解释和举例吗？例如，如果A，B作为Prop的目标A \/ B -> B \/ A如何仅由一堆exact证明？如果您还有其他更好的例子，请不要犹豫，以及回答。重点是对这个问题给出一些解释并给出一个不平凡的例子。
我无法证明使用coq的策略的简单逻辑max a b <= a+b。我应该如何解决它？以下是我到现在为止的代码。 s_le_n已被证明，但为简单起见，此处未提及。 Theorem s_le_n: forall (a b: nat), a <= b -> S a <= S b.
Proof. Admitted.
Theorem max_sum: forall (a b: nat), max a
我有一个string b和string a上比较，如果有平等的string c，否则有string x。我知道的假设fun x <= fun c。我如何证明以下陈述？ fun是一些函数，它发生在string并返回nat。 fun (if a == b then c else x) <= S (fun c)
的逻辑似乎是显而易见的，但我无法将拆分COQ的if语句。任何帮助，将不胜感激。 谢谢！
我需要在绑定器下泛化表达式。例如，我有我的目标，两个表达式： (fun a b => g a b c)
和 (fun a b => f (g a b c))
我想概括g _ _ c部分： 一种方法做的是第一重写它们分为： (fun a b => (fun x y => g x y c) a b)
第二入： (fun a b =>
f (
(fun x y => g
在Coq我有两个假设H和H0，这相互矛盾。问题是，他们只是为了一些专业而互相矛盾，在这个证明的背景下，情况并不那么专业化。 这时我的证明背景是这样的： color : Vertex -> bool
v : V_set
a : A_set
x0, x1 : Vertex
H : v x0 -> v x1 -> a (A_ends x0 x1) \/ a (A_ends x1 x0) -> c