(* RELOCATION MAP ***********************************************************)
coinductive sdj: relation rtmap ≝
-| sdj_pp: â\88\80f1,f2,g1,g2. sdj f1 f2 â\86\92 â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 → sdj g1 g2
-| sdj_np: â\88\80f1,f2,g1,g2. sdj f1 f2 â\86\92 ⫯f1 = g1 â\86\92 â\86\91f2 = g2 → sdj g1 g2
-| sdj_pn: â\88\80f1,f2,g1,g2. sdj f1 f2 â\86\92 â\86\91f1 = g1 â\86\92 ⫯f2 = g2 → sdj g1 g2
+| sdj_pp: â\88\80f1,f2,g1,g2. sdj f1 f2 â\86\92 ⫯f1 = g1 â\86\92 ⫯f2 = g2 → sdj g1 g2
+| sdj_np: â\88\80f1,f2,g1,g2. sdj f1 f2 â\86\92 â\86\91f1 = g1 â\86\92 ⫯f2 = g2 → sdj g1 g2
+| sdj_pn: â\88\80f1,f2,g1,g2. sdj f1 f2 â\86\92 ⫯f1 = g1 â\86\92 â\86\91f2 = g2 → sdj g1 g2
.
interpretation "disjointness (rtmap)"
(* Basic inversion lemmas ***************************************************)
-lemma sdj_inv_pp: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 → f1 ∥ f2.
+lemma sdj_inv_pp: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 ⫯f2 = g2 → f1 ∥ f2.
#g1 #g2 * -g1 -g2
#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
[ lapply (injective_push … Hx1) -Hx1
]
qed-.
-lemma sdj_inv_np: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 â\86\91f2 = g2 → f1 ∥ f2.
+lemma sdj_inv_np: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 ⫯f2 = g2 → f1 ∥ f2.
#g1 #g2 * -g1 -g2
#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
[ elim (discr_next_push … Hx1)
]
qed-.
-lemma sdj_inv_pn: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 ⫯f2 = g2 → f1 ∥ f2.
+lemma sdj_inv_pn: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 â\86\91f2 = g2 → f1 ∥ f2.
#g1 #g2 * -g1 -g2
#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
[ elim (discr_next_push … Hx2)
]
qed-.
-lemma sdj_inv_nn: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 ⫯f2 = g2 → ⊥.
+lemma sdj_inv_nn: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 → ⊥.
#g1 #g2 * -g1 -g2
#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
[ elim (discr_next_push … Hx1)
(* Advanced inversion lemmas ************************************************)
-lemma sdj_inv_nx: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1. ⫯f1 = g1 →
- â\88\83â\88\83f2. f1 â\88¥ f2 & â\86\91f2 = g2.
+lemma sdj_inv_nx: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1. â\86\91f1 = g1 →
+ â\88\83â\88\83f2. f1 â\88¥ f2 & ⫯f2 = g2.
#g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1
[ lapply (sdj_inv_np … H … H1 H2) -H /2 width=3 by ex2_intro/
| elim (sdj_inv_nn … H … H1 H2)
]
qed-.
-lemma sdj_inv_xn: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f2. ⫯f2 = g2 →
- â\88\83â\88\83f1. f1 â\88¥ f2 & â\86\91f1 = g1.
+lemma sdj_inv_xn: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f2. â\86\91f2 = g2 →
+ â\88\83â\88\83f1. f1 â\88¥ f2 & ⫯f1 = g1.
#g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2
[ lapply (sdj_inv_pn … H … H1 H2) -H /2 width=3 by ex2_intro/
| elim (sdj_inv_nn … H … H1 H2)
]
qed-.
-lemma sdj_inv_xp: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f2. â\86\91f2 = g2 →
- â\88¨â\88¨ â\88\83â\88\83f1. f1 â\88¥ f2 & â\86\91f1 = g1
- | â\88\83â\88\83f1. f1 â\88¥ f2 & ⫯f1 = g1.
+lemma sdj_inv_xp: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f2. ⫯f2 = g2 →
+ â\88¨â\88¨ â\88\83â\88\83f1. f1 â\88¥ f2 & ⫯f1 = g1
+ | â\88\83â\88\83f1. f1 â\88¥ f2 & â\86\91f1 = g1.
#g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2
[ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_np … H … H1 H2) ] -H -H2
/3 width=3 by ex2_intro, or_introl, or_intror/
qed-.
-lemma sdj_inv_px: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1. â\86\91f1 = g1 →
- â\88¨â\88¨ â\88\83â\88\83f2. f1 â\88¥ f2 & â\86\91f2 = g2
- | â\88\83â\88\83f2. f1 â\88¥ f2 & ⫯f2 = g2.
+lemma sdj_inv_px: â\88\80g1,g2. g1 â\88¥ g2 â\86\92 â\88\80f1. ⫯f1 = g1 →
+ â\88¨â\88¨ â\88\83â\88\83f2. f1 â\88¥ f2 & ⫯f2 = g2
+ | â\88\83â\88\83f2. f1 â\88¥ f2 & â\86\91f2 = g2.
#g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1
[ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_pn … H … H1 H2) ] -H -H1
/3 width=3 by ex2_intro, or_introl, or_intror/
(* Properties with isid *****************************************************)
-corec lemma sdj_isid_dx: â\88\80f2. ð\9d\90\88â¦\83f2â¦\84 → ∀f1. f1 ∥ f2.
+corec lemma sdj_isid_dx: â\88\80f2. ð\9d\90\88â\9dªf2â\9d« → ∀f1. f1 ∥ f2.
#f2 * -f2
#f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) *
/3 width=5 by sdj_np, sdj_pp/
qed.
-corec lemma sdj_isid_sn: â\88\80f1. ð\9d\90\88â¦\83f1â¦\84 → ∀f2. f1 ∥ f2.
+corec lemma sdj_isid_sn: â\88\80f1. ð\9d\90\88â\9dªf1â\9d« → ∀f2. f1 ∥ f2.
#f1 * -f1
#f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) *
/3 width=5 by sdj_pn, sdj_pp/
(* Inversion lemmas with isid ***********************************************)
-corec lemma sdj_inv_refl: â\88\80f. f â\88¥ f â\86\92 ð\9d\90\88â¦\83fâ¦\84.
+corec lemma sdj_inv_refl: â\88\80f. f â\88¥ f â\86\92 ð\9d\90\88â\9dªfâ\9d«.
#f cases (pn_split f) * #g #Hg #H
[ lapply (sdj_inv_pp … H … Hg Hg) -H /3 width=3 by isid_push/
| elim (sdj_inv_nn … H … Hg Hg)