我有幾個證據遵循相同的結構。其中第一個可以用trivial完成，其他所有用auto with foo_db完成，其中foo_db是在第一個證明完成後填充提示的提示數據庫。我想寫一個使用auto with foo_db來解決所有這些證明的Ltac程序。但是，當運行該Ltac解決我的第一個證明foo_db尚不存在，所以科克抱怨：Error: No such Hint database: foo_db.
考慮下面的代碼： Inductive Even : nat -> Prop :=
| EO : Even O
| ESS : forall n, Even n -> Even (S (S n)).
Fixpoint is_even_prop (n : nat) : Prop :=
match n with
| O => True
| S O => False
Inductive ty: Set :=
| I
| O.
Definition f (x: ty) (y: ty): nat :=
if x = y then 0 else 1.
我想要的功能f比較ty類型的兩個方面，但它並不能編譯，我看到這個錯誤： The term x = y has type Prop which is not a (co-)inductive typ
假設我寫勒柯克一個已知點的算法，總結了一個號碼的所有「半」： Fixpoint sum_of_halves (a : nat) : nat :=
match a with
| 0 => 0
| 2 * k => a + (sum_of_halves k)
| S (2 * k) => a + (sum_of_halves k)
end.
試圖評
在問題Is there a minimal complete set of tactics in Coq?中，回答提到exact就足以證明所有目標。有人可以解釋和舉例嗎？例如，如果A，B作爲Prop的目標A \/ B -> B \/ A如何僅由一堆exact證明？如果您還有其他更好的例子，請不要猶豫，以及回答。重點是對這個問題給出一些解釋並給出一個不平凡的例子。
如何在fq（x）= 0的情況下定義函數，如f（x）= 0？ 如果我做這樣的事情在OСaml， Definition test (i:nat):nat :=
if i < 5 then 0 else 1.
它抱怨 Error: The term i < 5 has type Prop which is not a (co-)inductive type.
我試圖從Software Foundations, vol. 2端口msubst_R Agda。我試圖通過對術語使用類型化表示來避免繁重的工作。下面是我的一切到msubst_R;我認爲以下一切都很好，但這是有問題的部分。 open import Data.Nat
open import Relation.Binary.PropositionalEquality hiding (subst)
o
Require Import FMapAVL.
Require Import OrderedTypeEx.
Module M := FMapAVL.Make(Nat_as_OT).
Fixpoint cc (n: nat) (c: M.t nat):bool :=
match M.find n c with
| None => false
| Some e =