1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/relocation/pr_tl.ma".
17 (* INCLUSION FOR PARTIAL RELOCATION MAPS ************************************)
20 coinductive pr_sle: relation pr_map ≝
22 | pr_sle_push (f1) (f2) (g1) (g2):
23 pr_sle f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → pr_sle g1 g2
25 | pr_sle_next (f1) (f2) (g1) (g2):
26 pr_sle f1 f2 → ↑f1 = g1 → ↑f2 = g2 → pr_sle g1 g2
28 | pr_sle_weak (f1) (f2) (g1) (g2):
29 pr_sle f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → pr_sle g1 g2
33 "inclusion (partial relocation maps)"
34 'subseteq f1 f2 = (pr_sle f1 f2).
36 (* Basic constructions ******************************************************)
39 corec lemma pr_sle_refl:
41 #f cases (pr_map_split_tl f) #H
42 [ @(pr_sle_push … H H) | @(pr_sle_next … H H) ] -H //
45 (* Basic inversions *********************************************************)
48 lemma pr_sle_inv_push_dx:
49 ∀g1,g2. g1 ⊆ g2 → ∀f2. ⫯f2 = g2 →
50 ∃∃f1. f1 ⊆ f2 & ⫯f1 = g1.
52 #f1 #f2 #g1 #g2 #H #H1 #H2 #x2 #Hx2 destruct
53 [ lapply (eq_inv_pr_push_bi … Hx2) -Hx2 /2 width=3 by ex2_intro/ ]
54 elim (eq_inv_pr_push_next … Hx2)
58 lemma pr_sle_inv_next_sn:
59 ∀g1,g2. g1 ⊆ g2 → ∀f1. ↑f1 = g1 →
60 ∃∃f2. f1 ⊆ f2 & ↑f2 = g2.
62 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #Hx1 destruct
63 [2: lapply (eq_inv_pr_next_bi … Hx1) -Hx1 /2 width=3 by ex2_intro/ ]
64 elim (eq_inv_pr_next_push … Hx1)
68 lemma pr_sle_inv_push_next:
69 ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → f1 ⊆ f2.
71 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
72 [ elim (eq_inv_pr_next_push … Hx2)
73 | elim (eq_inv_pr_push_next … Hx1)
74 | lapply (eq_inv_pr_push_bi … Hx1) -Hx1
75 lapply (eq_inv_pr_next_bi … Hx2) -Hx2 //
79 (* Advanced inversions ******************************************************)
82 lemma pr_sle_inv_push_bi:
83 ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2.
84 #g1 #g2 #H #f1 #f2 #H1 #H2
85 elim (pr_sle_inv_push_dx … H … H2) -g2 #x1 #H #Hx1 destruct
86 lapply (eq_inv_pr_push_bi … Hx1) -Hx1 //
90 lemma pr_sle_inv_next_bi:
91 ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ⊆ f2.
92 #g1 #g2 #H #f1 #f2 #H1 #H2
93 elim (pr_sle_inv_next_sn … H … H1) -g1 #x2 #H #Hx2 destruct
94 lapply (eq_inv_pr_next_bi … Hx2) -Hx2 //
98 lemma pr_sle_inv_push_sn:
99 ∀g1,g2. g1 ⊆ g2 → ∀f1. ⫯f1 = g1 →
100 ∨∨ ∃∃f2. f1 ⊆ f2 & ⫯f2 = g2
101 | ∃∃f2. f1 ⊆ f2 & ↑f2 = g2.
103 elim (pr_map_split_tl g2) #H2 #H #f1 #H1
104 [ lapply (pr_sle_inv_push_bi … H … H1 H2)
105 | lapply (pr_sle_inv_push_next … H … H1 H2)
107 /3 width=3 by ex2_intro, or_introl, or_intror/
111 lemma pr_sle_inv_next_dx:
112 ∀g1,g2. g1 ⊆ g2 → ∀f2. ↑f2 = g2 →
113 ∨∨ ∃∃f1. f1 ⊆ f2 & ⫯f1 = g1
114 | ∃∃f1. f1 ⊆ f2 & ↑f1 = g1.
116 elim (pr_map_split_tl g1) #H1 #H #f2 #H2
117 [ lapply (pr_sle_inv_push_next … H … H1 H2)
118 | lapply (pr_sle_inv_next_bi … H … H1 H2)
120 /3 width=3 by ex2_intro, or_introl, or_intror/
123 (* Constructions with pr_tl *************************************************)
126 lemma pr_sle_push_sn_tl:
127 ∀g1,g2. g1 ⊆ g2 → ∀f1. ⫯f1 = g1 → f1 ⊆ ⫰g2.
129 elim (pr_sle_inv_push_sn … H … H1) -H -H1 * //
133 lemma pr_sle_next_dx_tl:
134 ∀g1,g2. g1 ⊆ g2 → ∀f2. ↑f2 = g2 → ⫰g1 ⊆ f2.
136 elim (pr_sle_inv_next_dx … H … H2) -H -H2 * //
141 ∀f1,f2. f1 ⊆ f2 → ⫰f1 ⊆ ⫰f2.
142 #f1 elim (pr_map_split_tl f1) #H1 #f2 #H
143 [ lapply (pr_sle_push_sn_tl … H … H1) -H //
144 | elim (pr_sle_inv_next_sn … H … H1) -H //
148 (* Inversions with pr_tl ****************************************************)
150 (*** sle_inv_tl_sn *)
151 lemma pr_sle_inv_tl_sn:
152 ∀f1,f2. ⫰f1 ⊆ f2 → f1 ⊆ ↑f2.
153 #f1 elim (pr_map_split_tl f1) #H #f2 #Hf12
154 /2 width=5 by pr_sle_next, pr_sle_weak/
157 (*** sle_inv_tl_dx *)
158 lemma pr_sle_inv_tl_dx:
159 ∀f1,f2. f1 ⊆ ⫰f2 → ⫯f1 ⊆ f2.
160 #f1 #f2 elim (pr_map_split_tl f2) #H #Hf12
161 /2 width=5 by pr_sle_push, pr_sle_weak/