More than 5 years have passed since last update.
整数を使った証明（整数精度のHaar変換）のトライアル
目的
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)などの定理を使えるように読んでいます。
(* ライブラリの読み込み *)FrommathcompRequireImportall_ssreflectall_algebra.(* 便利なおまじない。よく分かっていません。 *)SetImplicitArguments.UnsetStrictImplicit.UnsetPrintingImplicitDefensive.(* 証明で使うスコープの設定。*)(* 整数の足し算系（今回はいらないような気もしますが。） *)ImportintZmod.(* 整数の大小の比較系 *)ImportintOrdered.(* 整数の+や*といった演算子の環に関わるもの *)ImportGRing.Theory.OpenScopering_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変換 *)Definitionenc1(mn:int):=m-n.Definitionenc2(mn:int):=((m+n)%/2)%Z.(* Haar逆変換 *)Definitiondec1(e1:int)(e2:int):=((e1+e2*2+1)%/2)%Z.Definitiondec2(e1:int)(e2:int):=dec1e1e2-e1.(* Haar変換がもとに戻る定理 *)Theoremdec1_correct(mn:int):dec1(enc1mn)(enc2mn)=m.Proof.Admitted.Theoremdec2_correct(mn:int):dec2(enc1mn)(enc2mn)=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が多いのをうまく消せるのかは今後の課題です。
Lemmaaddmn(mn:int):(m+(-n)+m+n)=m*(2:int).Proof.rewriteaddrC.rewrite[m+(-n)+m]addrC.rewrite[m+(m+(-n))]addrA.rewrite[m+m+(-n)]addrCaddrA.rewriteaddrNadd0r.rewrite-{1}[m]mulr1.rewrite-{2}[m]mulr1.rewrite-mulrDr//=.Qed.Lemmadivmn(d:int):d-(d%%2)%Z=(d%/2)%Z*2.Proof.apply/subr0_eq.rewrite-opprB.rewrite[-(d-(d%%2)%Z)]opprBaddrA.rewrite-divz_eq//=.rewriteopprB.rewriteaddrN//.Qed.Lemmalezrl(nm:int):leznm=(n<=m).Proof.rewrite/lez//=.Qed.Lemmaltzrl(nm:int):ltznm=(n<m).Proof.rewrite/ltz//=.Qed.Lemmalt_d_1(d:int):(d%%2)%Z<=1.Proof.havelt_2:(d%%2)%Z<`|Posz2|.-rewriteltz_mod//.haveeq_2:`|Posz2|=Posz2.-by[].haveeq_21:(d%%2)%Z<2.-rewrite-{2}eq_2lt_2//rewriteltz_mod//.rewrite-ltz_add1r//.Qed.LemmamodDiv0(d:int):((1-(d%%2)%Z)%/2)%Z=0%Z.Proof.rewritedivz_small//.(* 0 <= 1 - (d %% 2)%Z < `|2|%N *)rewrite-lezrlsubz_ge0lezrllt_d_1/=.rewrite-lez_add1raddrA.rewrite-lezrl-subz_ge0lezrl.haveeq_2:1+1=(2:int).-by[].haveeq0_2:(2:int)+(-(2:int))=0.-by[].rewriteaddrCopprB/=.rewriteeq_2.rewrite[(d%%2)%Z+(-(2:int))]addrCaddrCaddrAeq0_2.rewriteadd0r.rewritemodz_ge0//.Qed.Theoremdec1_correct(mn:int):dec1(enc1mn)(enc2mn)=m.Proof.rewrite/dec1/enc1/enc2.rewrite-divmn.rewrite!addrA.rewrite[m-n+m+n]addmn.havedivrMDl2(m0:int):((m*(Posz2)+m0)%/(Posz2))%Z=m+(m0%/(Posz2))%Z.-rewritedivzMDl//.rewrite{1}addrC!addrA.rewrite[1+m*2]addrC.setmn:=-((m+n)%%2)%Z.rewrite-/mn.setmn1:=1+mn.rewriteaddrCaddrA.rewriteaddrCaddrA.rewrite-/mn1.rewriteaddrC.rewritedivrMDl2.rewrite/mn1/mnmodDiv0.rewriteaddr0//.Qed.Theoremdec2_correct(mn:int):dec2(enc1mn)(enc2mn)=n.Proof.rewrite/dec2.rewritedec1_correct/enc1.rewrite[-(m-n)]opprBaddrA.rewriteaddrCaddrAaddNradd0r//.Qed.まとめ
mathcompのssralgやintdivのライブラリを用いて整数に関する証明になれるという目的のもと整数精度のHaar変換が可逆であることを証明できました。明らかに簡単そうなLemmaが多いのをうまく消せるのかは今後の課題です。
参考資料
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme