目的
Coqのtacticsを改良？したssreflectと定理のライブラリであるmathcompを使って整数精度のHaar変換が可逆であること証明を通じて、整数に関する証明に慣れるのが目的です。
今回のHaar変換の証明のソースはこちらです。
前回Elgamal暗号＆復号の証明をしましたが、それは自然数の処理でした。（今回は整数）
整数の定理はmathcompのalgebraのライブラリのssralg,ssrint,intdivなどに含まれています。(一方、自然数の定理はmathcompのssreflectのライブラリのssrnat,div,primeなどに含まれています。)
algebraライブラリの資料はほとんど見当たらずCoq Winter School 2017-2018 (SSReflect & MathComp)のalgebraの資料を参考にしました。
mathcompの整数のライブラリの使い方
下記の宣言をしてmathcompのalgebraの整数のライブラリを利用します。
algebraライブラリはssrintなど個別にロードしてもいいですが、all_algebraで全部読み込んでいます。
intZmodやintOrderdはssrintにあるSectionの定理のスコープを設定しています。
設定しなくてもintOrdered.lezなどで参照できますが、面倒なのでImportします。
整数の足し算や引き算はssralgにある環のライブラリに含まれています。
GRing.Theoryのところはその整数の交換則(addrCというLemma)や結合則(addrAというLemma)などの定理を使えるように読んでいます。
(* ライブラリの読み込み *)
From mathcomp Require Import all_ssreflect all_algebra.
(* 便利なおまじない。よく分かっていません。 *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* 証明で使うスコープの設定。*)
(* 整数の足し算系（今回はいらないような気もしますが。） *)
Import intZmod.
(* 整数の大小の比較系 *)
Import intOrdered.
(* 整数の+や*といった演算子の環に関わるもの *)
Import GRing.Theory.
Open Scope ring_scope.
Haar変換についてとその定式化
Haar変換はウェーブレットで使われる信号の処理で、画像圧縮のために直流と交流の成分に分割して圧縮しやすいデータに変換するために使われます。特に整数精度の変換が可逆圧縮に使われます。
整数精度のHaar変換はmとnの二つの整数をm-nと(m+n)/2という差分（交流）と平均値（直流）に変換するものです。m-nと(m+n)/2からmとnをデータのロスなく復元するできます。
また、mとnが8bitだとm-nは9bit、(m+n)/2は8bitと精度となり、変換によるbit数の増加が少ないです。
下記のようにHaar変換と逆変換がもとのデータに戻ることを定式化しました。
(* Haar変換 *)
Definition enc1 (m n:int) := m - n.
Definition enc2 (m n:int) := ((m + n) %/ 2)%Z.
(* Haar逆変換 *)
Definition dec1 (e1: int) (e2: int) := ((e1 + e2 * 2 + 1) %/2)%Z.
Definition dec2 (e1: int) (e2: int) := dec1 e1 e2 - e1.
(* Haar変換がもとに戻る定理 *)
Theorem dec1_correct (m n :int): dec1 (enc1 m n) (enc2 m n) = m.
Proof.
Admitted.
Theorem dec2_correct (m n :int): dec2 (enc1 m n) (enc2 m n) = n.
Proof.
Admitted.
証明とそのやり方
証明は下記のように行いました。
- 上記のdec1_correctの定理のdec1,enc1,enc2をすべて展開。
- mathcompのlemmaのssralg,intdivを参考に式の変形。
- addrA、addrCとか*r*は式の変形につかったssralgのLemmaです。
- ltz_modとか*z*は式の変形につかったintdivのLemmaです。
- 式変形に必要なLemmaはgrepで調べました。
- 整数の不等式(lez)と演算子の(<=)の切り替えがよくわからなくて、lezrlをいうLemmaを用意しました。
下記は実際のコードです。明らかに簡単そうなLemmaが多いのをうまく消せるのかは今後の課題です。
Lemma addmn (m n:int) : (m + (- n) + m + n) = m * (2:int).
Proof.
rewrite addrC.
rewrite [m + (-n) + m]addrC.
rewrite [m + (m + (-n))]addrA.
rewrite [m + m + (-n)]addrC addrA.
rewrite addrN add0r.
rewrite -{1}[m]mulr1.
rewrite -{2}[m]mulr1.
rewrite -mulrDr //=.
Qed.
Lemma divmn (d:int) : d - (d %% 2)%Z = (d %/ 2)%Z * 2.
Proof.
apply/subr0_eq.
rewrite -opprB.
rewrite [-(d - (d %% 2)%Z)]opprB addrA.
rewrite -divz_eq //=.
rewrite opprB.
rewrite addrN //.
Qed.
Lemma lezrl (n m:int): lez n m = (n <= m).
Proof.
rewrite /lez //=.
Qed.
Lemma ltzrl (n m:int): ltz n m = (n < m).
Proof.
rewrite /ltz //=.
Qed.
Lemma lt_d_1 (d:int) : (d %% 2)%Z <= 1 .
Proof.
have lt_2 : (d %% 2)%Z < `|Posz 2| .
- rewrite ltz_mod //.
have eq_2 : `|Posz 2| = Posz 2.
- by [].
have eq_21 : (d %% 2)%Z < 2 .
- rewrite -{2}eq_2 lt_2 //
rewrite ltz_mod //.
rewrite -ltz_add1r //.
Qed.
Lemma modDiv0 (d:int) : ((1 - (d %% 2)%Z) %/ 2)%Z = 0%Z.
Proof.
rewrite divz_small //.
(* 0 <= 1 - (d %% 2)%Z < `|2|%N *)
rewrite -lezrl subz_ge0 lezrl lt_d_1 /=.
rewrite -lez_add1r addrA.
rewrite -lezrl -subz_ge0 lezrl.
have eq_2 : 1 + 1 = (2:int).
- by [].
have eq0_2 : (2:int) + (-(2:int)) = 0.
- by [].
rewrite addrC opprB /=.
rewrite eq_2.
rewrite [(d %% 2)%Z + (-(2:int))]addrC addrC addrA eq0_2.
rewrite add0r.
rewrite modz_ge0 //.
Qed.
Theorem dec1_correct (m n :int): dec1 (enc1 m n) (enc2 m n) = m.
Proof.
rewrite /dec1 /enc1 /enc2.
rewrite -divmn.
rewrite !addrA.
rewrite [m - n + m + n]addmn.
have divrMDl2 (m0: int): ((m * (Posz 2) + m0) %/ (Posz 2))%Z = m + (m0 %/ (Posz 2))%Z.
- rewrite divzMDl //.
rewrite {1}addrC !addrA.
rewrite [1 + m * 2]addrC.
set mn := - ((m + n) %% 2)%Z.
rewrite -/mn.
set mn1 := 1 + mn.
rewrite addrC addrA.
rewrite addrC addrA.
rewrite -/mn1.
rewrite addrC.
rewrite divrMDl2.
rewrite /mn1 /mn modDiv0.
rewrite addr0 //.
Qed.
Theorem dec2_correct (m n :int): dec2 (enc1 m n) (enc2 m n) = n.
Proof.
rewrite /dec2.
rewrite dec1_correct /enc1.
rewrite [-(m - n)]opprB addrA.
rewrite addrC addrA addNr add0r //.
Qed.
まとめ
mathcompのssralgやintdivのライブラリを用いて整数に関する証明になれるという目的のもと整数精度のHaar変換が可逆であることを証明できました。明らかに簡単そうなLemmaが多いのをうまく消せるのかは今後の課題です。