天泣記

2023-03-01 (Wed)

#1 Coq/SSReflect で bool 変数ひとつの命題を b または ~~b に変形する方法

Coq/SSReflect で、bool 型の変数 b があったとき、b が true である、および、b が false である、 という命題の書き方はたくさんある

b は true であるという命題
* b                 実は is_true b
* b = true          is_true b を展開するとこれになるので、is_true b と convertible
* true = b
* b == true         is_true (b == true)
* true == b         is_true (true == b) で、じつは b と convertible
* b <> false        not (b = false)
* false <> b        not (false = b)
* ~(b == false)     not (is_true (b == false))
* ~(false == b)     not (is_true (false == b)) で、じつは ~(~~b) と convertible
* ~(~~b)            not (is_true (negb b))
* b != false        is_true (negb (b == false))
* false != b        is_true (negb (false == b)) で、じつは ~~(~~b) と convertible
* ~~b = false       negb b = false
* false = ~~b       false = negb b
* ~~b == false      is_true (negb b == false)
* false == ~~b      is_true (false == negb b) で、じつは ~~(~~b) と convertible

b は false であるという命題
* ~~b               is_true (negb b) で、mathcomp としてはこれがおすすめの表現
* ~b                not (is_true b) で、not を展開すると is_true b -> False になる
* b = false
* false = b
* b == false        is_true (b == false)
* false == b        is_true (false == b) で、じつは ~~b と convertible
* b <> true         not (b = true)
* true <> b         not (true = b)
* ~(b == true)      not (is_true (b == true))
* ~(true == b)      not (is_true (true == b)) で、じつは ~b と convertible
* b != true         is_true (negb (b == true))
* true != b         is_true (negb (true == b)) で、じつは ~~b と convertible
* ~~b = true        negb b = true
* true = ~~b        true = negb b
* ~~b == true       is_true (negb b == true)
* true == ~~b       is_true (true == negb b) で、じつは ~~b と convertible

さらにいえば、b1 = b2 は @eq bool b1 b2 であり、 b1 == b2 は @eq_op bool_eqType b1 b2 なのだが、ここでは bool しか扱わないので そこまでの展開は気にしないことにしよう。

このようにたくさんバリエーションがあると気がそがれるので、 統一された単純な形になっているのが望ましい。

また、b という形 (と b = true という形) は、その証明を、b を true に書き換えるために使えるので便利である。 同様に、b = false も書き換えに使えて便利である。

あと、いろいろな補題で、b の真偽が前提に必要な場合、形がばらばらだと (あと convertible でなければ)、その前提を満たすためにいちいち変換してやる必要がある

というわけで、真偽それぞれにおすすめの形がある。

真の場合は、まぁ、b とだけ書くのがいいのだろう、たぶん。 短いし。

偽の場合には ~~b がおすすめの表現であることは ssrbool.v に書いてある。 <URL:https://github.com/coq/coq/blob/V8.16.1/theories/ssr/ssrbool.v#L499-L502>

なお、~~b の証明 H があったとき、H は (そのままでは) b を false に書き換えるのには使えない。 b を false に書き換えたければ、rewrite (negbTE H) とすればよい。

というわけで、b の真偽を示す命題がいろいろな形で出てきたときに、標準的な形として b と ~~b という形に変形することが多々あるのだが、 あまりにたくさんの形があるので、どうやったらできるのか、いつも試行錯誤している気がする。

そこで、一念発起して真面目に考えようと思って、上に書いたのを変形してみた

真の場合            ゴールの先頭にある前提                          ゴール全体
* b                 これがおすすめの表現
* b = true          move/idP.                                       apply/idP.
* true = b          move/esym/idP.                                  apply/esym/idP.
* b == true         rewrite eqb_id.
                    move/eqP/idP.                                   apply/eqP/idP.
* true == b         rewrite -[true == b]/b.
                    move/eqP/esym/idP.                              apply/eqP/esym/idP.
                    rewrite eq_sym eqb_id.
* b <> false        move/eqP; rewrite negb_eqb addbF.               apply/eqP; rewrite negb_eqb addbF.
                    move/eqP; rewrite eqbF_neg negbK.
* false <> b        move/eqP; rewrite negbK.
                    move/eqP; rewrite negb_eqb addFb.               apply/eqP; rewrite negb_eqb addFb.
* ~(b == false)     move/negP; rewrite negb_eqb addbF.              apply/negP; rewrite negb_eqb addbF.
                    move/negP; rewrite eqbF_neg negbK.
* ~(false == b)     move/negP/negPn.                                apply/negP/negPn.
                    move/negP/negbNE.
                    move/negP; rewrite negbK.
                    move/negP; rewrite negb_eqb addFb.              apply/negP; rewrite negb_eqb addFb.
* ~(~~b)            move/negP/negbPn.                               apply/negP/negPn.
                    move/negP/negbNE.
                    move/negP; rewrite negbK.                       apply/negP; rewrite negbK.
* b != false        rewrite eq_sym negbK.
                    rewrite eq_sym => /negbNE.
                    rewrite negb_eqb addbF.                         同左
                    rewrite eqbF_neg negbK.
* false != b        move/negPn.                                     apply/negPn.
                    move/negbNE.
                    rewrite negb_eqb addFb.                         同左
* ~~b = false       move/negbFE.                                    apply/negbF.
* false = ~~b       move/esym/negbFE.                               apply/esym/negbF.
* ~~b == false      move/eqP/negbFE.                                apply/eqP/negbF.
* false == ~~b      move/eqP/esym/negbFE.                           apply/eqP/esym/negbF.
                      rewrite [false == _]negbK.

偽の場合            ゴールの先頭にある前提                          ゴール全体
* ~~b               これがおすすめの表現
* ~b                move/negP.                                      apply/negP.
* b = false         move/negbT.                                     apply/negbTE.
* false = b         move/esym/negbT.                                apply/esym/negbTE.
* b == false        move/eqP/negbT.                                 apply/eqP/negbTE.
                    rewrite eqbF_neg.
* false == b        move/idPn.                                      apply/idPn.
                    move/eqP/esym/negbT.                            apply/eqP/esym/negbTE.
                    rewrite eq_sym eqbF_neg.
                    rewrite -[false == b]/(~~b).
* b <> true         move/negP.                                      apply/negP.
* true <> b         move/eqP; rewrite eq_sym negb_eqb addbT.        move/esym; apply/negP.
* ~(b == true)      move/negP; rewrite negb_eqb addbT.              move/eqP; apply/negP.
                    rewrite eqb_id => /negP.                        rewrite eqb_id; apply/negP.
* ~(true == b)      move/(@negP b).                                 apply/(@negP b).
                    move/negP; rewrite eq_sym negb_eqb addbT.       apply/negP; rewrite eq_sym negb_eqb addbT.
                    rewrite eq_sym eqb_id => /negP.                 rewrite eq_sym eqb_id; apply/negP.
                    rewrite -[true == b]/b => /negP.
* b != true         rewrite negb_eqb addbT.                         同左
* true != b         rewrite eq_sym negb_eqb addbT.                  同左
* ~~b = true        move/negbRL/negbT.                              apply/negbLR/negbTE.
* true = ~~b        move/negbLR/esym/negbT.                         apply/negbRL/esym/negbTE.
* ~~b == true       move/eqP/negbRL/negbT.                          apply/eqP/negbLR/negbTE.
                    rewrite eqb_negLR eqbF_neg.                     同左
* true == ~~b       move/eqP/esym/negbRL/negbT.                     apply/eqP/esym/negbLR/negbTE.
                    rewrite -eqb_negLR eq_sym eqbF_neg.             同左
                    rewrite -[true == ~~b]/(~~b).

たくさんやって思ったのは いちばん良いやりかたをつきつめると、 個々のケースに応じて頑張るしかないようだ。 (なるべく短く書けるとか、証明項が小さいとか)

しかし、書き方が長くても、証明項が大きくても構わない、というなら、一般的に変形できるのではないか、とも思った

扱いたい命題を一般的に定義してみよう。

BNF で、対象の命題を表現する。 P が命題、B が bool 式、V が bool 変数である

2023-05-03 修正: B = B と書いてしまっていたが、これだと変数が両辺にでてきてしまい、is_true V もしくは is_true (negb V) には変形できないので、B = true, true = B, B = false, false = B として変数がひとつしかでてこないようにした

P = is_true B
  | B = true
  | true = B
  | B = false
  | false = B
  | not P
B = V
  | B == true
  | true == B
  | B == false
  | false == B
  | negb B

ここで、二重否定命題 not (not P) は扱わないことにすると以下のようになる (まぁ、扱うのは可能なのだが、簡単にやる方法はわからなかった)

P = is_true B
  | B = true
  | true = B
  | B = false
  | false = B
  | not (is_true B)
  | not (B = true)
  | not (true = B)
  | not (B = false)
  | not (false = B)
B = V
  | B == true
  | true == B
  | B == false
  | false == B
  | negb B

これを is_true V もしくは is_true (negb V) に変形するのは以下のようにできる。

• 外側が (X = Y), (not (X = Y) の場合は move/eqP あるいは apply/eqP して、is_true (X == Y), is_true (negb (X == Y)) に変形する
• 外側が (not (is_true B)) の場合は move/negP あるいは apply/negP して、is_true (negb B) に変形する
• 外側が is_true B の場合はすでに外側が is_true なのでそのままにする

そうすると、外側が is_true B になるので、B 内部の bool な式を

rewrite ?[true == _]eq_sym ?[false == _]eq_sym ?eqb_id ?eqbF_neg ?negbK.

と書き換える。

これは、

• ?[true == _]eq_sym で true == B を B == true に
• ?[false == _]eq_sym で false == B を B == false に
• ?eqb_id で B == true を B に
• ?eqbF_neg で B == false を negb B に
• ?negbK で negb (negb B) を B に

書き換える。

ぜんぶ ? がついているので、0回以上、書き換えられなくなるまで繰り返す。 まぁ、convertible で済むものも rewrite するので、証明項は必要以上に大きくなるかもしれないけれど。

そうすると、以下が残るはずである

P = is_true B
B = V
  | negb V

つまり is_true V と is_true (negb V) だけになるはず、というわけである。

2023-03-02 (Thu)

#1 convertible なものは change で済ます

昨日の

rewrite ?[true == _]eq_sym ?[false == _]eq_sym ?eqb_id ?eqbF_neg ?negbK.

で残念なのは、true == b と false == b がそれぞれ b と negb b と convertible で、 証明項を作らずに変えられるはずなのに、 eq_sym, eqb_id, eqbF_neg で書き換えるので、必要もなく証明項を作っていることである

convertible な命題の変形は change という tactic (あるいは SSReflect の rewrite の -[...]/... という形式) を使えば可能ではあるのだが 変更後の項を人間が書かないといけないという問題がある

なんとかいちいち人間が書かないでどうにかできないか、と思っていたのだが、Ltac を使えばできるのではないかと思いついた

調べると、以下のようにすればいいようだ

repeat match goal with
       | |- context C [true == ?b] => let t := context C [b] in change t
       | |- context C [false == ?b] => let t := context C [negb b] in change t
       end;
rewrite ?eqb_id ?eqbF_neg ?negbK.

2023-05-03 追記: change tactic では変形対象の項の一部を参照して変形後の項を記述できることがわかった。なので、Ltac を使わなくてもいけるようだ

repeat change (true == ?x) with x;
repeat change (false == ?x) with (~~x);
rewrite ?eqb_id ?eqbF_neg ?negbK.

あと、これを使うと、b = true も以下で b に変形できる (apply/eqP で b == true にしてから、とする必要はない)

change (?x = true) with (is_true x).

2023-03-03 (Fri)

#1 mathcomp book issue

GitHub math-comp/mcb/issues/146: The order of subgoals in proof of eqnP.

2023-03-11 (Sat)

#1 mathcomp book issue

GitHub math-comp/mcb/issues/148: The explanation for the proof of edivnP

[latest]