天泣記

2019-05-03 (Fri)

#1 Coq の Function で functional induction と functional inversion を使ってみる

Functional Scheme 関係を調べていたところ、 どうも、Functional Scheme の発展形が Function らしい。

論文は以下のようだ。Coq の syntax は見慣れたもので、古くない。

Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu. Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. FLOPS 2006, LNCS 3945, pp. 114–129, 2006. <URL:https://people.irisa.fr/David.Pichardie/papers/flops06.pdf>

Functional Scheme の論文と first author が同じである。

Function は非構造的再帰関数の定義のためのもの、という認識だったので、けっこう意外である。

構造的再帰関数 (といっていいのかちょっと自信がないが、とにかく Coq の termination checker を通る再帰関数) でも使えるようなので、Functional Scheme と同様に div2 で試してみよう。

まず、div2 を定義する。

From mathcomp Require Import all_ssreflect.
Require Import FunInd.

Function div2 (n:nat) : nat :=
match n with
| O => 0
| S O => 0
| S (S n') => S (div2 n')
end.

ここで、なにが定義されたのか確認してみると、 div2 以外に R_div2, R_div2_rect, R_div2_ind, R_div2_rec, div2_equation, div2_rect, div2_ind, div2_rec, R_div2_correct, R_div2_complete が定義された事がわかる。

Print All. (*
 >>>>>>> Library Top
div2 : nat -> nat
Inductive R_div2 : nat -> nat -> Set :=
    R_div2_0 : forall n : nat, n = 0 -> R_div2 0 0
  | R_div2_1 : forall n : nat, n = 1 -> R_div2 1 0
  | R_div2_2 : forall n n' : nat, n = n'.+2 -> forall _res : nat, R_div2 n' _res -> R_div2 n'.+2 _res.+1

For R_div2: Argument scopes are [nat_scope nat_scope]
For R_div2_0: Argument scopes are [nat_scope _]
For R_div2_1: Argument scopes are [nat_scope _]
For R_div2_2: Argument scopes are [nat_scope nat_scope _ nat_scope _]
R_div2_rect :
forall P : forall n n0 : nat, R_div2 n n0 -> Type,
(forall (n : nat) (e : n = 0), P 0 0 (R_div2_0 n e)) ->
(forall (n : nat) (e : n = 1), P 1 0 (R_div2_1 n e)) ->
(forall (n n' : nat) (e : n = n'.+2) (_res : nat) (r : R_div2 n' _res), P n' _res r -> P n'.+2 _res.+1 (R_div2_2 n n' e _res r)) ->
forall (n n0 : nat) (r : R_div2 n n0), P n n0 r
R_div2_ind :
forall P : forall n n0 : nat, R_div2 n n0 -> Prop,
(forall (n : nat) (e : n = 0), P 0 0 (R_div2_0 n e)) ->
(forall (n : nat) (e : n = 1), P 1 0 (R_div2_1 n e)) ->
(forall (n n' : nat) (e : n = n'.+2) (_res : nat) (r : R_div2 n' _res), P n' _res r -> P n'.+2 _res.+1 (R_div2_2 n n' e _res r)) ->
forall (n n0 : nat) (r : R_div2 n n0), P n n0 r
R_div2_rec :
forall P : forall n n0 : nat, R_div2 n n0 -> Set,
(forall (n : nat) (e : n = 0), P 0 0 (R_div2_0 n e)) ->
(forall (n : nat) (e : n = 1), P 1 0 (R_div2_1 n e)) ->
(forall (n n' : nat) (e : n = n'.+2) (_res : nat) (r : R_div2 n' _res), P n' _res r -> P n'.+2 _res.+1 (R_div2_2 n n' e _res r)) ->
forall (n n0 : nat) (r : R_div2 n n0), P n n0 r
div2_equation : forall n : nat, div2 n = match n with
                                         | n'.+2 => (div2 n').+1
                                         | _ => 0
                                         end
div2_rect :
forall P : nat -> nat -> Type,
(forall n : nat, n = 0 -> P 0 0) ->
(forall n : nat, n = 1 -> P 1 0) -> (forall n n' : nat, n = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) -> forall n : nat, P n (div2 n)
div2_ind :
forall P : nat -> nat -> Prop,
(forall n : nat, n = 0 -> P 0 0) ->
(forall n : nat, n = 1 -> P 1 0) -> (forall n n' : nat, n = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) -> forall n : nat, P n (div2 n)
div2_rec :
forall P : nat -> nat -> Set,
(forall n : nat, n = 0 -> P 0 0) ->
(forall n : nat, n = 1 -> P 1 0) -> (forall n n' : nat, n = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) -> forall n : nat, P n (div2 n)
R_div2_correct : forall n _res : nat, _res = div2 n -> R_div2 n _res
R_div2_complete : forall n _res : nat, R_div2 n _res -> _res = div2 n
*)

以前と同じく、div2 m <= m を証明するのに functional induction tactic を使う。

Lemma leq_div2 m: div2 m <= m.
Proof.
  functional induction (div2 m).
      by [].
    by [].
  by apply ltnW.
Qed.

証明項を表示すると、div2_ind を呼び出していることがわかる。

Print leq_div2. (* leq_div2 =
fun m : nat =>
let n := div2 m in
div2_ind (fun n0 n1 : nat => is_true (n1 <= n0))
  (fun (n0 : nat) (_ : n0 = 0) => leqnn 0)
  (fun (n0 : nat) (_ : n0 = 1) => leqnSn 0)
  (fun (n0 n' : nat) (_ : n0 = n'.+2) =>
   [eta @ltnW (div2 n').+1 n'.+2]) m
     : forall m : nat, is_true (div2 m <= m)
*)

div2_equation の証明項は Functional Scheme と同じだった。 証明しなおして同じになることを確認する。

Lemma div2_equation' : forall n : nat,
    div2 n = match n with
             | n'.+2 => (div2 n').+1
             | _ => 0
             end.
Proof.
  by case.
Defined.
Goal div2_equation = div2_equation'. Proof. reflexivity. Qed.

div2_ind (と div2_rec) は div2_rect を呼び出しているだけだった。

div2_rect は以下だが、これが困ったことに opaque になっている。 opaque な (Qed で終わった証明に相当する) 定数は展開できないので、 div2_rect = div2_rect' みたいな命題を証明できない。

About div2_rect. (*
div2_rect :
forall P : nat -> nat -> Type,
(forall n : nat, n = 0 -> P 0 0) ->
(forall n : nat, n = 1 -> P 1 0) ->
(forall n n' : nat, n = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
forall n : nat, P n (div2 n)

Argument scopes are [function_scope function_scope function_scope function_scope
  nat_scope]
div2_rect is opaque
Expands to: Constant Top.div2_rect
*)

しょうがないので、Print div2_rect で表示した項をコピーして定義しなおす。 (単純にこれをやると失敗することがあるが、implicit argument や coercion を省略せずに表示させるようにするとうまくいくようだ。 こんなことをしないで済む方法があればいいのだが。)

Definition div2_rect_org :=
(fun (P : nat -> nat -> Type) (f1 : forall n : nat, n = 0 -> P 0 0)
  (f0 : forall n : nat, n = 1 -> P 1 0)
  (f : forall n n' : nat, n = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) =>
fix div3 (n : nat) : P n (div2 n) :=
  @eq_rect_r nat match n with
                 | n'.+2 => (div2 n').+1
                 | _ => 0
                 end [eta P n]
    (let f2 := f1 n in
     let f3 := f0 n in
     let f4 := f n in
     match
       n as n0
       return
         (n = n0 ->
          (forall n' : nat, n0 = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
          (n0 = 1 -> P 1 0) ->
          (n0 = 0 -> P 0 0) ->
          P n0 match n0 with
               | n'.+2 => (div2 n').+1
               | _ => 0
               end)
     with
     | 0 =>
         fun (_ : n = 0)
           (_ : forall n' : nat,
                0 = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1)
           (_ : 0 = 1 -> P 1 0) (f7 : 0 = 0 -> P 0 0) =>
         unkeyed (f7 (erefl 0))
     | n0.+1 =>
         fun (_ : n = n0.+1)
           (f5 : forall n' : nat,
                 n0.+1 = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1)
           (f6 : n0.+1 = 1 -> P 1 0) (_ : n0.+1 = 0 -> P 0 0) =>
         match
           n0 as n1
           return
             (n0 = n1 ->
              (n1.+1 = 1 -> P 1 0) ->
              (forall n' : nat,
               n1.+1 = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
              P n1.+1 match n1 with
                      | 0 => 0
                      | n'.+1 => (div2 n').+1
                      end)
         with
         | 0 =>
             fun (_ : n0 = 0) (f8 : 1 = 1 -> P 1 0)
               (_ : forall n' : nat,
                    1 = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) =>
             unkeyed (f8 (erefl 1))
         | n1.+1 =>
             fun (_ : n0 = n1.+1) (_ : n1.+2 = 1 -> P 1 0)
               (f9 : forall n' : nat,
                     n1.+2 = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) =>
             let f10 :=
               let n' := n1 in let H : n1.+2 = n'.+2 := erefl n1.+2 in f9 n' H in
             unkeyed (let Hrec := div3 n1 in f10 Hrec)
         end (erefl n0) f6 f5
     end (erefl n) f4 f3 f2) (div2 n) (div2_equation n))
     : forall P : nat -> nat -> Type,
       (forall n : nat, n = 0 -> P 0 0) ->
       (forall n : nat, n = 1 -> P 1 0) ->
       (forall n n' : nat, n = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
       forall n : nat, P n (div2 n).

これを tactic で証明しなおすと、以下のようになり、同じ証明項になったことを確認できる。 なお、Functional Scheme で生成された div2_ind とは微妙に異なるようだ。

Lemma div2_rect' : forall P : nat -> nat -> Type,
       (forall n : nat, n = 0 -> P 0 0) ->
       (forall n : nat, n = 1 -> P 1 0) ->
       (forall n n' : nat, n = n'.+2 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
       forall n : nat, P n (div2 n).
Proof.
  move=> P H0 H1 H2.
  fix IH 1 => n.
  rewrite-> div2_equation'.
  move: (H2 n) (H1 n) (H0 n) => {H2 H1 H0}.
  case_eq n => [|n1] _ H2 H1 H0; first by apply H0.
  move: H1 H2.
  case_eq n1 => [|n2] _ H1 H2; first by apply H1.
  by apply H2; last apply IH.
Defined.

Goal div2_rect_org = div2_rect'. Proof. reflexivity. Qed.

さて、Function で定義されたもののうち、残りは R_div2, R_div2_rect, R_div2_ind, R_div2_rec, R_div2_correct, R_div2_complete である。

R_div2 は帰納型で、R_div2_rect, R_div2_ind, R_div2_rec は帰納型に対する 普通の induction principle である。

R_div2 を表示してみると、div2 の引数と返値の関係を帰納型として表現したものぽい。

Print R_div2. (*
Inductive R_div2 : nat -> nat -> Set :=
    R_div2_0 : forall n : nat, n = 0 -> R_div2 0 0
  | R_div2_1 : forall n : nat, n = 1 -> R_div2 1 0
  | R_div2_2 : forall n n' : nat,
               n = n'.+2 ->
               forall _res : nat, R_div2 n' _res -> R_div2 n'.+2 _res.+1
*)

R_div2_correct と R_div2_complete は関数 div2 と帰納型 R_div2 が対応していることの証明のようだ。

About R_div2_correct. (* : forall n _res : nat, _res = div2 n -> R_div2 n _res *)
About R_div2_complete. (* : forall n _res : nat, R_div2 n _res -> _res = div2 n *)

R_div2 がなんに使われるのか調べてみると、functional inversion という tactic で使われるようだ。 帰納型に対する inversion のようなことを関数に対して行えるらしいので試してみる。

inversion なので div2 が前提にないといけなくて、以下の定理を考えると functional inversion が使えた。

Lemma div2_0 : forall n, div2 n = 0 -> n < 2.
Proof.
  move=> n H.
  functional inversion H.
    by [].
  by [].
Defined.

div2_0 の証明項をみると、R_div2_correct で関数についての命題を帰納型についての命題に変換し、 帰納型についての inversion ぽいことを行い、R_div2_complete で帰納型についての命題から関数についての命題に戻しているようだ。

Print div2_0. (* div2_0 =
fun (n : nat) (H : div2 n = 0) =>
let H0 : 0 = div2 n := Logic.eq_sym H in
(fun H1 : 0 = div2 n =>
 (fun H2 : R_div2 n 0 =>
  let H3 : n = n -> 0 = 0 -> n < 2 :=
    match H2 in (R_div2 n0 n1) return (n0 = n -> n1 = 0 -> n < 2) with
    | R_div2_0 n0 H3 =>
        fun H4 : 0 = n =>
        ((fun H6 : 0 = n =>
          let H7 : 0 = n := H6 in
          eq_ind 0 (fun n1 : nat => 0 = 0 -> n0 = 0 -> n1 < 2)
            (fun (_ : 0 = 0) (_ : n0 = 0) =>
             (fun H10 : 0 = div2 n =>
              let H11 : div2 n = 0 := Logic.eq_sym H10 in
              (fun _ : div2 n = 0 => leqnSn 1) H11) (R_div2_complete n 0 H2)) n
            H7) H4)^~ H3
    | R_div2_1 n0 H3 =>
        fun H4 : 1 = n =>
        ((fun H6 : 1 = n =>
          let H7 : 1 = n := H6 in
          eq_ind 1 (fun n1 : nat => 0 = 0 -> n0 = 1 -> n1 < 2)
            (fun (_ : 0 = 0) (_ : n0 = 1) =>
             (fun H10 : 0 = div2 n =>
              let H11 : div2 n = 0 := Logic.eq_sym H10 in
              (fun _ : div2 n = 0 => leqnn 2) H11) (R_div2_complete n 0 H2)) n H7)
           H4)^~ H3
    | R_div2_2 n0 n' H3 _res H4 =>
        fun (H5 : n'.+2 = n) (H6 : _res.+1 = 0) =>
        (fun H7 : n'.+2 = n =>
         let H8 : n'.+2 = n := H7 in
         eq_ind n'.+2
           (fun n1 : nat => _res.+1 = 0 -> n0 = n'.+2 -> R_div2 n' _res -> n1 < 2)
           (fun H9 : _res.+1 = 0 =>
            let H10 : False :=
              eq_ind _res.+1
                (fun e : nat => match e with
                                | 0 => False
                                | _.+1 => True
                                end) I 0 H9 in
            False_ind (n0 = n'.+2 -> R_div2 n' _res -> n'.+2 < 2) H10) n H8) H5
          H6 H3 H4
    end in
  H3 (erefl n) (erefl 0)) (R_div2_correct n 0 H1)) H0
     : forall n : nat, div2 n = 0 -> n < 2
*)

さて、Functional Scheme でうまくいかなかった、div2' を Function でやってみると、 これもやはり同じようなメッセージでうまくいかない。

Function div2' (n:nat) : nat :=
  let f m :=
    match m with
    | O => 0
    | S m' => S (div2' m')
    end
  in
  match n with
  | O => 0
  | S n' => f n'
  end. (*
div2' is defined
div2' is recursively defined (decreasing on 1st argument)
Cannot define graph(s) for div2' [funind-cannot-define-graph,funind]
Cannot build inversion information [funind-cannot-build-inversion,funind]
*)

マニュアル (3.2.3 Advanced recursive functions) を読んだところ、 "Warning: Cannot define graph for ident." の説明があった。 R_ident (ここの例だと R_div2 とか) を graph relation と呼んでいて、その生成に失敗したときのメッセージと書いてある。 そして、それが失敗するのは (典型的には) 依存型のパターンマッチングを行っている場合と、 定義が pattern matching tree でない場合だという。

pattern matching tree についてはさらに少し説明があって、 "pure pattern matching tree (match ... with) with applications only at the end of each branch." と書いてある。

match 式で (分岐が) 作られた純粋な木で、関数適用は最後の分岐だけに現れる、ということだから、 たしかに let で括り出したものはそういう説明からは外れる気がする。

2019-04-30 (Tue)

#1 Functional Scheme の論文

Functional Scheme に関する論文を探してみたところ、たぶん以下だと思う。

Gilles Barthe, Pierre Courtieu. Efficient reasoning about executable specifications in Coq. Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002 Hampton, VA, USA, August 20–23, 2002 Proceedings (pp.31-46). http://cedric.cnam.fr/~courtiep/papers/barthe-courtieu-tphol2002.pdf

文法が今の Coq と違うようだ。

それはそれとして、let の束縛の中に match (古い文法では Case) が出てくる場合は 考慮されていない感じではある。

しかし、グラフについては触れてないと思う。

2019-04-26 (Fri)

#1 Coq の Functional Scheme で対応できない再帰関数

どんな再帰関数でも Functional Scheme で induction principle を作れるのか、 というと、きっと無理だと思う。

で、具体的な例を作ってみた。

From mathcomp Require Import all_ssreflect.
Require Import FunInd.

Fixpoint div2 (n:nat) : nat :=
match n with
| O => 0
| S O => 0
| S (S n') => S (div2 n')
end.

以下の div2' が Functional Scheme が対応できない例である。

Fixpoint div2' (n:nat) : nat :=
let f m :=
  match m with
  | O => 0
  | S m' => S (div2' m')
  end
in
match n with
| O => 0
| S n' => f n'
end.

div2' は、じつは div2 と convertible である。 (内側の match を関数として括り出しただけなので)

Goal div2 = div2'. Proof. reflexivity. Qed.

で、div2' に Functional Scheme を適用すると、エラーになる。

Fail Functional Scheme div2'_ind := Induction for div2' Sort Prop.
(* Cannot define graph(s) for div2' *)

マニュアル (5.2.2 Generation of induction principles with Functional Scheme) を 読み直してみたが、どういう場合にうまくいって、どういう場合にうまくいかないのかは 書いてないなぁ。

エラーメッセージをみると、なんかグラフを作れないみたいなので、 そのグラフがどういうものなのかわかればいいのかな。

2019-04-25 (Thu)

#1 Coq の Functional Scheme を使ってみる

再帰関数に対して、その関数専用の induction principle を作る Functional Scheme というコマンドがある。

試しに使ってみよう。

まず、div2 関数を定義する。

From mathcomp Require Import all_ssreflect.
Require Import FunInd.

Fixpoint div2 (n:nat) : nat :=
match n with
| O => 0
| S O => 0
| S (S n') => S (div2 n')
end.

この関数はリファレンスマニュアルに書いてあるとおりの例である。

ここで、forall m, div2 m <= m という命題を証明したいとしよう。 (この命題もリファレンスマニュアルに書いてあるのとほぼ同じだが、 こっちは ssreflect なので実際には微妙に異なる)

普通に (m について) 帰納法を使うとうまくいかない。 これは、(ペアノの自然数としての) m の構造と、 div2 の再帰の構造が異なるからである。 div2 n <= n を仮定して div2 n.+1 <= n.+1 を証明しろといわれても困る。 .+1 じゃなくて .+2 ならうまくいくんだけど。

Goal forall m, div2 m <= m.
Proof.
  elim.
    by [].
  move=> n.
  (* div2 n <= n -> div2 n.+1 <= n.+1 *)
  simpl.
Abort.

個人的に、こういうときには完全帰納法をつかっていた。 自然数に対する完全帰納法は Wf_nat.lt_wf_ind にあるので、 これを使えば証明できる。

Goal forall m, div2 m <= m.
Proof.
  move=> m.
  pattern m.
  apply Wf_nat.lt_wf_ind => {m}.
  case; first by [].
  case; first by [].
  move=> n IH /=.
  apply ltnW.
  apply IH.
  by apply/ltP.
Qed.

まぁ、自然数の場合は完全帰納法でとくに問題はないと思うのだが、 自然数でない場合には完全帰納法 (ないし整礎帰納法) が あらかじめ用意されているとは限らない。

そういうときのために、 関数の構造にあわせた induction principle を作ってくれる Functional Scheme があるのだろう。たぶん。

というわけで、Functional Scheme を使ってみよう。 呼び出してみると、div2_equation と div2_ind が定義されたと出てくる。

Functional Scheme div2_ind := Induction for div2 Sort Prop.
(*
div2_equation is defined
div2_ind is defined
*)

div2_equation と div2_ind がどういうものか表示してみる。 div2_equation が div2 を一段階展開する書き換えに使える定理になっている。 div2_ind は div2 の構造に対応した induction principle になっている。

About div2_equation. (* div2_equation :
forall n : nat, div2 n = match n with
                         | n'.+2 => (div2 n').+1
                         | _ => 0
                         end
*)

About div2_ind. (* div2_ind :
forall P : nat -> nat -> Prop,
(forall n : nat, n = 0 -> P 0 0) ->
(forall n n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0) ->
(forall n n0 : nat,
 n = n0.+1 ->
 forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
forall n : nat, P n (div2 n)
*)

div2_ind を使うと、div2 m <= m は以下のように証明できる。

Goal forall m, div2 m <= m.
Proof.
  move=> m.
  functional induction (div2 m).
      by [].
    by [].
  by apply ltnW.
Qed.

さて、div2_ind の中身がどんなものか表示してみると、ちょっと大きくて読みたくない感じである。

Print div2_ind. (* div2_ind =
fun (P : nat -> nat -> Prop) (f1 : forall n : nat, n = 0 -> P 0 0)
  (f0 : forall n n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0)
  (f : forall n n0 : nat,
       n = n0.+1 ->
       forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) =>
fix div3 (n : nat) : P n (div2 n) :=
  @eq_ind_r nat match n with
                | n'.+2 => (div2 n').+1
                | _ => 0
                end [eta P n]
    (let f2 : n = 0 -> P 0 0 := f1 n in
     let f3 : forall n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0 := f0 n in
     let f4 :
       forall n0 : nat,
       n = n0.+1 ->
       forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1 :=
       f n in
     match
       n as n0
       return
         (n = n0 ->
          (forall n1 : nat,
           n0 = n1.+1 ->
           forall n' : nat, n1 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
          (forall n1 : nat, n0 = n1.+1 -> n1 = 0 -> P 1 0) ->
          (n0 = 0 -> P 0 0) ->
          P n0 match n0 with
               | n'.+2 => (div2 n').+1
               | _ => 0
               end)
     with
     | 0 =>
         fun (_ : n = 0)
           (_ : forall n0 : nat,
                0 = n0.+1 ->
                forall n' : nat,
                n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1)
           (_ : forall n0 : nat, 0 = n0.+1 -> n0 = 0 -> P 1 0)
           (f7 : 0 = 0 -> P 0 0) => unkeyed (f7 (erefl 0))
     | n0.+1 =>
         fun (_ : n = n0.+1)
           (f5 : forall n1 : nat,
                 n0.+1 = n1.+1 ->
                 forall n' : nat,
                 n1 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1)
           (f6 : forall n1 : nat, n0.+1 = n1.+1 -> n1 = 0 -> P 1 0)
           (_ : n0.+1 = 0 -> P 0 0) =>
         let f8 : n0 = 0 -> P 1 0 :=
           let n1 := n0 in let H : n0.+1 = n1.+1 := erefl n0.+1 in f6 n1 H in
         let f9 :
           forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1 :=
           let n1 := n0 in let H : n0.+1 = n1.+1 := erefl n0.+1 in f5 n1 H in
         match
           n0 as n1
           return
             (n0 = n1 ->
              (n1 = 0 -> P 1 0) ->
              (forall n' : nat,
               n1 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
              P n1.+1 match n1 with
                      | 0 => 0
                      | n'.+1 => (div2 n').+1
                      end)
         with
         | 0 =>
             fun (_ : n0 = 0) (f10 : 0 = 0 -> P 1 0)
               (_ : forall n' : nat,
                    0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) =>
             unkeyed (f10 (erefl 0))
         | n1.+1 =>
             fun (_ : n0 = n1.+1) (_ : n1.+1 = 0 -> P 1 0)
               (f11 : forall n' : nat,
                      n1.+1 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) =>
             let f12 : P n1 (div2 n1) -> P n1.+2 (div2 n1).+1 :=
               let n' := n1 in let H : n1.+1 = n'.+1 := erefl n1.+1 in f11 n' H
               in
             unkeyed (let Hrec : P n1 (div2 n1) := div3 n1 in f12 Hrec)
         end (erefl n0) f8 f9
     end (erefl n) f4 f3 f2) (div2 n) (div2_equation n)
     : forall P : nat -> nat -> Prop,
       (forall n : nat, n = 0 -> P 0 0) ->
       (forall n n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0) ->
       (forall n n0 : nat,
        n = n0.+1 ->
        forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
       forall n : nat, P n (div2 n)

*)

とりあえず Print Assumptions div2_ind. として公理に依存していないことは確認できる。

Print Assumptions div2_ind. (* Closed under the global context *)

div2_equation も表示してみると、こちらはそれほど大きくない。

Print div2_equation. (* div2_equation =
fun n : nat =>
match
  n as n0 return (div2 n0 = match n0 with
                            | n'.+2 => (div2 n').+1
                            | _ => 0
                            end)
with
| 0 => erefl 0
| n0.+1 => erefl match n0 with
                 | 0 => 0
                 | n'.+1 => (div2 n').+1
                 end
end
     : forall n : nat, div2 n = match n with
                                | n'.+2 => (div2 n').+1
                                | _ => 0
                                end
*)

div2_equation 相当の定理を tactic で証明しなおしてみると、以下のようになる。 左辺を一段階展開したものが右辺なので、 そのまま reflexivity 一発、といきそうなものだが実際にはそうはいかない。 再帰関数 (fix項) を展開するには (展開してないものと展開したものが convertible になるという iota reduction では) decreasing argument の頭部が constructor であるという条件が必要で、 そのためには、div2 の (内部にある fix項の) 引数の n を場合分けして 頭部を constructor にする必要がある。 そうしてしまえばあとは問題ない。

Lemma div2_equation' : forall n : nat,
    div2 n = match n with
             | n'.+2 => (div2 n').+1
             | _ => 0
             end.
Proof.
  by case.
Defined.

もともとの div2_equation と証明し直した div2_equation' は以下のように等しい。 (というか、等しくなるように証明を作ったのだが)

Goal div2_equation = div2_equation'. Proof. reflexivity. Qed.

div2_ind も同様に証明しなおしてみよう。 大きな証明項は読みたくないのだが、がんばって読んでやってみたところ、 証明項に比べてずいぶんと小さくなった。

Lemma div2_ind' :  forall P : nat -> nat -> Prop,
       (forall n : nat, n = 0 -> P 0 0) ->
       (forall n n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0) ->
       (forall n n0 : nat,
        n = n0.+1 ->
        forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
       forall n : nat, P n (div2 n).
Proof.
  move=> P H0 H1 H2.
  fix IH 1 => n.
  rewrite div2_equation'.
  move: (H2 n) (H1 n) (H0 n) => {H2 H1 H0}.
  case_eq n => {n} [|n] _ H2 H1 H0; first by apply H0.
  move: (H1 n erefl) (H2 n erefl) => {H2 H1 H0}.
  case_eq n => {n} [|n] _ H1 H2; first by apply H1.
  apply (H2 n erefl).
  by apply IH.
Defined.

これも、元の証明 div2_ind と証明し直した div2_ind' は等しくなっていることが確認できる。

Goal div2_ind = div2_ind'. Proof. reflexivity. Qed.

div2_ind' の (tactic のほうの) 証明を見直すと、結局、 (fix tactic で作った) 再帰関数の中で、まず div2_equation で一段階 div2 を展開し、 引数を (div2 の分岐の構造と同じ構造で) 場合分けして証明を行っていることがわかる。

2019-04-26: 証明を簡単にしたり、説明を書き足したりした

2019-04-20 (Sat)

#1 RubyKaigi 2019 After Party

以下の発表を行った。

autoloadの話

2019-04-19 (Fri)

#1 RubyKaigi 2019 day 2

以下の発表を行った。

What is Domain Specific Language?

2019-03-27 (Wed)

#1 copy-on-write fork による親プロセスの速度低下

copy-on-write な fork では、 fork した時点で、親プロセスと子プロセスがメモリを read only で共有し、 write 時には page fault が起きてページをコピーして write 可能にした後、write を続行する。

ここで、子プロセスが exec した後は、そのメモリを使っているのは親プロセスだけになるのでコピーは不要になるが、 write しようとしたときに page fault が起きることは変わらない。

このあたりの動作は以下の NetBSD のドキュメントに動作が記述されている。 (もしかしたら、OSによっては微妙に動作が違うこともあるかもしれないけれど)

NetBSD ドキュメンテーション: なぜ伝統的な vfork()を実装したのか

この、親プロセスでメモリが read only になったままで、 書き込みのたびに page fault が起きるという動作は (コピーは起きないにせよ) かなり遅くなることもあるのではないか、 という疑問を感じた。

というわけで (Linux で) 試してみた。

% uname -mrsv
Linux 4.19.0-2-amd64 #1 SMP Debian 4.19.16-1 (2019-01-17) x86_64

まず、Transparent huge page (THP) を disable する。 (Ruby 2.6 では内部で THP を disable している ([Feature #14705], r63253) のだが、Ruby 2.5 以前ではしてないので、これは 4K page という動作で揃えている)

# echo never > /sys/kernel/mm/transparent_hugepage/enabled

この状態で、大きなメモリに (各ページ毎に 1byte の) 書き込みを行う時間を測定した。 10回測定し、fork してからまた 10回測定する。

以下の結果をみると、明らかに fork 直後の回が 10倍くらい遅くなっている。

% ruby-2.6.2 -e '
pagesize = 4096
n = 100000
s = "x" * (n*pagesize)
10.times {
  t1 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  n.times {|i| s.setbyte(i*pagesize,0) }
  t2 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  t = t2-t1
  printf "%.8f %s\n", t, "*"*(t*1000).to_i
}
puts
Process.wait fork {}
10.times {
  t1 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  n.times {|i| s.setbyte(i*pagesize,0) }
  t2 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  t = t2-t1
  printf "%.8f %s\n", t, "*"*(t*1000).to_i
}'
0.00733914 *******
0.00699243 ******
0.00674534 ******
0.00777585 *******
0.00836382 ********
0.00729977 *******
0.00705439 *******
0.00687936 ******
0.00667030 ******
0.00662619 ******

0.06490101 ****************************************************************
0.00664682 ******
0.00662405 ******
0.00670339 ******
0.00657027 ******
0.00700166 *******
0.00666423 ******
0.00650362 ******
0.00669207 ******
0.00651883 ******

次に、fork のかわりに、system("true") を使うと、以下のように、fork と違って遅くならない。 これは、vfork を使っているからだろう。

% ruby-2.6.2 -e '
pagesize = 4096
n = 100000
s = "x" * (n*pagesize)
10.times {
  t1 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  n.times {|i| s.setbyte(i*pagesize,0) }
  t2 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  t = t2-t1
  printf "%.8f %s\n", t, "*"*(t*1000).to_i
}
puts
system("true")
10.times {
  t1 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  n.times {|i| s.setbyte(i*pagesize,0) }
  t2 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  t = t2-t1
  printf "%.8f %s\n", t, "*"*(t*1000).to_i
}'
0.00758229 *******
0.00701581 *******
0.00680411 ******
0.00673921 ******
0.00668358 ******
0.00671528 ******
0.00657470 ******
0.00660746 ******
0.00661486 ******
0.00670212 ******

0.00674013 ******
0.00700635 *******
0.00678113 ******
0.00657952 ******
0.00659784 ******
0.00678082 ******
0.00658584 ******
0.00661802 ******
0.00653398 ******
0.00654583 ******

vfork を使うようになったのは ruby 2.2 からなので、 ruby 2.1.10 で試すと、これは system でも遅くなる。

% ruby-2.1.10 -e '
pagesize = 4096
n = 100000
s = "x" * (n*pagesize)
10.times {
  t1 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  n.times {|i| s.setbyte(i*pagesize,0) }
  t2 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  t = t2-t1
  printf "%.8f %s\n", t, "*"*(t*1000).to_i
}
puts
system("true")
10.times {
  t1 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  n.times {|i| s.setbyte(i*pagesize,0) }
  t2 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  t = t2-t1
  printf "%.8f %s\n", t, "*"*(t*1000).to_i
}'
0.00678418 ******
0.00661911 ******
0.00631097 ******
0.00615733 ******
0.00612787 ******
0.00625961 ******
0.00616606 ******
0.00614166 ******
0.00615436 ******
0.00616540 ******

0.06327575 ***************************************************************
0.00622857 ******
0.00624134 ******
0.00617376 ******
0.00617710 ******
0.00638290 ******
0.00618077 ******
0.00615743 ******
0.00615407 ******
0.00613252 ******

ここで、Transparent huge page (THP) を enable する。

# echo always > /sys/kernel/mm/transparent_hugepage/enabled

すると、そんなに遅くならないようになる。 THP って効く (ことがある) のだな。

% ruby-2.1.10 -e '
pagesize = 4096
n = 100000
s = "x" * (n*pagesize)
10.times {
  t1 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  n.times {|i| s.setbyte(i*pagesize,0) }
  t2 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  t = t2-t1
  printf "%.8f %s\n", t, "*"*(t*1000).to_i
}
puts
system("true")
10.times {
  t1 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  n.times {|i| s.setbyte(i*pagesize,0) }
  t2 = Process.clock_gettime(Process::CLOCK_THREAD_CPUTIME_ID)
  t = t2-t1
  printf "%.8f %s\n", t, "*"*(t*1000).to_i
}'
0.00914092 *********
0.00847733 ********
0.00838931 ********
0.00775660 *******
0.00810754 ********
0.00699371 ******
0.00679120 ******
0.00660573 ******
0.00733054 *******
0.00661029 ******

0.00728163 *******
0.00663571 ******
0.00679257 ******
0.00704892 *******
0.00651190 ******
0.00643143 ******
0.00643470 ******
0.00717451 *******
0.00673541 ******
0.00647267 ******

• 2000: 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2001: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2002: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2003: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2004: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2005: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2006: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2007: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2008: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2009: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2010: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2011: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2012: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2013: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2014: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2015: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2016: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2017: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2018: 01, 02, 03, 04, 05, 06, 07, 08, 09, 10, 11, 12
• 2019: 01, 02, 03, 04, 05
• latest