2008/06/22

是我證的?

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

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

--
距離 FLOLAC '08 還剩 23 天!


真的是我證的 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

Labels:

Blogger Thundermyth O.6/22/2008 4:01 pm 說:

經查,是你在睡夢中證完的 XD

 

<< 回到主頁