2007/12/28

重寫再重寫

改寫 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.

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

Labels: ,

<< 回到主頁