coq

2熱

1答えて

私はgeneralized rewriting features of Coqを使用しています。書き換えに失敗したときにどのリレーションや関数が欠けているかを理解するために、現在利用可能なセトイドとモチーフをsetoid_rewriteに印刷したいと思います。それを行う方法はありますか？

3熱

2答えて

Coq：1つのコマンドで複数の変数を持つ存在量限定子の逆転？

私は仮説 H : exists a b v, P a b v 私はinversion Hを使用する場合、私は罰金である a : nat H1 : exists b v, P a b v. を回復したが、その後、私は二倍以上反転を使用する必要があるとした証拠を通して働いていますbとvを復旧してください。 a、b、vを一度に復旧するコマンドはありますか？

2熱

1答えて

Coq head normal formのヘッドとは何ですか？

Coq/CICヘッドノーマルフォームの理解に問題があります。具体的には、私は頭が何かを理解していません。リファレンスマニュアル（8.5p1）は言うこと任意の用語は、以下のように書くことができるしかし、上記の定義は、否定的な意味である：それはではないt0が必要ですアプリケーションは、はt0ができることを言っていない。実際には、私が覚えている限り、t0 t1 t2 ...として書かれる唯一のものは

2熱

3答えて

タイプファミリーとマッチングするときのCoqタイプエラー

メモリからCPDTの例を再実装しようとしています。私が書いた： Inductive myType : Set := MyNat | MyBool. Definition typeDenote (t : myType) : Set := match t with | MyNat => nat | MyBool => bool end. Inductiv

1熱

2答えて

Coq：複雑な式間の強制/サブタイプ化

Coqでは不可能な印象を受けました。例 Parameter Arg: Type. Parameter F X XP: Arg. Parameter S P I PLS PI: Arg -> Type. Parameter tree car: P X. Parameter mary john: PLS XP. Parameter c: PLS XP -> P XP. Coercion c

0熱

1答えて

コック：強制の定義でエラーが発生しました

は、あなたがエラーを修正することができます：私は Coercion f (u:Arg) (x y z: Arg -> Prop) (t:x u /\ y u /\ z u): x u. tauto. Defined. Print f.

3熱

2答えて

Coqの角括弧構文[| - Set]とは何ですか？

私いくつかの回では、このような実存的変数に関する情報を印刷のように、特定の種類/セットを表すために、Coqの中で、この構文を参照してください。 ?T : [ |- Set] ?T0 : [ x : ?T |- Set ] 私はこの構文を検索する方法を知りません。この意味は？は ? T : Set と同じ最初のものですか？

1熱

1答えて

Coqでサブセット関係を表現するには？

Yのセットが別のセットXのサブセットであることをCoqでどのように記述できますか？私は次のようにテストした： Definition subset (Y X:Set) : Prop := forall y:Y, y:X. 、要素yがYである場合、その後、yがXであることを表現しようとしています。しかし、これは驚くことではないが、yについてのタイプエラーを生成する。 Coqでsubse

0熱

1答えて

MSetを使用しているcoqの証明

私はまだcoqに新しいです、そして、MSetsは私にいくつかの問題を与えています。要素がリストかセットかを計算する2つの関数は、set_containsの定義が正しいと思うかどうか、もっと良い方法があれば教えてください。助けてくれてありがとう。 Require Import MSets ZArith. Module mset := MSetAVL.Make Positive_as_OT.

0熱

1答えて

Coqで2つの 'int'型を比較する方法はありますか？

私はCoqのスペックファイルに次の定義を持っています。私は2つの "int"型の値を比較する命題を持つ必要があります。これら2つは 't'と 'Int.repr（i。（period1））'です（i.period1）と（i.period2）はタイプ 'Z'です。これは私のコードスニペットです：これは私に以下のエラーが発生します Definition trans_uni_r_reject (i: i