Changeset 1516 for src/Clight/casts.ma


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

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/casts.ma

    r1489 r1516  
    5454<add_with_carries_unfold
    5555cases (add_with_carries n x y c)
    56 #rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?) >bool_eta //
     56#rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?); >bool_eta //
    5757qed.
    5858
     
    6060  tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y.
    6161#n #hx #hy #x #y
    62 whd in ⊢ (??(???%)%)
     62whd in ⊢ (??(???%)%);
    6363<(add_with_carries_extend n hx hy x y false)
    6464cases (add_with_carries (S n) (hx:::x) (hy:::y) false)
     
    9595#m elim m
    9696[ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs
    97   whd in ⊢ (??%?) >truncate_eq >truncate_eq  @refl
     97  whd in ⊢ (??%?); >truncate_eq >truncate_eq  @refl
    9898| #m' #IH #n #x #y #c
    9999  >(hdtl … x) >(hdtl … y)
    100100  >truncate_head >truncate_head <IH
    101101  <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y))
    102   cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%)
     102  cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%);
    103103  <truncate_tail <truncate_tail @refl
    104104] qed.
     
    106106lemma truncate_plus : ∀m,n,x,y.
    107107  truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y).
    108 #m #n #x #y whd in ⊢ (??(???%)%) <truncate_add_with_carries
     108#m #n #x #y whd in ⊢ (??(???%)%); <truncate_add_with_carries
    109109cases (add_with_carries ????) //
    110110qed.
     
    114114#m0 elim m0
    115115[ #n #x >truncate_eq //
    116 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
     116| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
    117117] qed.
    118118
    119119theorem zero_plus_reduce : ∀m,n,x,y.
    120120  truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y.
    121 #m #n #x #y <(truncate_pad m n x) in ⊢ (???%) <(truncate_pad m n y) in ⊢ (???%)
     121#m #n #x #y <(truncate_pad m n x) in ⊢ (???%); <(truncate_pad m n y) in ⊢ (???%);
    122122@truncate_plus
    123123qed.
     
    130130#m0 elim m0
    131131[ #n #x >truncate_eq //
    132 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
     132| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
    133133] qed.
    134134
    135135theorem sign_plus_reduce : ∀m,n,x,y.
    136136  truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y.
    137 #m #n #x #y <(truncate_sign m n x) in ⊢ (???%) <(truncate_sign m n y) in ⊢ (???%)
     137#m #n #x #y <(truncate_sign m n x) in ⊢ (???%); <(truncate_sign m n y) in ⊢ (???%);
    138138@truncate_plus
    139139qed.
     
    171171  <add_with_carries_unfold
    172172  cases (add_with_carries n x y c)
    173   #lb #cs whd in ⊢ (??%%) >bool_eta
     173  #lb #cs whd in ⊢ (??%%); >bool_eta
    174174  //
    175175| *: skip
     
    181181#m #n #x @(vector_inv_n … x) #h #t elim n
    182182[ @refl
    183 | #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
     183| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?); >IH @refl
    184184] qed.
    185185
     
    201201lemma zero_negate_reduce : ∀m,n,x.
    202202  truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x.
    203 #m #n #x whd in ⊢ (??(???%)%)
     203#m #n #x whd in ⊢ (??(???%)%);
    204204lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
    205205cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
    206 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     206#rs #cs whd in ⊢ (??%? → ??(???%)?);
    207207>truncate_negation_bv
    208208>truncate_pad >truncate_zero cases (add_with_carries ????)
     
    212212lemma sign_negate_reduce : ∀m,n,x.
    213213  truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x.
    214 #m #n #x whd in ⊢ (??(???%)%)
     214#m #n #x whd in ⊢ (??(???%)%);
    215215>sign_bitflip <(zero_sign (S n) m)
    216216lapply (truncate_add_with_carries m (S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
    217217cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
    218 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     218#rs #cs whd in ⊢ (??%? → ??(???%)?);
    219219>truncate_sign >truncate_sign cases (add_with_carries ????)
    220220#rs' #cs' #E destruct //
     
    224224  truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y.
    225225#m #n #x #y
    226 whd in ⊢ (??(???%)%)
     226whd in ⊢ (??(???%)%);
    227227lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
    228228cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
    229 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     229#rs #cs whd in ⊢ (??%? → ??(???%)?);
    230230>zero_negate_reduce >truncate_pad
    231231cases (add_with_carries ????)
     
    236236  truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y.
    237237#m #n #x #y
    238 whd in ⊢ (??(???%)%)
     238whd in ⊢ (??(???%)%);
    239239lapply (truncate_add_with_carries m (S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
    240240cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
    241 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     241#rs #cs whd in ⊢ (??%? → ??(???%)?);
    242242>sign_negate_reduce >truncate_sign
    243243cases (add_with_carries ????)
Note: See TracChangeset for help on using the changeset viewer.