2007/12/08

吐舌

Relational derivation 好難!XD 現在 relational fold-fusion theorem 已經證到 inductive case,可是這才是最麻煩的部份,舉步維艱。好像要證好多好多好複雜的 lemma,還要定義更多的 composition XD。然後在做 equality reasoning 的時候可以很輕鬆對局部做代換,現在都不行了(因為變成 "inequality"),痛苦啊 XD。

--
現在 inductive case 實質上只證了一步 XD。


第二步證明中,我在錯誤訊息裡面看到 Set2 了!XD

--
Set2 耶 XD。


喔耶,第二步成功了!XD

Labels:

Anonymous scm12/08/2007 3:11 pm 說:

啊啊,辛苦了。真好奇想看看哩。

也許下週中間我們再見一面?

做 equality reasoning 時我們有 cong 可以用。現在我們則需要依靠 ○ 的 monotonicity :

R ⊆ S => T ○ R ⊆ T ○ S

或許用 application 來表達會比較好用:

R ⊆ S => T · R ⊆ T · S

你碰到的問題跟這有關嗎?

 
Blogger Josh Ko12/08/2007 3:37 pm 說:

現在都是硬做蠻幹,所以非常辛苦。看起來應該要先把一些基本的代數律寫好才會比較好寫。(我現在有點想把它整個刪掉重來,可是又捨不得 XD。)

我還是一樣,星期二下午和星期三下午有空。

我現在是倒著往回證,似乎還沒遇過 monotonicity,或是我沒察覺到。是不是先讀一點相關課本會比較有感覺?現在還常常會突然被符號弄混 XD。

 

<< 回到主頁