なぜか無い補題

Coqのライブラリにはなぜか無い補題というものがある。
例えばZmult_le_reg_rというレンマはZArithのZorderライブラリにあるが、
これの左バージョンは無いのだ。
ちなみにZmult_le_reg_rとは次のような内容である。

Zmult_le_reg_r : forall n m p:Z, p > 0 -> n * p <= m * p -> n <= m.

これは

「すべての整数n, m, pに対して, pが正で, n*p ≦ m*p ならば、n ≦ pである。」

ということを意味している大変便利なレンマであるが、整数においてa*b = b*aが成り立つので、同様のレンマで

「p*n ≦ p*m ならば n ≦ mである。」

というレンマもほしくなるが、なぜか無いのである。
rがあるならlも作っとけ！！といいたくなるけど、作ればいいので作りました。
証明の全貌

Lemma Zmult_le_reg_l : forall n m p : Z, p > 0 -> p * n <= p * m -> n <= m.
Proof.
intros.
apply (Zmult_le_reg_r n m p).
 apply H.
 rewrite (Zmult_comm n p).
   rewrite (Zmult_comm m p).
   apply H0.
Zmult_le_reg_l < Qed.

証明の流れ
まず、整数Z を使うので Z をインポートしておく。スコープもZ に合わせておく。こうすると単に + や ＞ を書いたときにZ上の演算と認識される。

Coq < Require Import ZArith.
Coq < Open Scope Z_scope.

じゃあ早速初めて見よう！

Coq < Lemma Zmult_le_reg_l : 
  forall n m p : Z, p > 0 -> p * n <= p * m -> n <= m.
1 subgoal
  
  ============================
   forall n m p : Z, p > 0 -> p * n <= p * m -> n <= m

最初はだいたいイントロス。

Zmult_le_reg_l < intros.
1 subgoal
  
  n : Z
  m : Z
  p : Z
  H : p > 0
  H0 : p * n <= p * m
  ============================
   n <= m

基本的にはr バージョンと同じなので忘れないうちに使っておこう。
ゴールの形とZmult_le_reg_rの右端の形が同じなのでapplyできる。

Zmult_le_reg_l < apply (Zmult_le_reg_r n m p). 
2 subgoals
  
  n : Z
  m : Z
  p : Z
  H : p > 0
  H0 : p * n <= p * m
  ============================
   p > 0

subgoal 2 is:
 n * p <= m * p

するとふたつのサブゴールができる。
だんだん燃えてきた！
最初のゴールはとっても簡単。ゴールと一致する仮定がバーの上にあるのでこういうときはどうするのかな？
そう！apply だ！
「ゴールと一致するときはapply」 と覚えておこう。

Zmult_le_reg_l < apply H.
1 subgoal
  
  n : Z
  m : Z
  p : Z
  H : p > 0
  H0 : p * n <= p * m
  ============================
   n * p <= m * p

次のゴールはH0 から明らかに示せるように思える。
しかし単純にapplyしてもうまくいかない（エラーになる）。
一見当たり前のように見えるこの事実すらapplyでは証明できない。
このようなジレンマはCoqを使う上で出てくることがある。そのたびに次のことを念頭に置いてほしい。
「定理を証明する上で、当たり前のことが証明できるということが最も大事である。当たり前のことが証明できるならば、そのときほとんどのことを証明できるようになっているだろう。」
素直な心で、なぜこれが当たり前に思えるか、考えてみよう。
不等号はここでは本質ではない。
本質は「かけ算が右左関係ない」ということである。
もう一度いう。ここで大切なことは整数のかけ算に置いてa×bとb×aは常に同じ値になるということである！
このことをかけ算の可換性という。
整数という集合上ではかけ算は可換性が成り立つのでCoqでは次のような補題が用意されている。

Zmult_comm : forall n m : Z, n * m = m * n

このイコールを使ってゴールを書き換えてしまおう。
イコールを使って書き換える場合はrewriteというタクティックを使おう！
「イコールを使うときはrewrite」

Zmult_le_reg_l < rewrite (Zmult_comm n p).
1 subgoal
  
  n : Z
  m : Z
  p : Z
  H : p > 0
  H0 : p * n <= p * m
  ============================
   p * n <= m * p

Zmult_le_reg_l < rewrite (Zmult_comm m p).
1 subgoal
  
  n : Z
  m : Z
  p : Z
  H : p > 0
  H0 : p * n <= p * m
  ============================
   p * n <= p * m

これで仮定H0とゴールが一致した！
最後にとどめをさそう。
「仮定とゴールが一致する場合はapply」

Zmult_le_reg_l < apply H0.
Proof completed.

できたー！！！

Zmult_le_reg_l < Qed.
intros.
apply (Zmult_le_reg_r n m p).
 apply H.
 rewrite (Zmult_comm n p).
   rewrite (Zmult_comm m p).
   apply H0.
Zmult_le_reg_l is defined

(* 実はomegaという強力なタクティックを使えば一気に証明を終わらせることができる。でも最初は多少どんくさくてもワンステップづつ進めていく方が何をやってるかわかりやすくて楽しい（でしょ？） *)