Is there a minimal complete set of tactics in Coq?の質問では、exactという回答はすべての目標を証明するのに十分であると述べています。誰かが説明して例を挙げることができますか？例えば、A \/ B -> B \/ AのA、BがPropであるという目標は、単にexactの束で証明されるのでしょうか？他にも良い例がある場合は、お気軽にお答えください。
もしxの場合f（x）= 0の場合はどうすれば定義できますか？<もしそうでなければ、Coq？ 私は、 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.
私はstring aを持っていて、string bと比較して、等価がstring cの場合はstring xです。私は、仮説ではfun x <= fun cだと知っています。これを証明するにはどうしたらいいですか？ funは、stringを取り込み、natを返す関数です。 fun (if a == b then c else x) <= S (fun c)
ロジックは明らかですが、私はcoqの
バインダーの下で式を一般化する必要があります。例えば、私は私の目標で二つの表現があります。 (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のもの：