Changeset 891 for src/common


Ignore:
Timestamp:
Jun 7, 2011, 4:53:53 PM (9 years ago)
Author:
campbell
Message:

Revise proofs affected by recent matita change.

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/Mem.ma

    r790 r891  
    6666  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    6767  update_block … x v f x = v.
    68 #A * * #ix #v #f whd in ⊢ (??%?);
    69 >(eqZb_z_z …) //;
     68#A * * #ix #v #f whd in ⊢ (??%?)
     69>eq_block_b_b //
    7070qed.
    7171
  • src/common/Smallstep.ma

    r700 r891  
    133133#tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar;
    134134[ #s2' #e2 #e3 #e4 destruct; @plus_one //;
    135 | #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 destruct;
    136     >(Eapp_assoc …) @(plus_left … H1)
     135| #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5
     136    >e1 >e4 >e2 >Eapp_assoc destruct @(plus_left … H1)
    137137    [ 2: @(star_right … H2 Hstep) //;
    138138    | skip;
  • src/common/Values.ma

    r797 r891  
    6464| @H2 % #E destruct elim H3 /2/
    6565] qed.
     66
     67lemma eq_block_b_b : ∀b. eq_block b b = true.
     68* * #z whd in ⊢ (??%?) >eqZb_z_z @refl
     69qed.
    6670
    6771(* Characterise the memory regions which the pointer representations can
     
    12251229lemma sign_ext_lessdef:
    12261230  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
    1227 #n #v1 #v2 #H inversion H;//;#v #e1 #e2 <e1 in H >e2 //;
     1231#n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) //
    12281232qed.
    12291233(*
Note: See TracChangeset for help on using the changeset viewer.