source: src/common/ExtraIdentifiers.ma @ 2801

Last change on this file since 2801 was 2801, checked in by piccolo, 7 years ago

Partial commit not yet finished

File size: 11.5 KB
Line 
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
15include "common/Identifiers.ma".
16
17(*Map for identifier_map *)
18definition map : ∀tag,A,B. identifier_map tag A → (A → B) → identifier_map tag B ≝
19λtag,A,B,m,f.match m with
20[an_id_map p ⇒ an_id_map … (map ?? f p)].
21
22lemma lookup_map : ∀A,B : Type[0].
23  ∀tag : identifierTag.
24  ∀m : identifier_map tag A.
25  ∀ f:A → B.
26  ∀ id.
27lookup tag B (map tag A B m f) id =
28! a ← lookup tag A m id; return f a.
29#A #B #tag * #m #f * #id normalize >lookup_opt_map %
30qed.
31
32
33lemma map_add : ∀tag : identifierTag.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
34map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
35#tag #A #B #f * #m * #id #v normalize @eq_f lapply v -v lapply id -id elim m
36[ #id elim id [#v %] #x #IH #id normalize >IH normalize inversion(pm_set ? ? ? ?)
37  normalize // cases x normalize [2,3,5,6: #y] #EQ destruct
38| #opt_a #l #r #Hl #Hr * [2,3: #x| #v normalize cases opt_a normalize [2: #a %]
39  cases (map_opt ? ? ? l) normalize [2: //] cases (map_opt ? ? ? r) normalize
40  //] #v normalize cases opt_a [2,4: #a] normalize //
41  [ cases(map_opt ? ? ? l) normalize // >Hr cases(map_opt ? ? ? r) normalize
42    [2: #opt_b #lb #rb] inversion(pm_set B x ? ?) normalize // cases x [2,3,5,6: #y]
43    normalize #EQ destruct
44  | >Hl cases(map_opt ? ? ? l) normalize [2: #opt_b #lb #rb]
45    inversion (pm_set B x ? ?) normalize //
46    [1,2: cases x [2,3,5,6: #y] normalize #EQ destruct]
47    #opt_b' #lb' #rb' #_ normalize #_ #EQ cases(map_opt ? ? ? r)
48    normalize nodelta [%] #opt_b'' #lb'' #rb'' >EQ %
49]
50qed.
51
52lemma update_ok_to_lookup : ∀ A : Type[0].
53∀ tag : identifierTag.
54∀m,m' : identifier_map tag A. ∀id,a.
55update tag A m id a = return m' →
56(lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧
57(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id')).
58#A #tag * #m * #m' * #id #a
59whd in ⊢ (??%% →  ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct]
60    #m1 #m1_spec #EQ destruct % [%]
61    [  normalize @(update_lookup_opt_same … m1_spec)
62    |3: * #id' * #id_spec' normalize @(update_lookup_opt_other … m1_spec ??)
63        % #EQ @id_spec' >EQ %
64    | % normalize lapply m1_spec lapply id lapply m' -id -m' elim m
65      [#m' * [|*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [|*: #x]
66      normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct]
67      inversion (update A x a ?) [1,3: #_ normalize #EQ destruct]
68      #pos_map #EQpos_map normalize #EQ destruct [@Hr|@Hl] assumption
69    ]
70qed.
71
72lemma update_def : ∀tag,A,m,i,v.
73  update tag A m i v =
74  match lookup tag A m i with
75  [ Some _ ⇒ OK ? (add tag A m i v)
76  | None ⇒ Error ? [MSG MissingId; CTX … i]
77  ].
78#tag #A #m #i #v inversion(update tag A m i v)
79[ #m' #EQm' cases(update_ok_to_lookup ?????? EQm') * #_
80 #H #_ elim H cases(lookup tag A m i) [#H @⊥ @H %]
81 #x #_ normalize <EQm' lapply EQm' cases i cases m cases m' -m -m' -i
82 normalize #m' #m #i inversion(update A i v m) normalize [#_ #ABS destruct]
83 #m'' #EQm'' #EQ destruct(EQ) @eq_f @eq_f lapply EQm'' -EQm'' lapply i -i
84 lapply m' -m' elim m [#m' * [2,3: #z] normalize #EQ destruct]
85 #opt_a #l #r #Hl #Hr #m' * [2,3: #z] normalize
86 [3: cases opt_a normalize [2: #y] #EQ destruct %
87 |*: inversion(update A z v ?) [2,4: #m'']  #EQm'' normalize #EQ destruct
88     [<(Hr … EQm'') | <(Hl … EQm'')] %
89 ]
90| #err cases m -m cases i -i #i #m normalize inversion(update A i v m) [2:#m']
91  #EQerr normalize #EQ destruct lapply EQerr lapply i elim m
92  [ normalize #x #_ %] #opt_a #l #r #Hl #Hr * [2,3:#z] normalize
93 [3: cases opt_a [2:#w] normalize #EQ destruct %
94 |*: inversion(update A z v ?) [2,4: #m'] #EQm' normalize #EQ destruct
95     [lapply(Hr … EQm') | lapply(Hl … EQm')] cases(lookup_opt A z ?) [2,4: #a]
96     normalize #EQ destruct %
97 ]
98]
99qed.
100
101lemma map_update_commute : ∀tag : identifierTag.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
102update tag B (map tag A B m f) id (f v) =
103!m' ← update tag A m id v; return map tag A B m' f.
104#tag #A #B #f #m #id #v >update_def >update_def >lookup_map
105cases (lookup tag A m id) [%] #a >m_return_bind >m_return_bind normalize nodelta
106whd in ⊢ (???%); @eq_f @sym_eq @map_add
107qed.
108
109(*restriction for maps *)
110definition restrict : ∀tag.∀A,B.
111identifier_map tag A → identifier_map tag B → identifier_map tag A ≝
112λtag,A,B,m1,m2.an_id_map …
113           (merge A B A (λo,o'.match o' with [None ⇒ None ? | Some _ ⇒ o])
114                  (match m1 with [an_id_map p1 ⇒ p1])
115                  (match m2 with [an_id_map p2 ⇒ p2])).
116
117interpretation "identifier map restriction" 'intersects a b = (restrict ??? a b).
118
119unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag).
120 
121lemma lookup_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
122∀i.lookup ?? (a ∩ b) i = if i ∈ b then lookup … a i else None ?.
123#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases (lookup_opt B i b)
124[2: #b] normalize % qed.
125
126lemma update_fail_lookup : ∀tag,A,m,i,v,e.update tag A m i v = Error … e → 
127  e = [MSG MissingId; CTX … i] ∧ lookup … m i = None ?.
128#tag #A #m #i #v #errmsg >update_def cases(lookup tag A m i) [2: #a] normalize
129#EQ destruct % //
130qed.
131
132lemma lookup_miss_update : ∀tag,A,m,i,v.lookup tag A m i = None ? → 
133  update … m i v = Error … [MSG MissingId; CTX … i].
134#tag #A #m #i #v #EQ >update_def >EQ normalize %
135qed.
136
137lemma update_ok_old_lookup : ∀tag,A,m,i,v,m'.update tag A m i v = OK ? m' →
138  i ∈ m.
139#tag #A #m #i #v #m' >update_def inversion(lookup tag A m i) [2: #a] #EQ normalize
140#EQ destruct >EQ normalize @I
141qed.
142
143lemma lookup_update_ok : ∀tag,A,m,i,v,m',i'.update tag A m i v = OK ? m' →
144  lookup … m' i' = if eq_identifier ? i' i then Some ? v else lookup … m i'.
145#tag #A #m #i #v #m' #i' >update_def inversion(lookup tag A m i) [2: #a] #EQ
146normalize nodelta #EQ1 destruct @eq_identifier_elim
147[ #H normalize nodelta >H @lookup_add_hit
148| #H normalize nodelta @lookup_add_miss assumption
149]
150qed.
151
152include "utilities/extra_bool.ma".
153
154lemma mem_set_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
155∀i.i ∈ a ∩ b = (i ∈ a ∧ i ∈ b).
156#tag #A #B * #a * #b  * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
157[2: #a1] normalize [2: @if_elim #_ %] cases(lookup_opt A i a) [2: #a2] normalize %
158qed.
159
160lemma lookup_set_minus : ∀tag,A,B. ∀a : identifier_map tag A. ∀b : identifier_map tag B.
161∀i. lookup ?? (a ∖ b) i = if i ∈ b then None ? else lookup … a i.
162#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
163[2: #b] % qed.
164
165lemma lookup_hit_update : ∀tag,A,m,i,v.i ∈ m → 
166  ∃m'.update tag A m i v = OK ? m'.
167#tag #A #m #i #v #H % [2: >update_def lapply(in_map_domain … m i) >H * #v #EQ >EQ
168normalize %|]
169qed.
170
171lemma add_set_minus  : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
172∀i,v.¬(i ∈ b) → add tag A (a ∖ b) i v = (add tag A a i v) ∖ b.
173#tag #A #B * #a * #b * #i #v @notb_elim @if_elim normalize [#_ *]
174@if_elim [2: #_ *] @if_elim [#_ *] inversion(lookup_opt B i b) normalize [2: #x #_ *]
175#H * * * * @eq_f lapply H -H lapply v -v lapply b -b lapply a -a elim i
176[  *
177  [ * [2: #opt_b #l #r] #v normalize in ⊢ (% → ?); #EQ destruct [2: %]
178  normalize in ⊢ (??%%); cases (map_opt ??? l) // normalize cases(map_opt ??? r)
179  normalize //
180  | * [2: #a] #l #r * [2,4: #opt_b #l1 #r1] #v normalize in ⊢ (% → ?); #EQ destruct
181    normalize [3: % |1,2: cases(merge ???? l l1) // cases(merge ???? r r1) //]
182    cases(map_opt ??? l) normalize // cases(map_opt ??? r) //
183  ]
184|2,3: #x #IH * [2,4: #opt_a #l #r] * [2,4,6,8: #opt_b #l1 #r1] #v
185      normalize in ⊢ (% → ?); #H whd in match (pm_set ????) in ⊢ (???%);
186      whd in match (merge ??????) in ⊢ (???%);
187      [1,2,3,4: <IH try assumption whd in match (pm_set ????) in ⊢ (??%?);
188                whd in match (merge ??????) in ⊢ (??%?); cases opt_b normalize
189                [2,4,6,8: #b] [5,6: cases opt_a normalize //]
190                [1,2,3,4: cases (merge ???? l l1) normalize [2,4,6,8: #opt_a2 #l2 #r2]
191                          // cases (merge ???? r r1) normalize
192                          [2,4,6,8,10,12: #opt_a3 #l3 #r3] inversion(pm_set ????)
193                          normalize // cases x
194                          [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
195                          normalize #EQ destruct
196                |*: cases(map_opt ??? l1) normalize [2,4,6,8: #opt_a2 #l2 #r2] //
197                    cases(map_opt ??? r1) normalize [2,4,6,8,10,12: #opt_a3 #l3 #r3]
198                    inversion(pm_set ????) normalize // cases x
199                    [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
200                    normalize #EQ destruct
201                ]
202     |*: whd in match (pm_set ????) in ⊢ (??%?);
203         whd in match (merge ??????) in ⊢ (??%?); [1,2: cases opt_a [2,4: #a]]
204         normalize
205         [1,2: @eq_f2 [1,4:%] | cases(map_opt ??? l) [2: #opt_a1 #l1 #r1] normalize
206         | cases(map_opt ??? r) [2: #opt_a1 #l1 #r1] normalize]       
207         [1,3,4: lapply(map_add tag A A (λx.x) (an_id_map … r) (an_identifier ? x) v)
208         |2,5,6: lapply(map_add tag A A (λx.x) (an_id_map … l) (an_identifier ? x) v)
209         |*: lapply(map_add tag A A (λx.x) (an_id_map … (pm_leaf ?)) (an_identifier ? x) v)
210         ] normalize #EQ destruct >e0 try % [4,5: cases x [2,3,5,6: #y] normalize %]
211           cases(map_opt ????) [2,4,6: #opt_a1 #l1 #r1] normalize
212           inversion(pm_set ????) normalize // cases x [2,3,5,6,8,9,11,12: #y]
213           normalize #EQ1 destruct
214     ]
215]
216qed.     
217
218lemma update_set_minus : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
219∀i,v.¬(i ∈ b) → update ?? (a ∖ b) i v =
220  ! a' ← update ?? a i v ; return a' ∖ b.
221#tag #A #B #a #b #id #v #H >update_def >lookup_set_minus @if_elim
222[ #H1 @⊥ lapply H1 lapply H @notb_elim >H1 normalize *] #_ >update_def
223cases (lookup tag A a id) normalize [ %] #a @eq_f @add_set_minus assumption
224qed.
225
226
227lemma add_idempotent : ∀tag,A.∀m : identifier_map tag A. ∀i,a1,a2.
228add tag A (add tag A m i a1) i a2 = add tag A m i a2.
229#tag #A * #m * #i #a1 #a2 normalize @eq_f lapply a1 -a1 lapply a2 -a2 lapply m -m
230elim i
231[ * [ #a1 #a2 %] #opt_a #l #r #a1 #a2 %] #x #IH *
232[1,3: #a1 #a2 normalize @eq_f2 try % @IH] #opt_a #l1 #l2 #a1 #a2 normalize
233@eq_f2 try % @IH
234qed.
235
236
237lemma empty_set_minus : ∀tag,A,B.∀m : identifier_map tag B. empty_map tag A =
238empty_map tag A ∖ m.
239#tag #A #B * #m normalize @eq_f elim m [%] #opt_b #l #r #IHl #IHr normalize
240cases opt_b normalize [2: #b] <IHl <IHr %
241qed.
242
243
Note: See TracBrowser for help on using the repository browser.