暴力證明 Relational Fold-Fusion

我想這個證明是一定要重寫的，所以我就不花時間多做解釋了 XD。基本上就是把 scm 老師給的證明很暴力地轉成 Agda。

首先是把 relational fold 重整成 functional fold。這個部份還好，用 ⊆ 的 reflexivity 就過去了。

fun-to-rel : {A B C : Set} -> 
  (R : C ← B) (S : B ← (A × B)) (T : C ← (A × C)) (U : ℙ B) (V : ℙ C) ->
  ∀ (\x -> (foldr (Λ₁ (T ○₁ (idR ⨉₁ ∈))) V x)
         ⊆ (Λ₁ (R ○₁ ∈) (foldr (Λ₁ (S ○₁ (idR ⨉₁ ∈))) U x))) ->
  (R ○ fold S U) ⊇ fold T V
fun-to-rel R S T U V ⊆-pf x =
  chain> Λ(fold T V) x
       ⊂ foldr (Λ₁ (T ○₁ (idR ⨉₁ ∈))) V x by refl-⊆
       ⊂ Λ₁(R ○₁ ∈) (foldr (Λ₁ (S ○₁ (idR ⨉₁ ∈))) U x) by ⊆-pf x
       ⊂ Λ₁(R ○₁ ∈) (Λ (fold S U) x) by refl-⊆
       ⊂ (Λ₁(R ○₁ ∈) ₁○ Λ (fold S U)) x by refl-⊆
       ⊂ Λ(R ○ fold S U) x by refl-⊆

接下來是在 funciontal fold 上證明 fusion。那些 lemmas 都是暴力產生的 XD。

fusion : {A B C : Set} ->
  (R : C ← B) (S : B ← (A × B)) (T : C ← (A × C)) (U : ℙ B) (V : ℙ C) ->
  (R ○ S) ⊇ (T ○ (idR ⨉ R)) -> V ⊆ Λ₁ (R ○₁ ∈) U ->
  ∀ (\x -> (foldr (Λ₁ (T ○₁ (idR ⨉₁ ∈))) V x)
         ⊆ (Λ₁ (R ○₁ ∈) (foldr (Λ₁ (S ○₁ (idR ⨉₁ ∈))) U x)))
fusion R S T U V step-cond base-cond [] =
  chain> (foldr (Λ₁ (T ○₁ (idR ⨉₁ ∈))) V [])
       ⊂ V by refl-⊆
       ⊂ Λ₁ (R ○₁ ∈) U by base-cond
fusion R S T U V step-cond base-cond (a :: x) =
  chain> foldr (Λ₁ (T ○₁ (idR ⨉₁ ∈))) V (a :: x)
       ⊂ Λ₁ (T ○₁ (idR ⨉₁ ∈)) < a , foldr (Λ₁(T ○₁ (idR ⨉₁ ∈))) V x >₁
           by refl-⊆
       ⊂ Λ₁ (T ○₁ (idR ⨉₁ ∈))
            < a , Λ₁(R ○₁ ∈) (foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x) >₁
           by lemma1 T (fusion R S T U V step-cond base-cond x) a
       ⊂ Λ₁ (T ○₁ (idR ⨉₁ ∈))
            (〈 id , Λ₁ (R ○₁ ∈) 〉₁ < a , foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x >₁)
           by lemma2 (Λ₁ (T ○₁ (idR ⨉₁ ∈))) R a
                     (foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x)
       ⊂ Λ₁ (T ○₁ (idR ⨉₁ (R ○₁ ∈)))
           < a , foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x >₁
           by lemma3 T (R ○₁ ∈) a (foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x)
       ⊂ Λ₁ ((T ○ (idR ⨉ R)) ○₁ (idR ⨉₁ ∈))
           < a , foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x >₁
           by lemma4 R T a (foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x)
       ⊂ Λ₁ ((R ○ S) ○₁ (idR ⨉₁ ∈))
           < a , foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x >₁
           by lemma5 R S T (idR ⨉₁ ∈) step-cond a
                     (foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x)
       ⊂ Λ₁ (R ○₁ ∈) (Λ₁ (S ○₁ (idR ⨉₁ ∈))
            < a , foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x >₁)
           by lemma6 R S (idR ⨉₁ ∈) a (foldr (Λ₁(S ○₁ (idR ⨉₁ ∈))) U x)
       ⊂ Λ₁ (R ○₁ ∈) (foldr (Λ₁ (S ○₁ (idR ⨉₁ ∈))) U (a :: x))
           by refl-⊆
  where
    lemma1 : {A B C : Set} {s t : ℙ B} (T : C ← (A × B)) -> s ⊆ t ->
               ∀ (\a -> Λ₁ (T ○₁ (idR ⨉₁ ∈)) < a , s >₁
                      ⊆ Λ₁ (T ○₁ (idR ⨉₁ ∈)) < a , t >₁)
    lemma1 _ s⊆t a x (∃-I < a' , b' > (/\-I (/\-I a≡a' sb') T<a',b'>x))=
      ∃-I < a' , b' > (/\-I (/\-I a≡a' (s⊆t b' sb')) T<a',b'>x)

    lemma2 : {A B C : Set} (F : (A ×₁ ℙ C) -> ℙ C) (R : C ← B) ->
               (a : A) -> (bs : ℙ B) ->
               F < a , Λ₁(R ○₁ ∈) bs >₁ ⊆ F (〈 id , Λ₁ (R ○₁ ∈) 〉₁ < a , bs >₁)
    lemma2 _ _ _ _ _ pf = pf

    lemma3 : {A B C : Set} (T : C ← (A × C)) (X : C ←₁ ℙ B) ->
               (a : A) -> (bs : ℙ B) ->
               Λ₁(T ○₁ (idR ⨉₁ ∈)) (〈 id , Λ₁ X 〉₁ < a , bs >₁)
             ⊆ Λ₁(T ○₁ (idR ⨉₁ X)) < a , bs >₁
    lemma3 T X a bs c (∃-I < a' , c' > pf) = ∃-I < a' , c' > pf

    lemma4 : {A B C : Set} (R : C ← B) (T : C ← (A × C)) ->
               (a : A) (bs : ℙ B) ->
               Λ₁ (T ○₁ (idR ⨉₁ (R ○₁ ∈))) < a , bs >₁
             ⊆ Λ₁ ((T ○ (idR ⨉ R)) ○₁ (idR ⨉₁ ∈)) < a , bs >₁
    lemma4 _ _ _ _ _
           (∃-I < a' , c' > (/\-I (/\-I pf1 (∃-I b' (/\-I pf2 pf3))) pf4)) =
      ∃-I < a' , b' >
          (/\-I (/\-I pf1 pf2) (∃-I < a' , c' > (/\-I (/\-I refl pf3) pf4)))

    lemma5 : {A B C : Set} (R : C ← B) (S : B ← (A × B)) 
                           (T : C ← (A × C)) (X : (A × B) ←₁ (A ×₁ ℙ B)) ->
               (R ○ S) ⊇ (T ○ (idR ⨉ R)) -> (a : A) -> (bs : ℙ B) ->
               Λ₁ ((T ○ (idR ⨉ R)) ○₁ X) < a , bs >₁
             ⊆ Λ₁ ((R ○ S) ○₁ X) < a , bs >₁
    lemma5 _ _ _ _ pf1 _ _ c (∃-I < a' , b' > (/\-I pf2 pf3)) =
      ∃-I < a' , b' > (/\-I pf2 (pf1 < a' , b' > c pf3))

    lemma6 : {A B C : Set}
               (R : C ← B) (S : B ← (A × B)) (X : (A × B) ←₁ (A ×₁ ℙ B)) ->
               (a : A) -> (bs : ℙ B) ->
               Λ₁ ((R ○ S) ○₁ X) < a , bs >₁
             ⊆ Λ₁ (R ○₁ ∈) (Λ₁ (S ○₁ X) < a , bs >₁)
    lemma6 _ _ _ _ _ c (∃-I < a , b > (/\-I pf1 (∃-I b' (/\-I pf2 pf3)))) =
      ∃-I b' (/\-I (∃-I < a , b > (/\-I pf1 pf2)) pf3)

最後把上面兩個證明組合起來，就得到整個 relational fold-fusion theorem。

rel-fold-fusion : {A B C : Set} ->
  (R : C ← B) (S : B ← (A × B)) (T : C ← (A × C)) (U : ℙ B) (V : ℙ C) ->
  (R ○ S) ⊇ (T ○ (idR ⨉ R)) -> V ⊆ Λ₁ (R ○₁ ∈) U -> (R ○ fold S U) ⊇ fold T V
rel-fold-fusion R S T U V step-cond base-cond =
  fun-to-rel R S T U V (fusion R S T U V step-cond base-cond)

--
真是太暴力了 XD。