下面的文本中SF书中提到： 这是我们如何使用并不表明0和1是NAT的不同元素： Theorem zero_not_one : ~(0 = 1).
Proof.
intros contra. inversion contra.
Qed.
Such inequality statements are frequent enough to warrant a special notat
比方说，这是我目前的房地和目标： IHl' : forall l' : list A, In a l'' \/ In a l' -> In a (l'' ++ l')
l' : list A
============================
....
现在，我想的假设得到转化这样的： IHl' : In a l'' \/ In a l' -> In a (
我在Coq中使用MathComp库进行反射时遇到了一些非常简单的问题。 假设我要证明这个定理： From mathcomp Require Import ssreflect ssrbool ssrnat.
Lemma example m n: n.+1 < m -> n < m.
Proof.
have predn_ltn_k k: (0 < k.-1) -> (0 < k).
的情况下，我一直尝试在各种情况下apply战术，似乎卡在以下情况时，前提是这样的： H1 : a
H2 : a -> forall e : nat, b -> g e
============================
...
当我尝试apply H2 in H1.，它给我的错误： Error: Unable to find an instance for
如果目标状态是这样的： a : Prop
b : Prop
H1 : a
H2 : b -> c
============================
c
然后，我可以将其转换为使用apply H2战术以下状态： a : Prop
b : Prop
H1 : a
H2 : b -> c
=======
我是Coq的新手，正在做一些练习，以便更熟悉它。 我的理解是，在证明勒柯克命题“真”是写下来加利纳一个类型，然后显示出它的使用战术方面确定性的方式结合在一起居住。 我不知道是否有一种方式来获得实际刑期的一个漂亮的印刷表示，所有的战术中删除。 在下面，plus_comm (x y : N) : plus x y = plus y x类型的匿名术语最终产生的例子。我想。如果我想看看，我应该怎么做？从某
我已经开始学习Coq的，而且我想证明的东西，似乎相当简单：如果列表包含X，然后在列表x的实例的数量将是> 0。 我已经定义了包含与如下计数功能： Fixpoint contains (n: nat) (l: list nat) : Prop :=
match l with
| nil => False
| h :: t => if beq_nat h n then T
我正在考虑COQ中的证据不相关性。 一个证明的声明说： 如果一个类型的平等是可判定则只能有一个平等的声明，即反身性的证明。 我不知道它是否可能在COQ中构造具有多个平等证明的类型。因此我想问下面的结构是否一致？ (*it is known that f=g is undecidable in COQ *)
Definition f(n:nat) := n.
Definition g(n:na