Changeset 1672


Ignore:
Timestamp:
Feb 1, 2012, 4:16:06 PM (6 years ago)
Author:
campbell
Message:

Matita now generates a couple of inversion lemmas that were manually
proved before.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1603 r1672  
    124124#ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
    125125[ #id #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
    126 | #id #sp #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
    127 | #e' #ty' #sp #l' #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
    128 | #e' #id #ty' #l' #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
    129 | #e' #id #ty' #l' #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
     126| #id #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
     127| #e' #ty' #sp #l' #pc #ofs #tr #H' #e1 #e2 #e3 #e4 #e5 -H destruct; //
     128| #e' #id #ty' #l' #ofs #id' #fs #d #tr #H' #e1 #e2 #e3 #e4 #e5 #e6 #e7 -H destruct; //
     129| #e' #id #ty' #l' #ofs #id' #fs #tr #H' #e1 #e2 #e3 #e4 #e5 #e6 -H destruct; //
    130130] qed.
    131131
  • src/Clight/CexecSound.ma

    r1647 r1672  
    285285    | #a #b #c #d #e #bad destruct (bad);
    286286    | #a #b #c #d #e #f #g #h #bad destruct (bad);
    287     | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad @False_ind destruct (bad);
    288     | #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
     287    | #a #b #c #d #e #f #g #h #i #j #k #l #bad @False_ind destruct (bad);
     288    | #a #b #c #d #e #f #g #h #i #j #bad destruct (bad);
    289289    ]
    290290| #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'
    291 | #a #b #c #d #e #f #g #h #i #bad destruct (bad);
    292 | #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
    293 | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad);
    294 | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad);
    295291| #a #b #c #d #e #f #g #h #bad destruct (bad);
    296 | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad destruct (bad);
     292| #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
     293| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
     294| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
     295| #a #b #c #d #e #f #g #bad destruct (bad);
     296| #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
     297| #a #b #c #d #e #f #g #bad destruct (bad);
     298| #a #b #c #d #e #f #g #h #i #j #k #l #bad  destruct (bad);
    297299| #a #b #c #d #e #f #g #h #bad destruct (bad);
    298 | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad  destruct (bad);
    299 | #a #b #c #d #e #f #g #h #i #bad destruct (bad);
    300 | #a #b #c #d #e #f #g #bad destruct (bad);
     300| #a #b #c #d #e #f #bad destruct (bad);
    301301] qed.
    302302
  • src/Clight/Csem.ma

    r1545 r1672  
    722722  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H)
    723723  ].
    724 
     724(*
    725725inverter eval_expr_inv_ind for eval_expr : Prop.
    726 
     726*)
    727727let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem)
    728728  (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
     
    744744ninverter eval_lvalue_inv_ind for eval_lvalue : Prop.
    745745*)
    746 
     746(*
    747747definition eval_lvalue_inv_ind :
    748748  ∀x1: genv.
     
    793793| *: skip
    794794] qed.
    795 
     795*)
    796796let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
    797797  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
Note: See TracChangeset for help on using the changeset viewer.