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/gr_tl.ma".
17 (* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
20 coinductive gr_sle: relation gr_map ≝
22 | gr_sle_push (f1) (f2) (g1) (g2):
23 gr_sle f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → gr_sle g1 g2
25 | gr_sle_next (f1) (f2) (g1) (g2):
26 gr_sle f1 f2 → ↑f1 = g1 → ↑f2 = g2 → gr_sle g1 g2
28 | gr_sle_weak (f1) (f2) (g1) (g2):
29 gr_sle f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → gr_sle g1 g2
33 "inclusion (generic relocation maps)"
34 'subseteq f1 f2 = (gr_sle f1 f2).
36 (* Basic constructions ******************************************************)
39 corec lemma gr_sle_refl:
41 #f cases (gr_map_split_tl f) #H
42 [ @(gr_sle_push … H H) | @(gr_sle_next … H H) ] -H //
45 (* Basic inversions *********************************************************)
48 lemma gr_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_gr_push_bi … Hx2) -Hx2 /2 width=3 by ex2_intro/ ]
54 elim (eq_inv_gr_push_next … Hx2)
58 lemma gr_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_gr_next_bi … Hx1) -Hx1 /2 width=3 by ex2_intro/ ]
64 elim (eq_inv_gr_next_push … Hx1)
68 lemma gr_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_gr_next_push … Hx2)
73 | elim (eq_inv_gr_push_next … Hx1)
74 | lapply (eq_inv_gr_push_bi … Hx1) -Hx1
75 lapply (eq_inv_gr_next_bi … Hx2) -Hx2 //
79 (* Advanced inversions ******************************************************)
82 lemma gr_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 (gr_sle_inv_push_dx … H … H2) -g2 #x1 #H #Hx1 destruct
86 lapply (eq_inv_gr_push_bi … Hx1) -Hx1 //
90 lemma gr_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 (gr_sle_inv_next_sn … H … H1) -g1 #x2 #H #Hx2 destruct
94 lapply (eq_inv_gr_next_bi … Hx2) -Hx2 //
98 lemma gr_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 (gr_map_split_tl g2) #H2 #H #f1 #H1
104 [ lapply (gr_sle_inv_push_bi … H … H1 H2)
105 | lapply (gr_sle_inv_push_next … H … H1 H2)
107 /3 width=3 by ex2_intro, or_introl, or_intror/
111 lemma gr_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 (gr_map_split_tl g1) #H1 #H #f2 #H2
117 [ lapply (gr_sle_inv_push_next … H … H1 H2)
118 | lapply (gr_sle_inv_next_bi … H … H1 H2)
120 /3 width=3 by ex2_intro, or_introl, or_intror/
123 (* Constructions with gr_tl *************************************************)
126 lemma gr_sle_push_sn_tl:
127 ∀g1,g2. g1 ⊆ g2 → ∀f1. ⫯f1 = g1 → f1 ⊆ ⫰g2.
129 elim (gr_sle_inv_push_sn … H … H1) -H -H1 * //
133 lemma gr_sle_next_dx_tl:
134 ∀g1,g2. g1 ⊆ g2 → ∀f2. ↑f2 = g2 → ⫰g1 ⊆ f2.
136 elim (gr_sle_inv_next_dx … H … H2) -H -H2 * //
141 ∀f1,f2. f1 ⊆ f2 → ⫰f1 ⊆ ⫰f2.
142 #f1 elim (gr_map_split_tl f1) #H1 #f2 #H
143 [ lapply (gr_sle_push_sn_tl … H … H1) -H //
144 | elim (gr_sle_inv_next_sn … H … H1) -H //
148 (* Inversions with gr_tl ****************************************************)
150 (*** sle_inv_tl_sn *)
151 lemma gr_sle_inv_tl_sn:
152 ∀f1,f2. ⫰f1 ⊆ f2 → f1 ⊆ ↑f2.
153 #f1 elim (gr_map_split_tl f1) #H #f2 #Hf12
154 /2 width=5 by gr_sle_next, gr_sle_weak/
157 (*** sle_inv_tl_dx *)
158 lemma gr_sle_inv_tl_dx:
159 ∀f1,f2. f1 ⊆ ⫰f2 → ⫯f1 ⊆ f2.
160 #f1 #f2 elim (gr_map_split_tl f2) #H #Hf12
161 /2 width=5 by gr_sle_push, gr_sle_weak/