- Timestamp:
- Aug 4, 2011, 1:55:53 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma
r1101 r1102 4 4 include "Cminor/syntax.ma". 5 5 include "common/Globalenvs.ma". 6 include "utilities/pair.ma". 7 include "utilities/deppair.ma". 6 8 7 9 (* XXX having to specify the return type in the match is annoying. *) … … 39 41 qed. 40 42 41 lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D.42 let 〈a,b〉 ≝ x in 〈P a b, Q a b〉 = 〈P (\fst x) (\snd x), Q (\fst x) (\snd x)〉.43 #A #B #C #D * // qed.44 45 lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D.46 R (Q (\fst x) (\snd x)) → R (\snd (let 〈a,b〉 ≝ x in 〈P a, Q a b〉)).47 #A #B #C #D *; normalize /2/48 qed.49 50 lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s.51 stmt_inv s.52 * #s #p @p53 qed.54 55 43 definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝ 56 44 λid,r,init. … … 63 51 | elim init 64 52 [ % // 65 | #h #t #IH whd in ⊢ (?(???%)) @ sndredex % [ % [ % // | @sig_stmt_inv] | @IH ]53 | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ] 66 54 ] qed. 67 55 … … 69 57 λvars. foldr ? (Σs:stmt. stmt_inv s) 70 58 (λ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. 71 % [ % [ % // | @ sig_stmt_inv ] | @sig_stmt_inv]59 % [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ] 72 60 qed. 73 61
Note: See TracChangeset
for help on using the changeset viewer.