株式の取引と売買価格を決定する板寄せアルゴリズムをCoq/SSReflectで形式検証する

#はじめに
証券システムにおける株式の売買成立を決定するアルゴリズムの1つに「板寄せアルゴリズム」があります。
本記事ではこのアルゴリズムが正しい仕様を満たしているかどうかを形式検証ツールの１つであるCoq/SSReflectを用いて形式検証していきます。

※私はフィンテックが独学であるため、専門用語の言い回しなどが稚拙な箇所があるかもしれません。あらかじめご了承ください。

この記事は「[ある証券会社の証券用語の解説に仕様バグが存在することを形式検証によって発見した話](https://qiita.com/nekonibox/private/5a58a7476df7dbf69604)」の続きです。

ソースコードは[こちら](https://github.com/nekonistyle/opentrade/blob/main/opentrade.v)です。


#問題設定

まず本記事で仮定する株式の売買と板寄せアルゴリズムの仕様について定義します。

まず、板寄せアルゴリズムの入出力を定義するために「注文」と「約定」を定義します。

##注文

注文とは、**注文数**×**注文種別**×**{売り,買い}**×**注文者情報**である。

**注文数**は自然数であり、**注文種別**は**成行**または**指値**であり、**指値**の場合は、全順序集合`Price`の要素である**価格**を設定する。


----

実際の取引には他にも逆指値などがありますが、本記事ではシンプルに**成行**と**指値**のみを考えます。


##約定



- **[狭義]** 約定とは注文のペアであり、任意の約定(注文1、注文2)に対し、注文1が売り注文かつ注文2が買い注文であり、それぞれの注文数と価格が等しいことである。

- **[広義]** 約定とは注文のペアであり、任意の約定(注文1、注文2)に対し、注文1が売り注文かつ注文2が買い注文であり、それぞれの注文数が等しく、注文1の価格は注文2の価格に等しいかそれ以下であることである。

---

約定するということは、取引が成立するということです。
つまり、片方が売り注文、もう片方が買い注文であり、それぞれの注文数が等しく、[狭義]では2つの注文価格が一致すること、[広義]では売り注文の価格が買い注文の価格以下、すなわち証券所が損しないようになっていなければなりません。(ただし、基本的には成行注文の場合にも必ず価格がつくが、元々の注文が成行注文のみの場合、価格をつけようがないため、両者価格なしがありうることに注意)

基本的には[狭義]の定義を使いますが、のちに[広義]を使う例も紹介します。




##板寄せアルゴリズムの入出力

板寄せアルゴリズムの入出力は上で定義した注文と約定で定義されます。

入力：**注文**の列と任意で約定価格の初期値
出力：**約定**の列と約定価格、及び未約定注文の列

----

ここで任意入力としての約定価格の初期値を取っているのは、指値注文が存在しない場合の約定価格を設定するのに必要だからです。
基本的には、前営業日の終値を入れれば問題ないと思いますが、新規公開株など、前営業日の終値が存在しないものでも対応できるようになっています。
(実際の実装はどうなっているのか分からないので、間違っている可能性があります。fintechに詳しい方、教えていただけると幸いです。)


ただし、この入出力は以下で述べる仕様を満たさなければいけません。


#板寄せアルゴリズムの仕様

詳細は[前回の記事](https://qiita.com/nekonibox/private/5a58a7476df7dbf69604)をご覧ください。

これらの条件を全て満たすようなアルゴリズムを考えます。


#板寄せアルゴリズムの型

板寄せアルゴリズムを形式検証ツールの1つであるCoq/SSReflectで実装します。


##準備

板寄せアルゴリズムの型を定義するための準備をします。

```coq
  Variable priceType : eqType.
  Variable pricerel : rel priceType.
  Variable otherdataType : eqType.
  Variable timerel : rel otherdataType.

  Definition orderType : Type
    := nat * option priceType * otherdataType.
  Variable tobool : pred otherdataType.
  Notation is_bid := (fun x : orderType => tobool x.2).
  Notation share_of := (fun x : orderType => x.1.1).
  Notation price_of := (fun x : orderType => x.1.2).
  Notation otherdata_of := (fun x : orderType => x.2).

  Notation orderbookType := (seq orderType * seq orderType:Type).
```


価格の型を`priceType : eqType`、価格における全順序関係を`pricerel : rel priceType`とし、注文者情報の型を`otherdataType : eqType`とします。

また、(買い/売り)の情報は注文者情報の中に入れておき、それを取り出す関数`toBool : pred otherdataType`を定義します。
ここでは、`toBool x = true`のときに売り注文、`toBool x = false`のときに買い注文を表すことにします。

なぜ、(売り/買い)の情報をの値を独立にせずに注文者情報の型に含めたかというと、どちらも約定前の注文と約定後の注文とで値が変化しないためです。
例えば、100株の買い注文をしたとしてもその全てが約定するとは限らず、50株だけで約定するかもしれないので、注文数が変化する可能性があり、成行注文が約定すると価格もつくので価格も変化します。しかしながら、(売り/買い)を変えてはいけないので、それならば注文者情報`otherdataType`にまとめてしまってよいと考えられるからです。

さらに、注文の型`orderType := nat * option priceType * otherdataType`とし、
第一引数が**注文数**、第二引数が**注文種別**、第三引数が**(売り/買い)**と**注文者情報**を表しています。
特に、**注文種別**は`option priceType`型であり、成行を`None`、価格`x`の指値を`Some x`で表します。

また、「時間優先の原理」を保つための関係`timerel : rel otherdataType`を定義しています。これは証明において特に使用しませんが、実装の上では注文時間でもソートされていることも想定しています。


これらを用いて、板寄せアルゴリズム`opentrade`の型を以下に定義します。

```coq
Check opentrade.
(*
opentrade
     : option priceType ->
       seq orderType * seq orderType ->
       option priceType * seq (orderType * orderType) * (seq orderType * seq orderType)
*)
```

第一引数が約定価格の初期値、第二引数が売り注文の列と売り注文の列を表しています。
返り値の１つ目が約定価格、２つ目が約定した注文、３つ目が未約定注文を表しています。

約定価格の初期値および約定価格は**注文種別**と同じ`option priceType`で表し、価格がつかないことを**成行**と同一視します。このように定義するとのちの計算が簡単になります。

これに対して、板寄せアルゴリズムの仕様を定義していきます。


#板寄せアルゴリズムの仕様の記述

上で定義した仕様をCoqで記述するのですが、その前にある`option`型に関する二項関係を定義します。

##準備

以下の関数を定義します。

```coq
  Definition orel T (R:rel T) : rel (option T) :=
    fun x y => match x, y with
               | None, _ => true
               | Some _, None => false
               | Some a, Some b => R a b
               end.
```

これは、型`T`と`T`上の二項関係`R`に対し、新たに最小元`None`を追加した二項関係`orel R : rel (option T)`を表しています。

これを何に使うかというと、成行と指値を同じ関数で比較するのに使います。

実は**成行はただの指値全体の集合に追加した最小元そのもの**だと考えることができます。具体的には、成行売り注文は無限小での指値、成行買い注文は無限大の指値だと考えると、板寄せアルゴリズムの処理する順番に一致します。（ただし、約定する価格に関しては別に考える必要があります）
また、本当に成行と指値を区別しなくてもいいのかどうかは、全体のアルゴリズムが仕様を満たすことを示すことによって間接的に示せます。言い換えれば、「仕様を満たす関数」であればその実装は問わないという考え方です。
今回定義する板寄せアルゴリズムは全ての仕様を満たすので、本記事の記事の実装では成行と指値を同一視します。


具体的に、成行と指値を同時に比較するような二項関係は以下のように定義します。

```coq
  Definition opricerel (mode:bool) : rel (option priceType) :=
    (orel (fun x y => if mode then pricerel x y else pricerel y x)).
```

注文種別上の順序`opricerel`は成行注文が最小元になるような価格における順序を表していていて、引数`mode`が売り注文であるかどうかを表す引数です。
具体的には、価格が実数の場合、成行注文は売り注文の場合は無限小の価格、買い注文の場合は無限大の価格を提示しているのと同じ扱いになります。(約定後の価格はもちろん無限小や無限大にならないようにしなければいけません。)


これを用いて、以下に板寄せアルゴリズムの仕様をCoq/SSReflectで実装していきます。

##仕様の記述

まず、そもそも板寄せアルゴリズムの返り値が約定の条件を満たしていることを保証するための命題を示します。

###返り値が約定であること

>- 約定とは注文のペアであり、任意の約定(注文1、注文2)に対し、それぞれの注文数と価格が等しく、注文1が売り注文かつ注文2が買い注文である。

```coq
  Variable (ple : rel priceType).
  Hypothesis (ple_refl : reflexive ple).
  (* ple x y := x == y or, opricerel x y *)

  Definition ople : rel (option priceType) :=
    fun x y => match x, y with
               | None, None => true
               | Some a, Some b => ple a b
               | _, _ => false
               end.

  Definition contract_valid (contracts:seq (orderType * orderType)) :=
    all (fun contract =>
           [&& is_bid contract.1, ~~ is_bid contract.2,
           share_of contract.1 == share_of contract.2 &
           ople (price_of contract.1) (price_of contract.2)]) contracts.
```

`contract_valid contracts`が注文のペアの列`contracts`が全て約定であることを表した命題で、注文のペア`contract`に対し、注文1が`contract.1`、注文2が`contract.2`を表します。
`is_bid contract.1`と`~~ is_bid contract.2`でそれぞれがちゃんと売り注文と買い注文であることを表し、その注文数`share_of`が等しく、`ople x y := x == y`のとき、価格が等しいことを表しています。

ここで変数`ople`が`==`のとき、[狭義]の定義になり、`ople`が`opricerel`のとき、[広義]になります。
また、どちらも反射律を満たすため`reflexive ple`が仮定されています。


###条件1

>- **[条件1]** **未約定(売り/買い)注文が存在するならば、**未約定(買い/売り)注文は全て指値である。

```coq
  Definition traderesult_valid1
             (result:
                option priceType * seq (orderType * orderType) * orderbookType)
    :=
    let book := result.2 in
    (book.2 <> [::] -> all (isSome \o price_of) book.1) /\
    (book.1 <> [::] -> all (isSome \o price_of) book.2).
```

`traderesult_valid1 result`が条件1を表した命題で、`result`が板寄せアルゴリズムの返り値のとき、`book := result.2`が未約定注文を表しています。
このとき、`book.1`が未約定の売り注文であり、`book.2`が未約定の買い注文を表します。
また、`isSome \o price_of : pred orderType`が注文が指値注文であることを表す述語になっていて、例えば、`(book.2 <> [::] -> all (isSome \o price_of) book.1)`は
未約定売り注文が存在するならば未約定買い注文は全て指値であることを表しています。


###条件2

>- **[条件2]** 約定値段が存在するならば、全ての**指値の**未約定(売り/買い)注文の価格は約定値段より(高い/低い)。

```coq
  Definition traderesult_valid2
             (result:
                option priceType * seq (orderType * orderType) * orderbookType)
    :=
    let price := result.1.1 in
    let book  := result.2 in
    all (fun x => price_of x ==> opricerel true price (price_of x)) book.1 &&
    all (fun x => price_of x ==> opricerel false price (price_of x)) book.2.
```

`traderesult_valid2 result`が条件2を表した命題で、`result`が板寄せアルゴリズムの返り値のとき、`price := result.1.1`が約定価格、`book := result.2`が未約定注文を表しています。
`fun x => price_of x ==> opricerel b price (price_of x)`とありますが、
`price_of x`は`isSome (price_of x)`の省略であり、`x`が指値であることを仮定しています。
このとき`b = true`のとき、`orel pricerel price (price_of x)`つまり`x`の価格が約定価格より高いこと、`b = false`のときは`x`の価格が約定価格より安いことを意味しています。


###条件3

>- **[条件3]** **約定値段が存在するならば、**未約定の売り注文か買い注文のうちどちらか全ての指値価格は約定価格と異なる。

```coq
  Definition traderesult_valid3
             (result:
                option priceType * seq (orderType * orderType) * orderbookType)
    :=
    let price := result.1.1 in
    let book  := result.2 in
    price ->
    all (fun x => price_of x != price) book.2 \/
    all (fun x => price_of x != price) book.1.
```

`traderesult_valid3 result`が条件3を表した命題で、条件2と同様に、`result`が板寄せアルゴリズムの返り値のとき、`price := result.1.1`が約定価格、`book := result.2`が未約定注文を表しています。
このとき、未約定の売り注文`book.1`か買い注文`book.2`のどちらか全ての価格が約定価格`price`と異なることを表しています。


###約定価格の存在性

>- **[約定価格の存在性]** 約定価格が存在することは以下のどちらかが成り立つことと同値である。
  + 約定価格の初期値が設定されていること。
  + 指値注文が存在すること。

```coq
  Lemma deals_price_isSomeP
        (price:option priceType) (book:orderbookType) :
    reflect
      [\/ isSome price,
       has (isSome \o price_of) book.1 |
       has (isSome \o price_of) book.2]
      (isSome (opentrade price book).1.1).
```
`deals_price_isSomeP price book`が板寄せアルゴリズムの入力である、価格の初期値`price`で注文が`book`であったときの約定価格の存在性を示した補題で、`reflect`を用いて同値性を表しています。
具体的には、約定価格`(opentrade price book).1.1`が存在する`isSome`ことと
約定価格の初期値`price`が存在するか、売り注文`book.1`か買い注文`book.2`の中に指値注文が存在する`has (isSome \o price_of)`ことの同値性を表しています。


###約定の健全性

>- **[約定の健全性1]** 任意の注文者情報に対し、その注文者情報を持つ(売り/買い)注文の注文数の合計と、その注文者情報を持つ約定した(売り/買い)注文及び未約定の(売り/買い)注文の注文数の合計が一致する。

```coq
  Definition contract_valid1_def (usr:otherdataType) (mode:bool)
             (book contracts rbook:seq orderType) :=
      let order := head (0,None,usr) [seq x <- book | otherdata_of x == usr] in
      let rorder :=
          head (0,None,usr) [seq x <- rbook | otherdata_of x == usr] in
      share_of order =
      share_of rorder +
      \sum_(x <- contracts | otherdata_of x == usr) share_of x.

  Definition contract_valid1 (book:orderbookType)
             (result:option priceType * seq (orderType * orderType)
                     * orderbookType) :=
    forall usr : otherdataType,
      let mode := tobool usr in
      if mode
      then contract_valid2_def
             usr mode book.1 [seq x.1 | x <- result.1.2] result.2.1
      else contract_valid2_def
             usr mode book.2 [seq x.2 | x <- result.1.2] result.2.2.
```

`contract_valid1 book result`が健全性1を表していて、
`book`が約定前注文の列、`result`が板寄せアルゴリズムの返り値であるとき、
任意の注文者情報`usr`に対し、それが売り注文`tobool usr = true`であるか買い注文`tobool usr = false`であるかで場合分けします。
それぞれの場合に対して、`contract_valid1_def`で定義される命題で具体的な条件を表します。

`contract_valid1_def usr mode book contracts rbook`の引数はそれぞれ、
`usr`が注文者情報、`mode`が(売り/買い)、`book`が取引前の(売り/買い)注文の列、`contrancs`が約定した(売り/買い)注文、`rbook`が未約定の(売り/買い)注文の列を表します。
このとき、`order`と`rorder`がそれぞれ注文者情報`usr`を含む取引前と未約定の注文で、存在しなければ`(0,None,usr)`となります。
同じ注文者情報の注文が複数ある場合がありますが、後に一意性を仮定するため、ここでは`head`関数を使って取り出しています。
このとき、取引前の注文数`share_of order`が未約定の注文数`share_of rorder`と約定した注文数の合計`\sum_(x <- contracts | otherdata_of x == usr) share_of x`の和が等しいことを表しています。


>- **[約定の健全性2]** 任意の注文者情報に対し、その注文者情報を持つ指値(売り/買い)注文が存在し、等しい注文者情報を持つ約定した(売り/買い)注文が存在する場合、その価格は元の注文の価格より(高い/安い)。

```coq
  Definition contract_valid2_def (usr:otherdataType) (mode:bool)
             (book contracts rbook:seq orderType) :=
      let order := head (0,None,usr) [seq x <- book | otherdata_of x == usr] in
      all (opricerel mode (price_of order) \o price_of)
　　　　　　[seq x <- contracts | otherdata_of x == usr].

  Definition contract_valid2 (book:orderbookType)
             (result:option priceType * seq (orderType * orderType)
                     * orderbookType) :=
    forall usr : otherdataType,
      let mode := tobool usr in
      if mode
      then contract_valid2_def
             usr mode book.1 [seq x.1 | x <- result.1.2] result.2.1
      else contract_valid2_def
             usr mode book.2 [seq x.2 | x <- result.1.2] result.2.2.
```

`contract_valid2`が健全性2を表した命題で、記述の仕方は健全性1とほぼ同じで、売り注文と買い注文の場合でそれぞれ`contract_valid2_def`を使って定義し、`contract_valid2_def`の引数も`contract_valid1_def`のときと同じです。
違うのは命題の中身で、約定した列のうち、注文者情報が`usr`のものに対して、全て`opricerel mode (price_of other) \o price_of`であることを主張していて、
これは、`mode = true`つまり売り注文の場合は元の注文`order`の価格より高い価格で約定したこと、`mode = false`つまり買い注文の場合は元の価格より安い価格で約定したことを表しています。
つまり損をしていないことを表しているということです。


#板寄せアルゴリズムの実装

板寄せアルゴリズムを実装していきます。
基本的には、こちらの[楽天証券/現物取引 取引ルール/板寄せ](https://www.rakuten-sec.co.jp/smartphone/domestic/stock/rule/agreed/itayose.html)を参考に定義するのですが、このサイトでは細かい実装が見えてこないのと、Coqでは停止性が示せるような実装にする必要があるため、多少異なるものになります。

具体的に板寄せアルゴリズム`opentrade`の実装を見ていきます。


##実装の考え方

参考元のアルゴリズムでは、まず

>売りと買いの注文が交錯した状態からまずは始値を仮定する

とあります。
しかし、これは取引実行関数が停止する条件と一致するので取引実行関数と分ける必要がなく、「取引実行関数において、先に再帰呼び出しして停止したときの返り値を取引価格として、その価格で約定する」というアルゴリズムにすれば取引と同時に計算できます。

また、次に

>売り成行注文と買い成行注文を約定させる

>500円より高い買いの指値注文と500円より低い売りの指値注文を約定させる

(500円は始値)

とあります。
しかしながら、**売り成行注文は最小元の指値**、**買い成行注文は最大元の指値**という扱いにすれば、成行と指値注文を区別する必要がありません。(ただし約定する価格にだけは注意する必要がある)

また、**各約定における約定価格をいくらに設定すればいいのか詳細の記載がない**ため、いくつか考えられるパタンを考えてみます。

例えば、始値500円のとき497円の売り注文と501円の買い注文が約定した場合、

- 売り注文の価格(497円)または買い注文の価格(501円)に統一する。
- それぞれの注文の平均価格(499円)に統一する。
- 始値(500円)に統一する。
- それぞれ注文した元の価格のまま約定する。このとき4円差額が発生するが、これを証券会社の収益にする。(※ただし約定価格が異なるため、[広義]の約定になる)

などが考えられ、どのパタンも

>- **[約定の健全性2]** 任意の注文者情報に対し、その注文者情報を持つ指値(売り/買い)注文が存在し、等しい注文者情報を持つ約定した(売り/買い)注文が存在する場合、その価格は元の注文の価格より(高い/安い)。

を満たします。

本記事では、注文の価格`x y : priceType`が約定したときの価格`priceop x y`を返す関数`priceop:priceType -> priceType -> priceType`を考え、
健全性2を満たす条件を探して仮定します。

最後に

>約定値段の売りまたは買い注文のいずれかがすべて約定する状態にする

を満たすように停止条件を定義すれば完成です。


##満たすべき漸化式

板寄せアルゴリズム`opentrade`が満たすべき漸化式は以下になります。

```coq
  Lemma opentrade_equation
        (price:option priceType) (book:orderbookType) : 
        opentrade price book =
  if book.1 is xa :: sa
  then
    if book.2 is xb :: sb
    then
      if check_price xa xb
      then
        if share_of xa == share_of xb
        then
          let result :=
              opentrade (deal_price price xa xb) (sa, sb) in
                (result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
        else
          if share_of xa > share_of xb
          then
            let result :=
                opentrade
                  (deal_price price xa xb)
                  ((share_of xa - share_of xb,
                    price_of xa, otherdata_of xa) :: sa, sb) in
            (result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
          else
            let result :=
                opentrade
                  (deal_price price xb xa)
                  (sa,
                   (share_of xb - share_of xa,
                    price_of xb, otherdata_of xb) :: sb) in
            (result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
      else
        (price_of xa, [::], book)
    else
      (head_price price book.1, [::], book)
  else
    (head_price price book.2, [::], book).
  Proof.
      by case : book =>[[|xa sa][|xb sb]].
  Qed.
```

ただし、

```coq
  Definition oop (T:Type) (op:T -> T -> T) (x y:option T) : option T :=
    match x,y with
    | None, _ => y
    | _, None => x
    | Some x', Some y' => Some (op x' y')
    end.

  Definition check_price : rel orderType :=
    fun x y =>
      match price_of x, price_of y with
      | Some x', Some y' => pricerel x' y'
      | _, _ => true
      end.

  Variable (priceop:priceType -> priceType -> priceType).

  Definition deal_price
             (default:option priceType) (x y:orderType) : option priceType :=
    let xy := oop priceop (price_of x) (price_of y) in
    if isSome xy then xy else default.
```

まず、約定価格の初期値`price`、注文が`book`で、特に売り注文の列が`book.1`、買い注文の列が`book.1`です。
このとき、`book.1`と`book.2`が価格に対してソートされて、(売り/買い)注文の列の先頭要素が最も価格の(安い/高い)と仮定します。
それぞれ先頭要素`xa`と`xb`を取り出し、停止条件`check_price xa xb`を見て、もし売り注文の価格の方が買い注文より安かったら約定させます。
具体的には、注文数が少ない方に合わせてその注文数だけ約定して再帰します。(実際には、始値を計算するために再帰してから約定します)

このように定義すれば、板寄せアルゴリズムが定義できます。

しかしながら、停止性が自明ではなく、Coqではそのまま定義できません。
そこで、Coqでは以下のように定義します。


###停止性を示すための実装

上の漸化式における再帰呼び出しでは売り注文と買い注文の列の長さのどちらか一方が必ず短くなっています。言い換えれば、辞書式順序で引数の長さが短くなっていると言えます。
そこで、「[Coq/SSReflectで辞書式順序で引数が構造的に小さくなる関数をFixpointで定義する](https://qiita.com/nekonibox/items/3d483edf4eb46adbfae7)」を応用して定義します。

```coq
  Fixpoint opentrade_rec
           (price:option priceType) (a:seq orderType) (b:seq orderType) :
    option priceType * seq (orderType * orderType) * orderbookType :=
    if a is xa :: sa
    then
      let fix recf (price:option priceType) (xa:orderType) (b:seq orderType) :
            option priceType * seq (orderType * orderType) * orderbookType :=
          if b is xb :: sb
          then
            if check_price xa xb
            then
              if share_of xa == share_of xb
              then
                let result :=
                    opentrade_rec (deal_price price xa xb) sa sb in
                (result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
              else
                if share_of xa > share_of xb
                then
                  let result :=
                      recf
                        (deal_price price xa xb)
                        (share_of xa - share_of xb,
                         price_of xa, otherdata_of xa) sb in
                  (result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
                else
                  let result :=
                      opentrade_rec
                        (deal_price price xb xa) sa
                        ((share_of xb - share_of xa,
                          price_of xb, otherdata_of xb) :: sb) in
                  (result.1.1, deals result.1.1 xa xb :: result.1.2, result.2)
            else
              (price_of xa, [::], (xa :: sa, b))
          else
            (head_price price (xa :: sa), [::], (xa :: sa, b))
      in recf price xa b
    else
      (head_price price b, [::], (a, b)).

  Definition opentrade (price:option priceType) (book:orderbookType)
    := opentrade_rec price book.1 book.2.
```

また、証明に使用するための帰納原理`opentrade_ind`と漸化式を満たすことの補題`opentrade_equation`(既に上に記載しています)も証明します。

```coq
  Lemma opentrade_ind
        (P:option priceType -> seq orderType -> seq orderType -> Prop) :
    (forall price b, P price [::] b) ->
    (forall price xa sa, P price (xa :: sa) [::]) ->
    (forall price xa sa xb sb,
        check_price xa xb -> share_of xa == share_of xb ->
        P (deal_price price xa xb) sa sb -> P price (xa :: sa) (xb :: sb)) ->
    (forall price xa sa xb sb,
        check_price xa xb -> share_of xa == share_of xb = false ->
        share_of xa > share_of xb ->
        P (deal_price price xa xb)
          ((share_of xa - share_of xb, price_of xa, otherdata_of xa) :: sa)
          sb -> P price (xa :: sa) (xb :: sb)) ->
    (forall price xa sa xb sb,
        check_price xa xb -> share_of xa == share_of xb = false ->
        share_of xa > share_of xb = false ->
        share_of xa < share_of xb ->
        P (deal_price price xb xa) sa
          ((share_of xb - share_of xa, price_of xb, otherdata_of xb) :: sb) ->
        P price (xa :: sa) (xb :: sb)) ->
    (forall price xa sa xb sb,
        check_price xa xb = false ->
        P price (xa :: sa) (xb :: sb)) ->
    forall price a b, P price a b.
```

4つ目と5つ目の仮定には`share_of xa == share_of xb = false`と`share_of xa > share_of xb`などが同時に存在し、冗長に見える部分があります。
しかしながら、帰納法を適用したときに`opentrade_equation`を使うと、if文の分岐条件に`share_of xa == share_of xb`が登場するため、場合分けしなくてもそのまま代入できるように、あえてこのように記述しています。


#板寄せアルゴリズムの入力が満たすべき仮定

上記のアルゴリズムは任意の入力に対しては仕様を満たしません。
そこで、入力が満たすべき性質を記述します。

```coq
  Definition seq_order_valid (mode:bool) : pred (seq orderType) :=
    fun book => [&& sorted (orderrel mode) book,
                 uniq [seq otherdata_of order | order <- book] &
                 all (fun k => is_bid k == mode) book].

  Definition orderbook_valid : pred orderbookType :=
    fun book => seq_order_valid true book.1 && seq_order_valid false book.2.
```

ただし

```coq
  Definition argrel (S T:Type) (f:S -> T) (R:rel T) : rel S :=
    fun x y => R (f x) (f y).

  Definition lexi : (T:eqType) (S:Type) (R:rel T) (S:rel S) : rel (T * S) :=
    fun x y => (x.1 == y.1) && Q x.2 y.2 || strict R x.1 y.1.

  Definition orderrel (mode:bool) : rel orderType :=
    argrel (fun x => (price_of x, otherdata_of x))
           (lexi (opricerel mode) timerel).
```

これが何を表しているかというと、
入力の(売り/買い)注文の列がちゃんと(売り/買い)注文のみからなる列であり、価格に対して(昇順/降順)にソートされていてかつ、注文者情報が全て異なっているということです。
(価格に対する順序は実際には(価格,注文時刻)に対する辞書式順序`lexi`で定義されています。)

価格のソートは板寄せアルゴリズムを成り立たせるための仮定であり、注文者情報の一意性は約定の健全性の証明に必要です。

これを仮定して、仕様を満たすことを証明していきます。


#仕様を満たすことを証明する

基本的には上で定義した帰納原理`opentrade_ind`を使って示します。

具体的な証明はソースにありますが、長くなるので命題だけ示します。

###返り値が約定であること

```coq
  Hypothesis (priceop_ple:
                forall x y, pricerel x y -> ple (priceop x y) (priceop y x)).

  Lemma opentrade_contract_valid (price:option priceType) (book:orderbookType):
    orderbook_valid book -> contract_valid (opentrade price book).1.2.
```

`priceop`に関する仮定として`proceop_ple`が必要です。この条件は上記の「約定価格を決定する関数」で紹介した全ての関数で満たします。


###条件1

```coq
  Theorem opentrade_valid1 (price:option priceType) (book:orderbookType) :
    orderbook_valid book -> traderesult_valid1 (opentrade price book).
  Proof.
```

###条件2

```coq
  Theorem opentrade_valid2 (price:option priceType) (book:orderbookType) :
    orderbook_valid book -> traderesult_valid2 (opentrade price book).
```

###条件3

```coq
  Theorem opentrade_valid3 (price:option priceType) (book:orderbookType) :
    orderbook_valid book -> traderesult_valid3 (opentrade price book).
```

###約定価格の存在性

```coq
  Lemma deals_price_isSomeP
        (price:option priceType) (book:orderbookType) :
    reflect
      [\/ isSome price,
       has (isSome \o price_of) book.1 |
       has (isSome \o price_of) book.2]
      (isSome (opentrade price book).1.1).
```

任意の入力に対し、板寄せアルゴリズムの返り値の約定価格がこれを満たすことを証明できます。


###約定の健全性1

```coq
  Lemma opentrade_contract_valid1
        (price:option priceType) (book:orderbookType) :
    orderbook_valid book -> contract_valid1 book (opentrade price book).
```

###約定の健全性2

```coq
  Hypothesis (pricerel_opl :
                forall x y, pricerel x y -> pricerel x (priceop x y)).
  Hypothesis (pricerel_opr :
                forall x y, pricerel x y -> pricerel (priceop y x) y).

  Lemma openorder_contract_valid2
        (price:option priceType) (book:orderbookType) :
    orderbook_valid book -> contract_valid2 book (opentrade price book).
```

`priceop`に関する仮定として`proceop_opl`および`priceop_opr`が必要です。この条件も上記の「約定価格を決定する関数」で紹介した全ての関数で満たします。


#まとめ

板寄せアルゴリズムをCoq/SSReflectで形式検証しました。

異なる指値価格の注文を約定させる関数によって、仕様を満たす複数の板寄せアルゴリズムが存在することも分かりました。