天泣記

2017-06-04 (Sun)

#1 Coq の Program で定義した div2 はとても遅い

Coq の Program で定義した div2 を実行して時間を測ってみた。

Time Eval vm_compute in div2 1. (* 0.012 secs (0.u,0.s) *)
Time Eval vm_compute in div2 2. (* 0.338 secs (0.243u,0.008s) *)
Time Eval vm_compute in div2 3. (* 9.522 secs (5.68u,0.3s) *)

3 / 2 で 9秒というのはなんというか、信じ難いほど遅い。まぁ、かなり大きな証明項を作るからしょうがないのかもしれない。

2017-05-30 (Tue)

#1 Coq の Program を試した

Coq には Program という機能があるらしいので、ちょっとためしてみた。

リファレンスマニュアル に書いてあった例に、書いてなかった証明を補完して、最後まで通るようにしてみた。

Require Import Program.
Require Import Arith.

Program Definition id (n : nat) : { x : nat | x = n } :=
        if dec (leb n 0) then 0
        else S (pred n).

Obligation 1.
Proof.
  apply Nat.leb_le in H.
  inversion H.
  auto.
Qed.

Obligation 2.
Proof.
  apply leb_complete_conv in H.
  inversion H; auto.
Qed.

Extraction id.
(*
let id n =
  match sumbool_of_bool (Nat.leb n O) with
  | Left -> O
  | Right -> S (pred n)
*)

Program Fixpoint div2 (n : nat) {measure n} :
        { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
        match n with
        | S (S p) => S (div2 p)
        | _ => O
        end.

Obligation 2.
Proof.
  simpl.
  destruct (div2 p (le_S (S p) (S p) (le_n (S p)))).
  simpl.
  rewrite<- plus_n_O in o.
  rewrite<- plus_n_Sm.
  rewrite<- plus_n_O.
  destruct o.
    left.
    auto.
  right.
  rewrite H.
  auto.
Qed.

Obligation 3.
Proof.
  clear div2.
  destruct n.
    left; auto.
  destruct n.
    right; auto.
  exfalso.
  apply (H n).
  reflexivity.
Qed.

Extraction div2.
(*
let rec div2 x =
  let div3 = fun n -> div2 n in
  (match x with
   | O -> O
   | S n ->
     (match n with
      | O -> O
      | S p -> S (div3 p)))
*)

試した結果 (あとマニュアルも読んだ結果)、これは sig 型を使いやすくしようという話だと理解した。

sig 型というのは { x : T | P x } みたいな、P が成り立つ T 型の値の集合、つまり T の部分集合を表現するやつである。プログラムの中ではいつでも T 型の式を { x : T | P x } 型の式として扱えて、でもそうやって扱ったところで P が成り立つことは後で証明しないといけない、という仕掛けのようだ。(なお、こういう、述語で値を制限する型は refinement type とも言うらしい。)

なお、Extraction すると、div2 のなかの div3 のように、変なもの (ソースにはない、証明のための変形の残骸) が出ることがあるようだ。

もうちょっと単純な例を作ってみた。(あと、こっちでは SSreflect を使ってみた)

From mathcomp Require Import ssreflect eqtype ssrbool ssrnat.
Require Import Program.

Program Definition f (n : { x : nat | x <= 3 }) : { x : nat | x <= 10 } := n.

Next Obligation.
Proof.
  by apply (@leq_trans 3).
Qed.

Print f.
(*
f =
fun n : {x : nat | x <= 3} =>
exist (fun x : nat => x <= 10) (` n)
  ((fun n0 : {x : nat | x <= 3} => f_obligation_1 n0) n)
     : {x : nat | x <= 3} -> {x : nat | x <= 10}
*)

これだと、3以下な引数 n を受け取って、10以下の値を返す、という振る舞いを型として記述できている。

2017-05-28 (Sun)

#1 Coq で完全帰納法 (SSReflect なし)

ついでに、Coq で (SSReflect を使わずに) 完全帰納法を証明してみた。

Theorem nat_complete_induction
  (P : nat -> Prop)
  (H : forall n, (forall k, (k < n -> P k)) -> P n)
  (n : nat): P n.
Proof.
  apply H.
  induction n.
    intros k Hk.
    inversion Hk.
  intros k Hk.
  inversion Hk.
    apply H.
    exact IHn.
  apply IHn.
  exact H1.
Qed.

証明の流れは当然同じ。うぅむ、SSReflect でない Coq のやりかたを忘れてしまっているな。(まぁ、SSReflect を使いはじめる前にたくさんは勉強していない気もする)

あ、auto を使えばこれだけでもいけるか。

Theorem nat_complete_induction
  (P : nat -> Prop)
  (H : forall n, (forall k, (k < n -> P k)) -> P n)
  (n : nat): P n.
Proof.
  apply H.
  induction n.
    intros k Hk.
    inversion Hk.
  intros k Hk.
  inversion Hk; auto.
Qed.

2017-05-27 (Sat)

#1 Coq/SSReflect で完全帰納法

ちょっと必要になるかと思って、自然数の完全帰納法 (complete induction, strong induction, 累積帰納法, course of values induction などいろいろ呼び方があるらしい) を証明したのだが、けっきょく不要だった。消してしまうのもなんなのでメモしておく。

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.

Theorem nat_complete_induction
  (P : nat -> Prop)
  (H : forall n, (forall k, (k < n -> P k)) -> P n)
  (n : nat): P n.
Proof.
  apply H.
  elim: n => [|i IH k]; first by [].
  rewrite ltnS leq_eqVlt => /orP.
  case=> [/eqP ->|]; last by apply IH.
  by apply: H IH.
Qed.

帰納法を適用する前に H を適用しておかないとうまくいかないことに気がつくのにしばらく時間がかかった。

前提が n 未満の k すべてについて成り立つという形なので、結論も n 未満の k すべてについて成り立つという形にしておかなければならない。まぁ、こう書いてしまうと自明に感じられて、なかなかうまくできなかった自分がマヌケに感じられる。

追記: どうやら標準ライブラリの Coq.Init.Wf に (もっと一般化された形で) すでに存在するようだ。(Wf は well-founded の略で、日本語だと整礎という。整礎関係を使った帰納法を整礎帰納法という。)

Require Import Arith Wf.
Check (well_founded_ind lt_wf).
(*
  well_founded_ind lt_wf
       : forall P : nat -> Prop,
         (forall x : nat, (forall y : nat, y < x -> P y) -> P x) ->
         forall a : nat, P a
*)

さらに、Coq.Arith.Wf_nat に nat 版がはじめから用意されているようだ。

Require Import Wf_nat.
Check lt_wf_ind.
(*
  lt_wf_ind
       : forall (n : nat) (P : nat -> Prop),
         (forall n0 : nat, (forall m : nat, m < n0 -> P m) -> P n0) -> P n
*)

たしかにこれらは nat_complete_induction と同じような型になっている。(いや、こっちは SSReflect じゃないから本当はけっこう違うんだけど)

参考:

2017-05-17 (Wed)

#2 arity が変化する関数 (依存型) を Scheme に extract する

ついでに、Scheme もやってみた。

Haskell のに対して、最後のところを以下のように変える。

Extraction Language Scheme.
Extraction M.

なお、ExtrOcamlBasic.v や ExtrHaskellBasic.v といった設定は Scheme にはないようだ。

結果は以下のようになる。

;; This extracted scheme code relies on some additional macros
;; available at http://www.pps.univ-paris-diderot.fr/~letouzey/scheme
(load "macros_extr.scm")


(define add (lambdas (n m)
  (match n
     ((O) m)
     ((S p) `(S ,(@ add p m))))))

(define f~ (lambdas (acc n)
  (match n
     ((O) acc)
     ((S n~) (lambda (v) (@ f~ (@ add acc v) n~))))))

(define f (lambda (n) (@ f~ `(O) n)))

(define g0 (f `(O)))

(define g1 (@ f `(S ,`(O)) `(S ,`(O))))

(define g2 (@ f `(S ,`(S ,`(O))) `(S ,`(O)) `(S ,`(S ,`(O)))))

(define g3
  (@ f `(S ,`(S ,`(S ,`(O)))) `(S ,`(O)) `(S ,`(S ,`(O))) `(S ,`(S ,`(S ,`(O))))))

(define g4
  (@ f `(S ,`(S ,`(S ,`(S ,`(O))))) `(S ,`(O)) `(S ,`(S ,`(O))) `(S ,`(S ,`(S ,`(O))))
    `(S ,`(S ,`(S ,`(S ,`(O)))))))

(define h1 (f `(S ,`(O))))

(define h2 (f `(S ,`(S ,`(O)))))

(define h3 (f `(S ,`(S ,`(S ,`(O))))))

どうもライブラリが必要なようなので、とってきて動かしてみる。

% gosh
gosh> (add-load-path ".")
("." "/usr/share/gauche-0.9/site/lib" "/usr/share/gauche-0.9/0.9.4/lib" "/usr/share/gauche/site/lib" "/usr/share/gauche/0.9/lib")
gosh> (load "a.scm")
#t
gosh> g0
(O)
gosh> g1
(S (O))
gosh> g2
(S (S (S (O))))
gosh> g3
(S (S (S (S (S (S (O)))))))
gosh> h1
#<closure (f~ f~ f~ f~)>
gosh> (h1 '(O))
(O)
gosh> (h1 '(S (O)))
(S (O))
gosh> (h2 '(S (O)))
#<closure (f~ f~ f~ f~)>
gosh> ((h2 '(S (O))) '(S (O)))
(S (S (O)))
gosh> (((h3 '(S (O))) '(S (O))) '(S (O)))
(S (S (S (O))))
gosh>

ふつうの整数を使う機能も用意されていないようで、気合が入っていない。

#1 arity が変化する関数 (依存型) を Haskell に extract する

ふと、関数ひとつずつじゃなくて、まとめて extract すれば Coq がうまいコードを吐いてくれるのではないかと思ってやってみたら、Haskell でも動いた。

Module M.
Fixpoint dt n :=
  match n with
  | O => nat
  | S n' => nat -> dt n'
  end.

Fixpoint f' acc n : dt n :=
  match n with
  | O => acc
  | S n' => fun v => f' (acc+v) n'
  end.

Definition f n : dt n := f' 0 n.

Definition g0 := f 0.
Definition g1 := f 1 1.
Definition g2 := f 2 1 2.
Definition g3 := f 3 1 2 3.
Definition g4 := f 4 1 2 3 4.

Definition h1 := f 1.
Definition h2 := f 2.
Definition h3 := f 3.
End M.

Extraction Language Haskell.
Require Import ExtrHaskellBasic.
Require Import ExtrHaskellNatInt.

Extraction M.

とすると、以下のコードが吐かれる。

{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module Main where

import qualified Prelude

#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
import qualified GHC.Prim
#else
-- HUGS
import qualified IOExts
#endif

#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif

#ifdef __GLASGOW_HASKELL__
type Any = GHC.Prim.Any
#else
-- HUGS
type Any = ()
#endif

type Dt = Any

f' :: Prelude.Int -> Prelude.Int -> Dt
f' acc n =
  (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    unsafeCoerce acc)
    (\n' ->
    unsafeCoerce (\v -> f' ((Prelude.+) acc v) n'))
    n

f :: Prelude.Int -> Dt
f n =
  f' 0 n

g0 :: Prelude.Int
g0 =
  unsafeCoerce f 0

g1 :: Prelude.Int
g1 =
  unsafeCoerce f (Prelude.succ 0) (Prelude.succ 0)

g2 :: Prelude.Int
g2 =
  unsafeCoerce f (Prelude.succ (Prelude.succ 0)) (Prelude.succ 0) (Prelude.succ
    (Prelude.succ 0))

g3 :: Prelude.Int
g3 =
  unsafeCoerce f (Prelude.succ (Prelude.succ (Prelude.succ 0))) (Prelude.succ 0)
    (Prelude.succ (Prelude.succ 0)) (Prelude.succ (Prelude.succ (Prelude.succ 0)))

g4 :: Prelude.Int
g4 =
  unsafeCoerce f (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ 0))))
    (Prelude.succ 0) (Prelude.succ (Prelude.succ 0)) (Prelude.succ (Prelude.succ
    (Prelude.succ 0))) (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ 0))))

h1 :: Prelude.Int -> Prelude.Int
h1 =
  unsafeCoerce f (Prelude.succ 0)

h2 :: Prelude.Int -> Prelude.Int -> Prelude.Int
h2 =
  unsafeCoerce f (Prelude.succ (Prelude.succ 0))

h3 :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int
h3 =
  unsafeCoerce f (Prelude.succ (Prelude.succ (Prelude.succ 0)))

これを a.hs に入れて、ghci a.hs とすると、動いた。

% ghci a.hs
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( a.hs, interpreted )
Ok, modules loaded: Main.
*Main> g0
0
*Main> g1
1
*Main> g2
3
*Main> g3
6
*Main> h0

<interactive>:6:1:
    Not in scope: `h0'
    Perhaps you meant one of these:
      `g0' (line 48), `h1' (line 72), `h2' (line 76)
*Main> h1 1
1
*Main> h2 1 2
3
*Main> h3 1 2 3
6

吐かれたコードを見ると、呼び出す側でも unsafeCoerce が必要なようだ。

2017-05-08 (Mon)

#1 依存型の型検査

ところで、f' の定義で、型を dt n から dt (n + 0) に変えても型検査を通る。

Fixpoint dt n :=
  match n with
  | O => nat
  | S n' => nat -> dt n'
  end.

Fixpoint f' acc n : dt (n + 0) :=
  match n with
  | O => acc
  | S n' => fun v => f' (acc+v) n'
  end.

これはどういうことだろうか。

n + 0 は n と convertible でない。convertible というのは Coq が項を同じものとみなすということであり、おおざっぱにいえば、計算を進められる限り進めて同じ項になるかどうかということで判定する。

ここで使っている二項演算子の + は Nat.add であり、Nat.add a b は a を減らしながら再帰するという定義である。n が変数であるため (減らせるかどうかわからないので)、n + 0 はそれ以上計算を進められないので、n にはならない。(n + 0 と n が等しいことを示すには帰納法が必要であり、証明済みの定理として plus_n_O があるが、Coq は convertible の判断においては定理を使わない。)

Print f' として f' がどんな項になっているのか表示してみる。

f' =
fix f' (acc : dt (0 + 0)) (n : nat) {struct n} : dt (n + 0) :=
  match n as n0 return (dt (n0 + 0)) with
  | 0 => acc
  | S n' => fun v : nat => f' (acc + v) n'
  end
     : dt (0 + 0) -> forall n : nat, dt (n + 0)

まず気になるのが acc が nat じゃなくて dt (0 + 0) になっていることだが、dt (0 + 0) は nat と convertible なので間違いではない、な。(仮引数のところで (acc : nat) と書いておくと nat になるし。)

match で n が 0 のときは、n0 が 0 で、dt (n0 + 0) の n0 を 0 に置き換えると dt (0 + 0) となって、acc はその型である、と。acc が dt (0 + 0) になったのはそこから来たのだろう、たぶん。

match で n が S n' のときは、return のところに書いてある型から考えると dt ((S n') + 0) であるはずで、これは (Nat.add の計算を進めて) dt (S (n' + 0)) と convertible であり、さらに (dt の計算を進めて) nat -> dt (n' + 0) と convertible である。中身の式から考えると f' の返り値の型は dt (n' + 0) で、それが lambda 式の中に入っているから nat -> dt (n' + 0) となる。return のところに書いてある型と中身の式から求めた型が convertible だから、型検査は通っておかしくない、か。なるほど。

以下のように n + 1 - 1 にすると型検査を通らなくなる。

Fixpoint f' acc n : dt (n + 1 - 1) :=
  match n with
  | O => acc
  | S n' => fun v => f' (acc+v) n'
  end.

Error: The type of this term is a product while it is expected to be
 "dt (S n' + 1 - 1)".

エラーメッセージに "this term" とあるが、これは (統合開発環境の) ソース内で、"fun v => f' (acc+v) n'" のところに underline が引かれてそこを指している。これは関数なので、型は関数型(これはじつは product 型ともいう)である。

return のほうから得られる型は S n' + 1 - 1 の計算を n' + 1 - 0 までしか進められず、外側に S が出てこなくて dt の計算を進めることができず、関数型までたどりつけないため、型が合わないのだろう。

2017-05-01 (Mon)

#2 arity が変化する関数 (依存型)

ふと思い立って、Coq で依存型を使って arity が変化する関数を書いてみた。

Fixpoint dt n :=
  match n with
  | O => nat
  | S n' => nat -> dt n'
  end.

Fixpoint f' acc n : dt n :=
  match n with
  | O => acc
  | S n' => fun v => f' (acc+v) n'
  end.

Definition f n : dt n := f' 0 n.

Goal f 0 = 0. Proof. reflexivity. Qed.
Goal f 1 10 = 10. Proof. reflexivity. Qed.
Goal f 2 10 20 = 30. Proof. reflexivity. Qed.
Goal f 3 10 20 30 = 60. Proof. reflexivity. Qed.
Goal f 9 10 20 30 40 50 60 70 80 90 = 450. Proof. reflexivity. Qed.

f は最初の引数でそれに続く引数の数を指定し、その数だけ nat を与えるとそれらの和を返す。最初の引数の値に依存して、0 なら nat を返し、そうでなければ関数を返す、という型なので、依存型というわけである。

Goal で確認してみるとちゃんと動いているようである。

ところで、Goal って unit test みたいですね。

さて、extraction もできないわけではない。

Require Import ExtrOcamlBasic.
Require Import ExtrOcamlNatInt.
Extraction f'.
Extraction f.

で、OCaml で動かすとなんか警告がでるが、動くようである。(int に cast しないと <poly> と表示されて中身がわからないが)

# let add = (+);;
val add : int -> int -> int = <fun>
# let rec f' acc n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ ->
    Obj.magic acc)
    (fun n' ->
    Obj.magic (fun v -> f' (add acc v) n'))
    n            ;;
            val f' : int -> int -> 'a = <fun>
# let f n =
  f' 0 n  ;;
  val f : int -> 'a = <fun>
# f 0;;
- : 'a = <poly>
# (f 0 : int);;
- : int = 0
# (f 1 10 : int);;
Warning 20: this argument will not be used by the function.
- : int = 10
# (f 2 10 20 : int);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
- : int = 30
# (f 9 10 20 30 40 50 60 70 80 90 : int);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
- : int = 450

まぁ、Obj.magic を使っていることからも分かるように、安全ではない。以下のように余計に引数を与えると SEGV する。

# f 0 100;;
Warning 20: this argument will not be used by the function.
zsh: segmentation fault  ocaml

Coq の Extraction は OCaml, Haskell, Scheme (と JSON) をサポートしている。Scheme なら型で問題になることはないだろうから、もうひとつ Haskell で試してみよう。

Require Import ExtrHaskellBasic.
Require Import ExtrHaskellNatInt.
Extraction Language Haskell.
Extraction dt.
Extraction f'.
Extraction f.

出てくるのは以下のコードである。

type Dt = Any

f' :: Prelude.Int -> Prelude.Int -> Dt
f' acc n =
  (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    unsafeCoerce acc)
    (\n' ->
    unsafeCoerce (\v -> f' ((Prelude.+) acc v) n'))
    n

f :: Prelude.Int -> Dt
f n =
  f' 0 n

んー、実行する方法がわからないな。ロードまでは以下の指定を先頭につければいいことがわかった。

import Unsafe.Coerce
import qualified GHC.Prim
type Any = GHC.Prim.Any

そういう内容を a.hs に入れて、以下のようにしてもエラーになってしまう。

% ghci a.hs
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( a.hs, interpreted )
Ok, modules loaded: Main.
*Main> f

<interactive>:2:1:
    No instance for (Show (Int -> Dt)) arising from a use of `print'
    Possible fix: add an instance declaration for (Show (Int -> Dt))
    In a stmt of an interactive GHCi command: print it
*Main> f 0

<interactive>:3:1:
    No instance for (Show Dt) arising from a use of `print'
    Possible fix: add an instance declaration for (Show Dt)
    In a stmt of an interactive GHCi command: print it
*Main> f 1

<interactive>:4:1:
    No instance for (Show Dt) arising from a use of `print'
    Possible fix: add an instance declaration for (Show Dt)
    In a stmt of an interactive GHCi command: print it
*Main> f 1 10

<interactive>:5:1:
    Couldn't match expected type `a0 -> t0'
                with actual type `GHC.Prim.Any *'
    The function `f' is applied to two arguments,
    but its type `Int -> Dt' has only one
    In the expression: f 1 10
    In an equation for `it': it = f 1 10
#1 Coq Bug 5507 - Spelling miss: 'Brujin' should be 'Bruijn'.

Coq Bug 5507 - Bug 5507 - Spelling miss: 'Brujin' should be 'Bruijn'.



田中哲