Changeset 1516 for src/common


Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

Location:
src/common
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1465 r1516  
    145145lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
    146146  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
    147 * * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct
     147* * #P #Hne #Heq whd in ⊢ (?%); try (@Heq @refl) @Hne % #E destruct
    148148qed.
    149149
     
    175175  (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d).
    176176#A * * #P #p #f #d #Q #Hne #Heq
    177 [ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))
    178 | *: whd in ⊢ (?%) @Hne % #E destruct
     177[ 1,5,9: whd in ⊢ (?%); @(Heq (refl ??))
     178| *: whd in ⊢ (?%); @Hne % #E destruct
    179179] qed.
    180180
     
    351351 #A #B #C #f #l elim l
    352352  [ #l' #E normalize in E; destruct %
    353   | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)
     353  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?);
    354354    [2: #err #E destruct
    355355    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
    356       cases (map_partial … f tl) in IH ⊢ %
    357       #x #IH normalize in ⊢ (??%? → ?) #ABS destruct normalize
     356      cases (map_partial … f tl) in IH ⊢ %;
     357      #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize
    358358      >(IH x) // ]]
    359359qed.
     
    487487 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
    488488 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
    489    #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct normalize in e1 ⊢ % >e0 //
     489   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 //
    490490   >e0 in e1; normalize #H @H ]
    491491qed.
     
    498498  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
    499499  (*CSC: interactive mode because of dependent types *)
    500   generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p))
     500  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
    501501  cases (map_partial … transf_partial_variable (prog_vars … p))
    502502  [ #vl #EQ
  • src/common/Events.ma

    r961 r1516  
    155155  ].
    156156[ *; #NE @False_rect_Type0 @NE @refl
    157 | % #E' >E' in E #E whd in E:(??%%); destruct (E);
     157| % #E' >E' in E; #E whd in E:(??%%); destruct (E);
    158158] qed.
    159159
  • src/common/FrontEndOps.ma

    r1410 r1516  
    139139  val_typ v' t'.
    140140#t #t' #op elim op
    141 [ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?)
    142   cases sg whd in ⊢ (??%? → ?) #E' destruct %
    143 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E' destruct %
     141[ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?);
     142  cases sg whd in ⊢ (??%? → ?); #E' destruct %
     143| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E' destruct %
    144144| #t'' #sz #sg cases t''
    145   [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?) #E' destruct cases (eq_bv ???) whd in ⊢ (?%?) %
     145  [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?); #E' destruct cases (eq_bv ???) whd in ⊢ (?%?); %
    146146  | #r #H #v #v' #H1 @(elim_val_typ … H1) whd %
    147     [ whd in ⊢ (??%? → ?) #E' destruct; %
    148     | #b #c #o whd in ⊢ (??%? → ?) #E' destruct %
     147    [ whd in ⊢ (??%? → ?); #E' destruct; %
     148    | #b #c #o whd in ⊢ (??%? → ?); #E' destruct %
    149149    ]
    150150  | #f *
    151151  ]
    152 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %
    153 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
    154 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
    155 | #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
    156 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %
    157 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %
    158 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2
    159 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2
    160 | #t'' #v #v' #H whd in ⊢ (??%? → ?) #E destruct @H
    161 | #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) cases (eq_bv ???)
    162   whd in ⊢ (??%? → ?) #E destruct //
     152| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %
     153| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     154| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     155| #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     156| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
     157| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
     158| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
     159| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
     160| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
     161| #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
     162  whd in ⊢ (??%? → ?); #E destruct //
    163163| #sz #sg #r #v #v' #H @(elim_val_typ … H) %
    164   [ whd in ⊢ (??%? → ?) #E destruct %
    165   | #b #c #o whd in ⊢ (??%? → ?) #E destruct
     164  [ whd in ⊢ (??%? → ?); #E destruct %
     165  | #b #c #o whd in ⊢ (??%? → ?); #E destruct
    166166  ]
    167167] qed.
  • src/common/GenMem.ma

    r1395 r1516  
    5353  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    5454  update_block … x v f x = v.
    55 #A * * #ix #v #f whd in ⊢ (??%?)
     55#A * * #ix #v #f whd in ⊢ (??%?);
    5656>eq_block_b_b //
    5757qed.
  • src/common/Identifiers.ma

    r1515 r1516  
    5656
    5757lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true.
    58 #tag * #id whd in ⊢ (??%?) >eqb_n_n @refl
     58#tag * #id whd in ⊢ (??%?); >eqb_n_n @refl
    5959qed.
    6060
     
    6464
    6565definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
    66 #tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %)
     66#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %);
    6767#E [ % | %2 ]
    6868lapply E @eqb_elim
     
    184184  ] (refl ? u').
    185185cases l in p E; cases m; -l' -m' #m' #l'
    186 whd in ⊢ (% → ?)
    187  whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?)
     186whd in ⊢ (% → ?);
     187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?);
    188188#NL #U cases NL #H @H @(update_fail … U)
    189189qed.
     
    194194  present tag A (update_present tag A m id' H' a) id.
    195195#tag #A * #m * #id #a * #id' #H #H'
    196 whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
     196whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta
    197197cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
    198 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ????? U)
     198[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U)
    199199  % #E' destruct
    200 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(??%%)?))
     200| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?));
    201201  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
    202202] qed.
  • src/common/Integers.ma

    r1512 r1516  
    124124
    125125lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y).
    126 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?) #E
     126#x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?); #E
    127127[ %1 lapply E @(eq_bv_elim … x y) [ // | #_ #X destruct ]
    128128| %2 lapply E @(eq_bv_elim … x y) [ #_ #X destruct | /2/ ]
  • src/common/Mem.ma

    r891 r1516  
    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 ⊢ (??%?)
     68#A * * #ix #v #f whd in ⊢ (??%?);
    6969>eq_block_b_b //
    7070qed.
     
    192192lemma align_size_chunk_divides:
    193193  ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
    194 #chunk cases chunk;[8:#r cases r ]normalize;/3/;
     194#chunk cases chunk;[8:#r cases r ]normalize;/3 by witness/;
    195195qed.
    196196
     
    735735lemma valid_not_valid_diff:
    736736  ∀m,b,b'. valid_block m b →  ¬(valid_block m b') → b ≠ b'.
    737 #m #b #b' #H #H' @nmk #e >e in H #H
     737#m #b #b' #H #H' @nmk #e >e in H; #H
    738738@(absurd ? H H')
    739739qed.
     
    759759#m #chunk #chunk2 #r #b #ofs #H1 #H2
    760760elim H2;#H3 #H4 #H5 #H6 #H7
    761 >H1 in H5 #H5
     761>H1 in H5; #H5
    762762% //;
    763763<(align_chunk_compat … H1) //;
     
    807807#b' cases (store_inv … STORE)
    808808#H1 #H2 >H2
    809 whd in ⊢ (??(?%?)?) whd in ⊢ (??%?)
    810 whd in ⊢ (??(?%)?) @eq_block_elim #E
     809whd in ⊢ (??(?%?)?); whd in ⊢ (??%?);
     810whd in ⊢ (??(?%)?); @eq_block_elim #E
    811811normalize //
    812812qed.
     
    864864#chunk #m1 #r #b #ofs #v #m2 #STORE
    865865#chunk' #r' #b' #ofs'
    866 * Hv;
     866* as Hv
    867867#Hvb #Hl #Hr #Halign #Hptr
    868868% //;
     
    878878#chunk #m1 #r #b #ofs #v #m2 #STORE
    879879#chunk' #r' #b' #ofs'
    880 * Hv;
     880* as Hv
    881881#Hvb #Hl #Hr #Halign #Hcompat
    882882% //;
     
    35143514  ∀m,a,v.
    35153515  storev Mint8signed m a v = storev Mint8unsigned m a v.
    3516 #m #a #v whd in ⊢ (??%%) elim a //
    3517 #r #b #p #ofs whd in ⊢ (??%%)
     3516#m #a #v whd in ⊢ (??%%); elim a //
     3517#r #b #p #ofs whd in ⊢ (??%%);
    35183518>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
    35193519qed.
     
    35223522  ∀m,a,v.
    35233523  storev Mint16signed m a v = storev Mint16unsigned m a v.
    3524 #m #a #v whd in ⊢ (??%%) elim a //
    3525 #r #b #p #ofs whd in ⊢ (??%%)
     3524#m #a #v whd in ⊢ (??%%); elim a //
     3525#r #b #p #ofs whd in ⊢ (??%%);
    35263526>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
    35273527qed.
  • src/common/Pointers.ma

    r1215 r1516  
    3434  P (eq_block b1 b2).
    3535#P * #r1 #i1 * #r2 #i2 #H1 #H2
    36 whd in ⊢ (?%) @eq_region_elim #H3
    37 [ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
     36whd in ⊢ (?%); @eq_region_elim #H3
     37[ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
    3838| @H2 % #E destruct elim H3 /2/
    3939] qed.
    4040
    4141lemma eq_block_b_b : ∀b. eq_block b b = true.
    42 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl
     42* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
    4343qed.
    4444
     
    7171
    7272lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
    73  whd in match eq_offset /2/
     73 whd in match eq_offset; /2/
    7474qed.
    7575
     
    109109
    110110lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true.
    111  #p whd in ⊢ (??%?) >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
     111 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
    112112qed.
  • src/common/PositiveMap.ma

    r1515 r1516  
    6262[ * //
    6363| #tl #IH *
    64   [ whd in ⊢ (??%%) @IH
     64  [ whd in ⊢ (??%%); @IH
    6565  | #x #l #r @IH
    6666  ]
    6767| #tl #IH *
    68   [ whd in ⊢ (??%%) @IH
     68  [ whd in ⊢ (??%%); @IH
    6969  | #x #l #r @IH
    7070  ]
     
    8080| #b' #IH *
    8181  [ * [ #NE @refl | #x #l #r #NE @refl ]
    82   | #c' * [ #NE whd in ⊢ (??%%) @IH /2/
    83           | #x #l #r #NE whd in ⊢ (??%%) @IH /2/
     82  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
     83          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
    8484          ]
    8585  | #c' * //
     
    8888  [ * [ #NE @refl | #x #l #r #NE @refl ]
    8989  | #c' * //
    90   | #c' * [ #NE whd in ⊢ (??%%) @IH /2/
    91           | #x #l #r #NE whd in ⊢ (??%%) @IH /2/
     90  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
     91          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
    9292          ]
    9393  ]
     
    110110[ * [ // | * // #x #l #r normalize #E destruct ]
    111111| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
    112                    cases (update A b' a r) in U ⊢ %
     112                   cases (update A b' a r) in U ⊢ %;
    113113                   [ // | normalize #t #E destruct ]
    114114            ]
    115115| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
    116                    cases (update A b' a l) in U ⊢ %
     116                   cases (update A b' a l) in U ⊢ %;
    117117                   [ // | normalize #t #E destruct ]
    118118            ]
     
    124124#A #b #a elim b
    125125[ * [ #t' normalize #E destruct
    126     | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?)
     126    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?);
    127127      #E destruct //
    128128    ]
    129129| #b' #IH *
    130130  [ #t' normalize #E destruct
    131   | #x #l #r #t' whd in ⊢ (??%? → ??%?)
     131  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
    132132    lapply (IH r)
    133133    cases (update A b' a r)
     
    138138| #b' #IH *
    139139  [ #t' normalize #E destruct
    140   | #x #l #r #t' whd in ⊢ (??%? → ??%?)
     140  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
    141141    lapply (IH l)
    142142    cases (update A b' a l)
Note: See TracChangeset for help on using the changeset viewer.