coq-tactic

5熱

2答えて

タイプの誘導原理は、命題Pについての単なる定理であることを読んだ。そこで私はListの誘導原理を正しい（または逆の）リストコンストラクタに基づいて構築しました。 Definition rcons {X:Type} (l:list X) (x:X) : list X := l ++ x::nil. 誘導原理自体は次のとおりです。 Definition true_for_nil {X:T

1熱

1答えて

コック：？「書き換え」または「適用」を使用して、真の簡素化（NEGB（neqb真）証明で

が、私は(negb (negb true))）も同様にfalseと（trueにを簡素化したい私はコックのnegb_involutive手順を知っています、。しかし、私の教科書は、それを導入していないので、私は私が何とかのみrewriteまたはapplyを使用してその機能を模倣するために管理する必要があることだと思う。

1熱

1答えて

Coq aac_tacticsの合理性ではなく整数に対しては書き直し

Coq書き換え方法モジューロ連合性と可換性（aac_tactics）をテストしていました。次の例は、整数（Z）に対して機能しますが、整数を有理数（Q）に置き換えるとエラーが発生します。 Require Import ZArith. Import Instances.Z. Goal (forall x:Z, x + (-x) = 0) -> forall a b c:Z, a + b + c

1熱

1答えて

Coq "ローカルアプリケーションの使用"の正しい使い方は何ですか？

私はだから私は、次のように、それぞれに2つのささいな戦術を適用しようとして2つのゴールで少しテストをした Local application of tactics Different tactics can be applied to the different goals using the following form: [ > expr1 | ::: | exprn ] The expres

7熱

1答えて

Coqで現在の目標を切り替えるにはどうすればよいですか？

Coqで現在の目標または副目標を証明するために切り替えることは可能ですか？例えば、私はこの（eexistsから）のような目標があります。 ______________________________________(1/1) ?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2) 私はsplitにされませんし、最初の右の論理積を証明したい何を。これは、

1熱

1答えて

は、タイプレベル

で書き換え私は、次の証明状態を持っている： 1 subgoals U : Type X : Ensemble U Y : Ensemble U f : U -> U g : U -> U pF : proof_dom_cod U X Y f pG : proof_dom_cod U X Y g fg : f = g H : proof_dom_cod U X Y g = proo

0熱

1答えて

誘導命題のCoq - disj_conj_intro_patterns

Coqの任意の誘導命題定義が与えられた場合、誘導命題に対して誘導戦略を呼び出すときに使用する合理的なdisj_conj_intro_patternを導出する一般的な式はありますか？一般に、帰納的定義のコンストラクタのいずれかの完全なintro_patternは、複数の仮説と複数の帰納仮説を（名前を）必要とすることがあります。この場合、パターンに含まれる名前の順序付けには、パラメータ、続いて1つの

0熱

2答えて

3つのargsの否定とそれをカバーする定理のCoq構文

以下の3つの引数の否定と定義を与えて、簡単に異なるケースを証明することができますが、 Coqを使用します。 Forall b1 b2 b3：boolのうちの1つがfalseであればtrueを返し、3つが真であればfalseを返します。どのように私はCoqでこの前提を書くのですか？私は分割などの戦術を使用して連結などを分割することができますか？ Definition negb (b:bool) :

3熱

2答えて

コックが依存型指定された誘導性の命題

のコンストラクタを区別することはできません私は私がいる問題を示すために、この例のタイプを作成しました：今 Inductive foo : nat -> Prop := | foo_1 : forall n, foo n | foo_2 : forall n, foo n. はっきりfoo_1 0 <> foo_2 0が、私はこれを証明することができないよ： Lemma bar : foo_

3熱

1答えて

Coqの "S"（succ）に "+ 1"（+ 1）を書き換えるにはどうすればよいですか？

私は不完全な証拠で、次の補題があります Lemma (s_is_plus_one : forall n:nat, S n = n + 1). Proof. intros. reflexivity. Qed. この証明は、これを証明する方法だろうeq_Sように思える Unable to unify "n + 1" with "S n". で失敗したが、私は（それを適用