考慮以下發展： Require Import Relation RelationClasses.
Set Implicit Arguments.
CoInductive stream (A : Type) : Type :=
| scons : A -> stream A -> stream A.
CoInductive stream_le (A : Type) {eqA R : r
的概念，定義如下： Inductive eq (A : Type) (x : A) : A → Prop := eq refl : (eq x) x
Parameter a b : A.
當我考慮它的實例eq a b之一，我讀A -> Prop類型的(eq a)。 那麼，我的問題是，(eq a) b如何確定a和b對應於同一個對象的事實？ 對我而言，奇怪的是我們沒有關於(eq a)究竟做什麼
我被卡在一個目標上。 假設我們有如下定義： Fixpoint iota (n : nat) : list nat :=
match n with
| 0 => []
| S k => iota k ++ [k]
end.
我們要證明： Theorem t1 : forall n, In n (iota n) -> False. 到目前爲止，我已成功地執行
我感到困惑勒柯克的類型系統對的小時以下的定義證明長期的匹配部分的行爲： Set Implicit Arguments.
Definition h := fun (a b : nat) (e : a = b) =>
(fun (x y : nat)(HC : b = y)(H : x = y) =>
(match H in (_ = y0) return (b = y0 -> b = x) w
如何在ltac中調用rewrite只重寫一個發生？我認爲coq的文檔提到了一些關於rewrite at的內容，但我在實踐中並沒有真正使用它，並且沒有例子。 這是什麼，我試圖做一個例子： Definition f (a b: nat): nat.
Admitted.
Theorem theorem1: forall a b: nat, f a b = 4.
Admitted.
Theor