定理証明手習い(a1) しゅくだい(9)

rcons版のreverse/reverseを証明します
reverse2/reverse2はどうしようかな

rconsとreverseの定義・証明

(defun defun.rcons ()
  (J-Bob/define (prelude)
    '(((defun rcons (x y)
         (if (atom x)
             (cons y x)
             (cons (car x) (rcons (cdr x) y))))
       (size x)
       ((Q) (natp/size x))
       (() (if-true (if (atom x) 't (< (size (cdr x)) (size x))) 'nil))
       ((E) (size/cdr x))
       (() (if-same (atom x) 't))))))

(defun defun.reverse ()
  (J-Bob/define (defun.rcons)
    '(((defun reverse (x)
         (if (atom x)
             x
             (rcons (reverse (cdr x)) (car x))))
       (size x)
       ((Q) (natp/size x))
       (() (if-true (if (atom x) 't (< (size (cdr x)) (size x))) 'nil))
       ((E) (size/cdr x))
       (() (if-same (atom x) 't))))))

ここまでは簡単
reverse/reverseもこの調子で証明できるかな

(J-Bob/prove (defun.reverse)
  '(((dethm reverse/reverse (x)
       (equal (reverse (reverse x)) x))
     (list-induction x)
     
     ; (if (atom x)
     ;     (equal (reverse (reverse x)) x)
     ;     (if (equal (reverse (reverse (cdr x))) (cdr x))
     ;         (equal (reverse (reverse x)) x)
     ;         't))

A部はreverseを2回展開したらあっさり't

     ((A 1 1) (reverse x))
     ((A 1 1) (if-nest-A (atom x) x (rcons (reverse (cdr x)) (car x))))
     ((A 1) (reverse x))
     ((A 1) (if-nest-A (atom x) x (rcons (reverse (cdr x)) (car x))))
     ((A) (equal-same x))

     ; (if (atom x)
     ;     't
     ;     (if (equal (reverse (reverse (cdr x))) (cdr x))
     ;         (equal (reverse (reverse x)) x)
     ;         't))

E部
まずは(reverse x)の展開

     ((E A 1 1) (reverse x))
     ((E A 1 1) (if-nest-E (atom x) x (rcons (reverse (cdr x)) (car x))))

     ; (if (atom x)
     ;     't
     ;     (if (equal (reverse (reverse (cdr x))) (cdr x))
     ;         (equal (reverse (rcons (reverse (cdr x)) (car x))) x)
     ;         't))

rconsが邪魔
うまく消せるかな
願望ベースで考えてみよう

  (reverse (reverse '(a b c)))
= (reverse (rcons (reverse '(a b)) 'c)))
= (cons 'c (reverse (reverse '(a b)))

みたいな変形ができれば後が続きそう
つまり(reverse (rcons x y)) = (cons y (reverse x))だといいのか
ここは別の定理にして証明しよう

(J-Bob/prove (defun.reverse)
  '(((dethm reverse/rcons (x y)
       (equal (reverse (rcons x y)) (cons y (reverse x))))
     ?

さてここはどんな種を入れればいいのか
rconsかreverseか
それともyはまったく変わらないからlist-inductionでもいいのか

やってみたら、どれでもいっしょでした

       ; (if (atom x)
       ;     (equal (reverse (rcons x y)) (cons y (reverse x)))
       ;     (if (equal (reverse (rcons (cdr x) y))
       ;                (cons y (reverse (cdr x))))
       ;         (equal (reverse (rcons x y)) (cons y (reverse x)))
       ;         't))

どれも(cdr x)で再帰するだけだからそうなるってことかな

A部

       ((A 1 1) (rcons x y))
       ((A 1 1) (if-nest-A (atom x)
                           (cons y x)
                           (cons (car x) (rcons (cdr x) y))))
       ((A 1) (reverse (cons y x)))
       ((A 1 Q) (atom/cons y x))
       ((A 1) (if-false (cons y x)
                        (rcons (reverse (cdr (cons y x)))
                               (car (cons y x)))))

       ; (if (atom x)
       ;     (equal (rcons (reverse (cdr (cons y x)))
       ;                   (car (cons y x)))
       ;            (cons y (reverse x)))
       ;     (if (equal (reverse (rcons (cdr x) y))
       ;                (cons y (reverse (cdr x))))
       ;         (equal (reverse (rcons x y)) (cons y (reverse x)))
       ;         't))
     
       ((A 1 1 1) (cdr/cons y x))
       ((A 1 2) (car/cons y x))
       ((A 1 1) (reverse x))
       ((A 1 1) (if-nest-A (atom x)
                           x
                           (rcons (reverse (cdr x)) (car x))))
       ((A 1) (rcons x y))
       ((A 1) (if-nest-A (atom x)
                         (cons y x)
                         (cons (car x) (rcons (cdr x) y))))
       ((A 2 2) (reverse x))
       ((A 2 2) (if-nest-A (atom x)
                           x
                           (rcons (reverse (cdr x)) (car x))))
       ((A) (equal-same (cons y x)))

       ; (if (atom x)
       ;     't
       ;     (if (equal (reverse (rcons (cdr x) y))
       ;                (cons y (reverse (cdr x))))
       ;         (equal (reverse (rcons x y))
       ;                (cons y (reverse x)))
       ;         't))

一本道でしたがA部の証明にしては長い感じ
どこか遠回りしたかなあ？
まあ'tになったので気にしない

E部
rconsを展開して

       ((E A 1 1) (rcons x y))
       ((E A 1 1) (if-nest-E (atom x)
                             (cons y x)
                             (cons (car x) (rcons (cdr x) y))))

       ; (if (atom x)
       ;     't
       ;     (if (equal (reverse (rcons (cdr x) y))
       ;                (cons y (reverse (cdr x))))
       ;         (equal (reverse (cons (car x) (rcons (cdr x) y)))
       ;                (cons y (reverse x)))
       ;         't))

うーん、どうしようかなあ
(rcons (cdr x) y)の形は残しておきたいがするので
若干力技な気がしますがこのままreverseを展開します

       ((E A 1) (reverse (cons (car x) (rcons (cdr x) y))))

       ; (if (atom x)
       ;     't
       ;     (if (equal (reverse (rcons (cdr x) y))
       ;                (cons y (reverse (cdr x))))
       ;         (equal
       ;          (if (atom (cons (car x) (rcons (cdr x) y)))
       ;              (cons (car x) (rcons (cdr x) y))
       ;              (rcons (reverse (cdr (cons (car x) (rcons (cdr x) y))))
       ;                     (car (cons (car x) (rcons (cdr x) y)))))
       ;          (cons y (reverse x)))
       ;         't))

ボリュームが増えましたがひるまずに進めます
いろいろ簡単な形にできます

       ((E A 1 Q) (atom/cons (car x) (rcons (cdr x) y)))
       ((E A 1) (if-false (cons (car x) (rcons (cdr x) y))
                          (rcons (reverse (cdr (cons (car x) (rcons (cdr x) y))))
                                 (car (cons (car x) (rcons (cdr x) y))))))
       ((E A 1 1 1) (cdr/cons (car x) (rcons (cdr x) y)))
       ((E A 1 2) (car/cons (car x) (rcons (cdr x) y)))

       ; (if (atom x)
       ;     't
       ;     (if (equal (reverse (rcons (cdr x) y))
       ;                (cons y (reverse (cdr x))))
       ;         (equal (rcons (reverse (rcons (cdr x) y)) (car x))
       ;                (cons y (reverse x)))
       ;         't))

前提が適用できる形になりました

       ((E A 1 1) (equal-if (reverse (rcons (cdr x) y))
                            (cons y (reverse (cdr x)))))

       ; (if (atom x)
       ;     't
       ;     (if (equal (reverse (rcons (cdr x) y))
       ;                (cons y (reverse (cdr x))))
       ;         (equal (rcons (cons y (reverse (cdr x))) (car x))
       ;                (cons y (reverse x)))
       ;         't))

意味がわかる式なせいかいけそうな感触があります
まだ手間はかかりそう

       ((E A 1) (rcons (cons y (reverse (cdr x))) (car x)))
       ((E A 1 Q) (atom/cons y (reverse (cdr x))))
       ((E A 1) (if-false
                 (cons (car x) (cons y (reverse (cdr x))))
                 (cons (car (cons y (reverse (cdr x))))
                       (rcons (cdr (cons y (reverse (cdr x))))
                              (car x)))))
       ((E A 1 1) (car/cons y (reverse (cdr x))))
       ((E A 1 2 1) (cdr/cons y (reverse (cdr x))))

       ; (if (atom x)
       ;     't
       ;     (if (equal (reverse (rcons (cdr x) y))
       ;                (cons y (reverse (cdr x))))
       ;         (equal (cons y (rcons (reverse (cdr x)) (car x)))
       ;                (cons y (reverse x)))
       ;         't))

(rcons (reverse (cdr x)) (car x))はなんとなく別で証明しておきたい形

(J-Bob/prove (defun.reverse)
  '(((dethm rcons/reverse (x)
       (if (atom x)
           't
           (equal (rcons (reverse (cdr x)) (car x))
                  (reverse x))))
     nil
     ((E 2) (reverse x))
     ((E 2) (if-nest-E (atom x)
                       x
                       (rcons (reverse (cdr x)) (car x))))
     ((E) (equal-same (rcons (reverse (cdr x)) (car x))))
     (() (if-same (atom x) 't)))))

で'tにできてしまったんですけどこれで証明できたってことでいいんですかね
再帰的な関数を含んでいるからと言って帰納法で証明しなければいけないわけではない？

ではreverse/rconsの証明に戻ります

       ((E A 1 2) (rcons/reverse x))
       ((E A) (equal-same (cons y (reverse x))))
       ((E) (if-same (equal (reverse (rcons (cdr x) y))
                            (cons y (reverse (cdr x))))
                     't))
       (() (if-same (atom x) 't))

できました

rcons/reverseはこれ以前にも出てきていて、適用は可能なんですが
まず前提を作ってやらないといけなかったりして結局短くなりませんでした

ではreverse/reverseの証明に戻ります

ここから

     ; (if (atom x)
     ;     't
     ;     (if (equal (reverse (reverse (cdr x))) (cdr x))
     ;         (equal (reverse (rcons (reverse (cdr x)) (car x))) x)
     ;         't))
     
     ((E A 1 2) (rcons/reverse x))
     ((E A) (equal-same (cons y (reverse x))))
     ((E) (if-same (equal (reverse (rcons (cdr x) y))
                          (cons y (reverse (cdr x))))
                   't))
     (() (if-same (atom x) 't))

     ; 't

できました

これでしゅくだいは提出できるようになってリベンジを果たしたと言えなくはありませんが
実際にはこういう書き方はしないのでreverse2/reverse2の方も再考します