0

そこで、Coq を学習しながら、ゲームの紙、はさみ、ロックを使った簡単な例を作成しました。データ型を定義しました。

Inductive PSR : Set := paper | scissor | rock.

そして3つの機能：

Definition me (elem: PSR) : PSR := elem.

Definition beats (elem: PSR) : PSR :=
 match elem with
  | paper => scissor
  | rock => paper
  | scissor => rock
 end.

Definition beatenBy (elem: PSR) : PSR :=
 match elem with
  | paper => rock
  | rock => scissor
  | scissor => paper
 end.

コンポジションも定義します (ただし、これは標準ライブラリのどこかにあるはずです)。

Definition compose {A B C} (g : B -> C) (f : A -> B) : (A -> C) :=
  fun x : A => g (f x).

ここで説明されているように、クラスのモノイドを実装します

Class Monoid {A : Type} (dot : A -> A -> A) (unit : A) : Type := {
 dot_assoc : forall x y z:A,
  dot x (dot y z)= dot (dot x y) z;
 unit_left : forall x,
  dot unit x = x;
 unit_right : forall x,
  dot x unit = x 
}.

asとasPSRの下でモノイドを形成できることをついに証明することができましたcompose+me1 

Instance MSPR : Monoid compose me.
 split.
 intros. reflexivity.
 intros. reflexivity.
 intros. reflexivity.
 Qed.

質問

Instance MSPR : Monoid compose me.申請するだけで仕事introsの証明ができるのはなぜreflexivityですか？正直なところ、私は自分が何をしていたかを知っていましたが、split次のようなものを得た後introsintros

3 subgoal
x : PSR -> PSR
y : PSR -> PSR
z : PSR -> PSR
______________________________________(1/3)
compose x (compose y z) = compose (compose x y) z

試しapply compose.ましたが、うまくいきませんでした。魔法reflexivity.のように解決しましたが、理由はわかりません。

サイドノート

このように力を定義すると、これは素晴らしく機能しました

Fixpoint power {A dot one} {M : @Monoid A dot one}(a:A)(n:nat) :=
 match n with 0 % nat => one
  | S p => dot a (power a p)
 end.

その後、Compute (power beats 2) paper.利回り

= rock
     : PSR

これをしたのはbeats (beats paper) = beats scissor = rock!!!

4

2 に答える 2

2

Coq の再帰性の原則は、予想どおり、単なる構文上の等価性よりも強力です。大まかに言えば、Coq は同じ値に単純化できる任意の 2 つのものを等しいと見なします。ここでの単純化は、たとえば、代数法則に従って式を操作することが許可されている代数よりも、わずかに制限的な意味で解釈されます。代わりに、Coq には、プログラムの計算方法を記述する計算規則の固定セットが付属しています。あなたの例では、式を単純化すると

compose x (fun a => y (z a)) = compose (fun a => x (y a)) z
fun a => x (y (z a)) = fun a => x (y (z a))

ここで、"fun" は無名関数、つまり名前のない関数に対する Coq の表記法です。これら 2 つのことは等しいので、再帰性で十分です。同じ考え方が他の目標にも当てはまります。

于 2014-06-26T08:21:57.490 に答える
1

の後で、 Coq に定義のみを展開するように依頼するintrosことができます。同等性の両側が構文的に同じであることがわかり、目標を解決することができます (定義を「見る」ことができます)。unfold composecomposereflexivityreflexivity

問題は残ります:なぜそれらは同じなのですか:それについてはアーサーの答えを参照してください;)

V.

于 2014-06-26T08:24:09.193 に答える