coq

0熱

1答えて

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

6熱

2答えて

coqでのステップバイステップの簡略化

一度に1つのステップを簡略化する方法はありますか？あなたは、単一のsimplを経由して順番に簡略化することができ、どちらもf1 (f2 x)があると、それは、最初のステップとしてf2 xを簡素化し、中間結果を検討し、その後f1を簡素化することができますか？例えば定理を取る： Theorem pred_length : forall n : nat, forall l : list nat,

3熱

1答えて

Coqに「ユニークなXが存在する」という表現方法は？

簡潔 Coqにユニークなもの（つまり固有の存在量限定子を書く）が存在するかどうか疑問に思っていましたか？たとえば、x s.t.が存在するとします。 2 + x = 4： Goal exists x, 2 + x = 4. どのように私は、同じプロパティを持つユニークxが存在することを書くことができますか？は、私はこのようなs.t.部分に述語を複製することができます知っている： Goal e

1熱

1答えて

はスコープ

This answer内の表記を広げ、簡単な便利なトリックを提供します：unfold ">="はunfold geと同じですが、>=がgeの表記法であることを知っているあなたを必要としません。スコープ内で表記法を同じにすることはできますか？それはge、ないN.geを展開しようとするためここ Require Import NArith. Goal forall x, (x >= x)%N.

-3熱

2答えて

リストにCoq変数があります

リストに存在する変数を証明することに問題があります。 Lemma exists_in_list_helper: forall (X : Type) (a : X) (P : X -> Prop), (exists b : X, In b [a] -> P b) -> P a. Proof. Admitted. 私は別の質問があります。リスト内の値に対してケース分析を

2熱

3答えて

Coq：環境内のユニバース内のすべての用語を表示する

環境内のユニバース内のすべての型またはすべての型を表示する方法はありますか？ Print Set. (*Syntax error: 'Firstorder' 'Solver' expected after 'Print' (in [vernac:command]).*)

-2熱

1答えて

四角形が等しい場合、オペランドも同じであることを示すにはどうすればよいですか？任意のヒントは非常に参考になる</p> <pre><code>Lemma l1 : forall m n : nat, m * m = n * n -> m = n. </code></pre> <p>：

私はこの補題の証明を仕上げ問題を抱えていました。 Require Import Arith Omega Nat. Lemma l1 : forall m n : nat, m * m = n * n -> m = n. Proof. intros. destruct (Nat.eq_dec m n). trivial. induction n. induction m. auto.

1熱

2答えて

Coqの矢印は普遍的な定量のエイリアスですか？

私はchapter 4 of the reference manual of Coqを読んでいます。参考文献に記載されているタイピング規則によれば、用語fun x: nat => xのタイプはforall x: nat, natである。 I Check Coqのことで、この用語は、それがnat -> nat入力されしかし Assume that E is [nat: Set].

5熱

2答えて

ex_introの定義を読むにはどうすればよいですか？

私が言うこれは、Mike Nahas's introductory Coq tutorialを読んでいる：に "ex_intro" 引数は次のとおりです。述語証人証人と呼ばれる前提の証明私はthe definition： Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (

2熱

1答えて

Coq：不十分な正当化エラー

私はCoqを初めて使用しており、仮説H3のためにInsufficient Justificationエラーが発生しています。私はそれを数回書き直そうとしましたが、エラーは持続します。誰かが理由を説明できますか？ありがとう。 Section GroupTheory. Variable G: Set. Variable operation: G -> G -> G. Variable e : G