Changeset 2108 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Jun 25, 2012, 2:39:06 PM (8 years ago)
Author:
mulligan
Message:

Various axioms closed and others moved around. Uncommented main lemma and found that it no longer compiles due to changing how we expand jumps. Problem in proof highlighted with XXX for Claudio.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2032 r2108  
    534534    \snd (half_add n l r).
    535535
    536 axiom add_zero:
     536lemma half_add_carry_Sn:
     537  ∀n: nat.
     538  ∀l: BitVector n.
     539  ∀hd: bool.
     540    \fst (half_add (S n) (hd:::l) (false:::(zero n))) =
     541      andb hd (\fst (half_add n l (zero n))).
     542  #n #l elim l
     543  [1:
     544    #hd normalize cases hd %
     545  |2:
     546    #n' #hd #tl #inductive_hypothesis #hd'
     547    whd in match half_add; normalize nodelta
     548    whd in match full_add; normalize nodelta
     549    normalize in ⊢ (??%%); cases hd' normalize
     550    @pair_elim #c1 #r #c1_r_refl cases c1 %
     551  ]
     552qed.
     553
     554lemma half_add_zero_carry_false:
     555  ∀m: nat.
     556  ∀b: BitVector m.
     557    \fst (half_add m b (zero m)) = false.
     558  #m #b elim b try %
     559  #n #hd #tl #inductive_hypothesis
     560  change with (false:::(zero ?)) in match (zero ?);
     561  >half_add_carry_Sn >inductive_hypothesis cases hd %
     562qed.
     563
     564axiom half_add_true_true_carry_true:
     565  ∀n: nat.
     566  ∀hd, hd': bool.
     567  ∀l, r: BitVector n.
     568    \fst (half_add (S n) (true:::l) (true:::r)) = true.
     569
     570lemma add_Sn_carry_add:
     571  ∀n: nat.
     572  ∀hd, hd': bool.
     573  ∀l, r: BitVector n.
     574    add (S n) (hd:::l) (hd':::r) =
     575      xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r.
     576  #n #hd #hd' #l elim l
     577  [1:
     578    #r cases hd cases hd'
     579    >(BitVector_O … r) normalize %
     580  |2:
     581    #n' #hd'' #tl #inductive_hypothesis #r
     582    cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct
     583    cases hd cases hd' cases hd'' cases hd'''
     584    whd in match (xorb ??);
     585    cases daemon
     586  ]
     587qed.
     588 
     589lemma add_zero:
    537590  ∀n: nat.
    538591  ∀l: BitVector n.
    539592    l = add n l (zero …).
     593  #n #l elim l try %
     594  #n' #hd #tl #inductive_hypothesis
     595  change with (false:::zero ?) in match (zero ?);
     596  >add_Sn_carry_add >half_add_zero_carry_false
     597  cases hd <inductive_hypothesis %
     598qed.
     599
     600axiom most_significant_bit_zero:
     601  ∀size, m: nat.
     602  ∀size_proof: 0 < size.
     603    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
     604  normalize in size_proof; normalize @le_S_S assumption
     605qed.
     606   
     607axiom zero_add_head:
     608  ∀m: nat.
     609  ∀tl, hd.
     610    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).
     611
     612lemma zero_add:
     613  ∀m: nat.
     614  ∀b: BitVector m.
     615    add m (zero m) b = b.
     616  #m #b elim b try %
     617  #m' #hd #tl #inductive_hypothesis
     618  <inductive_hypothesis in ⊢ (???%);
     619  >zero_add_head %
     620qed.
     621
     622axiom bitvector_of_nat_one_Sm:
     623  ∀m: nat.
     624    ∃b: BitVector m.
     625      bitvector_of_nat (S m) 1 ≃ b @@ [[true]].
     626
     627axiom increment_zero_bitvector_of_nat_1:
     628  ∀m: nat.
     629  ∀b: BitVector m.
     630    increment m b = add m (bitvector_of_nat m 1) b.
    540631
    541632axiom add_associative:
    542   ∀n: nat.
    543   ∀l, c, r: BitVector n.
    544     add … l (add … c r) = add … (add … l c) r.
     633  ∀m: nat.
     634  ∀l, c, r: BitVector m.
     635    add m l (add m c r) = add m (add m l c) r.
     636
     637lemma bitvector_of_nat_aux_buffer:
     638  ∀m, n: nat.
     639  ∀b: BitVector m.
     640    bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b.
     641  #m #n elim n
     642  [1:
     643    #b change with (? = add ? (zero …) b)
     644    >zero_add %
     645  |2:
     646    #n' #inductive_hypothesis #b
     647    whd in match (bitvector_of_nat_aux ???);
     648    >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%);
     649    >inductive_hypothesis >increment_zero_bitvector_of_nat_1
     650    >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1))
     651    <add_associative %
     652  ]
     653qed.
     654
     655definition sign_extension: Byte → Word ≝
     656  λc.
     657    let b ≝ get_index_v ? 8 c 1 ? in
     658      [[ b; b; b; b; b; b; b; b ]] @@ c.
     659  normalize
     660  repeat (@le_S_S)
     661  @le_O_n
     662qed.
     663
     664lemma bitvector_of_nat_sign_extension_equivalence:
     665  ∀m: nat.
     666  ∀size_proof: m < 128.
     667    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
     668  #m #size_proof whd in ⊢ (??%?);
     669  >most_significant_bit_zero
     670  [1:
     671    elim m
     672    [1:
     673      %
     674    |2:
     675      #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta
     676      whd in match (bitvector_of_nat_aux ???);
     677      whd in match (bitvector_of_nat_aux ???) in ⊢ (???%);
     678      >(bitvector_of_nat_aux_buffer 16 n')
     679      cases daemon
     680    ]
     681  |2:
     682    assumption
     683  ]
     684qed.
    545685
    546686axiom add_commutative:
Note: See TracChangeset for help on using the changeset viewer.