0

所以在学习 Coq 时，我用游戏纸、剪刀、石头做了一个简单的例子。我定义了一个数据类型。

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

以及三个功能：

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并且intros知道我在做什么，但是在intros我得到类似的东西之后

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 认为任何两个可以简化为相同值的事物都是相等的。此处的简化比在代数中的限制要稍微严格一些，例如，在代数中，允许根据代数定律来操作公式。相反，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 对匿名函数的表示法，即没有名称的函数。由于这两个东西是相等的，所以自反性就足够了。同样的想法也适用于其他目标。

于 2014-06-26T08:21:57.490 回答
1

之后intros，您可以unfold compose要求 Coq 仅展开compose定义，您会看到等式的两边在语法上是相同的，从而reflexivity设法解决您的目标（reflexivity可以通过定义“看到”）。

问题仍然存在：为什么它们相同：请参阅亚瑟的答案；）

五。

于 2014-06-26T08:24:09.193 回答