Proof of Paper, Scissor, Rock как экземпляр моноида в Coq

Итак, изучая 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 
}.

Наконец-то мне удалось доказать, что можно PSR формировать моноид под compose как + и me как 1

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 !!!


monoids coq proof
person Cristian Garcia    schedule 26.06.2014    source источник
comment
me — функция тождества; вы доказали, что функциональное пространство PSR -> PSR является моноидом с compose в качестве двоичной операции и id в качестве единицы. Это верно для любого набора эндоморфизмов. Ваши доказательства работают рефлексивно, потому что композиция функций ассоциативна (попробуйте использовать unfold compose и посмотрите, что произойдет).   -  person gallais    schedule 26.06.2014

Ответы (2)


arrow_upward
2
arrow_downward

Как можно было ожидать, принцип рефлексивности в 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))

Где «веселье» - это нотация Кока для анонимной функции, т.е. функция без имени. Поскольку эти две вещи равны, рефлексивности достаточно. Та же идея применима и к другим целям.

person Arthur Azevedo De Amorim    schedule 26.06.2014

arrow_upward
1
arrow_downward

После intros вы можете сделать unfold compose, чтобы попросить Coq развернуть только compose определение, вы увидите, что обе стороны равенства синтаксически одинаковы, таким образом, reflexivity удается решить вашу цель (reflexivity может «видеть» сквозь определения).

Остается вопрос: почему они одинаковы: см. ответ Артура на этот вопрос;)

V.

person Vinz    schedule 26.06.2014