天泣記

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-05-31 (Fri)

#1 all-ruby の rake sync が動かなかった --- 1年で最大1回しかないデバッグの機会を逃さない

Ruby 2.7.0 preview1 が出たので、 all-ruby でいつものように (versions/2.7.0-preview1.json を追加するため) rake sync としたが なんか追加されない。

Ruby 2.7.0 preview1 は 2.7 系列のはじめての tarball なので、 <URL:https://cache.ruby-lang.org/pub/ruby/> の下の 2.7 というディレクトリを検出しなければならない。

そのために <URL:https://cache.ruby-lang.org/pub/ruby/> をスクレイピングしているのだが、 HTML 記述がちょっと変化して検出できなかったようだ。

以前から存在するディレクトリは　versions/*.json から調べられるので、 これは安定して (スクレイピングに依存せずに) 求められる。

ということで、スクレイピングに依存しているのは新しいディレクトリができるときだけで、 新しいディレクトリができるのは (Ruby では1年に1回新しい系列ができるので) 1年に1回なので、 トラブルが起きるのも最大で1年に1回だが、 デバッグできる機会もそれしかない。

そのため、workaround として versions/2.7.0-preview1.json を手動で作る、としてしまうと、 デバッグの機会を 1年逃すことになる。

ということで、workaround の誘惑を断ちきり、デバッグしてから、Ruby 2.7.0 preview1 を install した。

[latest]