source: src/common/ExtraIdentifiers.ma @ 3217

Last change on this file since 3217 was 3217, checked in by piccolo, 6 years ago

Correctness of ERTL to LTL in place

File size: 15.0 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
17lemma fold_insert_singleton : ∀A,B : Type[0].∀a :A.
18∀i : Pos.∀f,b.
19fold A B f (pm_set A i (Some ? a) (pm_leaf A)) b = f i a b.
20#A #B #a #i elim i -i normalize
21[//] #i #IH #f #b @IH
22qed.
23   
24
25definition find_all : ∀tag,A. identifier_map tag A →
26(identifier tag → A → bool) → identifier_map tag A ≝
27λtag,A,m,P.foldi A (identifier_map tag A) tag
28(λi,a,l.if (P i a) then (add tag A l i a) else l) m (empty_map tag A).
29
30
31lemma find_all_lookup_predicate : ∀tag,A.∀m : identifier_map tag A.
32∀P : (identifier tag → A → bool).∀i,a.
33lookup tag A (find_all tag A m P) i = Some ? a →
34lookup tag A m i = Some ? a  ∧ (bool_to_Prop (P i a)).
35#tag #A #m #P #i #a whd in match find_all; normalize nodelta @foldi_ind
36[ normalize #EQ destruct
37| #k #ks #a1 #b * #H #H1 #H2 inversion(P k a1)
38  [ #H3 normalize nodelta >H3
39    cut(bool_to_Prop (eq_identifier tag i k) ∨
40     (bool_to_Prop (notb (eq_identifier tag i k))))
41    [@eq_identifier_elim #_ [ %%|%2 %]]
42    @eq_identifier_elim
43    [ #EQ destruct(EQ) #_ >lookup_add_hit #EQ destruct(EQ) %{H1} >H3 @I
44    | #H4 #_ >lookup_add_miss [2: assumption] @H2
45    ]
46  | #H3 normalize nodelta @H2
47  ]
48]
49qed.
50
51
52lemma find_find_all : ∀tag,A.∀m : identifier_map tag A.
53∀P : (identifier tag → A → bool).∀i,a. lookup tag A m i = Some ? a →
54P i a → lookup tag A (find_all tag A m P) i = Some ? a.
55#tag #A #m #P #i #a #H #H1 cut(present tag unit (domain_of_map … m) i)
56[ cases(domain_of_map_present tag A m i) #H2 #_ @H2 whd >H % #EQ destruct]
57whd in match find_all; normalize nodelta @foldi_ind
58[ whd in ⊢ (% → ?); * #H2 @⊥ @H2 %]
59#k #ks #a1 #b * #H2 #H3 #H4 #H5
60cut(bool_to_Prop (eq_identifier tag i k) ∨
61    (bool_to_Prop (notb (eq_identifier tag i k))))
62[ @eq_identifier_elim #_ [ % % | %2 %] ]
63@eq_identifier_elim
64[ #EQ destruct(EQ) #_ >H in H3; #EQ destruct(EQ) >H1 normalize nodelta @lookup_add_hit
65| #EQ #_ cases(P k a1) normalize nodelta
66  [>lookup_add_miss [2: assumption] ]
67  @H4 whd % #H6 elim H5 #H5 @H5 >lookup_add_miss //
68]
69qed.
70
71(*
72 whd in match (add ?????); whd in match (add ?????); normalize nodelta
73whd in match (domain_of_map ???); whd in match (domain_of_map ???); normalize nodelta @eq_f
74whd in match (domain_of_pm ??); whd in match (domain_of_pm ??) in ⊢ (???%); *)
75
76
77axiom add_find_all : ∀tag,A.∀m : identifier_map tag A.
78∀P : (identifier tag → A → bool).∀i,a.P i a →
79add tag A (find_all tag A m P) i a = find_all tag A (add tag A m i a) P.
80
81 
82(*Map for identifier_map *)
83definition map : ∀tag,A,B. identifier_map tag A → (A → B) → identifier_map tag B ≝
84λtag,A,B,m,f.match m with
85[an_id_map p ⇒ an_id_map … (map ?? f p)].
86
87lemma lookup_map : ∀A,B : Type[0].
88  ∀tag : identifierTag.
89  ∀m : identifier_map tag A.
90  ∀ f:A → B.
91  ∀ id.
92lookup tag B (map tag A B m f) id =
93! a ← lookup tag A m id; return f a.
94#A #B #tag * #m #f * #id normalize >lookup_opt_map %
95qed.
96
97
98lemma map_add : ∀tag : identifierTag.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
99map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
100#tag #A #B #f * #m * #id #v normalize @eq_f lapply v -v lapply id -id elim m
101[ #id elim id [#v %] #x #IH #id normalize >IH normalize inversion(pm_set ? ? ? ?)
102  normalize // cases x normalize [2,3,5,6: #y] #EQ destruct
103| #opt_a #l #r #Hl #Hr * [2,3: #x| #v normalize cases opt_a normalize [2: #a %]
104  cases (map_opt ? ? ? l) normalize [2: //] cases (map_opt ? ? ? r) normalize
105  //] #v normalize cases opt_a [2,4: #a] normalize //
106  [ cases(map_opt ? ? ? l) normalize // >Hr cases(map_opt ? ? ? r) normalize
107    [2: #opt_b #lb #rb] inversion(pm_set B x ? ?) normalize // cases x [2,3,5,6: #y]
108    normalize #EQ destruct
109  | >Hl cases(map_opt ? ? ? l) normalize [2: #opt_b #lb #rb]
110    inversion (pm_set B x ? ?) normalize //
111    [1,2: cases x [2,3,5,6: #y] normalize #EQ destruct]
112    #opt_b' #lb' #rb' #_ normalize #_ #EQ cases(map_opt ? ? ? r)
113    normalize nodelta [%] #opt_b'' #lb'' #rb'' >EQ %
114]
115qed.
116
117lemma update_ok_to_lookup : ∀ A : Type[0].
118∀ tag : identifierTag.
119∀m,m' : identifier_map tag A. ∀id,a.
120update tag A m id a = return m' →
121(lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧
122(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id')).
123#A #tag * #m * #m' * #id #a
124whd in ⊢ (??%% →  ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct]
125    #m1 #m1_spec #EQ destruct % [%]
126    [  normalize @(update_lookup_opt_same … m1_spec)
127    |3: * #id' * #id_spec' normalize @(update_lookup_opt_other … m1_spec ??)
128        % #EQ @id_spec' >EQ %
129    | % normalize lapply m1_spec lapply id lapply m' -id -m' elim m
130      [#m' * [|*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [|*: #x]
131      normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct]
132      inversion (update A x a ?) [1,3: #_ normalize #EQ destruct]
133      #pos_map #EQpos_map normalize #EQ destruct [@Hr|@Hl] assumption
134    ]
135qed.
136
137lemma update_def : ∀tag,A,m,i,v.
138  update tag A m i v =
139  match lookup tag A m i with
140  [ Some _ ⇒ OK ? (add tag A m i v)
141  | None ⇒ Error ? [MSG MissingId; CTX … i]
142  ].
143#tag #A #m #i #v inversion(update tag A m i v)
144[ #m' #EQm' cases(update_ok_to_lookup ?????? EQm') * #_
145 #H #_ elim H cases(lookup tag A m i) [#H @⊥ @H %]
146 #x #_ normalize <EQm' lapply EQm' cases i cases m cases m' -m -m' -i
147 normalize #m' #m #i inversion(update A i v m) normalize [#_ #ABS destruct]
148 #m'' #EQm'' #EQ destruct(EQ) @eq_f @eq_f lapply EQm'' -EQm'' lapply i -i
149 lapply m' -m' elim m [#m' * [2,3: #z] normalize #EQ destruct]
150 #opt_a #l #r #Hl #Hr #m' * [2,3: #z] normalize
151 [3: cases opt_a normalize [2: #y] #EQ destruct %
152 |*: inversion(update A z v ?) [2,4: #m'']  #EQm'' normalize #EQ destruct
153     [<(Hr … EQm'') | <(Hl … EQm'')] %
154 ]
155| #err cases m -m cases i -i #i #m normalize inversion(update A i v m) [2:#m']
156  #EQerr normalize #EQ destruct lapply EQerr lapply i elim m
157  [ normalize #x #_ %] #opt_a #l #r #Hl #Hr * [2,3:#z] normalize
158 [3: cases opt_a [2:#w] normalize #EQ destruct %
159 |*: inversion(update A z v ?) [2,4: #m'] #EQm' normalize #EQ destruct
160     [lapply(Hr … EQm') | lapply(Hl … EQm')] cases(lookup_opt A z ?) [2,4: #a]
161     normalize #EQ destruct %
162 ]
163]
164qed.
165
166lemma map_update_commute : ∀tag : identifierTag.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
167update tag B (map tag A B m f) id (f v) =
168!m' ← update tag A m id v; return map tag A B m' f.
169#tag #A #B #f #m #id #v >update_def >update_def >lookup_map
170cases (lookup tag A m id) [%] #a >m_return_bind >m_return_bind normalize nodelta
171whd in ⊢ (???%); @eq_f @sym_eq @map_add
172qed.
173
174(*restriction for maps *)
175definition restrict : ∀tag.∀A,B.
176identifier_map tag A → identifier_map tag B → identifier_map tag A ≝
177λtag,A,B,m1,m2.an_id_map …
178           (merge A B A (λo,o'.match o' with [None ⇒ None ? | Some _ ⇒ o])
179                  (match m1 with [an_id_map p1 ⇒ p1])
180                  (match m2 with [an_id_map p2 ⇒ p2])).
181
182interpretation "identifier map restriction" 'intersects a b = (restrict ??? a b).
183
184unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag).
185 
186lemma lookup_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
187∀i.lookup ?? (a ∩ b) i = if i ∈ b then lookup … a i else None ?.
188#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases (lookup_opt B i b)
189[2: #b] normalize % qed.
190
191lemma update_fail_lookup : ∀tag,A,m,i,v,e.update tag A m i v = Error … e → 
192  e = [MSG MissingId; CTX … i] ∧ lookup … m i = None ?.
193#tag #A #m #i #v #errmsg >update_def cases(lookup tag A m i) [2: #a] normalize
194#EQ destruct % //
195qed.
196
197lemma lookup_miss_update : ∀tag,A,m,i,v.lookup tag A m i = None ? → 
198  update … m i v = Error … [MSG MissingId; CTX … i].
199#tag #A #m #i #v #EQ >update_def >EQ normalize %
200qed.
201
202lemma update_ok_old_lookup : ∀tag,A,m,i,v,m'.update tag A m i v = OK ? m' →
203  i ∈ m.
204#tag #A #m #i #v #m' >update_def inversion(lookup tag A m i) [2: #a] #EQ normalize
205#EQ destruct >EQ normalize @I
206qed.
207
208lemma lookup_update_ok : ∀tag,A,m,i,v,m',i'.update tag A m i v = OK ? m' →
209  lookup … m' i' = if eq_identifier ? i' i then Some ? v else lookup … m i'.
210#tag #A #m #i #v #m' #i' >update_def inversion(lookup tag A m i) [2: #a] #EQ
211normalize nodelta #EQ1 destruct @eq_identifier_elim
212[ #H normalize nodelta >H @lookup_add_hit
213| #H normalize nodelta @lookup_add_miss assumption
214]
215qed.
216
217include "utilities/extra_bool.ma".
218
219lemma mem_set_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
220∀i.i ∈ a ∩ b = (i ∈ a ∧ i ∈ b).
221#tag #A #B * #a * #b  * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
222[2: #a1] normalize [2: @if_elim #_ %] cases(lookup_opt A i a) [2: #a2] normalize %
223qed.
224
225lemma lookup_set_minus : ∀tag,A,B. ∀a : identifier_map tag A. ∀b : identifier_map tag B.
226∀i. lookup ?? (a ∖ b) i = if i ∈ b then None ? else lookup … a i.
227#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
228[2: #b] % qed.
229
230lemma lookup_hit_update : ∀tag,A,m,i,v.i ∈ m → 
231  ∃m'.update tag A m i v = OK ? m'.
232#tag #A #m #i #v #H % [2: >update_def lapply(in_map_domain … m i) >H * #v #EQ >EQ
233normalize %|]
234qed.
235
236lemma add_set_minus  : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
237∀i,v.¬(i ∈ b) → add tag A (a ∖ b) i v = (add tag A a i v) ∖ b.
238#tag #A #B * #a * #b * #i #v @notb_elim @if_elim normalize [#_ *]
239@if_elim [2: #_ *] @if_elim [#_ *] inversion(lookup_opt B i b) normalize [2: #x #_ *]
240#H * * * * @eq_f lapply H -H lapply v -v lapply b -b lapply a -a elim i
241[  *
242  [ * [2: #opt_b #l #r] #v normalize in ⊢ (% → ?); #EQ destruct [2: %]
243  normalize in ⊢ (??%%); cases (map_opt ??? l) // normalize cases(map_opt ??? r)
244  normalize //
245  | * [2: #a] #l #r * [2,4: #opt_b #l1 #r1] #v normalize in ⊢ (% → ?); #EQ destruct
246    normalize [3: % |1,2: cases(merge ???? l l1) // cases(merge ???? r r1) //]
247    cases(map_opt ??? l) normalize // cases(map_opt ??? r) //
248  ]
249|2,3: #x #IH * [2,4: #opt_a #l #r] * [2,4,6,8: #opt_b #l1 #r1] #v
250      normalize in ⊢ (% → ?); #H whd in match (pm_set ????) in ⊢ (???%);
251      whd in match (merge ??????) in ⊢ (???%);
252      [1,2,3,4: <IH try assumption whd in match (pm_set ????) in ⊢ (??%?);
253                whd in match (merge ??????) in ⊢ (??%?); cases opt_b normalize
254                [2,4,6,8: #b] [5,6: cases opt_a normalize //]
255                [1,2,3,4: cases (merge ???? l l1) normalize [2,4,6,8: #opt_a2 #l2 #r2]
256                          // cases (merge ???? r r1) normalize
257                          [2,4,6,8,10,12: #opt_a3 #l3 #r3] inversion(pm_set ????)
258                          normalize // cases x
259                          [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
260                          normalize #EQ destruct
261                |*: cases(map_opt ??? l1) normalize [2,4,6,8: #opt_a2 #l2 #r2] //
262                    cases(map_opt ??? r1) normalize [2,4,6,8,10,12: #opt_a3 #l3 #r3]
263                    inversion(pm_set ????) normalize // cases x
264                    [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
265                    normalize #EQ destruct
266                ]
267     |*: whd in match (pm_set ????) in ⊢ (??%?);
268         whd in match (merge ??????) in ⊢ (??%?); [1,2: cases opt_a [2,4: #a]]
269         normalize
270         [1,2: @eq_f2 [1,4:%] | cases(map_opt ??? l) [2: #opt_a1 #l1 #r1] normalize
271         | cases(map_opt ??? r) [2: #opt_a1 #l1 #r1] normalize]       
272         [1,3,4: lapply(map_add tag A A (λx.x) (an_id_map … r) (an_identifier ? x) v)
273         |2,5,6: lapply(map_add tag A A (λx.x) (an_id_map … l) (an_identifier ? x) v)
274         |*: lapply(map_add tag A A (λx.x) (an_id_map … (pm_leaf ?)) (an_identifier ? x) v)
275         ] normalize #EQ destruct >e0 try % [4,5: cases x [2,3,5,6: #y] normalize %]
276           cases(map_opt ????) [2,4,6: #opt_a1 #l1 #r1] normalize
277           inversion(pm_set ????) normalize // cases x [2,3,5,6,8,9,11,12: #y]
278           normalize #EQ1 destruct
279     ]
280]
281qed.     
282
283lemma update_set_minus : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
284∀i,v.¬(i ∈ b) → update ?? (a ∖ b) i v =
285  ! a' ← update ?? a i v ; return a' ∖ b.
286#tag #A #B #a #b #id #v #H >update_def >lookup_set_minus @if_elim
287[ #H1 @⊥ lapply H1 lapply H @notb_elim >H1 normalize *] #_ >update_def
288cases (lookup tag A a id) normalize [ %] #a @eq_f @add_set_minus assumption
289qed.
290
291
292lemma add_idempotent : ∀tag,A.∀m : identifier_map tag A. ∀i,a1,a2.
293add tag A (add tag A m i a1) i a2 = add tag A m i a2.
294#tag #A * #m * #i #a1 #a2 normalize @eq_f lapply a1 -a1 lapply a2 -a2 lapply m -m
295elim i
296[ * [ #a1 #a2 %] #opt_a #l #r #a1 #a2 %] #x #IH *
297[1,3: #a1 #a2 normalize @eq_f2 try % @IH] #opt_a #l1 #l2 #a1 #a2 normalize
298@eq_f2 try % @IH
299qed.
300
301
302lemma empty_set_minus : ∀tag,A,B.∀m : identifier_map tag B. empty_map tag A =
303empty_map tag A ∖ m.
304#tag #A #B * #m normalize @eq_f elim m [%] #opt_b #l #r #IHl #IHr normalize
305cases opt_b normalize [2: #b] <IHl <IHr %
306qed.
307
308lemma map_opt_none : ∀A,B.∀m : positive_map A.
309      map_opt A B (λx.None ?) m = pm_leaf B.
310#A #B #m elim m [%] #opt_a #l #r #EQ1 #EQ2 cases opt_a [2: #a] normalize
311>EQ1 >EQ2 %
312qed.
313
314lemma set_minus_add :∀tag,A,B.∀a:identifier_map tag A.∀b:identifier_map tag B.
315           ∀i,v.i∈b→ (add tag A a i v)∖b = a ∖ b.
316#tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) [ #_ *]
317#v1 #EQv1 #_ @eq_f lapply EQv1 -EQv1 lapply v1 -v1 lapply v -v lapply b -b
318lapply i -i elim a
319[ #i elim i [ * [2: #opt_v #l #r] #v1 #v2 normalize #EQb destruct(EQb) %]
320#i1 #IH * [2,4: #opt_v #l #r] #v1 #v2 normalize [3,4: #ABS destruct(ABS)]
321cases opt_v [2,4: #v'] normalize nodelta #EQb >(IH … EQb) >map_opt_none %
322| #opt_v #l #r #IHl #IHr #i * [#v1 #v2 normalize #EQ destruct] #opt_v1 #l1 #r1
323  #c1 #c2 normalize cases i [2,3: #x] normalize [3: #EQ destruct] normalize nodelta
324[ %] #EQc2 cases opt_v [2,4: #c3] normalize cases opt_v1 [2,4,6,8: #c4] normalize
325[1,3,4,5,7: >(IHr … EQc2) inversion(merge A B A ? l l1) //
326            [2: #opt_v4 #l4 #r4 #_ #_] #EQ <EQ >(IHl … EQc2) //
327|*: >(IHl … EQc2) //
328]
329qed.
330           
331
Note: See TracBrowser for help on using the repository browser.