同じ構造に従ういくつかの証明があります。最初は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
このように、我々はいくつかの（半）グループ論的性質を形式化しようとしていると仮定します。つまり、我々は上記の定義のいずれかの式を逆転場合 Section Group.
Variable A: Type.
Variable op: A -> A -> A.
Definition is_left_neutral (e: A) := forall x: A, (op e x) = x.
De
Inductive ty: Set :=
| I
| O.
Definition f (x: ty) (y: ty): nat :=
if x = y then 0 else 1.
私はタイプtyの二つの用語を比較する機能fをしたいが、それはコンパイルできないと、私はこのエラーを参照してください。 The term x = y has type Prop which is n