是我證的？

剛剛想到 min-monotonic 其實可以用 min-universal 來證，於是打開 Minimum.agda，一看 ─ 竟然已經用 min-universal 證完了！我印象中是用 pointwise proof 啊，怎麼突然變成 point-free proof 勒？真的是我證的嗎？XD

不過稍後就順手把 Λ-substitution 改成 algebraic proof 了 XD。scm 老師也該回來了吧…？

--
距離 FLOLAC '08 還剩 2³ 天！

---

真的是我證的 XD。證據：

Tue Jun 10 00:08:35 CST 2008  joshs@...
  * more lemmas proved
[...]
diff -rN old-AoPA/Relations/Minimum.agda new-AoPA/Relations/Minimum.agda
3,4c3,4
< open import Data.Function  using (id)
< open import Data.Product  using (_×_; _,_; map-×)
---
> open import Data.Function  using (id; _$_)
> open import Data.Product  using (_×_; _,_; proj₁; proj₂; map-×)
65a66,81
> min-monotonic : {A B : Set} {R S : A ← A} {T : A ← B} ->
>   R ⊑ S -> min R ₁∘ Λ T ⊑ min S ₁∘ Λ T
> min-monotonic {_}{_} {R} {S} {T} =
>   ⇐-begin
>     min R ₁∘ Λ T ⊑ min S ₁∘ Λ T
>   ⇐⟨ min-universal-⇐ ⟩
>     (min R ₁∘ Λ T ⊑ T × (min R ₁∘ Λ T) ○ T ˘ ⊑ S)
>   ⇐⟨ (\next-line -> (proj₁ $ min-universal-⇒ ⊑-refl) , next-line) ⟩
>     (min R ₁∘ Λ T) ○ T ˘ ⊑ S
>   ⇐⟨ ⊑-trans $ ○-monotonic-l $
>         /-universal-⇒ $ proj₂ $ min-universal-⇒ ⊑-refl ⟩
>     (R / (T ˘)) ○ T ˘ ⊑ S
>   ⇐⟨ ⊑-trans $ /-universal-⇐ ⊑-refl ⟩
>     R ⊑ S
>   ⇐∎
> 
[...]

--
就是揮淚斬 AoPA 的那天嘛！XD