Ignore:
Timestamp:
Jul 24, 2012, 7:40:21 PM (8 years ago)
Author:
campbell
Message:

Use the return statement invariant. Restructure the invariants for Cminor
a bit to make them more understandable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r2251 r2252  
    3838    ]
    3939].
    40 % /2/
     40% /3/
    4141cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
    42 destruct;/3/
     42destruct;/4 by stmt_labels_mp, conj/
    4343qed.
    4444
     
    5050     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    5151  〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
    52 [ % /2/
     52[ % /3/
    5353| elim init
    54   [ % /2/
    55   | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%);
    56     % [ % [ % /2/ | @(pi2 … (init_datum …)) ] | @IH ]
     54  [ % /3/
     55  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair
     56    %
     57    [ /3/
     58    | % [ @(pi2 … (init_datum …)) | @IH ]
     59    ]
    5760] qed.
    5861
    5962definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
    6063λvars. foldr ? (Σs:stmt. stmt_inv s)
    61   (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? (conj ?? I I) I)) vars.
    62 % [ % [ % /2/ | @(pi2 … s) ] | @(pi2 … (init_var …)) ]
    63 qed.
     64  (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip ?) vars.
     65[ % [ /3/ | % [ @(pi2 … s) | @(pi2 … (init_var …)) ] ]
     66| /4/
     67] qed.
    6468
    6569lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
    6670#s elim s //
    67 [ #s1 #s2 #IH1 #IH2 * * * * #_ #_ #_ #H1 #H2 whd in ⊢ (??%?);
     71[ #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
    6872  >(IH1 H1) >(IH2 H2) @refl
    69 | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
     73| #sz #sg #e #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
    7074  >(IH1 H1) >(IH2 H2) @refl
    7175| #l #s #IH * * * #_ *
    72 | #l #s #IH * * #_ #_ #H @(IH H)
     76| #l #s #IH * #_ #H @(IH H)
    7377] qed.
    7478
     
    9599      | inr _ ⇒ 〈id',f'〉 ]) ].
    96100%
    97 [ % [ % // |
    98   @(stmt_P_mp … H) #s * * #V #L #R %
    99   [ @(stmt_vars_mp … V) #i #t *
    100   | @(stmt_labels_mp … L) #l *
    101   | cases s in R ⊢ %; // #x *
     101[ % //
     102| %
     103  [ @(stmt_P_mp … H) #s * * #V #L #R %
     104    [ @(stmt_vars_mp … V) #i #t *
     105    | @(stmt_labels_mp … L) #l *
     106    | cases s in R ⊢ %; // #x *
     107    ]
     108  | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
    102109  ]
    103   ]
    104 | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
    105110] qed.
    106111
Note: See TracChangeset for help on using the changeset viewer.