1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.tcs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/notation/relations/parallel_2.ma".
16 include "ground_2/relocation/rtmap_isid.ma".
18 (* RELOCATION MAP ***********************************************************)
20 coinductive sdj: relation rtmap ≝
21 | sdj_pp: ∀f1,f2,g1,g2. sdj f1 f2 → ↑f1 = g1 → ↑f2 = g2 → sdj g1 g2
22 | sdj_np: ∀f1,f2,g1,g2. sdj f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → sdj g1 g2
23 | sdj_pn: ∀f1,f2,g1,g2. sdj f1 f2 → ↑f1 = g1 → ⫯f2 = g2 → sdj g1 g2
26 interpretation "disjointness (rtmap)"
27 'Parallel f1 f2 = (sdj f1 f2).
29 (* Basic properties *********************************************************)
31 axiom sdj_eq_repl_back1: ∀f2. eq_repl_back … (λf1. f1 ∥ f2).
33 lemma sdj_eq_repl_fwd1: ∀f2. eq_repl_fwd … (λf1. f1 ∥ f2).
34 #f2 @eq_repl_sym /2 width=3 by sdj_eq_repl_back1/
37 axiom sdj_eq_repl_back2: ∀f1. eq_repl_back … (λf2. f1 ∥ f2).
39 lemma sdj_eq_repl_fwd2: ∀f1. eq_repl_fwd … (λf2. f1 ∥ f2).
40 #f1 @eq_repl_sym /2 width=3 by sdj_eq_repl_back2/
43 corec lemma sdj_sym: symmetric … sdj.
45 #f1 #f2 #g1 #g2 #Hf #H1 #H2
46 [ @(sdj_pp … H2 H1) | @(sdj_pn … H2 H1) | @(sdj_np … H2 H1) ] -g2 -g1
50 (* Basic inversion lemmas ***************************************************)
52 lemma sdj_inv_pp: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ∥ f2.
54 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
55 [ lapply (injective_push … Hx1) -Hx1
56 lapply (injective_push … Hx2) -Hx2 //
57 | elim (discr_push_next … Hx1)
58 | elim (discr_push_next … Hx2)
62 lemma sdj_inv_np: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → f1 ∥ f2.
64 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
65 [ elim (discr_next_push … Hx1)
66 | lapply (injective_next … Hx1) -Hx1
67 lapply (injective_push … Hx2) -Hx2 //
68 | elim (discr_push_next … Hx2)
72 lemma sdj_inv_pn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → f1 ∥ f2.
74 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
75 [ elim (discr_next_push … Hx2)
76 | elim (discr_push_next … Hx1)
77 | lapply (injective_push … Hx1) -Hx1
78 lapply (injective_next … Hx2) -Hx2 //
82 lemma sdj_inv_nn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → ⊥.
84 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
85 [ elim (discr_next_push … Hx1)
86 | elim (discr_next_push … Hx2)
87 | elim (discr_next_push … Hx1)
91 (* Advanced inversion lemmas ************************************************)
93 lemma sdj_inv_nx: ∀g1,g2. g1 ∥ g2 → ∀f1. ⫯f1 = g1 →
94 ∃∃f2. f1 ∥ f2 & ↑f2 = g2.
95 #g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1
96 [ lapply (sdj_inv_np … H … H1 H2) -H /2 width=3 by ex2_intro/
97 | elim (sdj_inv_nn … H … H1 H2)
101 lemma sdj_inv_xn: ∀g1,g2. g1 ∥ g2 → ∀f2. ⫯f2 = g2 →
102 ∃∃f1. f1 ∥ f2 & ↑f1 = g1.
103 #g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2
104 [ lapply (sdj_inv_pn … H … H1 H2) -H /2 width=3 by ex2_intro/
105 | elim (sdj_inv_nn … H … H1 H2)
109 lemma sdj_inv_xp: ∀g1,g2. g1 ∥ g2 → ∀f2. ↑f2 = g2 →
110 ∨∨ ∃∃f1. f1 ∥ f2 & ↑f1 = g1
111 | ∃∃f1. f1 ∥ f2 & ⫯f1 = g1.
112 #g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2
113 [ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_np … H … H1 H2) ] -H -H2
114 /3 width=3 by ex2_intro, or_introl, or_intror/
117 lemma sdj_inv_px: ∀g1,g2. g1 ∥ g2 → ∀f1. ↑f1 = g1 →
118 ∨∨ ∃∃f2. f1 ∥ f2 & ↑f2 = g2
119 | ∃∃f2. f1 ∥ f2 & ⫯f2 = g2.
120 #g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1
121 [ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_pn … H … H1 H2) ] -H -H1
122 /3 width=3 by ex2_intro, or_introl, or_intror/
125 (* Properties with isid *****************************************************)
127 corec lemma sdj_isid_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ∥ f2.
129 #f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) *
130 /3 width=5 by sdj_np, sdj_pp/
133 corec lemma sdj_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ∥ f2.
135 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) *
136 /3 width=5 by sdj_pn, sdj_pp/
139 (* Inversion lemmas with isid ***********************************************)
141 corec lemma sdj_inv_refl: ∀f. f ∥ f → 𝐈⦃f⦄.
142 #f cases (pn_split f) * #g #Hg #H
143 [ lapply (sdj_inv_pp … H … Hg Hg) -H /3 width=3 by isid_push/
144 | elim (sdj_inv_nn … H … Hg Hg)