coq

    0

    1答えて

    で平等FORALL: Lemma Foo (A : Type) (n : nat) (gen : forall p : nat, p < S n -> A) (ic0 : 0 < S n) (ic1 : 0 mod S n < S n): gen (n - n) ic1 = gen 0 ic0. n-nはNat.sub_diagで0であると0 mod S nはNat.mod_0_l

    2

    1答えて

    私はコインシデンスタイプを試していましたし、自然数とベクトル(型のサイズがリスト)のコインシデンスバージョンを定義することに決めました。私は彼らとように無限の数に定義: CoInductive conat : Set := | cozero : conat | cosuc : conat -> conat. CoInductive covec (A : Set) : conat -> Se

    1

    2答えて

    私は現在、容易に生成できる用語(この具体例では、tauto)を使用して存在量限定子をインスタンス化する手法を作成しようとしています。私の最初の試み: Ltac mytac := match goal with | |- (exists (_ : ?X), _) => cut X; [ let t := fresh "t" in intro t ; exis

    0

    1答えて

    私が証明する必要があります: i < Datatypes.length (l0 ++ f :: nil) -> H 私はi < Datatypes.length l0とi = Datatypes.length l0用に別の仮説を持っています。

    0

    1答えて

    、これは可能ですか? 私はキャンセルがグループで働くことを証明しようとしています。 私は a, b, x : G H: a <+> x = b <+> x を持っていると私は a = b 私の考えを証明したいと思いますが(iが逆関数である)仮説 H2: a <+> x <+> i x = a <+> x <+> i x を取得することでした。 私は pose proof eq_ref

    1

    2答えて

    Coqのベクトルの順列について、私は理由を考える必要があります。標準ライブラリには、リストの置換定義のみが含まれています。私の最初の試みとして、私はのようなベクターのためにそれを模倣しようとした: Inductive VPermutation: forall n, vector A n -> vector A n -> Prop := | vperm_nil: VPermutation

    0

    1答えて

    Coqで要素のすべての親を取得するにはどうすればよいですか? 次のように私はコックにセットを定義します。私は3の親要素、すなわち[1,2]を取得したい、今すぐ Definition g1 = BGen 1 2. Definition g2 = BGen 2 3. : Inductive Gen : Set := | BGen : nat -> nat -> Gen. は、次のような多く

    3

    1答えて

    私はCoqの2つのパラメータにネストされた再帰関数を定義しようとしています。 Require Import List. Import ListNotations. Fixpoint map_sequence2 {A B C : Set} (f : A -> B -> option C) (xs : list A) (ys : list B) : option (list C) :=

    1

    1答えて

    私はCoqを学習しています。初めて、ring戦術を使用する必要があります。私はRequire Ring.またはRequire ArithRing.の後にそれを使って私が目標として持っている方程式の右辺を簡略化しようとしましたが、Coqはそれが存在しない参照を取ります。これらの戦術を呼び出すには Lemma sum_n_p : forall n, 2 * sum_n n + n = n * n.

    4

    1答えて

    私は、HaskellとOCamlプログラムにCoqプログラムを抽出できることを知っています。 Cでこれを行う方法はありますか? 私はC言語をモデル化したライブラリを想像しています。おそらく、そのようなライブラリには、C構造がプロセスメモリとどのようにやりとりするか、そしてIEEE浮動小数点数に関する公理と定理についての公理の集合が含まれるでしょう。それから、プログラムについての定理とともにCoq内