coq

    1

    2答えて

    における機能の終了 証明します。資料はthisの5ページ目です。この関数は、正規表現(Isabelle/HOLで形式化されています)の正規化関数の一部として実行されます。 le_regex関数は同じ論文から適合されています。私は決定的な合計順序でregexのパラメータ化を避けるためにasciiを使用しています(プログラムを抽出したい)。 Inductive regex : Set :=

    2

    1答えて

    subtypesをCoqに、そしてssreflectを使用して簡単に処理しようとしています。しかし、私はいつもサブタイプを書き直すときにいくつかの問題に遭遇します。例えば:それはそこに立ち往生している理由 Require Import Omega. From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype. (*

    0

    2答えて

    私は補助証拠COQを使用しています。私の最初の質問は、Induction.vファイルについてです。Require Import basicsの代わりにRequire Export Basicsを使用するのはなぜですか?また、基本名をMybasics.vに変更した場合でも、Export basics.vを作成すると、なぜ機能しますか? Require Export Basics.は何をしますか?それ

    4

    1答えて

    に私はのCoQ 8.6でBIGNUM $ opam upgrade bignum Already up-to-date. をインストールするためにOPAMを使用していないRequire Import BigN.はCoQは8.7でライブラリをインポートしたが、 Iエラーが発生します。 私は、このコード行をファイルbignum_problem.vに分離します。そして、 coqc bignum_p

    5

    2答えて

    私は自分自身に説明できないCoqの終了チェッカーの動作につまづいています。考えてみましょう: Require Import Coq.Lists.List. Record C a := { P : a -> bool }. Arguments P {_}. Definition list_P {a} (a_C : C a) : list a -> bool := existsb (P a

    3

    1答えて

    私は2つの短いファイルを持っている:cc_testが Lemma cc: 4 = 4. Proof. auto. Qed. によって与えられ、libtestは私が実行 Require Import cc_test. Check cc. で与えられる ディレクトリ内coqc -R . ClosureLib -top ClosureLib cc_test "/ホーム/バリー/ SVN /コック/ Cl

    2

    3答えて

    私は、ASCII文字が空白であるかどうかの決定手順を自動化しようとしています。ここに私が現在持っているものがあります。 Require Import Ascii String. Scheme Equality for ascii. Definition IsWhitespace (c : ascii) := (c = "009"%char) \/ (c = "032"%char). D

    2

    1答えて

    時には私は、別の空間に投影することによって最もよく行われる証拠を持っています。私は、次の操作を行い、現時点では: Ltac project x y := let z := fresh in remember x as y eqn:z; clear z; clear x. しかし、私は次のエラーを取得する: remember (f x) as y eqn:H; clear H

    6

    1答えて

    自然数が決定的な総順序をサポートしているので、ascii型に決定可能な合計順序が誘導されます。 Coqでこれを表現する簡潔で慣用的な方法は何でしょうか? (タイプクラス、モジュールなどの有無にかかわらず)