同じ構造に従ういくつかの証明があります。最初はtrivialで終わることができ、他のすべてはauto with foo_dbで終わることができます。foo_dbは、最初の証明が完了した後にヒントが埋め込まれたヒントデータベースです。私はauto with foo_dbを使用してこれらの証明をすべて解決するLtacプロシージャを作成したいと思います。しかし、そのLtacを実行して私の証明の最初のもの
この簡単な開発を考えてみましょう。私は2つの些細なデータ型を持っている： Inductive A :=
| A1
| A2.
Inductive B :=
| B1 : A -> B
| B2.
は、今私は関係の概念を導入し、データ型AとBに発注定義誘導データ型として表現： Definition relation (X : Type) := X -> X -> Prop.
Re
時には私は、別の空間に投影することによって最もよく行われる証拠を持っています。私は、次の操作を行い、現時点では： Ltac project x y :=
let z := fresh in
remember x as y eqn:z; clear z; clear x.
しかし、私は次のエラーを取得する： remember (f x) as y eqn:H; clear H
バインダーの下で式を一般化する必要があります。例えば、私は私の目標で二つの表現があります。 (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)
および第2のもの：
私はそれに合うようにその名前でhypotesisを得る方法を探しています。 H0 : A /\ B
==================
A
Coq < mytactic H0.
ありがとう：次のように使用される Ltac mytactic h_name :=
let h := hyp_from_name h_name in
match h with
| _ /\
私は現在、容易に生成できる用語（この具体例では、tauto）を使用して存在量限定子をインスタンス化する手法を作成しようとしています。私の最初の試み： Ltac mytac :=
match goal with
| |- (exists (_ : ?X), _) => cut X;
[ let t := fresh "t" in intro t ; exis