Changeset 2308 for src/RTLabs


Ignore:
Timestamp:
Aug 30, 2012, 7:20:43 PM (7 years ago)
Author:
campbell
Message:

More proof (and corrections) on cost checking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2307 r2308  
    9494    match t with
    9595    [ nil ⇒ λSC. (* single successor *)
     96      let PR' ≝ ? in
     97      let st' ≝ lookup_present … g h PR' in
     98      if is_cost_label st' then stop_now else
    9699      match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with
    97100      [ Some to_check' ⇒ λH'.
    98         let PR' ≝ ? in
    99         let st' ≝ lookup_present … g h PR' in
    100         if is_cost_label st' then stop_now else
    101           if h ∈ checking_tail then None ? else
    102             check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
     101          check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
    103102      | None ⇒ λ_.
    104103          if h == checking ∨ h ∈ checking_tail then None ? else
     
    121120    successors (lookup_present … g l PR) = [ ] →
    122121    check_label_bounded_spec g l tl toch toch
    123 | clbs_checked : ∀l,PR,l',tl,toch.
     122| clbs_checked : ∀l,PR,l',tl,toch. (* this case overlaps with clbs_cost *)
    124123    successors (lookup_present … g l PR) = [l'] →
    125124    ¬ l' ∈ toch →
     
    129128| clbs_cost : ∀l,PR,l',PR',tl,toch.
    130129    successors (lookup_present … g l PR) = [l'] →
    131     l' ∈ toch →
    132130    is_cost_label (lookup_present … g l' PR') →
    133131    check_label_bounded_spec g l tl toch toch
     
    159157
    160158lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
     159  (∀l. l∈to_check → ¬ l∈checking::checking_tail) →
    161160  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
    162161  check_label_bounded_spec g checking checking_tail to_check to_check'.
    163162#n elim n
    164163[ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *)
    165 | #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check'
     164| #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check' #REMOVING
    166165  whd in ⊢ (??%? → ?);
    167166  generalize in ⊢ (??(?%)? → ?);
     
    169168  cases (successors (lookup_present … PR)) in ⊢ (???% → %);
    170169  [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 //
    171   | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' generalize in ⊢ (??(?%)? → ?);
    172            lapply (refl ? (try_remove … to_check h))
    173            cases (try_remove ????) in ⊢ (???% → %);
    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
     170  | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' @if_elim
     171           [ #CS #E destruct @(clbs_cost … SUCC) //
     172           | #NCS generalize in ⊢ (??(?%)? → ?);
     173             lapply (refl ? (try_remove … to_check h))
     174             cases (try_remove ????) in ⊢ (???% → %);
     175             [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim
     176               [ #H' #E destruct
     177               | #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC)
     178                 [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
     179                 | % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) *
     180                 | assumption
     181                 ]
    180182               ]
    181              ]
    182            | * * #to_check'' #RM #H whd in ⊢ (??%? → ?);
    183              @if_elim
    184              [ #CS #E destruct @(clbs_cost … SUCC … CS)
    185                cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L //
    186              | #CS
    187                @if_elim
    188                [ #IN whd in ⊢ (??%? → ?); #E destruct
    189                | #OUT whd in ⊢ (??%? → ?); #H
    190                  @(clbs_step … SUCC OUT CS RM) @(IH … H)
     183             | * * #to_check'' #RM #H whd in ⊢ (??%? → ?);
     184               whd in ⊢ (??%? → ?); #H
     185               cases (try_remove_some ?????? RM) * #L1 #L2 #L3
     186               @(clbs_step … SUCC ? NCS RM)
     187               [ @notb_Prop @(not_to_not … (Prop_notb … (REMOVING h ?))) /2/
     188                 whd in ⊢ (?%); >L1 //
     189               | @(IH … H)
     190                 #l #IN'' @notb_Prop % whd in ⊢ (?% → ?); @if_elim
     191                 [ #E #_ whd in IN'':(?%); >(proj1 ?? (eqb_true …) E) in IN'';
     192                   >L2 *
     193                 | #NE lapply (REMOVING l ?)
     194                   [ whd in ⊢ (?%); cases (L3 l) [ #E destruct cases (Prop_notb … NE) #X @⊥ @X @eq_true_to_b @(proj2 ?? (eqb_true …)) %
     195                     | #L >L @IN''
     196                     ]
     197                   | cases (l∈checking::checking_tail) * *
     198                   ]
     199                 ]
    191200               ]
    192201             ]
     
    210219  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
    211220  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
    212   whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
     221  whd in ⊢ (??%?); @if_elim [ // ] #NCS generalize in ⊢ (??(?%)?);
    213222  cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ // | * * ] ]
    214223  #L >(proj2 … (try_remove_empty …) L) #H2
    215224  whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl)
    216225  %
    217 | #l #PR #l' #PR' #tl #toch #SUCC #IN #CS
     226| #l #PR #l' #PR' #tl #toch #SUCC #CS
    218227  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
    219228  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 ⊢ (??%?); %
     229  whd in ⊢ (??%?);  >CS whd in ⊢ (??%?); %
    224230| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH
    225231  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
    226232  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
     233  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS))
    227234  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2
    228   whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS))
    229235  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN))
    230236  whd in ⊢ (??%?); >(IH term_check' ??) %
     
    332338  | #IN %1 assumption
    333339  ]
    334 | #l #PR #l' #PR' #tl #toch #SUCC #IN #CS #INV #l'' *
     340| #l #PR #l' #PR' #tl #toch #SUCC #CS #INV #l'' *
    335341  [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ]
    336342  | /2/
     
    379385] qed.
    380386
     387(* TODO: share with Traces.ma. *)
     388inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝
     389| gl_end : bad_label_list g head head
     390| gl_step : ∀l1,l2,H.
     391    l2 ∈ successors (lookup_present … g l1 H) →
     392    ¬ is_cost_label (lookup_present … g l1 H) →
     393    bad_label_list g head l2 →
     394    bad_label_list g head l1.
     395(*
     396inductive checked_label_costs (g:graph statement) : list label → label → Prop ≝
     397| clc_start : ∀l. checked_label_costs g [ ] l
     398| clc_two : ∀l,H,l'. ¬ is_cost_label (lookup_present … g l H) → checked_label_costs g [l'] l
     399| clc_many : ∀h,t,l,H. ¬ is_cost_label (lookup_present … g h H) → checked_label_costs g t l → checked_label_costs g (h::t) l.
     400*)
     401lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM.
     402  (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) →
     403  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? →
     404  ∃head,PR'. bool_to_Prop (¬ is_cost_label (lookup_present … g head PR')) ∧
     405  (bad_label_list g head head ∨
     406   (bool_to_Prop (head ∈ checking::checking_tail) ∧ bad_label_list g head checking)).
     407#g #CL #term_check elim term_check
     408[ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct
     409| #term_check' #IH
     410  #checking #PR #checking_tail #to_check #TERM #PRECS
     411  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); lapply (refl ? (successors (lookup_present … PR)))
     412  cases (successors ?) in ⊢ (???% → %);
     413  [ #H #H' whd in ⊢ (??%? → ?); #E destruct ]
     414  #h * [2: #y #zs #H #H' whd in ⊢ (??%? → ?); #E destruct ]
     415  #SUCC #PR' whd in ⊢ (??%? → ?); @if_elim
     416  [ #CS #E destruct ] #NCS generalize in ⊢ (??(?%)? → ?);
     417  cases (try_remove ????)
     418  [ #H whd in ⊢ (??%? → ?); @if_elim
     419      (* base case - we've found the head of the list *)
     420    [ #IN #_ %{h} % [ @PR' @eq_true_to_b @memb_hd ] % [ @NCS ] %2 %
     421      [ cases (orb_Prop_true … IN) /2/
     422      | @(gl_step … (gl_end …))
     423        [ @PR
     424        | >SUCC @eq_true_to_b @memb_hd
     425        | cases (orb_Prop_true … IN)
     426          [ #E <(proj1 ?? (eqb_true …) E) in PR ⊢ %; //
     427          | cases checking_tail in PRECS ⊢ %;
     428            [ #_ * | #h' #t #H #_ @H % #E destruct ]
     429          ]
     430        ]
     431      ]
     432    | #_ #E destruct
     433    ]
     434  | * * #to_check' #H1 whd in ⊢ (??%? → ?);
     435    #CHECK' cases (IH … CHECK')
     436    [ #head * #PRhead * #NCShead *
     437      [ #BLL %{head} %{PRhead} % /2/
     438      | * whd in ⊢ (?% → ?); @if_elim
     439        [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead ⊢ %; #PRh #BLL %{h} %{PRh} %{NCS} %1 @BLL
     440        | #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % //
     441          @(gl_step … BLL)
     442          [ @PR
     443          | >SUCC @eq_true_to_b @memb_hd
     444          | cases checking_tail in PRECS INtl;
     445            [ #_ #INc <(memb_single … INc) in PR ⊢ %; //
     446            | #h #t #H #_ @H % #E destruct
     447            ]
     448          ]
     449        ]
     450      ]
     451    | #_ //
     452    ]
     453  ]
     454] qed.
     455     
     456
     457
     458
    381459let rec check_graph_bounded
    382460  (g : graph statement)
     
    386464  (start : label)
    387465  (PR : present ?? g start)
     466  (REMOVED : notb (member ?? to_check start))
    388467  (SMALLER : gt (id_map_size … g) (id_map_size … to_check))
    389468  (term_check : nat)
     
    399478    [ None ⇒ λ_.λ_.λ_. true
    400479    | Some l_to_check'' ⇒ λL,SUB',C.
    401         check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ?? term_check' ?
     480        check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ??? term_check' ?
    402481    ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check')
    403482  ] (refl ??)
    404483].
    405 [ 2,3,4,5: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB'
    406   lapply (check_label_bounded_subset … (check_label_bounded_s … H')) #SUB''
     484[ 2,3,4,5,6: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB'
     485  lapply (check_label_bounded_subset … (check_label_bounded_s … H'))
     486  [ 1,3,5,7,9: #l' #IN @notb_Prop % #IS >(memb_single … IS) in IN; #IN'
     487    @(absurd … IN' (Prop_notb … REMOVED)) ]
     488   #SUB''
    407489]
    408490[ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN
    409491| @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L //
     492| cases (L … (refl ??)) * #L1 #L2 #L3 whd in ⊢ (?(?%)); >L2 //
    410493| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
    411494| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
     
    414497] qed.
    415498
    416 lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,SMALLER,TERM.
     499lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
    417500  (∀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 →
     501  check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = true →
    419502  (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) →
    420503  ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n.
    421504#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
     505[ #to_check #SUB #start #PR #REMOVED #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
     506| #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM #WCL
    424507  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
    425508  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
     
    435518      | //
    436519      | @WCL
     520      | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
     521        >(memb_single … IN') in IN; //
    437522      | #l' #IN_g #NIN_to_check #NEQ #_ @H //
    438523      | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
     
    454539        | //
    455540        | @WCL
     541        | #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN'
     542          >(memb_single … IN') in IN; //
    456543        | #l' #IN_g #NIN_to_check #NEQ #_ @H //
    457544        | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
     
    491578  [ None ⇒ λEMP. ⊥
    492579  | Some to_check ⇒ λ_.λCARD,L.
    493               check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ?? (|f_graph fn|) ?
     580              check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ??? (|f_graph fn|) ?
    494581  ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn)))
    495582    (try_remove_some_card ????)
     
    506593  ]
    507594| cases (f_entry fn) //
    508 | 4,5: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) //
     595| cases to_check in L ⊢ %; * #to_check0 #L cases (L … (refl ??)) * #L1 #L2 #L3
     596  whd in ⊢ (?(?%)); >L2 //
     597| 5,6: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) //
    509598] qed.
    510599
Note: See TracChangeset for help on using the changeset viewer.