Changeset 1464 for src/Cminor/toRTLabs.ma

Timestamp:

Oct 25, 2011, 7:12:50 PM (9 years ago)

Author:

campbell

Message:

Use unification hints to simplify the graph monotonicity proofs.

File:

• src/Cminor/toRTLabs.ma (modified) (8 diffs)

src/Cminor/toRTLabs.ma

@@ -284 +284 @@
 ] qed.
 
-lemma present_inc : ∀le,f,l.
-  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
+lemma present_included : ∀le,f,f',l.
+  fn_graph_included le f f' →
   present ?? (pf_graph le f) l →
   present ?? (pf_graph le f') l.
-#le #f #l * #f' * #H1 #H2 @H1 @H2 qed.
+#le #f #f' #l * #H1 #H2 @H1 @H2 qed.
+
+(* Some definitions for the add_stmt function later, which we introduce now so
+   that we can build the whole fn_graph_included machinery at once. *)
+
+(* We need to show that the graph only grows, and that Cminor labels will end
+   up in the graph. *)
+definition Cminor_labels_added ≝ λle,s,f'.
+∀l. Exists ? (λl'.l=l') (labels_of s) →
+∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
+
+record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
+{ stmt_graph_inc : fn_graph_included ? f f'
+; stmt_labels_added : Cminor_labels_added le s f'
+}.
+
+(* Build some machinery to solve fn_graph_included goals. *)
+
+(* A datatype saying how we intend to prove a step. *)
+inductive fn_inc_because (le:label_env) : partial_fn le → Type[0] ≝
+| fn_inc_eq : ∀f. fn_inc_because le f
+| fn_inc_sig : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
+    ∀f3:(Σf3:partial_fn le.fn_graph_included le f2 f3). fn_inc_because le f3
+| fn_inc_addinv : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
+    ∀s.∀f3:(Σf3:partial_fn le.add_stmt_inv le s f2 f3). fn_inc_because le f3
+.
+
+(* Extract the starting function for a step. *)
+let rec fn_inc_because_left le f0  (b:fn_inc_because le f0) on b : partial_fn le ≝
+  match b with [ fn_inc_eq f ⇒ f | fn_inc_sig f _ _ _ ⇒ f | fn_inc_addinv f _ _ _ _ ⇒ f ].
+
+(* Some unification hints to pick the right step to apply.  The dummy variable
+   is there to provide goal that the lemma can't apply to, which causes an error
+   and forces the "repeat" tactical to stop.  The first hint recognises that we
+   have reached the desired starting point. *)
+
+unification hint 0 ≔ le:label_env, f:partial_fn le, dummy:True;
+  f' ≟ f,
+  b  ≟ fn_inc_eq le f
+⊢
+  fn_graph_included le f f' ≡ fn_graph_included le (fn_inc_because_left le f' b) f'
+.
+
+unification 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);
+  b ≟ fn_inc_sig le f1 f2 H12 f3
+⊢
+  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
+.
+
+unification 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);
+  b ≟ fn_inc_addinv le f1 f2 H12 s f3
+⊢
+  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
+.
+
+(* A lemma to perform a step of the proof.  We can repeat this to do the whole
+   proof. *)  
+lemma fn_includes_step : ∀le,f. ∀b:fn_inc_because le f. fn_graph_included le (fn_inc_because_left le f b) f.
+#le #f *
+[ #f @fn_graph_included_refl
+| #f1 #f2 #H12 * #f2 #H23 @(fn_graph_inc_trans … H12 H23)
+| #f1 #f2 #H12 #s * #f2 * #H23 #X @(fn_graph_inc_trans … H12 H23)
+] qed.
+
 
 axiom BadCminorProgram : String.
@@ -332 +395 @@
     let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
       «f, ?»
-] Env.
+] Env. 
 (* For new labels, we need to step back through the definitions of f until we
    hit the point that it was added. *)
-try @fn_graph_included_refl
+try (repeat @fn_includes_step @I)
 try (#l #H @H)
-[ 7: #l #H whd % [ @H |
-    @present_inc
-    @present_inc
-    @present_inc
-    @(use_sig ? (present ???)) ]
-| 8: #l #H
-    @present_inc
-    @(use_sig ? (present ???))
-(* For the monotonicity properties, we just keep going back until we're at the
-   start.  The repeat tactical helps here. *)
-| *: repeat @fn_graph_included_sig @fn_graph_included_refl
+[ #l #H whd % [ @H | @(present_included … (use_sig … lfalse)) repeat @fn_includes_step @I ]
+| #l #H @(present_included … (use_sig ?? resume_at)) repeat @fn_includes_step @I
 ] qed.
 
@@ -364 +418 @@
     ]
 ] Env pf.
-[ //
-| 2,3: normalize in pf; destruct
-| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
+try (repeat @fn_includes_step @I)
+[ 1,2: normalize in pf; destruct
 | @Env
 | @(proj2 … Env)
-| normalize in pf; destruct @e0 ] qed.
+| normalize in pf; destruct @e0
+] qed.
 
 axiom UnknownLabel : String.
@@ -417 +471 @@
 qed.
 
-(* We need to show that the graph only grows, and that Cminor labels will end
-   up in the graph. *)
-definition Cminor_labels_added ≝ λle,s,f'.
-∀l. Exists ? (λl'.l=l') (labels_of s) →
-∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
-
-record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
-{ stmt_graph_inc : fn_graph_included ? f f'
-; stmt_labels_added : Cminor_labels_added le s f'
-}.
-
 lemma empty_Cminor_labels_added : ∀le,s,f'.
   labels_of s = [ ] → Cminor_labels_added le s f'.
@@ -439 +482 @@
 qed.
 
-lemma fn_graph_included_inv : ∀label_env,s,f,f0.
-  ∀f':Σf':partial_fn label_env. add_stmt_inv label_env s f0 f'.
-  fn_graph_included label_env f f0 →
-  fn_graph_included label_env f f'.
-#label_env #s #f #f0 * #f' * #H1 #H2 #H3
-@(fn_graph_inc_trans … H3 H1)
-qed.
-
-lemma present_inc' : ∀le,s,f,l.
-  ∀f':(Σf':partial_fn le. add_stmt_inv le s f f').
-  present ?? (pf_graph le f) l →
-  present ?? (pf_graph le f') l.
-#le #s #f #l * #f' * * #H1 #H2 #H3
-@H1 @H3
+lemma Cminor_labels_inc : ∀le,s,f,f'.
+  fn_graph_included le f f' →
+  Cminor_labels_added le s f →
+  Cminor_labels_added le s f'.
+#le #s #f #f' #INC #ADDED
+#l #E cases (ADDED l E) #l' * #L #P
+%{l'} % [ @L | @(present_included … P) @INC ]
 qed.
 
@@ -461 +497 @@
 #le #s #s' #f * #f' * #H1 #H2 #H3
 #l #E cases (H3 l E) #l' * #L #P
-%{l'} % [ @L | @present_inc' @P ]
+%{l'} % [ @L | @(present_included … P) @H1 ]
 qed.
 
@@ -470 +506 @@
 #le #s #f * #f' #H1 #H2
 #l #E cases (H2 l E) #l' * #L #P
-%{l'} % [ @L | @present_inc @P ]
+%{l'} % [ @L | @(present_included … P) @H1 ]
 qed.
 
@@ -580 +616 @@
 try @(π2 (π1 Env))
 try @mk_add_stmt_inv
+try (repeat @fn_includes_step @I)
 try (@empty_Cminor_labels_added @refl)
 try (@(All_mp … (use_sig ?? exits)))
-try @fn_graph_included_refl
-try (repeat @fn_graph_included_inv repeat @fn_graph_included_sig @fn_graph_included_refl)
 try (#l #H @I)
 try (#l #H @H)
 [ -f @(choose_regs_length … (sym_eq … Eregs))
-| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
 | whd in Env @(π1 (π1 (π1 Env)))
 | -f @(choose_regs_length … (sym_eq … Eregs))
-| @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl
 | #l #H cases (Exists_append … H)
   [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1)
-  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (use_sig ?? f2))
-  ]
-| #l #H @present_inc' @H
-| #l #H @present_inc' @use_sig
-| @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
+  | @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I | @(stmt_labels_added ???? (use_sig ?? f2)) ]
+  ]
+| #l #H @(present_included … H) repeat @fn_includes_step @I
+| #l #H @(present_included … (use_sig ?? l_next)) repeat @fn_includes_step @I
 | #l #H cases (Exists_append … H)
-  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f1)) 
-  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f2)) 
-  ]
-| #l #H % [ @H | @present_inc @present_inc' @present_inc @(use_sig ?? (pf_entry ? f2)) ]
-| #l #H @present_inc @present_inc' @H
-| #l #H @present_inc @H
+  [ @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f1))) repeat @fn_includes_step @I
+  | @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f2))) repeat @fn_includes_step @I
+  ]
+| #l #H % [ @H | @(present_included … (use_sig ?? l2)) repeat @fn_includes_step @I ]
+| 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
 | @(use_sig ?? (pf_entry ??))
-| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_refl
 | @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
 | % [ @use_sig | @(use_sig ?? exits) ]
 | @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
 | #l #H @use_sig
-| #l #H @present_inc @use_sig
-| #l #H % [ @present_inc @present_inc @present_inc @present_inc @use_sig | @H ]
-| @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
+| #l #H @(present_included … (use_sig ?? l_default)) repeat @fn_includes_step @I
+| #l #H % [ @(present_included … (use_sig ?? l_case)) repeat @fn_includes_step @I | @H ]
 | @use_sig
-| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
 | #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
         |@Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?))
         ]
 | #l1 #H whd %2 @lookup_label_lpresent
-| @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl
 | @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
 ] qed.
-
-(*
-definition mk_fn : ∀le. partial_fn le → internal_function ≝
-λle, f.
-  mk_internal_function
-    (pf_labgen ? f)
-    (pf_reggen ? f)
-    (pf_result ? f)
-    (pf_params ? f)
-    (pf_locals ? f)
-    (pf_stacksize ? f)
-    (pf_graph ? f)
-    ?
-    (pf_entry ? f)
-    (pf_exit ? f).
-#l #s #E @(labels_P_mp … (pf_closed ? f l s E))
-#l' * [ // | #H
-*)
 
 definition c2ra_function (*: internal_function → internal_function*) ≝