Changeset 3217


Ignore:
Timestamp:
Apr 29, 2013, 11:46:01 PM (4 years ago)
Author:
piccolo
Message:

Correctness of ERTL to LTL in place

Location:
src
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ExtraIdentifiers.ma

    r2843 r3217  
    1515include "common/Identifiers.ma".
    1616
     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 
    1782(*Map for identifier_map *)
    1883definition map : ∀tag,A,B. identifier_map tag A → (A → B) → identifier_map tag B ≝
     
    262327|*: >(IHl … EQc2) //
    263328]
    264 qed.           
    265 
     329qed.
     330           
     331
Note: See TracChangeset for help on using the changeset viewer.