Changeset 1464


Ignore:
Timestamp:
Oct 25, 2011, 7:12:50 PM (8 years ago)
Author:
campbell
Message:

Use unification hints to simplify the graph monotonicity proofs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1410 r1464  
    284284] qed.
    285285
    286 lemma present_inc : ∀le,f,l.
    287   ∀f':Σf':partial_fn le. fn_graph_included le f f'.
     286lemma present_included : ∀le,f,f',l.
     287  fn_graph_included le f f' →
    288288  present ?? (pf_graph le f) l →
    289289  present ?? (pf_graph le f') l.
    290 #le #f #l * #f' * #H1 #H2 @H1 @H2 qed.
     290#le #f #f' #l * #H1 #H2 @H1 @H2 qed.
     291
     292(* Some definitions for the add_stmt function later, which we introduce now so
     293   that we can build the whole fn_graph_included machinery at once. *)
     294
     295(* We need to show that the graph only grows, and that Cminor labels will end
     296   up in the graph. *)
     297definition Cminor_labels_added ≝ λle,s,f'.
     298∀l. Exists ? (λl'.l=l') (labels_of s) →
     299∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
     300
     301record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
     302{ stmt_graph_inc : fn_graph_included ? f f'
     303; stmt_labels_added : Cminor_labels_added le s f'
     304}.
     305
     306(* Build some machinery to solve fn_graph_included goals. *)
     307
     308(* A datatype saying how we intend to prove a step. *)
     309inductive fn_inc_because (le:label_env) : partial_fn le → Type[0] ≝
     310| fn_inc_eq : ∀f. fn_inc_because le f
     311| fn_inc_sig : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
     312    ∀f3:(Σf3:partial_fn le.fn_graph_included le f2 f3). fn_inc_because le f3
     313| fn_inc_addinv : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
     314    ∀s.∀f3:(Σf3:partial_fn le.add_stmt_inv le s f2 f3). fn_inc_because le f3
     315.
     316
     317(* Extract the starting function for a step. *)
     318let rec fn_inc_because_left le f0  (b:fn_inc_because le f0) on b : partial_fn le ≝
     319  match b with [ fn_inc_eq f ⇒ f | fn_inc_sig f _ _ _ ⇒ f | fn_inc_addinv f _ _ _ _ ⇒ f ].
     320
     321(* Some unification hints to pick the right step to apply.  The dummy variable
     322   is there to provide goal that the lemma can't apply to, which causes an error
     323   and forces the "repeat" tactical to stop.  The first hint recognises that we
     324   have reached the desired starting point. *)
     325
     326unification hint 0 ≔ le:label_env, f:partial_fn le, dummy:True;
     327  f' ≟ f,
     328  b  ≟ fn_inc_eq le f
     329
     330  fn_graph_included le f f' ≡ fn_graph_included le (fn_inc_because_left le f' b) f'
     331.
     332
     333unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, f3:(Σf3:partial_fn le. fn_graph_included le f2 f3);
     334  b ≟ fn_inc_sig le f1 f2 H12 f3
     335
     336  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
     337.
     338
     339unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, s:stmt, f3:(Σf3:partial_fn le. add_stmt_inv le s f2 f3);
     340  b ≟ fn_inc_addinv le f1 f2 H12 s f3
     341
     342  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
     343.
     344
     345(* A lemma to perform a step of the proof.  We can repeat this to do the whole
     346   proof. *) 
     347lemma fn_includes_step : ∀le,f. ∀b:fn_inc_because le f. fn_graph_included le (fn_inc_because_left le f b) f.
     348#le #f *
     349[ #f @fn_graph_included_refl
     350| #f1 #f2 #H12 * #f2 #H23 @(fn_graph_inc_trans … H12 H23)
     351| #f1 #f2 #H12 #s * #f2 * #H23 #X @(fn_graph_inc_trans … H12 H23)
     352] qed.
     353
    291354
    292355axiom BadCminorProgram : String.
     
    332395    let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
    333396      «f, ?»
    334 ] Env.
     397] Env. 
    335398(* For new labels, we need to step back through the definitions of f until we
    336399   hit the point that it was added. *)
    337 try @fn_graph_included_refl
     400try (repeat @fn_includes_step @I)
    338401try (#l #H @H)
    339 [ 7: #l #H whd % [ @H |
    340     @present_inc
    341     @present_inc
    342     @present_inc
    343     @(use_sig ? (present ???)) ]
    344 | 8: #l #H
    345     @present_inc
    346     @(use_sig ? (present ???))
    347 (* For the monotonicity properties, we just keep going back until we're at the
    348    start.  The repeat tactical helps here. *)
    349 | *: repeat @fn_graph_included_sig @fn_graph_included_refl
     402[ #l #H whd % [ @H | @(present_included … (use_sig … lfalse)) repeat @fn_includes_step @I ]
     403| #l #H @(present_included … (use_sig ?? resume_at)) repeat @fn_includes_step @I
    350404] qed.
    351405
     
    364418    ]
    365419] Env pf.
    366 [ //
    367 | 2,3: normalize in pf; destruct
    368 | @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
     420try (repeat @fn_includes_step @I)
     421[ 1,2: normalize in pf; destruct
    369422| @Env
    370423| @(proj2 … Env)
    371 | normalize in pf; destruct @e0 ] qed.
     424| normalize in pf; destruct @e0
     425] qed.
    372426
    373427axiom UnknownLabel : String.
     
    417471qed.
    418472
    419 (* We need to show that the graph only grows, and that Cminor labels will end
    420    up in the graph. *)
    421 definition Cminor_labels_added ≝ λle,s,f'.
    422 ∀l. Exists ? (λl'.l=l') (labels_of s) →
    423 ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
    424 
    425 record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
    426 { stmt_graph_inc : fn_graph_included ? f f'
    427 ; stmt_labels_added : Cminor_labels_added le s f'
    428 }.
    429 
    430473lemma empty_Cminor_labels_added : ∀le,s,f'.
    431474  labels_of s = [ ] → Cminor_labels_added le s f'.
     
    439482qed.
    440483
    441 lemma fn_graph_included_inv : ∀label_env,s,f,f0.
    442   ∀f':Σf':partial_fn label_env. add_stmt_inv label_env s f0 f'.
    443   fn_graph_included label_env f f0 →
    444   fn_graph_included label_env f f'.
    445 #label_env #s #f #f0 * #f' * #H1 #H2 #H3
    446 @(fn_graph_inc_trans … H3 H1)
    447 qed.
    448 
    449 lemma present_inc' : ∀le,s,f,l.
    450   ∀f':(Σf':partial_fn le. add_stmt_inv le s f f').
    451   present ?? (pf_graph le f) l →
    452   present ?? (pf_graph le f') l.
    453 #le #s #f #l * #f' * * #H1 #H2 #H3
    454 @H1 @H3
     484lemma Cminor_labels_inc : ∀le,s,f,f'.
     485  fn_graph_included le f f' →
     486  Cminor_labels_added le s f →
     487  Cminor_labels_added le s f'.
     488#le #s #f #f' #INC #ADDED
     489#l #E cases (ADDED l E) #l' * #L #P
     490%{l'} % [ @L | @(present_included … P) @INC ]
    455491qed.
    456492
     
    461497#le #s #s' #f * #f' * #H1 #H2 #H3
    462498#l #E cases (H3 l E) #l' * #L #P
    463 %{l'} % [ @L | @present_inc' @P ]
     499%{l'} % [ @L | @(present_included … P) @H1 ]
    464500qed.
    465501
     
    470506#le #s #f * #f' #H1 #H2
    471507#l #E cases (H2 l E) #l' * #L #P
    472 %{l'} % [ @L | @present_inc @P ]
     508%{l'} % [ @L | @(present_included … P) @H1 ]
    473509qed.
    474510
     
    580616try @(π2 (π1 Env))
    581617try @mk_add_stmt_inv
     618try (repeat @fn_includes_step @I)
    582619try (@empty_Cminor_labels_added @refl)
    583620try (@(All_mp … (use_sig ?? exits)))
    584 try @fn_graph_included_refl
    585 try (repeat @fn_graph_included_inv repeat @fn_graph_included_sig @fn_graph_included_refl)
    586621try (#l #H @I)
    587622try (#l #H @H)
    588623[ -f @(choose_regs_length … (sym_eq … Eregs))
    589 | @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
    590624| whd in Env @(π1 (π1 (π1 Env)))
    591625| -f @(choose_regs_length … (sym_eq … Eregs))
    592 | @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
    593626| #l #H cases (Exists_append … H)
    594627  [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1)
    595   | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (use_sig ?? f2))
    596   ]
    597 | #l #H @present_inc' @H
    598 | #l #H @present_inc' @use_sig
    599 | @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
     628  | @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I | @(stmt_labels_added ???? (use_sig ?? f2)) ]
     629  ]
     630| #l #H @(present_included … H) repeat @fn_includes_step @I
     631| #l #H @(present_included … (use_sig ?? l_next)) repeat @fn_includes_step @I
    600632| #l #H cases (Exists_append … H)
    601   [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f1))
    602   | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f2))
    603   ]
    604 | #l #H % [ @H | @present_inc @present_inc' @present_inc @(use_sig ?? (pf_entry ? f2)) ]
    605 | #l #H @present_inc @present_inc' @H
    606 | #l #H @present_inc @H
     633  [ @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f1))) repeat @fn_includes_step @I
     634  | @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f2))) repeat @fn_includes_step @I
     635  ]
     636| #l #H % [ @H | @(present_included … (use_sig ?? l2)) repeat @fn_includes_step @I ]
     637| 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
    607638| @(use_sig ?? (pf_entry ??))
    608 | @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_refl
    609639| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
    610640| % [ @use_sig | @(use_sig ?? exits) ]
    611641| @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
    612642| #l #H @use_sig
    613 | #l #H @present_inc @use_sig
    614 | #l #H % [ @present_inc @present_inc @present_inc @present_inc @use_sig | @H ]
    615 | @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
     643| #l #H @(present_included … (use_sig ?? l_default)) repeat @fn_includes_step @I
     644| #l #H % [ @(present_included … (use_sig ?? l_case)) repeat @fn_includes_step @I | @H ]
    616645| @use_sig
    617 | @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
    618646| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
    619647        |@Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?))
    620648        ]
    621649| #l1 #H whd %2 @lookup_label_lpresent
    622 | @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
    623650| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
    624651] qed.
    625 
    626 (*
    627 definition mk_fn : ∀le. partial_fn le → internal_function ≝
    628 λle, f.
    629   mk_internal_function
    630     (pf_labgen ? f)
    631     (pf_reggen ? f)
    632     (pf_result ? f)
    633     (pf_params ? f)
    634     (pf_locals ? f)
    635     (pf_stacksize ? f)
    636     (pf_graph ? f)
    637     ?
    638     (pf_entry ? f)
    639     (pf_exit ? f).
    640 #l #s #E @(labels_P_mp … (pf_closed ? f l s E))
    641 #l' * [ // | #H
    642 *)
    643652
    644653definition c2ra_function (*: internal_function → internal_function*) ≝
Note: See TracChangeset for help on using the changeset viewer.