比方說，這是我目前的房地和目標： 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