3.1〜3.6 setoid equality によるrewrite (Lost in Manhattan)

Manhattan ProofCafe #69 2017_10_21 @suharahiromichi

A Gentle Introduction to Type Classes and Relations in Coq

本文3.1~3.6 Relations and rewriting の前半

Setoid equality による rewrte について説明します。サンプルコードの内容から、Lost in N.Y. または Lost in Manhattan とも呼ばれます。 


  1. サンプルコード
    • (公式) Lost_in_NY.v
    • (ProofCafe) https://github.com/suharahiromichi/coq/blob/master/gitcrc/coq_gitcrc_3_digest.v


  1. Coq RM
  • 8.6  Rewriting expressions    https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic117

        forall (x1:A1) … (xn:An)eq term1 term2. where eq is the Leibniz equality or a registered setoid equality.

        つまり、ふつうのrewrteタクティクで、setoid equalityの書き換えもできる。ただし、登録が必要である。

  • Chapter 27  Generalized rewriting     https://coq.inria.fr/refman/Reference-Manual030.html

     

  1. Setoid equality
        • Leibniz equality
eq_ind : forall (A : Type) (x : A) (P : A -> Prop), P x -> forall y : A, x = y -> P y
  • Setoid equality
同値関係(Equivalence Relation)の成立する等号を(好きなように)定義する。

  1. 説明
  • Instance eqn_Equiv : Equivalence eqn.
これを証明して登録すると、eqn x y であるゴールに対して、reflexivity, symmetry, transitivity タクティクが使えるようになる。

Equivalence は、eqn が、Reflexive、Symmetric、Transitive が満たすことをいう。

Coq RM Chapter 27. によると、Add Parametric Relation ... と同じである。

  • Instance f_Proper :  Proper (eq1 ==> eq2 ==> eq3 ... eqm ==> eqn) (f).

                            これを証明して登録すると、f_Porper は、f が eq1 .. eqn についてProperであるという。

Coq RM Chapter 27. によると、Add Parametric Morphism .. と同じである。

前提が、

H1 : eq1 x1 y1

H2 : eq2 x2 y2

H3 : eq3 x3 y3

...

Hm : eqm xm ym

のとき、ゴール

eqn (f x1 x2 x3 ... xm) (f y1 y2 y3 ... ym)

rewrite H1

によって、

eqn (f y1 x2 x3 ... xm) (f y1 y2 y3 ... ym)

に書き換えることができる。x2, x3, ... xm についても同様である。


  1. Setoid equality の使用例
  • Lost_in_NY.v

Instance cons_route_Proper (d : direction) : Proper (route_equiv ==> route_equiv) (cons d) .

route_equiv について cons d (consをカリー化したもの) は、Properである。

route_equiv (r =r= r') であるとは、r r' : routeの関係で、任意のP : Pointから同じPointにmoveすること。

(cons d) r は、r : route に、ひとつのd : distance を追加する。

前提が、

H : r =r= r'

のとき、ゴールが、

d :: r =r= d :: r'

のとき、

rewrite H

によって、

d :: r' =r= d :: r'

となる。


Instance move_Proper : Proper (route_equiv ==> route_equiv ==> route_equiv) (@app direction).

Instance app_route_Proper : Proper (route_equiv ==> @eq Point ==> @eq Point) move . 


  • Sorting/Permutation.v


 Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10.

 Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10.

 Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10.

 Proper (@Permutation A ==> @Permutation A) (@rev A) | 10.

 Proper (@Permutation A ==> Logic.eq) (@length A) | 10.

 Proper (@Permutation A ==> iff) (@NoDup A) | 10.

 Proper (@Permutation A ==> @Permutation B) (map f) | 10.


  • 圏論の例
可換であることeqv (===) は、合成 compositive (\\o)    に対して Proper である。 

Class Setoid : Type :=

  {

    carrier : Type;

    eqv : carrier -> carrier -> Prop;

    eqv_equivalence : Equivalence eqv

  }.

Coercion carrier : Setoid >-> Sortclass.

Notation "x === y" := (eqv x y).

Class Category `(Hom : Obj -> Obj -> Setoid) : Type :=

  {

    hom := Hom where "a ~> b" := (hom a b);

    obj := Obj;

    iid  : forall {a : Obj}, (a ~> a);

    comp : forall {a b c : Obj}, (b ~> c) -> (a ~> b) -> (a ~> c) where "f \\o g" := (comp f g);

    comp_respects   : forall {a b c : Obj}, Proper (eqv ==> eqv ==> eqv) (@comp a b c);

    left_identity   : forall `{f : a ~> b}, iid \\o f === f;

    right_identity  : forall `{f : a ~> b}, f \\o iid === f;

    associativity   : forall `{f : c ~> d} `{g : b ~> c} `{h : a ~> b}, f \\o g \\o h === f \\o (g \\o h)

}.

Coercion obj : Category >-> Sortclass.

圏をInstanceで定義するとき、comp_respects を証明する。



  1. Coqでの定義
  • Setoids/Setoid.v
  •         Classes/SetoidTactics.v
  •                 Classes/Morphisms.v                       Properの定義
  •                 Classes/RelationClass.v                    Equivalenceの定義
  •                 Classes/Equivalence.v


以上

Comments