Changeset 2843 for src/common


Ignore:
Timestamp:
Mar 11, 2013, 1:02:02 PM (7 years ago)
Author:
piccolo
Message:

1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ExtraIdentifiers.ma

    r2801 r2843  
    241241qed.
    242242
    243 
     243lemma map_opt_none : ∀A,B.∀m : positive_map A.
     244      map_opt A B (λx.None ?) m = pm_leaf B.
     245#A #B #m elim m [%] #opt_a #l #r #EQ1 #EQ2 cases opt_a [2: #a] normalize
     246>EQ1 >EQ2 %
     247qed.
     248
     249lemma set_minus_add :∀tag,A,B.∀a:identifier_map tag A.∀b:identifier_map tag B.
     250           ∀i,v.i∈b→ (add tag A a i v)∖b = a ∖ b.
     251#tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) [ #_ *]
     252#v1 #EQv1 #_ @eq_f lapply EQv1 -EQv1 lapply v1 -v1 lapply v -v lapply b -b
     253lapply i -i elim a
     254[ #i elim i [ * [2: #opt_v #l #r] #v1 #v2 normalize #EQb destruct(EQb) %]
     255#i1 #IH * [2,4: #opt_v #l #r] #v1 #v2 normalize [3,4: #ABS destruct(ABS)]
     256cases opt_v [2,4: #v'] normalize nodelta #EQb >(IH … EQb) >map_opt_none %
     257| #opt_v #l #r #IHl #IHr #i * [#v1 #v2 normalize #EQ destruct] #opt_v1 #l1 #r1
     258  #c1 #c2 normalize cases i [2,3: #x] normalize [3: #EQ destruct] normalize nodelta
     259[ %] #EQc2 cases opt_v [2,4: #c3] normalize cases opt_v1 [2,4,6,8: #c4] normalize
     260[1,3,4,5,7: >(IHr … EQc2) inversion(merge A B A ? l l1) //
     261            [2: #opt_v4 #l4 #r4 #_ #_] #EQ <EQ >(IHl … EQc2) //
     262|*: >(IHl … EQc2) //
     263]
     264qed.           
     265
Note: See TracChangeset for help on using the changeset viewer.