重寫再重寫

改寫 pipe reasoning 使它也能處理 (B : Set) <- (A : Set1) 的東西，卻發現難以下手，直到我終於會用小黑點，才明白 scm 老師當初的苦心 XD。之後把所有的暴力證明全部用 pipe reasoning 重寫一遍，有比較好看一點。例如剛剛那個 subcase 現在變成

... | no  a≰b =
  a , b ∷ x
  ≫ combine → b ∷ insert a x by inj₂ (exists {_} {_} {b , insert a x}
                                   ((≡-refl , insert⊑combine (a , x)
                                   (insert a x) ≡-refl) , ≡-refl))
  → ordered? → b ∷ insert a x by (
      b ,₁ ordered? (insert a x)
      ≫₁ idR ⨉₁ ∈ → b , insert a x by ≡-refl , insert-respects-order
                                                 a x ordered-x-x
      → cons ○ (lbound ﹖) → b ∷ insert a x by (
          b , insert a x
          ≫ lbound ﹖ → b , insert a x by ≡-refl ,
                                          insert-respects-lbound 
                                            a b x lbound-b,x
                                            (<-relax (≰-elim a≰b))
          → cons → b ∷ insert a x by ≡-refl
          →∎)
      →∎)
  ↪ y by insert-a-b∷x≡y
  →∎

知道 pipe reasoning 在幹麼的話應該就比較容易看得懂，不過這只是形式上改寫，實質上做的事情是一樣的。（可是這種東西本來就是 formal？XD）scm 老師看到我寫出那團亂碼，特地寄來三頁代數證明，就甘心耶！所以再看看有沒有機會把它改成代數式證明。剛才把最新的 code 推上 darcs repository，發現 scm 老師也在剛剛把 paper revision 推上去，大家都在拚命工作 XD。

Projects 和 finals 紛紛出籠了，而且都不太溫和。從現在到學期末前應該沒一刻得閒。AI term project 要和不認識的人在一星期內搞定；DCL final project 還不知道難度；知識論期末考的題目有深度，不開始準備不行；宋明理學下半段已經談了程頤、朱熹，抓不太到綱領；作業系統和資料庫系統印象都模糊一片；圖論也不是讀得那麼顆粒分明。Anyway, let's do it.

--
覺得自己好弱喔，大三都過一半了，是不是覺悟得太晚了…