]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_sdj.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/notation/relations/parallel_2.ma".
16 include "ground/relocation/pr_tl.ma".
17
18 (* DISJOINTNESS FOR PARTIAL RELOCATION MAPS *********************************)
19
20 (*** sdj *)
21 coinductive pr_sdj: relation pr_map ≝
22 (*** sdj_pp *)
23 | pr_sdj_push_bi (f1) (f2) (g1) (g2):
24   pr_sdj f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → pr_sdj g1 g2
25 (*** sdj_np *)
26 | pr_sdj_next_push (f1) (f2) (g1) (g2):
27   pr_sdj f1 f2 → ↑f1 = g1 → ⫯f2 = g2 → pr_sdj g1 g2
28 (*** sdj_pn *)
29 | pr_sdj_push_next (f1) (f2) (g1) (g2):
30   pr_sdj f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → pr_sdj g1 g2
31 .
32
33 interpretation
34   "disjointness (partial relocation maps)"
35   'Parallel f1 f2 = (pr_sdj f1 f2).
36
37 (* Basic constructions ******************************************************)
38
39 (*** sdj_sym *)
40 corec lemma pr_sdj_sym:
41             symmetric … pr_sdj.
42 #f1 #f2 * -f1 -f2
43 #f1 #f2 #g1 #g2 #Hf #H1 #H2
44 [ @(pr_sdj_push_bi … H2 H1)
45 | @(pr_sdj_push_next … H2 H1)
46 | @(pr_sdj_next_push … H2 H1)
47 ] -g2 -g1
48 /2 width=1 by/
49 qed-.
50
51 (* Basic inversions *********************************************************)
52
53 (*** sdj_inv_pp *)
54 lemma pr_sdj_inv_push_bi:
55       ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ∥ f2.
56 #g1 #g2 * -g1 -g2
57 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
58 [ lapply (eq_inv_pr_push_bi … Hx1) -Hx1
59   lapply (eq_inv_pr_push_bi … Hx2) -Hx2 //
60 | elim (eq_inv_pr_push_next … Hx1)
61 | elim (eq_inv_pr_push_next … Hx2)
62 ]
63 qed-.
64
65 (*** sdj_inv_np *)
66 lemma pr_sdj_inv_next_push:
67       ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → f1 ∥ f2.
68 #g1 #g2 * -g1 -g2
69 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
70 [ elim (eq_inv_pr_next_push … Hx1)
71 | lapply (eq_inv_pr_next_bi … Hx1) -Hx1
72   lapply (eq_inv_pr_push_bi … Hx2) -Hx2 //
73 | elim (eq_inv_pr_push_next … Hx2)
74 ]
75 qed-.
76
77 (*** sdj_inv_pn *)
78 lemma pr_sdj_inv_push_next:
79       ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → f1 ∥ f2.
80 #g1 #g2 * -g1 -g2
81 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
82 [ elim (eq_inv_pr_next_push … Hx2)
83 | elim (eq_inv_pr_push_next … Hx1)
84 | lapply (eq_inv_pr_push_bi … Hx1) -Hx1
85   lapply (eq_inv_pr_next_bi … Hx2) -Hx2 //
86 ]
87 qed-.
88
89 (*** sdj_inv_nn *)
90 lemma pr_sdj_inv_next_bi:
91       ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → ⊥.
92 #g1 #g2 * -g1 -g2
93 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
94 [ elim (eq_inv_pr_next_push … Hx1)
95 | elim (eq_inv_pr_next_push … Hx2)
96 | elim (eq_inv_pr_next_push … Hx1)
97 ]
98 qed-.
99
100 (* Advanced inversions ******************************************************)
101
102 (*** sdj_inv_nx *)
103 lemma pr_sdj_inv_next_sn:
104       ∀g1,g2. g1 ∥ g2 → ∀f1. ↑f1 = g1 →
105       ∃∃f2. f1 ∥ f2 & ⫯f2 = g2.
106 #g1 #g2 elim (pr_map_split_tl g2) #H2 #H #f1 #H1
107 [ lapply (pr_sdj_inv_next_push … H … H1 H2) -H /2 width=3 by ex2_intro/
108 | elim (pr_sdj_inv_next_bi … H … H1 H2)
109 ]
110 qed-.
111
112 (*** sdj_inv_xn *)
113 lemma pr_sdj_inv_next_dx:
114       ∀g1,g2. g1 ∥ g2 → ∀f2. ↑f2 = g2 →
115       ∃∃f1. f1 ∥ f2 & ⫯f1 = g1.
116 #g1 #g2 elim (pr_map_split_tl g1) #H1 #H #f2 #H2
117 [ lapply (pr_sdj_inv_push_next … H … H1 H2) -H /2 width=3 by ex2_intro/
118 | elim (pr_sdj_inv_next_bi … H … H1 H2)
119 ]
120 qed-.
121
122 (*** sdj_inv_xp *)
123 lemma pr_sdj_inv_push_dx:
124       ∀g1,g2. g1 ∥ g2 → ∀f2. ⫯f2 = g2 →
125       ∨∨ ∃∃f1. f1 ∥ f2 & ⫯f1 = g1
126        | ∃∃f1. f1 ∥ f2 & ↑f1 = g1.
127 #g1 #g2 elim (pr_map_split_tl g1) #H1 #H #f2 #H2
128 [ lapply (pr_sdj_inv_push_bi … H … H1 H2)
129 | lapply (pr_sdj_inv_next_push … H … H1 H2)
130 ] -H -H2
131 /3 width=3 by ex2_intro, or_introl, or_intror/
132 qed-.
133
134 (*** sdj_inv_px *)
135 lemma pr_sdj_inv_push_sn:
136       ∀g1,g2. g1 ∥ g2 → ∀f1. ⫯f1 = g1 →
137       ∨∨ ∃∃f2. f1 ∥ f2 & ⫯f2 = g2
138        | ∃∃f2. f1 ∥ f2 & ↑f2 = g2.
139 #g1 #g2 elim (pr_map_split_tl g2) #H2 #H #f1 #H1
140 [ lapply (pr_sdj_inv_push_bi … H … H1 H2)
141 | lapply (pr_sdj_inv_push_next … H … H1 H2)
142 ] -H -H1
143 /3 width=3 by ex2_intro, or_introl, or_intror/
144 qed-.