Changeset 1930


Ignore:
Timestamp:
May 9, 2012, 6:30:41 PM (7 years ago)
Author:
campbell
Message:

Tidy up labelling simulation stuff a bit.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1713 r1930  
    4646[ //
    4747| #H' @False_ind @(absurd … H H')
    48 ] qed.
    49 
    50 lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
    51 #P #f #p #Q #H cases f;
    52 [ @H
    53 | #np cut False [ @(absurd ? p np) | * ]
    54 ] qed.
    55 
    56 lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
    57 #P #f #p #Q #H cases f;
    58 [ #np cut False [ @(absurd ? np p) | * ]
    59 | @H
    6048] qed.
    6149
  • src/Clight/labelSimulation.ma

    r1922 r1930  
    1515}.
    1616
    17 lemma commute_fst_pair : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → B → C×D.
    18   \fst (let 〈x,y〉 ≝ e in F x y) =  let 〈x,y〉 ≝ e in \fst (F x y).
    19 #A #B #C #D * //
    20 qed.
    21 
     17(* Useful for breaking up the labeling functions, because we don't care about
     18   *which* cost labels are added here and so can throw away the resulting name
     19   generator. *)
    2220lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D.
    2321  \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) =  F (\fst e).
     
    2523qed.
    2624
    27 (* lemma to break up label_expr, label_exprs and label_statement in the labelling
    28    functions *)
     25(* Similarly, lemma to break up label_expr, label_exprs and label_statement in
     26   the labelling functions *)
    2927lemma label_gen_elim : ∀Syn:Type[0].∀syn,u.∀T:Type[0].∀L:Syn → universe CostTag → Syn × (universe CostTag). ∀F:Syn → universe CostTag → T. ∀P:T → Type[0].
    3028  (∀u'. P (F (\fst (L syn u)) u')) →
     
    4341
    4442
    45 
    4643lemma label_expr_type : ∀e,u.
    4744  typeof (\fst (label_expr e u)) = typeof e.
     
    4946qed.
    5047
     48(* Formalise the notion of a trace with extra cost labels added.  Note that
     49   we don't require the left trace to be cost free.  *)
    5150inductive trace_with_extra_labels : trace → trace → Prop ≝
    5251| twel_0 : trace_with_extra_labels E0 E0
     
    7170 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
    7271
    73 lemma label_expr_ok : ∀ge,ge',en,m.
     72theorem label_expr_ok : ∀ge,ge',en,m.
    7473  related_globals ge ge' →
    7574  (∀e,v,tr.
     
    8079          ∀u. ∃tr'. exec_lvalue' ge' en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
    8180                    trace_with_extra_labels tr tr').
     81(* Proof goes by breaking up the execution in the hypothesis, breaking up the
     82   labelling function to get a new term and executing it by rewriting what we
     83   learned from the hypothesis. *)
    8284#ge #ge' #en #m #RG @expr_lvalue_ind_combined
    8385[ 1,2: normalize /3 by ex_intro, conj/
     
    278280] qed.
    279281
    280 (* Plan:
    281      - extend labelling functions to continuations and hence states
    282        NO - this doesn't work because we don't know *which* cost labels to add
    283        realistically we'll have to define erasure functions
    284        BETTER - use predicate so that we don't need to insist on the absence of
    285        cost labels in the source
    286      - build a simulation relation linking states to their labelled counterparts
    287      - write a predicate stating that two traces are the same except for some
    288        extra costs
    289      - show some labelling relationship for global environments
    290      - prove that
    291          exec_step ge s1 = = Value … 〈tr,s2〉 →
    292          cost_related s1 s1' →
    293          ∃tr'. equal_up_to_costs tr tr' ∧
    294                plus ge' s1' tr' s2' ∧
    295                cost_related s2 s2'
    296        using some relationship between ge and ge'.
    297 *)
    298 
     282
     283(* Now we move on to describe the simulation relation.  First, relate the
     284   continuations. *)
    299285inductive cont_with_labels : cont → cont → Prop ≝
    300286| cwl_stop : cont_with_labels Kstop Kstop
     
    322308qed.
    323309
     310(* Now define almost all of the simulation relation... *)
    324311inductive state_with_labels_partial : state → state → Prop ≝
    325312| swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)
     
    338325.
    339326
    340 (* We handle the switch states after the rest so that we can reuse the partial
    341    result. *)
     327(* ... and add the states where the cases from switch statements are expanded.
     328   We do these separately because in the LSdefault case we have to execute a
     329   cost label alongside an arbitrary statement, and we want to reuse the result
     330   on arbitrary statements we get for state_with_labels_partial. *)
    342331inductive state_with_labels : state → state → Prop ≝
    343332| swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s'
     
    347336.
    348337
     338(* TODO: this (or something like it) ought to be elsewhere. *)
    349339inductive plus (ge:genv) : state → trace → state → Prop ≝
    350340| plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2
    351341| plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3.
    352342
    353 definition eplus ≝ λn. repeat n io_out io_in clight_fullexec.
    354 
    355 inductive hplus (ge:genv) : state → trace → trace → state → Prop ≝
    356 | hplus_one : ∀tr,s2,s1',tr1,tr2,s2'.
    357     exec_step ge s1' = OK … 〈tr2,s2'〉 →
    358     trace_with_extra_labels tr (tr1⧺tr2) →
    359     state_with_labels s2 s2' →
    360     hplus ge s1' tr1 tr s2
    361 | hplus_succ : ∀s1,tr,s2,tr1,tr2,s3.
    362     exec_step ge s1 = OK … 〈tr2,s2〉 →
    363     hplus ge s2 (tr1⧺tr2) tr s3 →
    364     hplus ge s1 tr1 tr s3.
    365 
     343(* Some details are invariant under labelling. *)
    366344lemma label_function_return : ∀f.
    367345  fn_return (label_function f) = fn_return f.
     
    374352qed.
    375353
    376 lemma bindIO_inversion: ∀O,I.
    377   ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
    378   (f »= g = return y) →
    379   ∃x. (f = return x) ∧ (g x = return y).
    380 #O #I #A #B #f #g #y cases f normalize
    381 [ #o #k #E destruct
    382 | #a #e %{a} /2 by conj/
    383 | #m #H destruct (H)
    384 ] qed.
    385 
    386 lemma io_eq_to_res : ∀O,I. ∀T:Type[0]. ∀e:res T. ∀v.
    387   err_to_io … e = Value O I T v →
    388   e = OK T v.
    389 #O #I #T *
    390 [ #e #v #E normalize in E; destruct @refl
    391 | #m #v #E normalize in E; destruct
    392 ]
    393 qed.
    394 
    395 coercion io_eq_from_res :
    396   ∀O,I,T,e,v. ∀E:err_to_io O I T e = Value O I T v. e = OK T v ≝ io_eq_to_res
    397   on _E:eq (IO ???) ?? to eq (res ?) ??.
    398 
    399 lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.
    400   exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =
    401   exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.
    402 #ge #e #m #a #ty #u
    403 whd in ⊢ (??(????(???%))?); >shift_fst @refl
    404 qed.
    405 
    406354lemma label_expr_fun_typeof : ∀a,u.
    407355  fun_typeof (\fst (label_expr a u)) = fun_typeof a.
     
    415363normalize cases (label_statement ??) #body' #u
    416364normalize cases (fresh ??) //
     365qed.
     366
     367lemma label_fn_params : ∀f.
     368  fn_params (label_function f) = fn_params f.
     369* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
     370qed.
     371
     372lemma label_fn_vars : ∀f.
     373  fn_vars (label_function f) = fn_vars f.
     374* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
     375qed.
     376
     377(* Some annoying rewrite rules *)
     378lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.
     379  exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =
     380  exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.
     381#ge #e #m #a #ty #u
     382whd in ⊢ (??(????(???%))?); >shift_fst @refl
    417383qed.
    418384
     
    427393| #fd' #H #E normalize in E; destruct >(H (refl ??)) //
    428394] qed.
    429 
    430 (*
    431 lemma step_with_labels : ∀ge,s1,s1',tr,s2.
    432   state_with_labels s1 s1' →
    433   exec_step ge s1 = OK … 〈tr,s2〉 →
    434   hplus ge s1' E0 tr s2.
    435 #ge #Xs1 #Xs1' #tr #s2 *
    436 [ #f #us #s #k #k' #e #m #KL cases s
    437   [ #EX inversion KL
    438     [ #E1 #E2 #_ destruct @hplus_one [3: whd in EX:(??%?) ⊢ (??%?);
    439       >label_function_return >EX in ⊢ (??%?); | 1,2:skip | // | %1
    440       cases f in EX ⊢ %; #rty #params #vars #body #EX whd in ⊢ (??(match ?% with [_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?])?); >EX
    441      whd in EX:(??%?) ⊢ (??(λ_.?(?(??%?)?)?));
    442 
    443 lemma step_with_labels : ∀ge,s1,s1',tr,s2.
    444   state_with_labels s1 s1' →
    445   exec_step ge s1 = OK … 〈tr,s2〉 →
    446   ∃n,tr',s2'. eplus n ge s1' = OK … 〈tr',s2'〉 ∧
    447             trace_with_extra_labels tr tr' ∧
    448             state_with_labels s2 s2'.
    449 #ge #Xs1 #Xs1' #tr #s2 *
    450 [ #f #us #s #k #k' #e #m #KL cases s
    451   [ #EX %{1} %{tr} inversion KL
    452     [ #E1 #E2 #_ destruct
    453      whd in EX:(??%?) ⊢ (??(λ_.?(?(??%?)?)?));
    454      whd in EX:(??%?) ⊢ (??(λ_.?(?(??(?????%?)?)?)?));
    455      normalize in EX:(??%?) ⊢ (??(λ_.?(?(??(%??????)?)?)?));
    456       % [2: % [ % [ @plus_one whd in EX:(??%?) ⊢ (??%?); >EX whd in ⊢ (??(??(??%???))?); @EX >EX @refl
    457 *)
    458395
    459396lemma labelled_not_skip : ∀s,u.
     
    477414[ #E @⊥ @(absurd ? E) @labelled_not_skip //
    478415| /2/
    479 ] qed.
    480 
    481 (* TODO: this is from CexecComplete, but should live somewhere else *)
    482 lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
    483 #P #f #p #Q #H cases f;
    484 [ @H
    485 | #np cut False [ @(absurd ? p np) | * ]
    486 ] qed.
    487 
    488 lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
    489 #P #f #p #Q #H cases f;
    490 [ #np cut False [ @(absurd ? np p) | * ]
    491 | @H
    492416] qed.
    493417
     
    527451] qed.
    528452
     453(* Break up labelling function in one go for statements. *)
    529454lemma blindly_label : ∀u,s. ∀P:statement → Prop.
    530455match s with
     
    557482] qed.
    558483
    559 lemma label_fn_params : ∀f.
    560   fn_params (label_function f) = fn_params f.
    561 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
    562 qed.
    563 
    564 lemma label_fn_vars : ∀f.
    565   fn_vars (label_function f) = fn_vars f.
    566 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
    567 qed.
    568 
    569 (* Apply induction hypothesis while getting Matita to infer the continuations
    570    k0 and k0', and the universe u0. *)
     484(* Apply induction hypothesis in label_find_label proof below while getting
     485   Matita to infer the continuations k0 and k0', and the universe u0, rather
     486   than having to give them explicitly. *)
    571487lemma lfl_IH : ∀s0,lbl.
    572488  ∀C:option (statement×cont) → option (statement×cont) → Prop.
     
    580496qed.
    581497
     498(* Finding a goto label in a cost-labelled program gives a labelled version of
     499   the statement and continuation found by the original function, if any. *)
    582500lemma label_find_label : ∀lbl,s,k,k',u.
    583501  cont_with_labels k k' →
     
    747665qed.
    748666
     667
    749668(* We show the main simulation in two stages.  First, we show it for all states
    750669   in the relation *except* those for labeled_statements, then we'll show the
     
    759678             trace_with_extra_labels tr tr' ∧
    760679             state_with_labels s2 s2'.
     680
     681(* General plan is like the expressions result, except that we do case analysis
     682   on the simulation first, then:  break up the original execution, break up the
     683   cost labelling, use the earlier results to deal with expressions, then
     684   run the labelled version for enough steps.  We try to avoid having to write
     685   out the final trace and state and "skip" them afterwards. *)
    761686#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
    762687[ #f #us #s #k #k' #e #m #KL cases s
     
    11251050] qed.
    11261051
    1127 lemma step_with_labels : ∀ge,ge'.
     1052
     1053theorem step_with_labels : ∀ge,ge'.
    11281054  related_globals ge ge' →
    11291055  ∀s1,s1',tr,s2.
  • src/common/IOMonad.ma

    r1920 r1930  
    237237| #m #f #v #P #H #E whd in E:(??%?); destruct
    238238] qed.
     239
     240lemma bindIO_inversion: ∀O,I.
     241  ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
     242  (f »= g = return y) →
     243  ∃x. (f = return x) ∧ (g x = return y).
     244#O #I #A #B #f #g #y cases f normalize
     245[ #o #k #E destruct
     246| #a #e %{a} /2 by conj/
     247| #m #H destruct (H)
     248] qed.
     249
     250(* When something in the error monad has found its way into the IO monad,
     251   ensure that we can implicitly go back. *)
     252lemma io_eq_to_res : ∀O,I. ∀T:Type[0]. ∀e:res T. ∀v.
     253  err_to_io … e = Value O I T v →
     254  e = OK T v.
     255#O #I #T *
     256[ #e #v #E normalize in E; destruct @refl
     257| #m #v #E normalize in E; destruct
     258]
     259qed.
     260
     261coercion io_eq_from_res :
     262  ∀O,I,T,e,v. ∀E:err_to_io O I T e = Value O I T v. e = OK T v ≝ io_eq_to_res
     263  on _E:eq (IO ???) ?? to eq (res ?) ??.
     264
  • src/utilities/extralib.ma

    r1882 r1930  
    114114qed.
    115115
     116(* Replace decision functions by result. *)
     117
     118lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
     119#P #f #p #Q #H cases f;
     120[ @H
     121| #np cut False [ @(absurd ? p np) | * ]
     122] qed.
     123
     124lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
     125#P #f #p #Q #H cases f;
     126[ #np cut False [ @(absurd ? np p) | * ]
     127| @H
     128] qed.
     129
     130
    116131lemma not_exists_forall:
    117132  ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x.
Note: See TracChangeset for help on using the changeset viewer.