$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2007/12/09

### 暴力證明 Relational Fold-Fusion

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-⊆


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)


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)


--

Labels: