我正在嘗試使用可以輕鬆生成的術語(在此特定示例中,從tauto)實例化存在量詞的策略。我第一次嘗試: Ltac mytac :=
match goal with
| |- (exists (_ : ?X), _) => cut X;
[ let t := fresh "t" in intro t ; exists t; firstorder
Ltac checkForall H :=
let T := type of H in
match T with
| forall x, ?P x =>
idtac
| _ =>
fail 1 "not a forall"
end.
Example test : (forall x, x) -> True.
Proof.
我有幾個證據遵循相同的結構。其中第一個可以用trivial完成,其他所有用auto with foo_db完成,其中foo_db是在第一個證明完成後填充提示的提示數據庫。我想寫一個使用auto with foo_db來解決所有這些證明的Ltac程序。但是,當運行該Ltac解決我的第一個證明foo_db尚不存在,所以科克抱怨:Error: No such Hint database: foo_db.
如何在ltac中調用rewrite只重寫一個發生?我認爲coq的文檔提到了一些關於rewrite at的內容,但我在實踐中並沒有真正使用它,並且沒有例子。 這是什麼,我試圖做一個例子: Definition f (a b: nat): nat.
Admitted.
Theorem theorem1: forall a b: nat, f a b = 4.
Admitted.
Theor
我需要在綁定器下泛化表達式。例如,我有我的目標,兩個表達式: (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
獲取假名'類型 我正在尋找一種通過它的名字獲得假名以匹配它的方法。就像這樣: Ltac mytactic h_name :=
let h := hyp_from_name h_name in
match h with
| _ /\ _ => do_something
| _ => print_error_message
end
.
這將是像這樣使用: