コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

IdrisでStateモナド

Idris

本記事では、関数型言語に触れているよくでてくる モナド について書きます。

Stateモナドを数学的に実装する

Idrisでやってみた。
Control.Monad.Stateにもある。そこではモナド変換子として実装されている。

module MyState

%default total
-- %language ElabReflection
-- %hide return

-- Stateモナド
record State (stateType : Type) (a : Type) where
  constructor ST
  runState : stateType -> (a, stateType)

implementation Functor (State stateType) where
  map f (ST g) = ?rhs1

implementation Applicative (State stateType) where
  pure x = ST $ \s => (x, s)
  (ST f) <*> (ST a) = ?rhs2

implementation Monad (State stateType) where
  m >>= k = ST $ \s =>
              let (x, s0) = runState m s
              in runState (k x) s0

-- プレリュードでやってる
-- return : Monad m => a -> m a
-- return = pure
get : State x x
get = ST $ \s => (s, s)
put : s -> State s ()
put s = ST $ const ((), s)
-- -------------------------


-- アキュムレータ
-- xを取り、stateに加え、更新したstateを出力
accumulator : Int -> State Int Int
accumulator x = do
  state <- get
  let y = state + x
  put y
  return y
-- 実行
-- bind(>>=)は左から右へ進む
-- > runState ((accumulator 3) >>= accumulator) 4
-- (14, 14) : (Int, Int)

-- アキュムレータ2
accumulator2 : List Int -> State Int (List Int)
accumulator2 [] = return []
accumulator2 (x::_) = do
  state <- get
  let y = state + x
  put y
  return [y]
partial -- ↓どこが全域でないか分からないが……
multiple : State Int (List Int)
multiple = do
  (a::_) <- accumulator2 [1] -- [2]が返る
  (b::_) <- accumulator2 [1] -- [3]が返る、参照透過じゃない！（と、見せかけている）
  (c::_) <- accumulator2 [2]
  (d::_) <- accumulator2 [3]
  (e::_) <- accumulator2 [0]
  (f::_) <- accumulator2 [-1]
  return [a, b, c, d, e, f]
-- 実行
-- runStateの中でだけ、状態が保持される
-- > runState multiple 1
-- ([2, 3, 5, 8, 8, 7], 7) : (List Int, Int)

元記事のメイン内容だけど、随伴からStateモナドが作られるのですね。
知らなかった。
自分もそこまでやるかは分からない。
　
　
　
　
　

Idrisでrev_rev_id

Idris

rev_rev_idとは、リストに、逆順にする事を2回すると、元に戻る、というやつだ。

みょんみょんさんがIsabelleで、
いとうかつとしさんがAgdaで、実装動画を上げている。

ならば僕は、Idrisでやろう、と奮い立った。
（Idrisを起動するときは、> idris -XElabReflectionってやったら良い事があるかもしれない）
出来た物はこちら。

module rev_rev_id

%default total

a : List Nat
a = [1, 2, 3, 4]

snoc : List Nat -> Nat -> List Nat
snoc []      y = [y]
snoc (x::xs) y = x :: snoc xs y

myReverse : List Nat -> List Nat
myReverse []      = []
myReverse (x::xs) = snoc (myReverse xs) x

lemma : (xs:List Nat) -> (y:Nat) -> myReverse (snoc xs y) = y :: (myReverse xs)
lemma []      _ = Refl
lemma (x::xs) y = rewrite lemma xs y in Refl

theorem : (xs:List Nat) -> myReverse (myReverse xs) = xs
theorem []      = Refl
theorem (x::xs) = rewrite lemma (myReverse xs) x in
                  rewrite theorem xs in Refl

お二人と、ほぼ同じ形になった。
これでも苦労したのですよ、簡約されすぎたりして。

あと話は変わるけれど、Idrisのコマンドプロンプトはカラフルでかっこいい。

181020 追記　Reasoningを使った証明もやってみた。
libs/base/Syntax/PreorderReasoning.idr　にライブラリがある。

module rev_rev_id02

-- > idris -p base
import Syntax.PreorderReasoning

%default total
-- %language ElabReflection


snoc : List a -> a -> List a
snoc []      y = [y]
snoc (x::xs) y = x :: snoc xs y

myReverse : List a -> List a
myReverse []      = []
myReverse (x::xs) = snoc (myReverse xs) x

lemma : (xs:List a) -> (y:a) -> myReverse (snoc xs y) = y :: (myReverse xs)
lemma []      _ = Refl
lemma (x::xs) y = rewrite lemma xs y in Refl

theorem : (xs:List a) -> myReverse (myReverse xs) = xs
theorem []        = Refl
theorem (x :: xs) =
  (myReverse (myReverse (x::xs)))       ={ Refl                        }=
  (myReverse (snoc (myReverse xs) x))   ={ lemma (myReverse xs) x      }=
  (x :: (myReverse (myReverse xs)))     ={ cong {f=(x::)} (theorem xs) }=
  (x :: xs)                                QED

　
　
　
　
　

Agdaで整数　その5

Agda

整数の定義を素朴なものに戻した。

--（succ (succ (pred zero))などが有効、という弱点がある）
data Z : Set where
  zero : Z
  succ : Z -> Z
  pred : Z -> Z

それに加法、反数、乗法を定義したものがこちら。
整数の素朴な定義

この整数が環をなすことをAgdaで証明した。
証明にはrewriteばかり使っている。-Reasoningは使わなかった。
あれ使いづらいもん。
整数が環をなす


ガチな定義も考えたけどね

--（succ (succ (pred zero))などはもうできない）
mutual
  data Z : Set where
    zero : Z
    succ : (x : Z) -> isTrue (zeroOrSucc x) -> Z
    pred : (x : Z) -> isTrue (zeroOrPred x) -> Z

  zeroOrSucc : Z -> Bool
  zeroOrSucc zero = true
  zeroOrSucc (succ x p) = true
  zeroOrSucc (pred x p) = false
  zeroOrPred : Z -> Bool
  zeroOrPred zero = true
  zeroOrPred (succ x p) = false
  zeroOrPred (pred x p) = true
-- succ (succ zero tt) tt のように使う

　
　
　
　
　

定理証明手習いをCoqで　第6章

Coq 定理証明手習い

定理証明手習い

定理証明手習い

@suharahiromichi
この文書のソースコードは以下にあります。
https://github.com/suharahiromichi/coq/blob/master/lisp/tlp_lisp_3.v

「The Little Prover」のCoqでの実現

以下のコードを実行するときは、氏のCoqコードを読み込んだ後にお願いします。

リスト型帰納法による証明をおこなう。

(** Chapter6 最後まで考え抜くのです *)

(* 書き換え用に公理を付け足す *)
Variable xs : star.
Variable membE :
  memb (CONS (CAR xs) (remb (CDR xs))) =
    (_IF (ATOM (CONS (CAR xs) (remb (CDR xs))))
         'NIL
         (_IF (EQUAL (CAR (CONS (CAR xs) (remb (CDR xs)))) '?)
              'T
              (memb (CDR (CONS (CAR xs) (remb (CDR xs))))))).
Variable rembE :
  remb xs =
  (_IF (ATOM xs)
       '()
       (_IF (EQUAL (CAR xs) '?)
            (remb (CDR xs))
            (CONS (CAR xs) (remb (CDR xs))))).
Variable EQA : (EQUAL 'NIL 'NIL) = 'T.

Theorem memb_remb :
  ~ ATOM xs -> ATOM xs -> ~ (EQUAL (CAR xs) '?) -> (EQUAL (CAR xs) '?) -> (EQUAL (memb (remb (CDR xs))) 'NIL) ->
    (_IF (ATOM xs)
         (EQUAL (memb (remb xs)) 'NIL)
         (_IF (EQUAL (memb (remb (CDR xs))) 'NIL)
              (EQUAL (memb (remb xs)) 'NIL)
              'T)).
Proof.
  move => H0 H1 H2 H3 H4.
  rewrite rembE.
  rewrite {1}(iffLR ifAP (if_nest_A
    (ATOM xs)
    '()
    (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs))))
  )).
  rewrite membB.
  rewrite atomB.
  rewrite (equal_eq (if_true 'NIL
     (_IF (EQUAL (CAR '()) '?) 'T (memb (CDR '()))))).
  rewrite EQA.

  (* rewrite rembE. *)
  rewrite (iffLR ifEP (if_nest_E
    (ATOM xs)
    '()
    (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs))))
  )).
(* --- ifの持ち上げ --- *)
  rewrite -(equal_eq (if_same
    (EQUAL (CAR xs) '?)
    (memb (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs)))))
  )).
  rewrite {1}(iffLR ifAP (if_nest_A
    (EQUAL (CAR xs) '?)
    (remb (CDR xs))
    (CONS (CAR xs) (remb (CDR xs)))
  )).
  rewrite (iffLR ifEP (if_nest_E
    (EQUAL (CAR xs) '?)
    (remb (CDR xs))
    (CONS (CAR xs) (remb (CDR xs)))
  )).
(* --- ifの持ち上げ --- *)
  rewrite {2}(iffLR ifAP (equal_if (memb (remb (CDR xs))) 'NIL)).
  rewrite membE.
  rewrite (equal_eq (atom_cons (CAR xs) (remb (CDR xs)))).
  rewrite (equal_eq (if_false 'NIL
    (_IF (EQUAL (CAR (CONS (CAR xs) (remb (CDR xs)))) '?)
              'T
              (memb (CDR (CONS (CAR xs) (remb (CDR xs)))))))).
  rewrite (equal_eq (car_cons (CAR xs) (remb (CDR xs )))).
  rewrite (equal_eq (cdr_cons (CAR xs) (remb (CDR xs )))).
  rewrite (iffLR ifEP (if_nest_E
    (EQUAL (CAR xs) '?)
    'T
    (memb (remb (CDR xs)))
  )).
  rewrite {2}(iffLR ifAP (equal_if (memb (remb (CDR xs))) 'NIL)).

  rewrite (equal_eq (if_same (EQUAL (CAR xs) '?) 'NIL)).
  rewrite EQA.
  rewrite (equal_eq (if_same (EQUAL (memb (remb (CDR xs))) 'NIL) 'T)).
  rewrite (equal_eq (if_same (ATOM xs) 'T)).
  done.

  done.
  done.
  done.
  done.
  done.
  done.
  done.
Qed.

　
　
　
　
　
　

【番外編】定理証明手習いをAgdaで

Agda 定理証明手習い

定理証明手習い

定理証明手習い

番外編ということで、定理証明手習いをAgdaでやってみた。
最初は、組み込み関数を普通に定義して、公理をpostulateで定義した。
そしたら問題が発生。

以下を考える。

data Star : Set where
  NIL : Star
  TRU : Star
  N   : Nat → Star
  S   : String → Star
  C   : Star → Star → Star

ATOM : Star → Star
ATOM (C _ _) = NIL
ATOM _ = TRU

ATOMを使った証明にxs:Starを引数とすると、
xsをコンストラクタでばらせないから、ATOMが計算できず、エラーになる。
引数にC x yとか渡さないといけない。これはやりたくない。

  • Reasoningを使った証明もしんどかった。

長いSchemeの定理を何度も書かないといけない。
congの位置合わせも手間だった。

というわけで全部postulateにした。
証明もrewriteを使うようにした。
これなら書けるかもしれない。

rewriteで証明ステップが5つくらい一気に進んだのは謎。


ソースはこちらです。
TLP01.agdaボツネタ
TLP02.agda