Changeset 2307


Ignore:
Timestamp:
Aug 30, 2012, 4:47:58 PM (7 years ago)
Author:
campbell
Message:

Half the proofs for sound cost labelling check.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2286 r2307  
    13851385qed.
    13861386
     1387lemma Prop_notb : ∀b:bool. notb b → Not (bool_to_Prop b).
     1388* /2/
     1389qed.
     1390
    13871391lemma eq_false_to_notb: ∀b. b = false → ¬ b.
    13881392 *; /2 by eq_true_false, I/
  • src/RTLabs/CostCheck.ma

    r2305 r2307  
    2929definition check_well_cost_fn : internal_function → bool ≝
    3030λf.
    31   idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement f s (f_closed f l s PR)) ∧
     31  idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement (f_graph f) s (f_closed f l s PR)) ∧
    3232  is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
    3333cases (f_entry f) //
     
    9696      match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with
    9797      [ Some to_check' ⇒ λH'.
    98         if h ∈ checking_tail then None ? else
    9998        let PR' ≝ ? in
    10099        let st' ≝ lookup_present … g h PR' in
    101100        if is_cost_label st' then stop_now else
    102           check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
    103       | None ⇒ λ_. stop_now (* already checked successor *)
     101          if h ∈ checking_tail then None ? else
     102            check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
     103      | None ⇒ λ_.
     104          if h == checking ∨ h ∈ checking_tail then None ? else
     105            stop_now (* already checked successor *)
    104106      ] (try_remove_some_card … to_check h)
    105107    | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *)
     
    122124    successors (lookup_present … g l PR) = [l'] →
    123125    ¬ l' ∈ toch →
     126    l' ≠ l →
     127    ¬ l' ∈ tl →
    124128    check_label_bounded_spec g l tl toch toch
    125129| clbs_cost : ∀l,PR,l',PR',tl,toch.
     
    148152qed.
    149153
     154lemma not_orb : ∀b,c:bool.
     155  ¬ (b∨c) →
     156  (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)).
     157* * normalize /2/
     158qed.
     159
    150160lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
    151161  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
     
    162172           lapply (refl ? (try_remove … to_check h))
    163173           cases (try_remove ????) in ⊢ (???% → %);
    164            [ #RM whd in ⊢ (? → ??%? → ?); #H #E destruct @(clbs_checked … SUCC)
    165              whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
     174           [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim
     175             [ #H' #E destruct
     176             | #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC)
     177               [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
     178               | % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) *
     179               | assumption
     180               ]
     181             ]
    166182           | * * #to_check'' #RM #H whd in ⊢ (??%? → ?);
    167183             @if_elim
    168              [ #IN whd in ⊢ (??%? → ?); #E destruct
    169              | #OUT whd in ⊢ (??%? → ?);
     184             [ #CS #E destruct @(clbs_cost … SUCC … CS)
     185               cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L //
     186             | #CS
    170187               @if_elim
    171                [ #CS #E destruct @(clbs_cost … SUCC … CS)
    172                  cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L //
    173                | #CS #H @(clbs_step … SUCC OUT CS RM) @(IH … H)
     188               [ #IN whd in ⊢ (??%? → ?); #E destruct
     189               | #OUT whd in ⊢ (??%? → ?); #H
     190                 @(clbs_step … SUCC OUT CS RM) @(IH … H)
    174191               ]
    175192             ]
     
    181198] qed.
    182199
    183 
     200lemma check_label_bounded_c : ∀g,CL,checking,checking_tail,to_check,to_check'.
     201  check_label_bounded_spec g checking checking_tail to_check to_check' →
     202  ∀term_check,TERM,PR.
     203  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check'.
     204#g #CL #X1 #X2 #X3 #X4 #X elim X
     205[ #l #PR #tl #toch #SUCC
     206  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
     207  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
     208  whd in ⊢ (??%?); %
     209| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl
     210  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
     211  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
     212  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
     213  cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ // | * * ] ]
     214  #L >(proj2 … (try_remove_empty …) L) #H2
     215  whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl)
     216  %
     217| #l #PR #l' #PR' #tl #toch #SUCC #IN #CS
     218  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
     219  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
     220  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
     221  cut (lookup … toch l' = Some ? it) [ whd in IN:(?%); cases (lookup ????) in IN ⊢ %; [ * | * // ] ]
     222  #L cases (try_remove_this ????? L) #to_check' #RM >RM #H2
     223  whd in ⊢ (??%?); >CS whd in ⊢ (??%?); %
     224| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH
     225  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
     226  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
     227  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2
     228  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS))
     229  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN))
     230  whd in ⊢ (??%?); >(IH term_check' ??) %
     231| #l #PR #x #y #zs #tl #toch #SUCC
     232  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
     233  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
     234  whd in ⊢ (??%?); %
     235] qed.
    184236
    185237lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'.
     
    192244[ #E destruct whd in ⊢ (?%); >L1 //
    193245| #L4 whd in ⊢ (?%); >L4 @IH @IN
     246] qed.
     247
     248lemma bound_on_instrs_to_cost_prime : ∀g,l,n.
     249  bound_on_instrs_to_cost g l n →
     250  bound_on_instrs_to_cost' g l n.
     251#g #l #n #H inversion H
     252#l' #n' #PR #H' #E1 #E2 #_ destruct
     253lapply (refl ? (is_cost_label (lookup_present … g l' PR)))
     254cases (is_cost_label ?) in ⊢ (???% → ?); #CS
     255[ @boitc_here [ @PR | @eq_true_to_b @CS ]
     256| @boitc_later [ @PR | @eq_false_to_notb @CS | @H ]
     257] qed.
     258
     259lemma present_member : ∀tag,A,m,id.
     260  present tag A m id → member tag A m id.
     261#tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??))
     262qed.
     263
     264(* TODO: move and eliminate dup in Traces.ma *)
     265lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
     266  Exists S (λy. y = x) l →
     267  x ∈ l.
     268#S #x #l elim l
     269[ //
     270| #h #t #IH
     271  normalize lapply (eqb_true … x h)
     272  cases (x==h) *
     273  [ #E #_ >(E (refl ??)) //
     274  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
     275            | #H @IH @H
     276            ]
     277  ]
     278] qed.
     279
     280lemma successors_inv : ∀st,x,y,zs.
     281  successors st = x::y::zs →
     282  ∃r,l1,l2. st = St_cond r l1 l2.
     283* normalize
     284#a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l destruct
     285/4/
     286qed.
     287
     288include alias "utilities/deqsets.ma".
     289
     290lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g.
     291  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
     292  ∀l,PR,x,y,zs. successors (lookup_present … g l PR) = x::y::zs →
     293  ∀l'. ∀IN : l' ∈ successors (lookup_present … g l PR).
     294  is_cost_label (lookup_present … g l' ?).
     295[2: @(successors_present … IN) @(CL l) @lookup_lookup_present ]
     296#g #CL #WCL #l #PR #x #y #zs #SUCCS
     297cases (successors_inv … SUCCS)
     298#r * #l1 * #l2 #E
     299#l' #IN generalize in ⊢ (?(?(?????%))); #OR' >E in IN;
     300lapply (WCL l PR) generalize in ⊢ (?(???%) → ?); >E in ⊢ (% → % → ?); #LP #WCst
     301cases (andb_Prop_true ?? WCst)
     302#H1 #H2
     303whd in ⊢ (?% → ?); @eqb_elim
     304[ 2: #_ #IN lapply (memb_single … IN) ]
     305#E destruct //
     306qed.
     307
     308
     309lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'.
     310  ∀CL:graph_closed g.
     311  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
     312  check_label_bounded_spec g checking checking_tail to_check to_check' →
     313  (∀l. l∈g → ¬l ∈ to_check → l≠checking → ¬l∈checking_tail → ∃n. bound_on_instrs_to_cost g l n) →
     314  ∀l. l = checking ∨ bool_to_Prop (l∈to_check) →
     315  bool_to_Prop (l∈to_check') ∨ ∃n. bound_on_instrs_to_cost g l n.
     316#g #X1 #X2 #X3 #X4 #CL #WCL #X elim X
     317[ #l #PR #tl #toch #SUCC #INV #l' *
     318  [ #E destruct %2 %{1} % [ @PR | >SUCC #l' * ]
     319  | #IN %1 @IN
     320  ]
     321| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl #INV #l'' *
     322  [ #E destruct %2
     323    cases (INV l' ????)
     324    [ #n #B
     325      %{(S n)} % [ @PR | >SUCC #l'' * [2: *] #E destruct /2/ ]
     326    | @present_member @(successors_present … (CL l ? (lookup_lookup_present … PR)))
     327      >SUCC @eq_true_to_b @memb_hd
     328    | assumption
     329    | assumption
     330    | assumption
     331    ]
     332  | #IN %1 assumption
     333  ]
     334| #l #PR #l' #PR' #tl #toch #SUCC #IN #CS #INV #l'' *
     335  [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ]
     336  | /2/
     337  ]
     338| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN_tl #NCS #RM #H #IH #INV #l'' *
     339  [ #E destruct %2 cases (IH ? l' ?)
     340    [ #IN @⊥ lapply (check_label_bounded_subset … H l' IN) #IN'
     341      cases (try_remove_some ?????? RM) * #_ #L #_ whd in IN':(?%);
     342      cases (lookup ????) in IN' L; [ * | * #_ #E destruct ]
     343    | * #n #B %{(S n)} % [ // | #l'' >SUCC * [2: *] #E destruct /2/ ]
     344    | #l'' #INg #INch' #NEQ #NIN_ltl @(INV l'' INg ???)
     345      [ @notb_Prop % #INch @(absurd ?? (Prop_notb … INch'))
     346        cases (try_remove_some ?????? RM) * #_ #_ #L
     347        cases (L l'') [ #E destruct cases NEQ #X cases (X (refl ??)) ]
     348        #L' whd in ⊢ (?%); <L' @INch
     349      | % #E destruct cases (Prop_notb … NIN_ltl) #X @X @eq_true_to_b @memb_hd
     350      | @notb_Prop @(not_to_not … (Prop_notb … NIN_ltl)) #IN @eq_true_to_b @memb_cons @IN
     351      ]
     352    | %1 %
     353    ]
     354  | #IN @(IH ? l'' ?)
     355    [ #l''' #INg #NINch' #NEQ #NINtl @INV
     356      [ assumption
     357      | @notb_Prop @(not_to_not … (Prop_notb … NINch'))
     358        cases (try_remove_some ?????? RM) * #L1 #L2 #L3
     359        cases (L3 l''')
     360        [ #E destruct @⊥ cases NEQ /2/
     361        | #L whd in ⊢ (?% → ?%); >L //
     362        ]
     363      | % #E destruct cases (Prop_notb … NINtl) #X @X @eq_true_to_b @memb_hd
     364      | @notb_Prop @(not_to_not … (Prop_notb … NINtl)) #IN @eq_true_to_b @memb_cons @IN
     365      ]
     366    | cases (try_remove_some ?????? RM) * #L1 #L2 #L3
     367      cases (L3 l'') [ #E destruct %1 % | #L %2 whd in ⊢ (?%); <L @IN ]
     368    ]
     369  ]
     370| #l #PR #x #y #zs #tl #toch #SUCCS #INV #l' *
     371  [ #E destruct %2 %{1} % [ // ]
     372    #l' #EX @boitc_here
     373    [ @(successors_present … (CL l ? (lookup_lookup_present … PR)))
     374      @Exists_memb @EX
     375    | @(after_branch_are_cost_labels … WCL … SUCCS)
     376    ]
     377  | /2/
     378  ]
    194379] qed.
    195380
     
    229414] qed.
    230415
     416lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,SMALLER,TERM.
     417  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
     418  check_graph_bounded g CL to_check SUB start PR SMALLER term_check TERM = true →
     419  (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) →
     420  ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n.
     421#g #CL #term_check elim term_check
     422[ #to_check #SUB #start #PR #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
     423| #term_check' #IH #to_check #SUB #start #PR #SMALLER #TERM #WCL
     424  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
     425  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
     426  [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ]
     427  generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
     428  lapply (choose_empty … to_check')
     429  cases (choose LabelTag unit to_check')
     430  [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN
     431    cases (true_or_false_Prop (l∈to_check ∨ l == start))
     432    [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
     433      [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; *
     434      | //
     435      | //
     436      | @WCL
     437      | #l' #IN_g #NIN_to_check #NEQ #_ @H //
     438      | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
     439      ]
     440    | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
     441    ]
     442 | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
     443   #CHECK #H @(IH … CHECK)
     444   [ @WCL
     445   | #l #INg #NIN'' #NEQ
     446     cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN''))
     447                          cases (H4 … (refl ??)) * #L1 #L2 #L3
     448                          cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ]
     449     #NIN'
     450      cases (true_or_false_Prop (l∈to_check ∨ l == start))
     451      [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
     452        [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN'))
     453        | //
     454        | //
     455        | @WCL
     456        | #l' #IN_g #NIN_to_check #NEQ #_ @H //
     457        | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
     458        ]
     459      | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
     460      ]
     461   ]
     462 ]
     463] qed.
     464
    231465(* TODO: move *)
    232466definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
     
    275509] qed.
    276510
    277 axiom check_sound_cost_fn_ok : ∀fn. bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
     511axiom check_sound_cost_fn_ok : ∀fn.
     512  well_cost_labelled_fn fn →
     513  bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
     514(*
     515#fn #WCL %
     516[ whd in ⊢ (?% → %);
     517  generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?);
     518  cases (try_remove ????)
     519  [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
     520    lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
     521    >(E (refl ??)) * /3/
     522  | * * #to_check #H1 #H2 #H3
     523    whd in ⊢ (?% → ?); #CHECK
     524    #l #PR @(check_graph_bounded_ok … CHECK)
     525    [ #l' #PR' cases WCL //
     526    | #l' #IN #NIN #NEQ @⊥
     527      cases (H1 … (refl ??)) * #L1 #L2 #L3
     528      @(absurd ?? (Prop_notb … NIN))
     529      cases (L3 l')
     530      [ #E >E in NEQ; * #H cases (H (refl ??))
     531      | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …))
     532        @member_present @IN
     533      ]
     534    | /2/
     535    ]
     536  ]
     537| TODO
     538*)
    278539
    279540definition check_cost_program : RTLabs_program → bool ≝
     
    287548[ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp
    288549  * #id * #fd
    289   [ #H cases (andb_Prop_true … H) #W #S %
    290     [ @(proj1 … (check_well_cost_fn_ok … )) //
     550  [ #H cases (andb_Prop_true … H) #W #S
     551    lapply (proj1 … (check_well_cost_fn_ok …) W) #W'
     552    %
     553    [ //
    291554    | @(proj1 … (check_sound_cost_fn_ok …)) //
    292555    ]
  • src/RTLabs/CostSpec.ma

    r2303 r2307  
    1717   between labels to catch loops for soundness (is this sufficient?). *)
    1818
    19 definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → bool ≝
    20 λf,s. match s return λs. labels_present ? s → bool with
     19definition well_cost_labelled_statement : ∀g:graph statement. ∀s. labels_present g s → bool ≝
     20λg,s. match s return λs. labels_present g s → bool with
    2121[ St_cond _ l1 l2 ⇒ λH.
    22     is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
    23     is_cost_label (lookup_present … (f_graph f) l2 ?)
     22    is_cost_label (lookup_present … g l1 ?) ∧
     23    is_cost_label (lookup_present … g l2 ?)
    2424(*| St_jumptable _ ls ⇒ λH.
    2525    (* I did have a dependent version of All here, but it's a pain. *)
    26     All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls*)
     26    All … (λl. ∃H. is_cost_label (lookup_present … g l H) = true) ls*)
    2727| _ ⇒ λ_. true
    2828]. whd in H;
     
    3232
    3333definition well_cost_labelled_fn : internal_function → Prop ≝
    34 λf. (∀l. ∀H:present … (f_graph f) l.
    35          well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
     34λf. (∀l,PR. well_cost_labelled_statement (f_graph f) (lookup_present … (f_graph f) l PR) (f_closed f l …)) ∧
    3635    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
    3736[ @lookup_lookup_present | cases (f_entry f) // ] qed.
  • src/RTLabs/Traces.ma

    r2300 r2307  
    722722  @bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
    723723  lapply (Hbody (next fr) (next_ok fr))
    724   generalize in ⊢ (???% → ?);
    725   >Estmt #LP'
    726   whd in ⊢ (% → ?);
    727   * #H1 #H2 [ @H1 | @H2 ]
     724  generalize in ⊢ (?(???%) → ?);
     725  >Estmt #LP' #WS
     726  cases (andb_Prop_true … WS) #H1 #H2 [ @H1 | @H2 ]
    728727(*| * #r * #ls #Estmt
    729728  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
     
    29552954] qed.
    29562955
    2957 lemma Prop_notb : ∀b:bool. notb b → Not (bool_to_Prop b).
    2958 * /2/
    2959 qed.
    2960 
    29612956(* And then we get our counterpart to no_loops_in_tal for calls: *)
    29622957
  • src/common/Identifiers.ma

    r2305 r2307  
    979979* #_ #H @H
    980980qed.
     981
     982lemma try_remove_this : ∀tag,A,m,id,a.
     983  lookup tag A m id = Some A a →
     984  ∃m'. try_remove tag A m id = Some ? 〈a,m'〉.
     985#tag #A * #m * #id #a #L
     986cases (pm_try_remove_some' A id m a L)
     987#m' #R %{(an_id_map tag A m')} whd in ⊢ (??%?); >R %
     988qed.
    981989 
    982990
  • src/common/PositiveMap.ma

    r2305 r2307  
    548548] qed.
    549549
    550 
    551 
     550lemma pm_try_remove_some' : ∀A,p,t,a.
     551  lookup_opt A p t = Some A a →
     552  ∃t'. pm_try_remove A p t = Some ? 〈a,t'〉.
     553#A #p elim p
     554[ * [ #a #L normalize in L; destruct
     555    | #q #l #r #a #L normalize in L; destruct % [2: % | skip ]
     556    ]
     557| #q #IH *
     558  [ #a #L normalize in L; destruct
     559  | #x #l #r #a #L cases (IH r a L) #r' #R
     560    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
     561  ]
     562| #q #IH *
     563  [ #a #L normalize in L; destruct
     564  | #x #l #r #a #L cases (IH l a L) #l' #R
     565    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
     566  ]
     567] qed.
     568
     569
Note: See TracChangeset for help on using the changeset viewer.