Ignore:
Timestamp:
Jan 31, 2013, 5:15:49 PM (7 years ago)
Author:
tranquil
Message:
  • map_opt and map on positive maps are now clean (erase empty subtrees)
  • minor changes to blocks
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2541 r2599  
    341341#tag #A * #m * #id * #id' #NE
    342342@lookup_opt_pm_set_miss
    343 /2/
     343/2 by not_to_not/
    344344qed.
    345345
     
    511511  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
    512512  [1:
    513     * #k_eq_hyp @⊥ /2/
     513    * #k_eq_hyp @⊥ /2 by absurd/
    514514  |2:
    515     #Some_eq_hyp' /2/
     515    #Some_eq_hyp' /2 by /
    516516  ]
    517517qed.
     
    537537#tag #A #map #k #v #k' normalize
    538538cases (identifier_eq ? k k')
    539 [ #E /2/
    540 | #NE >lookup_add_miss /3/
     539[ #E /2 by or_introl/
     540| #NE >lookup_add_miss /3 by or_intror, conj, absurd, nmk/
    541541] qed.
    542542
     
    675675[ % | #x %{x} % ]
    676676qed.
    677 
     677(*
    678678lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
    679679#tag * normalize #m >map_opt_id_eq_ext // * %
     
    694694>map_opt_id >map_opt_id //
    695695qed.
    696 
     696*)
    697697lemma mem_set_union : ∀tag.∀i : identifier tag.∀s,s' : identifier_set tag.
    698698  i ∈ (s ∪ s') = (i ∈ s ∨ i ∈ s').
     
    10151015[ whd in C:(??%?); cases (pm_choose A m) in C ⊢ %; normalize [ #E destruct | * * #x #y #z #E destruct % ] ]
    10161016* * * #L1 #L2 #L3 #_
    1017 % [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2/ | #L4 %2 @L4 ] ]
     1017% [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2 by or_introl/ | #L4 %2 @L4 ] ]
    10181018qed.
    10191019
     
    10631063[ whd in C:(??%?); cases (pm_try_remove A id m) in C ⊢ %; normalize [ #E destruct | * #x #y #E destruct % ] ]
    10641064* * * #L1 #L2 #L3 #_
    1065 % [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2/ | #L4 %2 @L4 ] ]
     1065% [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2 by or_introl/ | #L4 %2 @L4 ] ]
    10661066qed.
    10671067
     
    11401140  Exists ? (λid'. id = id') l.
    11411141#tag #l #id whd in match (set_of_list ??);
    1142 cut (¬present ?? ∅ id) [ /3/ ]
     1142cut (¬present ?? ∅ id) [ /3 by refl, absurd, nmk/ ]
    11431143generalize in match ∅;
    11441144elim l
     
    11461146| #id' #tl #IH #s #F #PR whd in PR:(???%?);
    11471147  cases (identifier_eq … id id')
    1148   [ #E destruct /2/
     1148  [ #E destruct /2 by or_introl/
    11491149  | #NE %2 @(IH … PR)
    1150     @(not_to_not … F) /2/
     1150    @(not_to_not … F) /2 by present_add_present/
    11511151  ]
    11521152] qed.
     
    11731173[ @P0
    11741174| #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps))
    1175   [ normalize >FR /3/
     1175  [ normalize >FR /3 by absurd, nmk/
    11761176  | @L
    11771177  | @pre
     
    11841184  foldi A B tag f m b = b' →
    11851185  P b' (domain_of_map … m).
    1186 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11  destruct @foldi_ind /2/
    1187 qed.
    1188 
     1186#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11  destruct @foldi_ind /2 by /
     1187qed.
     1188
Note: See TracChangeset for help on using the changeset viewer.