Coq 8.7は一般的なSsreflectライブラリを統合しています。そのライブラリは、したがって、次のようにインポートすることができます。 From Coq Require Import ssreflect ssrfun ssrbool.
しかし、私はssrnatをインポートしようとすると、それはそれはUnable to locate library ssrnat with prefix C
f : x -> y -> zという定義があるとします。ここで、xは簡単に推測できます。 を使用してxに暗黙の引き数を設定することを選択しました。 は、次の例を考えてみましょう： Definition id : forall (S : Set), S -> S :=
fun S s => s.
Arguments id {_} s.
Check (id 1).
明らかにS = nat
2つの固定点定義を含む一見単純な補助定理に苦しんでいます。次の二つの軸方向カラーライブラリからの定義は以下のとおりです。 From Coq Require Import Vector Program.
Import VectorNotations.
Program Fixpoint Vnth {A:Type} {n} (v : t A n) : forall i, i < n -> A :=
a : nat
fvs : list nat
H : a = max (maxNum fvs) a + 1
H1 : max (maxNum fvs) a >= a
Doing rewrite H in H1.は、aの両方を置き換えますが、私はRHSのaを書き直したいだけです。それはできますか？私は上記の2つの仮説から虚偽を証明したい。
if a then b else cがmatch a with true => b | false => c endを表すチュートリアルを読んでいます。しかし、前者は非常に奇妙なことにaのタイプをチェックしませんが、後者はもちろんaがブール値であることを保証します。例えば、 Coq < Check if nil then 1 else 2.
if nil then 1 else 2
:
代数構造（たとえばすべてのモノイドのクラス）に対応するクラスを正式化しようとすると、必要なすべてのモデルをモデル化する製品タイプとしてmonoid (a:Type)タイプを作成するのが自然な設計です（要素e:a、オペレータapp : a -> a -> a、モノイド法が満たされていることの証明など）。その際、マップmonoid: Type -> Typeを作成しています。このアプローチの潜在的な欠
私はPosetsで事実を実装することで、COQを学びたいと思っています。私の最初の定理を証明しながら、私はここで立ち往生しています。 Class Poset {A: Type} (leq : A -> A -> Prop) : Prop := {
reflexivity: forall x y : A, x = y -> (leq x y);
antisymmetry: for