mathcomp だと elim: n {-2}n (leqnn n) を簡単にするために ubnPgeq が使えたように、 elim: n.+1 {-2}n (ltnSn n) を簡単にするのが用意されてないかな、と思って調べたところ、 ssrnat.v のコメントに書いてあった
あまりよくわかってないが、ubnP というのがあって、以下のように使えるようだ
From mathcomp Require Import all_ssreflect.
Parameter P : nat -> Prop.
Goal forall n, P n.
move=> m.
have [n] := ubnP m.
elim: n m => // n IH m => /ltnSE.
(* IH : forall m : nat, m < n -> P m *)
rewrite leq_eqVlt => /orP [/eqP -> {m}|]; last by apply IH.
admit. (* P n *)さて、どっちがマシかな
Goal forall n, P n.
move=> n.
elim: n.+1 {-2}n (ltnSn n) => {n} [|n IH m]; first by [].
rewrite ltnS leq_eqVlt => /orP [/eqP -> {m}|]; last by apply IH.
admit. (* P n *)
Restart.
elim/Wf_nat.lt_wf_ind => n IH'.
have IH m : m < n -> P m. by move/ltP; apply IH'.
clear IH'.
admit. (* P n *)
行数はだいたい同じだけど、lt_wf_ind を使った方が簡単に感じられる
(もちろん、lt_wf_ind の中身は別にあるわけなので、それを使わずにここまで行数を近づけられる、ともいえる)
命題 P n を forall j i : nat, i < j -> P i という形に一般化すれば、 Wf_nat.lt_wf_ind みたいにできるのではないかと思いついた (i=n, j=n+1 と特殊化すると i<j は簡単に証明できるので、P n が出てくる)
試したところ、move: n.+1 {-2}n (ltnSn n) とすればそのように一般化できるようだ
そうした後で、m について帰納法を行うと、m = 0 の場合には n < m が偽になるので P に関係なく証明でき、 P の中身について考えなければならないゴールはひとつで済み、Wf_nat.lt_wf_ind と同じになる
From mathcomp Require Import all_ssreflect.
Section S.
Parameter P : nat -> Prop.
Goal forall n, P n.
move=> n.
elim: n.+1 {-2}n (ltnSn n) => {n} [|n IH m]; first by [].
(* IH : forall n0 : nat, n0 < n -> P n0 *)
rewrite ltnS leq_eqVlt => /orP [/eqP -> {m}|]; last by apply IH.
admit. (* P n *)vanilla Coq で整礎帰納法を使うには、 整礎帰納法のための induction principle (Wf_nat.lt_wf_ind とか) を使う
Require Import Wf_nat. Section S. Parameter P : nat -> Prop. Goal forall n, P n. intro n. induction n using lt_wf_ind. (* n : nat H : forall m : nat, m < n -> P m ______________________________________(1/1) P n *)
SSReflect でも Coq の induction principle を使うことができる
From mathcomp Require Import all_ssreflect. Section S. Parameter P : nat -> Prop. Goal forall n, P n. elim/Wf_nat.lt_wf_ind. (* forall n : nat, (forall m : nat, (m < n)%coq_nat -> P m) -> P n *)
しかしこれだと、(m < n)%coq_nat というように、 vanilla Coq の比較が出てくるので、SSReflect のスタイルじゃなくてちょっと扱いづらい
SSReflect のスタイルに直すには以下のようにすればよい
move=> n IH'. have IH : forall m : nat, m < n -> P m. move=> m mn. by apply/IH'/ltP. clear IH'. (* IH : forall m : nat, m < n -> P m *)
vanilla Coq の比較がはじめから出てこない、SSReflect 流の整礎帰納法のやりかたはないのか探してみると、 An Ssreflect Tutorial (2009) に elim: n {-2}n (leqnn n) というやり方が載っていた (strong induction で探すと出てくる。 載っているのは、elim: m {-2}m 0 (leqnn m) という形で、変数が m で、さらに命題の中にある 0 を一般化している。)
これだけだとなにをやっているのかわからないけれど、説明を読むと、 P n を forall m, m <= n -> P m に一般化してから普通の自然数の帰納法 (nat_ind) を使うという流れのようだ
From mathcomp Require Import all_ssreflect.
Section S.
Parameter P : nat -> Prop.
Goal forall n, P n.
move=> n.
elim: n {-2}n (leqnn n).
(*
______________________________________(1/2)
forall n : nat, n <= 0 -> P n
______________________________________(2/2)
forall n : nat,
(forall n0 : nat, n0 <= n -> P n0) -> forall n0 : nat, n0 <= n.+1 -> P n0
*)
うぅむ、lt_wf_ind を使った場合よりも複雑になっている
まず lt_wf_ind ではゴールがひとつだったが、こちらはゴールがふたつになる (普通の帰納法なので、0 の場合と 1以上の場合のふたつになるのはそうならざるを得ない)
ひとつめは P 0 の場合で、 ふたつめは n 以下の場合について成り立つなら n+1 以下について成り立つ、というやつ
ひとつめは P の中身がわからないとこれ以上はどうしようもない
ふたつめは、n+1 以下の場合のなかで、n 以下の場合は前提から証明できるので、 n+1 の場合だけにできる
そのように変形するには以下のようにすればよい
move=> n.
elim: n {-2}n (leqnn n) => [[] // _|n IH m].
admit. (* P 0 *)
rewrite leq_eqVlt => /orP []; last by rewrite ltnS; apply IH.
move/eqP => -> {m}.
(* IH : forall n0 : nat, n0 <= n -> P n0 *)
admit. (* P n.+1 *)
しかし... これが本当にお勧めの方法なのだろうか?
さらに調べると、 mathcomp の本 (2021) には この方向でちょっと進んだやつが載っていてどうも本気らしいと感じる (こっちだと -2 という場所の指定をしなくていいという点が進歩している)
move=> n. case: (ubnPgeq n) => m. elim: n m => [[] // _|n IH m]. admit. (* P 0 *) rewrite leq_eqVlt => /orP []; last by rewrite ltnS; apply IH. move/eqP => ->. (* IH : forall m : nat, m <= n -> P m *) admit. (* P n.+1 *)
うぅむ、あらかじめ整礎帰納法の induction principle を用意しておかなくていいという利点は理解できるが、 正直、Wf_nat.lt_wf_ind を使った方が簡単だと感じられる
SSReflect のやりかたのほうがいい場合はどういう場合だろう? 0 とそれ以外の場合わけが必要になるとき? 一般化のところをいじりたいとき?
Canonical の最低限の例を作ってみた。
適当にレコードを定義して、そのメンバのひとつ (RecT) は型であり、 :> とすることで型の文脈で使われたらそのメンバが自動的に使われるよう coercion も定義する。 RecT 以外になにもないと寂しいので、特に意味は無いが、nat 型の RecN メンバも加える。
Record rec := Rec { RecT :> Type; RecN : nat }.
rec 型の値を適当に定義する。
Definition bool_Rec := Rec bool 0.
rec 型の値と、その値を型とする値を受け取る関数を定義する。
Definition f (T : rec) (x : T) := 0.
coersion を表示するように設定すると、以下の RecT T というように、T の中から取り出した RecT メンバを型として扱って、 それが引数の型となっていることがわかる。
Check f. (* f : forall T : rec, RecT T -> nat *)
ここで、f _ true として、f の適用で、第1引数 T を省略してみると、T がなにかわからないので失敗する。
Fail Check f _ true. (* The term "true" has type "bool" while it is expected to have type "RecT ?T". *)
Canonical で bool_Rec を登録する。
Canonical bool_Rec.
再度 f _ true として、T を省略してみると、今度は T に bool_Rec が埋められて成功する。
Check f _ true. (* f bool_Rec true *)
もちろん、T を bool_Rec で埋めていいのは f の第2引数 x が bool のときだけである。 なので、f _ 0 は依然として失敗する。
Fail Check f _ 0. (* The term "0" has type "nat" while it is expected to have type "RecT ?T". *)
SSReflect の eqType もこの機構を使っている。 eqType の場合は、(上記の RecN のかわりに) 同値性を判定する関数と、その関数が本当に同値性である (反射律、対称律、推移律を満たす) という証明が入っている。 x == y は @eq_op eqtype x y のことで、eq_op は eqtype から同値性を判定する関数を取り出して x と y に適用するというしかけになっている。 x == y という記法では eqtype を記述しないのだが、Canonical により x と y の型から Canonical で指定されたもの (bool_eqType とか nat_eqType) が埋められる。 あと、eqtype に入っている証明は (x == y) = (y == x) などといった定理の証明に使われる。
Static detection of DoS vulnerabilities in programs that use regular expressions という論文を眺めた
ReDoS が起きる (backtracking regexp engine で時間計算量が Ω(2**n) や Ω(n**2) や になってしまう) NFA の形が明確に書いてあった
指数関数的になるのが Fig.4 で、2乗になるのが Fig.6
指数関数的になるのは同じ状態にふたつ (以上) のループがついている形で、 2乗になるのはふたつのループが並んでいる形
たしかにそういう形ならそういう計算量になるだろうな、と思う
(また、そういう計算量になるのはそういう形が NFA に含まれているときだけ、とも書いてあるが、 こちらは簡単に納得できる話ではなく、証明は読んでいない)
論文にはそれだけじゃなくて、プログラムの外から与えられるデータが実際に正規表現とのマッチにたどりつけるかとかも がんばって解析している
Coq で、関数の中を rewrite するにはどうしたらいいか。 たとえば、以下で、(fun n => (n + 1) + n) という関数の中の n + 1 を n.+1 に書き換えたいとしよう
Lemma L1 s : map (fun n => (n + 1) + n) s = map (fun n => n.+1 + n) s. Proof. Fail rewrite addn1. apply: eq_map => n. by rewrite addn1. Qed.
最初に Fail rewrite addn1. 書いてあるのは、 そこでは rewrite addn1 が失敗するという意味である。 なんで失敗するかというと、n + 1 の n は (fun n => ...) というところで束縛されている変数であるため、 ゴールを P (n + 1) という形に beta expansion できないからである。
そのため、上の証明ではいきなり rewrite するのはあきらめて、まず eq_map を使って変形している。 ということは、(n + 1) という項自体の性質ではなく、 その外側にある map についての性質を利用して証明しているわけである。
しかし、eq_map みたいな補題を探すのは面倒で嫌だ、という場合を考えよう。 これは、FunctionalExtensionality という公理を使うと可能となる
Require Import FunctionalExtensionality.
Lemma L2 s : map (fun n => (n + 1) + n) s =
map (fun n => n.+1 + n) s.
Proof.
change (map (fun n => (fun x => x + 1) n + n) s =
map (fun n => n.+1 + n) s).
rewrite (_ : (fun x => x + 1) = (fun x => x.+1)).
by [].
(* (fun x : nat => x + 1) = (fun x : nat => x.+1) *)
apply functional_extensionality => x.
(* x + 1 = x.+1 *)
by rewrite addn1.
Qed.
ここでは書き換えたい n + 1 を (fun x => x + 1) n と変形して 束縛変数 n が含まれない (fun x => x + 1) という項を作り出し、 (fun x => x + 1) を (fun x => x.+1) に書き換えている
(fun x => x + 1) を (fun x => x.+1) に書き換えるのは functional_extensionality (と addn1) を使うと可能である
この証明では、eq_map のような、書き換えたいところ以外の部分の性質は使っていない。 そのため、外側に謎の関数が使ってあっても証明できる。
Parameter P : (nat -> nat) -> seq nat -> seq nat.
Lemma L3 s : P (fun n => (n + 1) + n) s =
P (fun n => n.+1 + n) s.
Proof.
change (P (fun n => (fun x => x + 1) n + n) s =
P (fun n => n.+1 + n) s).
rewrite (_ : (fun x => x + 1) = (fun x => x.+1)).
by [].
(* (fun x : nat => x + 1) = (fun x : nat => x.+1) *)
apply functional_extensionality => x.
(* x + 1 = x.+1 *)
by rewrite addn1.
Qed.
ここでは、P という中身が謎な関数を使っている中で (束縛変数 n を含む) n + 1 を n.1 に書き換えている
OCaml で、配列の要素になんか関数を適用して、 その関数が成功したらその結果を返す、という関数を書きたいことがあった
これは高階関数で、'a array 型の配列と、 その要素を受け取って 'b option 型の値を返す関数 f を受け取る。 配列の最初の要素から順に f に与えて、f が None を返したら次の要素に進む。 最初に Some x を返したらそれを返す、というものである。 なお、最後まで Some が返されなかったら None を返す。
let array_find_map (f : 'a -> 'b option) (s : 'a array) : 'b option = ...
さて、どうやって実装するか
配列なのでとりあえず for ループでやるか、と考えて、ループの途中で脱出するのは例外を使えばいいだろう、 ということで、以下を書いた
let array_find_map (f : 'a -> 'b option) (s : 'a array) : 'b option =
let exception Found of 'b option in
try
for i = 0 to Array.length s do
let v = f s.(i) in
match v with
| None -> ()
| Some _ -> raise (Found v)
done;
None
with Found v ->
v
しかしこれはエラーになる
Error: The type variable 'b is unbound in this type declaration.
どうも、例外の引数は多相型にはできないぽい
まぁ、再帰を使えば例外を使わずに書けるからいいけど
let array_find_map (f : 'a -> 'b option) (s : 'a array) : 'b option =
let n = Array.length s in
let rec aux i =
if i < n then
let v = f s.(i) in
match v with
| None -> aux (i+1)
| Some _ -> v
else
None
in
aux 0
でも、ループで書けないのは気になる。 検索すると、Locally abstract types なるものを使えるようだ
The OCaml Manual, Locally abstract types
以下のようにしたら通った
let array_find_map (type a b) (f : a -> b option) (s : a array) : b option =
let module M = struct exception Found of b option end in
try
for i = 0 to Array.length s do
let v = f s.(i) in
match v with
| None -> ()
| Some _ -> raise (M.Found v)
done;
None
with M.Found v ->
v
しかし、これが通るんならなんで最初のが通らんのだ、意味もなく module が必要でよろしくない、 と思ったが、試すと module を使わなくてもいいようだ
let array_find_map (type a b) (f : a -> b option) (s : a array) : b option =
let exception Found of b option in
try
for i = 0 to Array.length s do
let v = f s.(i) in
match v with
| None -> ()
| Some _ -> raise (Found v)
done;
None
with Found v ->
v
とすると、最初のが通らないのは、単に型変数のスコープから外れているから、というだけの話なのかな