The little prover 筆記

動機

久遠筆記搬到github這裡，不過也是改寫超多東西的

keyword

premise，在if的條件有可以用在想改寫的東西

theorem，永遠為true的expression (要證過)

axiom，不用證明的theorem

claim，還沒證的theorem

defun，函數，但應該當成類似macro的東西

total，不論什麼參數都會有值的函數

axioms

(dethm equal-same (x)
    (equal (equal x x) 't))

(dethm equal-swap (x y)
    (equal (equal x y) (equal y x)))

(dethm equal-if (x y)
    (if (equal x y) (equal x y) 't))

(dethm if-true (x y)
    (equal (if 't x y) x))

(dethm if-false (x y)
    (equal (if 'nil x y) y))

(dethm if-same (x y)
    (equal (if x y y) y))
(dethm if-nest-A (x y z)
    (if x (equal (if x y z) y) 't))

(dethm if-nest-E (x y z)
    (if x 't (equal (if x y z) z)))

(dethm atom/cons (x y)
    (equal (atom (cons x y)) 'nil))

(dethm car/cons (x y)
    (equal (car (cons x y)) x))

(dethm cons/car+cdr (x)
    (if (atom x) 't (equal (cons (car x) (cdr x)) x)))

(dethm cdr/cons (x y)
    (equal (cdr (cons x y)) y))

(dethm natp/size (x)
    (equal (natp (size x)) 't))

(dethm size/car (x)
    (if (atom x) 't (equal (< (size (car x)) (size x)) 't)))

(dethm size/cdr (x)
    (if (atom x) 't (equal (< (size (cdr x)) (size x)) 't)))

(dethm identity-+ (x)
     (if (natp x) (equal (+ 0 x) x) ‘t))

(dethm commute-+ (x y)
     (equal (+ x y) (+ y x)))

(dethm associate+ (x y z)
     (equal (+ (+ x y) z) (+ x (+ y z))))

(dethm positives+ (x y)
     (if (< 0 x) (if (< 0 y) (equal (< 0 (+ x y)) ‘t) ‘t) ‘t))

(dethm natp+ (x y)
     (if (natp x) (if (natp y) (equal (natp (+ x y)) ‘t) ‘t) ‘t))

(dethm  common-addends-< (x y z)
     (equal (< (+ x z) (+ y z)) (< x y)))

怎麼用theorem

要改寫用的equal只能在if-answer或if-else，同時該equal不能出現在if-question或function call的參數中．

(dethm ?? (x)
    (if (A x) 
        (if (B x)
          (equal (F1 x) '1)
          (equal (F2 x) '2)) 
        (if (C x)
          (equal (F3 x) '3)
          (equal (F4 x) '4)))) 


(cons 'gyre
     (if (C '(callooh callay)) 
        (cons 'gimble
          (if (A '(callooh callay)) 
              (cons '1 '(outgrabe))
              (cons '3 '(wabe))))
        (cons (F4 '(callooh callay)) '(vorpal))))

試著用??來改寫這個式子．

(F4 '(callooh callay))能被改寫成’4嗎？

有C的前提，同時該位置也在if-else，但是沒有A的前提，所以不行．

那1與3可以改寫成(F1 …)與(F2 …)嗎？

可以！！

A與C的前提都有，同時都在相對應的位置上，所以可以．

要total才行，partial function

(defun partial (x)
     (if (partial x)
         'nil
         't))

(dethm contradiction () 'nil)

‘nil

-> if-same

(if (partial x) nil nil)

-> if-nest-A (enlarge

(if (partial x)
    (if (partial x) nil t)
    ‘nil)

-> if-nest-E (enlarge

(if (partial x)
    (if (partial x) nil t)
    (if (partial x) t nil))

-> expand(use) (partial x) (self-reference)

(if (partial x)
    (if (if (partial x) nil t) nil t)
    (if (if (partial x) nil t) t nil))

-> if-nest-A & if-nest-E (shrink

(if (....)
    (if nil nil t)
    (if t t nil))

-> t

measure

measure，追蹤某個參數的長度 (證明遞迴會收斂)

(defun sub (x y)
    (if (atom y)
        (if (equal y '?)
        x
        y)
    (cons (sub x (car y))
        (sub x (cdr y)))))
measure: (size y)

totality claim

(if (natp (size x))
    (if (atom x)
        't
        (< (size (cdr x)) (size x)))
    'nil)

If Lifting

(A (if x y z)) -> (if x (A y) (A z))

(ctx
    (focus
      (if Q A E)))

=> if-same

(ctx
  (if Q
    (focus
        (if Q A E))
    (focus
        (if Q A E))))

=> if-next-A&E

(ctx
  (if Q
    (focus
         A)
    (focus
         E)))

做Totality Claims

(defun add-atoms (x ys)
    (if (atom x)
        (if (member? x ys)
            ys
            (cons x ys))
        (add-atoms (car x)
            (add-atoms (cdr x) ys))))

基本上就是把每一次遞迴所apply的參數，apply到measure去，同時寫下這次遞迴比原本的measure小

針對每個case建分支

(if (atom x)
        ...
        ...)

找自己的遞迴，沒有的直接換成’t

(if (atom x)
        't
        ...)

從第一個遞迴開始轉成measure，measure參數代此遞迴的參數，如果不只一個就用if包起來

(if (atom x)
        't
        (if (< (size (car x)) (size x))
            (< (size (cdr x)) (size x))
            nil))

最後用natp包起來(證明size是自然數)

(if (natp (size x))
    (if (atom x)
            't
            (if (< (size (car x)) (size x))
                (< (size (cdr x)) (size x))
                'nil))
    'nil)

做induction template

(defun set? (xs)
    (if (atom xs)
        't
        (if (member? (car xs) (cdr xs))
            'nil
            (set? (cdr xs)))))
(defun add-atoms (x ys)
    (if (atom x)
        (if (member? x ys)
            ys
            (cons x ys))
        (add-atoms (car x)
            (add-atoms (cdr x) ys))))

(dethm set?/add-atoms (a)
    (equal (set? (add-atoms a '())) 't))

把所有東西參數化

(equal (set? (add-atoms a bs)) 't)

分析裡面的參數，讓他在所有情況下都會成立

先從bs開始，因為在add-atoms裡面他沒有涉及到遞迴的部分，比較簡單

要怎麼讓(equal (set? (add-atoms a bs)) 't)成立? bs要讓set?為’t

讓主體的前提滿足

(if (set? bs)
    (equal (set? (add-atoms a bs)) 't)
    't))

只要有bs都會有這一段，等一下還會看到很多次

接著是a，他有兩個case

atom，沒有遞迴，直接抄前面的

(if (atom a)
    (if (set? bs)
        (equal (set? (add-atoms a bs)) 't)
        't))
    ...)

list，有遞迴裡面有遞迴!! (add-atoms (car x) (add-atoms (cdr x) ys))

先處理最外面的add-atoms，直接把(car x)與(add-atoms (cdr x) ys)當成input，試著讓我們要證的東西成立

(if (set? (add-atoms (cdr x) ys))
    (equal (set? (add-atoms (car x) (add-atoms (cdr x) ys))) 't)
    't))

剛剛是第一個前提，接著是(add-atoms (cdr x) ys)，用同樣的方法

(if (set? (cdr x))
    (equal (set? (add-atoms (cdr x) ys) 't)
    't))

這是第二個前提，我們把所有前依據以順序組合在一起(用if)

(if (atom a)
    (if (set? bs)
        (equal (set? (add-atoms a bs)) 't)
        't)
    (if (if (set? (add-atoms (cdr x) ys))
            (equal (set? (add-atoms (car x) (add-atoms (cdr x) ys))) 't)
            't)
            (if (if (set? (cdr x))
                (equal (set? (add-atoms (cdr x) ys) 't)
                't))
                ...
                't)))

最後的…，就是我們在這個case原本想證的東西

(if (atom a)
    (if (set? bs)
        (equal (set? (add-atoms a bs)) 't)
        't)
    (if (if (set? (add-atoms (cdr x) ys))
            (equal (set? (add-atoms (car x) (add-atoms (cdr x) ys))) 't)
            't)
            (if (if (set? (cdr x))
                (equal (set? (add-atoms (cdr x) ys) 't)
                't))
                (if (set? bs)
                    (equal (set? (add-atoms a bs)) 't)
                    't))
                't)))

等等，有些變數對不上啊其實變數就依據case的變數去改就好，alpha reduction

(if (atom x)
    (if (set? ys)
        (equal (set? (add-atoms a ys)) 't)
        't)
    (if (if (set? (add-atoms (cdr x) ys))
            (equal (set? (add-atoms (car x) (add-atoms (cdr x) ys))) 't)
            't)
            (if (if (set? (cdr x))
                (equal (set? (add-atoms (cdr x) ys) 't)
                't))
                (if (set? ys)
                    (equal (set? (add-atoms x ys)) 't)
                    't))
                't)))

看到這裡，會發現totality claim與induction template的做法其實很像

分析case
從被遞迴的input開始，切case
沒遞迴的case就是滿足其他參數的條件，包好就完成沒遞迴的case
遞迴的case要從最外層的遞迴一層一層建，建法與沒遞迴的case的結果很像，不過參數要代成遞迴時代入的參數
把所有前提寫完，就把要證的帶進去，當然要注意其他參數的條件要滿足!!

這邊附上兩個常見template

Proof by List Induction

measure: (size x)

(if (atom x)
    C
    (if Ccdr
        C
        't))

Proof by Star Induction

measure: (size x)

(if (atom x)
    C
    (if Ccar
        (if Ccdr
            C 
            t)
    't))

Insights

選好做的

But some approaches will find a proof faster than others.

(equal (if (equal (first-of (cons a (cons '? '()))) 
                  '?)
            't
            (equal (second-of (cons a (cons '? '()))) ?))
        ‘t)

如果從second-of開始改寫，會變成’t，就可以if-same再改成’t

這樣就不用管first-of如何．

Insight: Rewrite from the Inside Out

從if-ans,if-else, arg來改寫，再apply func，如果真的不行了，再改寫外部．

Insight: Pull Ifs Outward

當if被func或其他if包起來時，用if lifting把if拉出來．

Insight: Keep Theorems in Mind

看到可以用的就用，看到很像的，想辦法改寫到可以用．

Insight: Don’t Touch Inductive Premises

歸納前提就是重點，不要動

如果不能用，也許是

用錯歸納法template了
需要其他lemma

Insight: Combine Ifs

用if lifting把if條件中的if拿出來

Insight: Create Helpers for Induction

To rewrite the application of a recursive function, prove a separate theorem about the recursive function using induction. Do this if the current proof either does not use induction, or uses induction for a different kind of recursion from the function, or uses induction on different arguments from the application.

Insight: Create Helpers for Repetition

If a proof performs similar sequences of steps over and over, state a theorem that can perform the same rewrite as those steps via the Law of Dethm. Use that theorem in place of the sequence of steps to shorten the proof.

proof for memb?/remb

(defun remb (xs)
    (if (atom xs)
        '()
        (if (equal (car xs) '?)
            (remb (cdr xs))
            (cons (car xs)
                (remb (cdr xs))))))

(defun memb? (xs)
    (if (atom xs)
        'nil
        (if (equal (car xs) '?)
            't
            (memb? (cdr xs)))))

(dethm memb?/remb (xs)
    (equal (memb? (remb xs)) 'nil))

the inductive claim

(if (atom xs)
    (equal (memb? (remb xs)) 'nil)
    (if (equal (memb? (remb (cdr xs))) 'nil)
        (equal (memb? (remb xs)) 'nil)
        't))

先從(atom xs)的if-ans開始

(if (atom xs)
    (equal (memb?
              (if (atom xs)
                  ‘()
                  (if (equal (car xs) ‘?)
                      (remb (cdr xs))
                      (cons (car xs) (remb (cdr xs))))))
            nil)
    ...)

-> if-nest-A

(if (atom xs)
    (equal (memb? ‘()) nil)
    ...)

-> expand memb? & atom & if-true

(if (atom xs)
    't
    ...)

接著是not (atom xs)與(equal (memb? (remb (cdr xs))) nil)

(equal (memb? (remb xs)) nil)

-> remb

(equal (memb?
        (if (atom xs) ‘()
        (if (equal (car xs) ‘?)
            (remb (cdr xs)
            (cons (car xs) (remb (cdr xs)))))
      nil)

-> if-nest-E & if lifting for memb?

(equal (if (equal (car xs) ‘?)
            (memb? (remb (cdr xs))
            (memb? (cons (car xs) (remb (cdr xs)))))
      nil)

-> inductive premise

(equal (if (equal (car xs) ‘?)
            nil
            (memb? (cons (car xs) (remb (cdr xs)))))
      nil)

-> memb?

(equal (if (equal (car xs) ‘?)
            nil
            (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)))))))
      nil)

-> atom/cons & if-false

(equal (if (equal (car xs) ‘?)
            nil
            (if (equal (car (cons (car xs) (remb (cdr xs)))) ‘?)
                ‘t
                (memb? (cdr (cons (car xs) (remb (cdr xs))))))
	    nil)

-> car/cons & if-false & cdr/cons & inductive premise

(equal (if (...) nil nil) nil)

-> if-same & equal-same

proof for ctx?/sub

(defun ctx? (x)
  (if (atom x)
    (equal x '?)
    (if (ctx? (car x))
      't
      (ctx? (cdr x)))))

(defun sub (x y)
  (if (atom y)
    (if (equal y '?)
      x
      y)
    (cons (sub x (car y))
          (sub x (cdr y)))))

證

(dethm ctx?/sub (x y)
  (if (ctx? x)
      (if (ctx? y)
          (equal (ctx? (sub x y)) 't)
          't)
  't))

把body填入templete(有夠噁心的

(if (atom y)
	(if (ctx? x)
    (if (ctx? y)
      (equal (ctx? (sub x y)) 't)
      't)
  't)
  (if (if (ctx? x)
        (if (ctx? (car y))
          (equal (ctx? (sub x (car y))) 't)
          't)
      't)
      (if (if (ctx? x)
            (if (ctx? (cdr y))
              (equal (ctx? (sub x (cdr y))) 't)
              't)
            ‘t)
			    (if (ctx? x)
            (if (ctx? y)
              (equal (ctx? (sub x y)) 't)
              't)
            't)
          't)
        ‘t))

先看到有一堆(if (ctx? x)，用if lifting抽出來(這裡就不好用(A (if …)) -> (if (A ….))來理解，要用if-same來做就很直覺)

同時把if-else的部分用if-same去掉

(if (ctx? x)
  (if (atom y)
      (if (ctx? y)
        (equal (ctx? (sub x y)) 't)
        't)
      (if (if (ctx? (car y))
          (equal (ctx? (sub x (car y))) 't)
          't)
        (if (if (ctx? (cdr y))
              (equal (ctx? (sub x (cdr y))) 't)
              't)
              (if (ctx? y)
                (equal (ctx? (sub x y)) 't)
              't)
            't)
          ‘t))
  't)

對sub用if-nest-A

(if (ctx? x)
  (if (atom y)
      (if (ctx? y)
          (equal (ctx? (if (equal y '?) x y)) 't)
          't)
      (if (if (ctx? (car y))
          (equal (ctx? (sub x (car y))) 't)
          't)
        (if (if (ctx? (cdr y))
              (equal (ctx? (sub x (cdr y))) 't)
              't)
              (if (ctx? y)
                (equal (ctx? (sub x y)) 't)
              't)
            't)
          ‘t))
  't)

if lifting

(if (ctx? x) ;; 可以用這個改寫成’t嗎
  (if (atom y)
      (if (ctx? y)
        (if (equal y '?)
      	    (equal (ctx? x) 't) ;; 不行，(ctx? x)可以是’t以外的東西(total)，也沒定理
            (equal (ctx? y) 't))
        't)
      (if (if (ctx? (car y))
          (equal (ctx? (sub x (car y))) 't)
          't)
        (if (if (ctx? (cdr y))
              (equal (ctx? (sub x (cdr y))) 't)
              't)
              (if (ctx? y)
                (equal (ctx? (sub x y)) 't)
              't)
            't)
          ‘t))
  't)

但ctx?只會回傳’t或’nil而且如果我們有這種定理的話？

(dethm ctx?/t (x)
    (if (ctx? x)
        (equal (ctx? x) ‘t)
        ‘t))

那就可以改寫了

(if (ctx? x)
  (if (atom y)
      (if (ctx? y)
        (if (equal y '?)
      	    ‘t
            ‘t)) 
        't)
      (if (if (ctx? (car y))
          (equal (ctx? (sub x (car y))) 't)
          't)
        (if (if (ctx? (cdr y))
              (equal (ctx? (sub x (cdr y))) 't)
              't)
              (if (ctx? y)
                (equal (ctx? (sub x y)) 't)
              't)
            't)
          ‘t))
  't)

if-same*2

(if (ctx? x)
  (if (atom y)
      ‘t
      (if (if (ctx? (car y))
          (equal (ctx? (sub x (car y))) 't)
          't)
        (if (if (ctx? (cdr y))
              (equal (ctx? (sub x (cdr y))) 't)
              't)
              (if (ctx? y)
                (equal (ctx? (sub x y) 't)
                't)
            't)
          ‘t))
  't)

atom與if-nest-E

(if (ctx? x)
  (if (atom y)
      ‘t
      (if (if (ctx? (car y))
          (equal (ctx? (sub x (car y))) 't)
          't)
        (if (if (ctx? (cdr y))
              (equal (ctx? (sub x (cdr y))) 't)
              't)
              (if (ctx? y)
                (equal (ctx? (cons (sub x (car y)) (sub (cdr y)))) 't)
              't)
            't)
          ‘t))
  't)

ctx?

(if (ctx? x)
  (if (atom y)
      ‘t
      (if (if (ctx? (car y))
          (equal (ctx? (sub x (car y))) 't)
          't)
          (if (if (ctx? (cdr y))
                  (equal (ctx? (sub x (cdr y))) 't)
                  't)
              (if (ctx? y)
                  (equal (if (ctx? (sub x (car y)))
                              ‘t
                              (ctx? (sub x (cdr y))))
                        't)
                  't)
              't)
          ‘t))
  't)

ctx?

(if (ctx? x)
  (if (atom y)
      ‘t
      (if (if (ctx? (car y)) ;; here
              (equal (ctx? (sub x (car y))) 't)
              't)
          (if (if (ctx? (cdr y))
                (equal (ctx? (sub x (cdr y))) 't)
                't)
              (if (if (ctx? (car y)) ;; here
                      ‘t
                      (ctx? (cdr y)))
                  (equal (if (ctx? (sub x (car y)))
                            ‘t
                            (ctx? (sub x (cdr y))))
                        't)
                  't)
              't)
          ‘t))
  't)

if lifting

(if (ctx? x)
  (if (atom y)
      ‘t
      (if (ctx? (car y))
          (if (equal (ctx? (sub x (car y))) 't);; inductive promsing!!
                (if (if (ctx? (cdr y))
                        (equal (ctx? (sub x (cdr y))) 't)
                        't)
                    (equal (if (ctx? (sub x (car y)))
                                ‘t
                                (ctx? (sub x (cdr y))))
                            't)
                    't)
                (if (if (ctx? (cdr y))
                        (equal (ctx? (sub x (cdr y))) 't)
                        't)
                    (if (ctx? (cdr y))
                        (equal (if (ctx? (sub x (car y)))
                                    ‘t
                                    (ctx? (sub x (cdr y))))
                                't)
                        't)
                    ‘t))))
  't)

inductive promsing

(if (ctx? x)
  (if (atom y)
      ‘t
      (if (ctx? (car y))
                t
                (if (if (ctx? (cdr y))
                        (equal (ctx? (sub x (cdr y))) 't)
                        't)
                    (if (ctx? (cdr y))
                        (equal (if (ctx? (sub x (car y)))
                                    ‘t
                                    (ctx? (sub x (cdr y))))
                                't)
                        't)
                    ‘t)))

't)

if lifting

(if (ctx? x)
  (if (atom y)
      ‘t
      (if (ctx? (car y))
          t
          (if (ctx? (cdr y))
              (if (equal (ctx? (sub x (cdr y))) 't) ;; inductive promsing!!
                  (equal (if (ctx? (sub x (car y)))
                                ‘t
                                (ctx? (sub x (cdr y))))
                          ‘t)
                  't)
              ‘t)))
  't)

inductive promsing & if-same & if-true

(剩下的那一個，就pass，打這個好累)

發現有許多差不多的前提，用if-nest-A/E或if lifting把他們化簡

把inductive promise湊出來

一次化簡或處理一個case

proof for set?/add-atoms

if lifting is our friend.

(atom case) add-atoms, if-nest-A, (atom a)

(if (atom a)
    (if (set? bs)
      	(equal (set? (if (member? a bs)
                          bs
                          (cons a bs))) ‘t)
	      ‘t)
    (if (if (set? (add-atoms (cdr x) bs))
	          (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
	          ‘t)
        (if (if (set? bs)
	              (equal (set? (add-atoms (cdr x) bs)) ‘t)
	              ‘t)
            (if (set? bs)
                (equal (set? (add-atoms a bs)) ‘t)
                ‘t)
            ‘t)
        ‘t))

if lifting, promise (another claim)

(if (atom a)
    (if (set? bs)
      	(equal (if (member? a bs)
                    (set? bs)
                    (set? (cons a bs))) ‘t)
	      ‘t)
    (if (if (set? (add-atoms (cdr x) bs))
	          (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
	          ‘t)
        (if (if (set? bs)
	              (equal (set? (add-atoms (cdr x) bs)) ‘t)
	              ‘t)
            (if (set? bs)
                (equal (set? (add-atoms a bs)) ‘t)
                ‘t)
            ‘t)
          ‘t))

set?, member?, if-nest-E, if-same, equal, if-same

(if (atom a)
    't
    (if (if (set? (add-atoms (cdr x) bs))
	          (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
	          ‘t)
        (if (if (set? bs)
	              (equal (set? (add-atoms (cdr x) bs)) ‘t)
	              ‘t)
            (if (set? bs)
                (equal (set? (add-atoms a bs)) ‘t)
                ‘t)
            ‘t)
          ‘t))

if lifting

(if (atom a)
    't
    (if (if (set? (add-atoms (cdr x) bs))
	          (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
	          ‘t)
        (if (set? bs)
            (if (equal (set? (add-atoms (cdr x) bs)) ‘t)
                (equal (set? (add-atoms a bs)) ‘t)
                ‘t)
            't)
        ‘t))

if lifting again!!

(if (atom a)
    't
    (if (set? bs)
        (if (if (set? (add-atoms (cdr x) bs))
                (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
                ‘t)
            (if (equal (set? (add-atoms (cdr x) bs)) ‘t)
                (equal (set? (add-atoms a bs)) ‘t)
                ‘t)
            ‘t)
        't))

if lifting

(if (atom a)
    't
    (if (set? bs)
        (if (set? (add-atoms (cdr x) bs)) ;;可以用嗎？
          (if (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
              (if (equal (set? (add-atoms (cdr x) bs)) ‘t)
                  (equal (set? (add-atoms a bs)) ‘t)
                  ‘t)
              ‘t)
          (if (equal (set? (add-atoms (cdr x) bs)) ‘t) ;; need a new claim
              (equal (set? (add-atoms a bs)) ‘t)
              ‘t))
        't))

(dethm set?/nil (xs)
    (if (set? xs)
        ‘t
        (equal (set? xs) ‘nil)))

set?/nil & set?/t

(if (atom a)
    't
    (if (set? bs)
        (if (set? (add-atoms (cdr x) bs)) ;;用!!
          (if (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
              (if (equal ‘t ‘t)
                  (equal (set? (add-atoms a bs)) ‘t)
                  ‘t)
              ‘t)
          (if (equal ‘nil ‘t)
              (equal (set? (add-atoms a bs)) ‘t)
              ‘t))
        't))

equal

(if (atom a)
    't
    (if (set? bs)
        (if (set? (add-atoms (cdr x) bs))
          (if (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
              (equal (set? (add-atoms a bs)) ‘t)
              ‘t)
           t)
        't))

add-atoms & if-nest-E

(if (atom a)
    't
    (if (set? bs)
        (if (set? (add-atoms (cdr x) bs)) ;;用!!
          (if (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
               (equal (set? (add-atoms (car x) (add-atoms (cdr x) bs))) ‘t)
              ‘t)
           t)
        't))

promise

證原本要證的

(dethm set?/atoms (a)
      (equal (set? (atoms a)) 't))

先把(atoms a)換成(add-atoms a ‘())

(equal (set? (dad-atoms a ‘())) 't)

要有(set? xs)，才能用set?/add-atoms

if-true

(if t
    (equal (set? (add-atoms a ‘())) 't)
    t)

if-true

(if (if t
        t
        (if (member? (car ‘()) (cdr ‘()))
            nil
	          (set? (cdr ‘()))))
    (equal (set? (add-atoms a ‘())) 't)
    t)

(equal t (atom ())

(if (if (atom ())
        t
        (if (member? (car ‘()) (cdr ‘()))
            nil
	          (set? (cdr ‘()))))
    (equal (set? (add-atoms a ‘())) 't)
    t)

set?

(if (set? ())
    (equal (set? (add-atoms a ‘())) 't)
    t)

set?/add-atoms

Ch10 different measure & change the promise

(defun rotate (x)
    (cons (car (car x))
        (cons (cdr (car x)) (cdr x))))

(defun align (x)
  (if (atom x)
      x
      (if (atom (car x))
          (cons (car x) (align (cdr x)))
          (align (rotate x)))))

(size x) ??

align的長度都一樣，需要別的measure

(defun wt (x)
  (if (atom x)
      '1
      (+ (+ (wt (car x)) (wt (car x)))
          (wt (cdr x)))))

measure: (size x)

totality claim是

(if (natp (wt x))
    (if (atom x)
        't
        (if (atom (car x))
            (< (wt (cdr x)) (wt x))
            (< (wt (rotate x)) (wt x))))
    'nil)

(dethm natp/wt (x)
     (equal (natp (wt x)) 't))

(if (natp (size x))
    (if (atom x)
        't
        (if (atom (car x))
            (< (wt (cdr x)) (wt x))
            (< (wt (rotate x)) (wt x))))
    'nil)

=> natp/wt

(if (atom x)
    't
    (if (atom (car x))
        (< (wt (cdr x)) (wt x))
        (< (wt (rotate x)) (wt x))))

=> wt

(if (atom x)
    't
    (if (atom (car x))
        (< (wt (cdr x)) (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x))))
        (< (wt (rotate x)) (wt x))))

=> if-true, natp/wt

(if (atom x)
    't
    (if (atom (car x))
        (if (natp (wt (cdr x)))
            (< (wt (cdr x)) (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x))))
            t)
        (< (wt (rotate x)) (wt x))))

=> identity-+, common-addends-<

(if (atom x)
    't
    (if (atom (car x))
        (if (natp (wt (cdr x)))
            (< 0 (+ (wt (car x)) (wt (car x)))))
            t)
        (< (wt (rotate x)) (wt x))))

=> change promise (natp (wt (cdr x))) -> t -> (equal (< ‘0 (wt x))) t)

(if (atom x)
    't
    (if (atom (car x))
        (if (< ‘0 (wt (car x))))
            (< 0 (+ (wt (car x)) (wt (car x)))))
            t)
        (< (wt (rotate x)) (wt x))))

=> positive-+

(e04, 後面的很長，pass)

最後還有一個align/align，但就是之前的綜合體，不過歸納template要自己生，至於證明就不展開了太長了!!

(defun align (x)
    (if (atom x)
        x
        (if (atom (car x))
            (cons (car x) (align (cdr x)))
            (align (rotate x)))))

(dethm align/align (x)
    (equal (align (align x)) (align x)))

(if (atom x)
    (equal (align (align x)) (align x))
    (if (atom (car x))
        (if (equal (align (align (cdr x))) (align (cdr x)))
            (equal (align (align x)) (align x)) 't)
        (if (equal (align (align (rotate x))) (align (rotate x)))
            (equal (align (align x)) (align x))
            't)))

J-Bob

TODO

有時間會補!!

動機#

keyword#

axioms#

怎麼用theorem#

要total才行，partial function#

measure#

If Lifting#

做Totality Claims#

做induction template#

Proof by List Induction#

Proof by Star Induction#

Insights#

選好做的#

Insight: Rewrite from the Inside Out#

Insight: Pull Ifs Outward#

Insight: Keep Theorems in Mind#

Insight: Don’t Touch Inductive Premises#

Insight: Combine Ifs#

Insight: Create Helpers for Induction#

Insight: Create Helpers for Repetition#

proof for memb?/remb#

proof for ctx?/sub#

proof for set?/add-atoms#

Ch10 different measure & change the promise#

J-Bob#

動機

keyword

axioms

怎麼用theorem

要total才行，partial function

measure

If Lifting

做Totality Claims

做induction template

Proof by List Induction

Proof by Star Induction

Insights

選好做的

Insight: Rewrite from the Inside Out

Insight: Pull Ifs Outward

Insight: Keep Theorems in Mind

Insight: Don’t Touch Inductive Premises

Insight: Combine Ifs

Insight: Create Helpers for Induction

Insight: Create Helpers for Repetition

proof for memb?/remb

proof for ctx?/sub

proof for set?/add-atoms

Ch10 different measure & change the promise

J-Bob