Changeset 1102 for Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

Timestamp:

Aug 4, 2011, 1:55:53 PM (10 years ago)

Author:

campbell

Message:

Tidy up branch

File:

• Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma (modified) (4 diffs)

Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

@@ -4 +4 @@
 include "Cminor/syntax.ma".
 include "common/Globalenvs.ma".
+include "utilities/pair.ma".
+include "utilities/deppair.ma".
 
 (* XXX having to specify the return type in the match is annoying. *)
@@ -39 +41 @@
 qed.
 
-lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D.
-  let 〈a,b〉 ≝ x in 〈P a b, Q a b〉 = 〈P (\fst x) (\snd x), Q (\fst x) (\snd x)〉.
-#A #B #C #D * // qed.
-
-lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D.
-  R (Q (\fst x) (\snd x)) → R (\snd (let 〈a,b〉 ≝ x in 〈P a, Q a b〉)).
-#A #B #C #D *; normalize /2/
-qed.
-
-lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s.
-  stmt_inv s.
-* #s #p @p
-qed.
-
 definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
 λid,r,init.
@@ -63 +51 @@
 | elim init
   [ % //
-  | #h #t #IH whd in ⊢ (?(???%)) @sndredex % [ % [ % // | @sig_stmt_inv ] | @IH ]
+  | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
 ] qed. 
 
@@ -69 +57 @@
 λvars. foldr ? (Σs:stmt. stmt_inv s)
   (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
-% [ % [ % // | @sig_stmt_inv ] | @sig_stmt_inv ]
+% [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
 qed.