失敗の記録です。
いつにも増して投げやりですが、許してください。
そんな、Egisonで定理証明なんて、無謀っすよ。
部分的な証明
;; (load-file "rev_rev_id.egi") ;; reverse 4要素以上 (define $myReverse (lambda [$xs] (match xs (list something) {[<nil> {}] [<snoc $x <cons $x2 $rs>> (snoc x2 (cons x (myReverse rs)))] [$y {y}] ;; ←誤魔化しがあるかも }))) ;; snoc (define $snoc (lambda [$x $xs] (append xs {x}) )) ;; proof (define $theorem (lambda [] (let {[$rs (myReverse (myReverse rs))]} ;; こっちが本来 (eq? (snoc x (cons x2 rs)) (eq? (snoc x (cons x2 (myReverse (myReverse rs)))) (myReverse (myReverse (snoc x (cons x2 rs)))) )))) じっこ C:\me\Egison\rev_rev_id egison Egison Version 3.7.12 (C) 2011-2018 Satoshi Egi https://www.egison.org Welcome to Egison Interpreter! > (load-file "rev_rev_id.egi") > (theorem) #t >
帰納法のinduction case、
(myReverse (myReverse rs)) = rsという仮定の元で、
(myReverse (myReverse (snoc x (cons x2 rs)))) = (snoc x (cons x2 rs))
を証明している。
read "x"を返す
「←誤魔化しがあるかも」のところを
read "(myReverse xs)"
とやれば、「xsを分解できない時は評価しない」を表現できる。
例として、
> (read "(* 3 5)")
(* 3 5)
>
となるのだが、これを再評価する手立ては無い。
"*"がついているのだが、これは関数ではなく、得体の知れない何かです。
まあ、ダメだってことです。
数学的帰納法
これも実装しないといけない。
rewrite
showで文字列に変えて、S.replaceで置換したらいけるかも。
一度文字列にしたら、readで戻しても評価できないので、最後にしかできない。
ガチでやるとしたら
「定理証明手習い」のJ-Bobとか、ACL2とかの実装が参考になると思う。
思っただけです。やらないです。