吐舌
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: Agda
啊啊，辛苦了。真好奇想看看哩。
也許下週中間我們再見一面？
做 equality reasoning 時我們有 cong 可以用。現在我們則需要依靠 ○ 的 monotonicity :
R ⊆ S => T ○ R ⊆ T ○ S
或許用 application 來表達會比較好用:
R ⊆ S => T · R ⊆ T · S
你碰到的問題跟這有關嗎？
現在都是硬做蠻幹，所以非常辛苦。看起來應該要先把一些基本的代數律寫好才會比較好寫。（我現在有點想把它整個刪掉重來，可是又捨不得 XD。）
我還是一樣，星期二下午和星期三下午有空。
我現在是倒著往回證，似乎還沒遇過 monotonicity，或是我沒察覺到。是不是先讀一點相關課本會比較有感覺？現在還常常會突然被符號弄混 XD。
<< 回到主頁