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

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

Egisonでrev_rev_id?

失敗の記録です。
いつにも増して投げやりですが、許してください。
そんな、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とかの実装が参考になると思う。
思っただけです。やらないです。