天泣記

2017-07-23 (Sun)

#1 Proof Summit 2017

Proof Summit 2017 で「Coq からの C プログラム生成」発表した

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 が必要なようだ。



田中哲