little typer 後篇(8~16) 整理與筆記

來證明啦

ch8 & ch9 & ch10 & ch11

現在說用type證明，但實際上怎麼做?

在claim寫下想證的東西，在define證出來

incr & +

(claim incr
  (-> Nat Nat))
(define incr
  (λ (n)
    (iter-Nat n
      1
      (+ 1))))

(claim +
  (-> Nat Nat Nat))
(define +
  (λ (a b)
    (iter-Nat a
      b
      (λ (ret)
        (add1 ret)))))

+1=add1

證對於任何整數，add1等於+1

(claim +1=add1
  (Pi ((n Nat))
    (= Nat (+ 1 n) (add1 n))))

所以我們需要一個value的type是(= Nat (+ 1 n) (add1 n))) 先把1帶入+中，會發現根本就是(add1 n)

也就是兩邊都一樣，same!!

(define +1=add1
  (λ (n)
    (same (+ 1 n))))

incr=add1

同樣的來試試incr=add1

(claim incr=add1
  (Pi ((a Nat))
    (= Nat (incr a) (add1 a))))

直接帶入沒有像+1=add1之類的好事，只能用歸納法了這裡對n做歸納

這裡motive與base都很好懂，那step呢? 同樣展開incr，會發現(incr n) => (+ 1 n-1) 而另一邊是add1，其實就是(+ 1 n-1)

歸納法會回傳n-1的證明，那我們只要把它擴充成n的就好了把n-1的兩邊同時(+ 1)，cong

(define incr=add1
  (λ (n)
    (ind-Nat n
      (λ (a) (= Nat (incr a) (add1 a)))
      (same 1)
      (λ (n-1)
        (λ (prev)
          (cong prev (+ 1)))))))

replace

雖然說incr=add1證好了，但這邊要介紹另一個工具來改寫一部份的type

歸納法會回傳n-1的證明(prev,(= (incr n-1) (add1 n-1)))，而我們要的證明是(= (add1 (incr n-1)) (add1 (add1 n-1)))，那利用prev去改寫嗎?

把prev看成(incr n-1)可以變成(add1 n-1)，就可以用replace把出現(incr n-1)換成(add1 n-1)

所以用(same (add1 (incr n-1)))，就有空間去換!!

(define incr=add1
  (λ (n)
    (ind-Nat n
      (λ (a) (= Nat (incr a) (add1 a)))
      (same 1)
      (λ (n-1)
        (λ (prev)
          (replace prev
            (λ (k) (= Nat (add1 (incr n-1)) (add1 k))) ;; 這裡k就是要換的部分，當成挖空
            (same (add1 (incr n-1)))))))))

twice=double

(claim twice
  (-> Nat Nat))
(define twice
  (λ (n)
    (+ n n)))

(claim double
  (-> Nat Nat))
(define double
  (λ (n)
    (iter-Nat n
      0
      (λ (ret)
        (+ 2 ret)))))

(claim twice=double
  (Pi ((n Nat))
    (= Nat (twice n) (double n))))

(define twice=double
  (λ (n)
    (ind-Nat n
      (λ (k) (= Nat (twice k) (double k)))
      (same 0)
      (λ (n-1)
        (λ (prev) ;; (= Nat (twice n-1) (double n-1))
          TODO)))))

在Pie可以用TODO去看現在Pie想要什麼type，會噴 TODO

整理一下，其實就是

(= Nat (add1 (+ n-1 (add1 n-1)))
       (add1 (add1 (double n-1))))

wow，我們有prev，(= Nat (+ n-1 n-1) (double n-1))，如果兩邊都變成(add1 (add1 …))的話，就能用cong了

所以要證+add1=add1+

+add1=add1+

直接帶(add1 n-1)，到motive中 (= Nat (+ (add1 (add1 n-1)) b) (+ (add1 n-1) (add1 b)))

而我們有prev，(= Nat (+ (add1 n-1) b) (+ n-1 (add1 b)))

把(= Nat (+ (add1 (add1 n-1)) b) (+ (add1 n-1) (add1 b)))的add1拉出來變成(= Nat (add1 (+ (add1 n-1)) b)) (add1 (+ n-1 (add1 b))))

只與prev差add1，用cong

(claim add1+=+add1
  (Pi ((n Nat)
       (b Nat))
    (= Nat (+ (add1 n) b) (+ n (add1 b)))))

(define add1+=+add1
  (λ (n b)
    (ind-Nat n
      (λ (x) (= Nat (+ (add1 x) b) (+ x (add1 b))))
      (same (add1 b))
      (λ (n-1 prev)
        (cong prev (+ 1))))))

twice=double with +add1=add1+

可以回來證twice=double

用replace把位置換過來就可以cong了

(define twice=double
  (λ (n)
    (ind-Nat n
      (λ (k) (= Nat (twice k) (double k)))
      (same 0)
      (λ (n-1)
        (λ (prev)
          (replace (add1+=+add1 n-1 n-1)
            (λ (k)
              (= Nat (add1 k) (+ 2 (double n-1))))
            (cong prev (+ 2))))))))

這裡也告訴我們位置不對是會影響證明的，下面的就是一個例子

double-vec & twice-vec

(claim double-vec
  (Pi ((A U)
       (n Nat))
    (-> (Vec A n) (Vec A (double n)))))
(claim mot-double-vec
  (Pi ((A U)
       (n Nat))
    U))
(define mot-double-vec
  (λ (A x) (-> (Vec A x) (Vec A (double x)))))
(define double-vec
  (λ (A n)
    (ind-Nat n
      (mot-double-vec A)
      (λ (v) (the (Vec A 0) vecnil))
      (λ (n-1 f v)
        (vec:: (head v) (vec:: (head v) (f (tail v))))))))

直接寫寫看twice-vec，但會發現ind-Nat沒辦法用，要注意到twice-vec要求的base是n!! 用TODO會看到

double-vec

twice-vec

所以要寫twice-vec，可以用replace把double-Vec的double換成twice

(claim twice-vec
  (Pi ((A U)
       (n Nat))
    (-> (Vec A n) (Vec A (twice n)))))

(define twice-vec
  (λ (A n v)
    (replace (symm (twice=double n))
      (λ (x) (Vec A x)) ;; 把要抽換的部分，抽象出來回傳type的函數
      (double-vec A n v)))) ;; base是值!!

用type去擋掉一些奇怪的實作

List->Vec

看宣告好像很合理，但實作可以亂搞

(claim List->Vec
  (Pi ((A U))
    (-> (List A)
      (Sigma ((l Nat)) ;; Sigma是有一個的意思，所以這裡的意思是有一個nat可以滿足(vec A l)
        (Vec A l)))))

(define List->Vec
    (λ (E)
        (λ (es)
            ;; Sigma的實體是list
            (cons 0 vecnil)))) ;; WTF

所以幫他加個條件，生出來的長度要與原本的一樣

(claim List->Vec
  (Pi ((A U)
       (l (List A)))
        (Vec A (len A l)))) ;; i am better
(define List->Vec
  (λ (A)
    (λ (x)
      (ind-List x
        (λ (x) (Vec A (len A x)))
        (the (Vec A 0) vecnil)
        (λ (a x-1)
          (λ (ret)
            (vec:: a ret)))))))

內容物不用一樣嗎? (書上其實有一個可以重複atom的function) 所以可以再寫證明

用證明去擋一些奇怪的實作

這裡是用Vec->List去寫一個證明，Vec->List與List->Vec的內容物實一樣的

(claim Vec->List
  (Pi ((A U)
       (n Nat))
    (-> (Vec A n) (List A))))
(define Vec->List
  (λ (A n v)
    (ind-Vec n v
      (λ (n v) (List A))
      (the (List A) nil)
      (λ (n-1 a v-1 ret)
        (:: a ret)))))

(claim Vec->List=List->Vec
  (Pi ((A U)
       (l (List A)))
    (= (List A) l (Vec->List A (len A l) (List->Vec A l)))))

(define Vec->List=List->Vec
  (λ (A l)
    (ind-List l
      (λ (x) (= (List A) x (Vec->List A (len A x) (List->Vec A x))))
      (same nil)
      (λ (a l-1 ret)
        (cong ret (the (-> (List A) (List A)) (λ (x) (:: a x))))))))

ch12 & ch13

數學套餐開始啦

odd & even

(claim Even
  (Pi ((n Nat))
    U))
(define Even
  (λ (n)
    (Sigma ((x Nat))
           (= Nat n (double x)))))

(claim Odd
  (Pi ((n Nat))
    U))
(define Odd
  (λ (n)
    (Sigma ((x Nat))
           (= Nat n (add1 (double x))))))

+2=even

(claim +2=even
  (Pi ((n Nat))
    (-> (Even n) (Even (+ 2 n)))))
(define +2=even
  (λ (n eve)
    (cons (+ 1 (car eve)) (cong (cdr eve) (+ 2))))) ;;這邊不用用到歸納法，因為我們已經有 (Even n) 了!!

add1-even->odd

(claim add1-even->odd
  (Pi ((n Nat))
    (-> (Even n) (Odd (add1 n)))))
(define add1-even->odd
  (λ (n eve)
    ;; (Even 10) => (5 (same 10))
    ;; (Odd 11)  => (5 (same 11))
    (cons (car eve) (cong (cdr eve) (+ 1)))))

add1-odd->even

(claim add1-odd->even
  (Pi ((n Nat))
    (-> (Odd n) (Even (add1 n)))))
(define add1-odd->even
  (λ (n eve)
    ;; (Odd 11)  => (5 (same 11))
    ;; (Even 12) => (6 (same 12))
    (cons (add1 (car eve)) (cong (cdr eve) (+ 1)))))

ackermann function

(claim rep
  (-> (-> Nat Nat) Nat Nat))
(define rep
  (λ (f n)
    (iter-Nat n
      (f 1)
      (λ (ret)
        (f ret)))))
;; (rep f 5) => (f (f (f (f (f 1)))))
(claim ackermann
  (-> Nat Nat Nat))
(define ackermann
  (λ (n)
    (iter-Nat n
      (+ 1)
      (λ (ret)
        (rep ret)))))

Even-or-Odd

這裡用到ind-Either，Either是一種type，它只有兩種constructor，left與right

ind-Either，就只處理兩種case，left與right剩下就是motive

(claim Even-or-Odd
  (Pi ((n Nat))
    (Either (Even n) (Odd n))))
(define Even-or-Odd
  (λ (n)
    (ind-Nat n
      (λ (x) (Either (Even x) (Odd x)))
      (left (the (Even 0) (cons 0 (same 0))))
      (λ (n-1)
        (λ (ret)
          (ind-Either ret
            (λ (e) (Either (Even (add1 n-1)) (Odd (add1 n-1))))
            (λ (left-val)  (right (add1-even->odd n-1 left-val)))
            (λ (right-val) (left  (add1-odd->even n-1 right-val)))))))))

ch14 & ch15 & ch16

也有數學套餐，但多Absurd與bem與deciable了!!

Maybe

(claim Maybe
  (-> U U))
(define Maybe
  (-> A (Either A Trivial)))

(claim Nothing
  (Pi ((A U))
    (Maybe A)))
(define Nothing
  (λ (A)
    (right sole)))

(claim Just
  (Pi ((A U)
       (a A))
    (Maybe A)))
(define Just
  (λ (A a)
    (left a)))

maybe-head & maybe-tail

(claim maybe-head
  (Pi ((A U)
       (l (List A)))
    (Maybe A)))
(define maybe-head
  (λ (A l)
    (rec-List l
      (Nothing A)
      (λ (a l-1 ret)
        (Just A a)))))
(claim maybe-tail
  (Pi ((A U)
       (l (List A)))
    (Maybe (List A))))
(define maybe-tail
  (λ (A l)
    (rec-List l
      (Nothing (List A))
      (λ (a l-1 ret)
        (Just (List A) l-1)))))

list-ref

(claim list-ref
  (Pi ((A U)
       (i Nat)
       (l (List A)))
    (Maybe A)))
(define list-ref
  (λ (A i)
    (rec-Nat i
      (maybe-head A)
      (λ (i-1)
        (λ (ret)
          (λ (l)
            (ind-Either (maybe-tail A l)
              (λ (x) (Maybe A))
              (λ (lhs) (ret lhs))
              (λ (rhs) (Nothing A)))))))))

Absurd!!

這個要給多一點尊重

Absurd是type但沒有任何值 (WTF)

但是有eliminator (WTF) eliminate後可以生出任何值 (WTF)

If a false statement were true, then we might as well say anything at all. (the Principle of Explosion or ex falso quodlibet, which means “from false, anything.”)

Q: 如果沒有值怎麼eliminate? A: 假裝有 (從lambda的參數來)

  (λ (1=6) ;; WTF
    (ind-Absurd 1=6
        {return type}))

所以Not就是(-> X Absurd)，也就是X只能推出Absurd，什麼都沒有，也就是沒有證明

vec-ref

這個十分複雜，看不懂沒差，但說說大該是怎麼做的

用Fin去控制vec要不要繼續往下走，看ind-Ether 如果真的走到空(base case)，用ind-Absurd把Absurd劃掉(這樣就是total function了)

(vec-ref Nat 4 (fzero 3) (vec:: 1 (vec:: 2 (vec:: 3 (vec:: 4 vecnil)))))
;; (the Nat 1)
 (vec-ref Nat 4 (fadd1 3 (fzero 2)) (vec:: 1 (vec:: 2 (vec:: 3 (vec:: 4 vecnil)))))
;; (the Nat 2)
(vec-ref Nat 4 (fadd1 3 (fadd1 2 (fzero 1))) (vec:: 1 (vec:: 2 (vec:: 3 (vec:: 4 vecnil)))))
;; (the Nat 3)

把fadd1與fzero看成tail與head，所以vec-ref的任務是把一連串fadd1與fzero用成tail與head在Vec上跑

(claim Fin
  (-> Nat U))
(define Fin
  (λ (n)
    (iter-Nat n
      Absurd
      (λ (ret)
        (Maybe ret)))))
;; 每一個Maybe會分岔出Nothing，所以在iter時都有機會可以到base case
(claim fzero
  (Pi ((n Nat))
    (Fin (add1 n))))
(define fzero
  (λ (n)
    (Nothing (Fin n))))
(claim fadd1
  (Pi ((n Nat))
    (-> (Fin n) (Fin (add1 n)))))
(define fadd1
  (λ (n fin)
    (Just (Fin n) fin)))

(define vec-ref
  (λ (A i)
    (ind-Nat i
      (λ (k) (-> (Fin k) (Vec A k) A))
      (λ (fin v)
        (ind-Absurd fin
          A))
      (λ (i-1)
        (λ (ret)
          (λ (fin v)
            (ind-Either fin
              (λ (k) A)
              (λ (lhs)
                (ret lhs (tail v)))
              (λ (rhs)
                (head v)))))))))

=consequence

	0	(add1 j-1)
0	Trivial	Absurd
(add1 n-1)	Absurd	(= Nat (add1 n-1) (add1 j-1))

(claim =cases
  (-> Nat Nat U)) ;; U 就是兩個比較後，可以知道什麼
(define =cases
  (λ (a b)
    (which-Nat a
      (which-Nat b
        Trivial           ;; 0 = 0 is trivial
        (λ (b-1) Absurd)) ;; 0 = other Nat is Absurd
      (λ (a-1)
        (which-Nat b
          Absurd          ;; other = 0 Nat is Absurd
          (λ (b-1)
            (= Nat a-1 b-1))))))) ;;
(claim =cases-same
  (Pi ((a Nat))
    (=cases a a)))
(define =cases-same
  (λ (a)
    (ind-Nat a
      (λ (x) (=cases x x))
      sole
      (λ (a-1)
        (λ (ret)
          (same a-1))))))

use-Nat= : 生 Not 的函數

(claim use-Nat=
  (Pi ((a Nat)
       (b Nat))
    (-> (= Nat a b) (=cases a b))))
(define use-Nat=
  (λ (a b)
    (λ (a=b)
  (replace a=b ;; 不管是不是真的有就先replace =cases出來的值就對了，
        (λ (x) (=cases a x))
        (=cases-same a)))))
(claim 0!=n+1
  (Pi ((n Nat))
    (-> (= Nat 0 (add1 n)) Absurd)))
(define 0!=n+1
  (λ (n)
    (use-Nat= 0 (add1 n))))

1-!=-6

(claim dount-absurdity
  (-> (= Nat 0 6) (= Atom 'hi 'wow)))
(define dount-absurdity
  (λ (0=6)
    (ind-Absurd (0!=n+1 5 0=6)
      (= Atom 'hi 'wow))))
(claim sub1=
  (Pi ((n Nat)
       (j Nat))
    (-> (= Nat (add1 n) (add1 j))
        (= Nat n j))))
(define sub1=
  (λ (n j)
    ;; (= Nat (add1 n) (add1 j)) 在 =cases 有!!
    ;; 而 use-Nat= 可以生出 =cases
    (use-Nat= (add1 n) (add1 j))))
(claim 1-!=-6
  (-> (= Nat 1 6) Absurd))
(define 1-!=-6
  (λ (1=6) ;; 這裡就是假設有1=6這東西的地方(歸謬法)
    ((use-Nat= 0 5) ((sub1= 0 5) 1=6))))

front

(claim front
  (Pi ((A U)
       (n Nat))
    (-> (Vec A (add1 n)) A))) ;; 這邊無法寫成(-> (Vec A n) A))，因為有要求證明(= Nat n (add1 l))，會強迫把claim改成(-> (Vec A (add1 n)) A)))
(define front
  (λ (A n)
    (λ (v)
      ((ind-Vec (add1 n) v
         (λ (n v)
           (Pi ((l Nat))
             (-> (= Nat n (add1 l)) A))) ;; 要求當前的n必須至少大於1(是某個有1的數字)
           (λ (l)
             (λ (0=otherNat)
               (ind-Absurd (0!=n+1 l 0=otherNat) ;; 假設有0=otherNat的proof，來拉出Absurd
                 A)))
         (λ (n a v-1)
           (λ (ret)
             (λ (l proofWhichWeDontNeed)
               a))))
        n (same (add1 n))))))

排中律(pem，principle excluded middle)

沒有直接的proof說他是對的或錯的但我們可證明pem不是不對的

當初用natural deduction在那邊想很久也沒寫出來，看了解答也是wtf(疑惑) 如今看這個也是wtf(讚嘆)

(claim pem-not-false
  (Pi ((A U))
    (-> (-> (Either A (-> A Absurd))
            Absurd)
        Absurd)))
(define pem-not-false
  (λ (A)
    (λ (!PEM)
      (!PEM (right ;; (1) ??
              (λ (a) ;; WTF 幹，我們有A的value了
                ;; 教訓: 要有function type才有相對應的值
                ;; 值的產生方式: 1. 直接造 2. 從function拉出來 (而function也是值，所以也可以直接造或從function拉出來)
                (!PEM (left a))))))))

decidable : function that decides whether they are true or false

(claim Dec
  (-> U U))
(define Dec
  (λ (X)
    (Either X (-> X Absurd))))
(claim zero?
  (Pi ((n Nat))
    (Dec (= Nat 0 n))))
(define zero?
  (λ (n)
    (ind-Nat n
      (λ (x) (Dec (= Nat 0 x)))
      (left (same 0))
      (λ (n-1)
        (λ (ret)
          (right
            (0!=n+1 n-1)))))))

nat=?

(claim ?orez
  (Pi ((n Nat))
    (Dec (= Nat n 0))))
(define ?orez
  (λ (n)
    (ind-Nat n
      (λ (x) (Dec (= Nat x 0)))
      (left (same 0))
      (λ (n-1)
        (λ (ret)
          (right
            (n+1!=0 n-1)))))))
(claim nat=?
  (Pi ((a Nat)
       (b Nat))
    (Dec (= Nat a b))))
(define nat=?
  (λ (a b)
    ((ind-Nat a
       (λ (k) (Pi ((x Nat))
                (Dec (= Nat k x))))
       (λ (j) (zero? j))
       (λ (a-1)
         (λ (ret)
           (λ (j)
             (ind-Nat j
               (λ (k) (Dec (= Nat (add1 a-1) k)))
               (?orez (add1 a-1))
               (λ (j-1)
                 (λ (ret2)
                   (ind-Either (ret j-1)
                     (λ (x) (Dec (= Nat (add1 a-1) (add1 j-1))))
                     (λ (lhs) (left (cong lhs (+ 1))))
                     (λ (rhs) (right (λ (a=j)
                                       (rhs (sub1= a-1 j-1 a=j)))))))))))))
      b)))

TODO

The Way Forward
Rules are made to be spoken

等看過了

Practical Foundations for Programming Languages, Types and Programming Languages, Semantics Engineering with PLT Redex. <= Prefer this

其中一本再說

ch8 & ch9 & ch10 & ch11#

incr & +#

+1=add1#

incr=add1#

replace#

twice=double#

+add1=add1+#

twice=double with +add1=add1+#

double-vec & twice-vec#

用type去擋掉一些奇怪的實作#

List->Vec#

用證明去擋一些奇怪的實作#

ch12 & ch13#

odd & even#

+2=even#

add1-even->odd#

add1-odd->even#

ackermann function#

Even-or-Odd#

ch14 & ch15 & ch16#

Maybe#

maybe-head & maybe-tail#

list-ref#

Absurd!!#

vec-ref#

=consequence#

use-Nat= : 生 Not 的函數#

1-!=-6#

front#

排中律(pem，principle excluded middle)#

decidable : function that decides whether they are true or false#

nat=?#

TODO#