Changeset 1928 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
May 9, 2012, 1:36:35 PM (8 years ago)
Author:
mulligan
Message:

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1870 r1928  
    178178 | #H / by I/
    179179 ]
     180qed.
     181
     182axiom nat_of_bitvector_bitvector_of_nat_inverse:
     183  ∀n: nat.
     184  ∀b: nat.
     185    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
     186
     187axiom bitvector_of_nat_inverse_nat_of_bitvector:
     188  ∀n: nat.
     189  ∀b: BitVector n.
     190    bitvector_of_nat n (nat_of_bitvector n b) = b.
     191
     192lemma nat_of_bitvector_aux_injective:
     193  ∀n: nat.
     194  ∀l, r: BitVector n.
     195  ∀acc_l, acc_r: nat.
     196    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
     197      acc_l = acc_r ∧ l ≃ r.
     198  #n #l
     199  elim l #r
     200  [1:
     201    #acc_l #acc_r normalize
     202    >(BitVector_O r) normalize /2/
     203  |2:
     204    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
     205    normalize normalize in inductive_hypothesis;
     206    cases (BitVector_Sn … r)
     207    #r_hd * #r_tl #r_refl destruct normalize
     208    cases hd cases r_hd normalize
     209    [1:
     210      #relevant
     211      cases (inductive_hypothesis … relevant)
     212      #acc_assm #tl_assm destruct % //
     213      lapply (injective_plus_l ? ? ? acc_assm)
     214      -acc_assm #acc_assm
     215      change with (2 * acc_l = 2 * acc_r) in acc_assm;
     216      lapply (injective_times_r ? ? ? ? acc_assm) /2/
     217    |4:
     218      #relevant
     219      cases (inductive_hypothesis … relevant)
     220      #acc_assm #tl_assm destruct % //
     221      change with (2 * acc_l = 2 * acc_r) in acc_assm;
     222      lapply(injective_times_r ? ? ? ? acc_assm) /2/
     223    |2:
     224      #relevant 
     225      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
     226        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
     227      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
     228      [1:
     229        #eqb_true_assm
     230        lapply (eqb_true_to_refl … eqb_true_assm)
     231        #refl_assm
     232        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
     233      |2:
     234        #eqb_false_assm
     235        lapply (eqb_false_to_not_refl … eqb_false_assm)
     236        #not_refl_assm cases not_refl_assm #absurd_assm
     237        cases (inductive_hypothesis … relevant) #absurd
     238        cases (absurd_assm absurd)
     239      ]
     240    |3:
     241      #relevant 
     242      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
     243        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
     244      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
     245      [1:
     246        #eqb_true_assm
     247        lapply (eqb_true_to_refl … eqb_true_assm)
     248        #refl_assm
     249        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
     250        -refl_assm #refl_assm
     251        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
     252      |2:
     253        #eqb_false_assm
     254        lapply (eqb_false_to_not_refl … eqb_false_assm)
     255        #not_refl_assm cases not_refl_assm #absurd_assm
     256        cases (inductive_hypothesis … relevant) #absurd
     257        cases (absurd_assm absurd)
     258      ]
     259    ]
     260  ]
     261qed.
     262
     263lemma nat_of_bitvector_destruct:
     264  ∀n: nat.
     265  ∀l_hd, r_hd: bool.
     266  ∀l_tl, r_tl: BitVector n.
     267    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
     268      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
     269  #n #l_hd #r_hd #l_tl #r_tl
     270  normalize
     271  cases l_hd cases r_hd
     272  normalize
     273  [4:
     274    /2/
     275  |1:
     276    #relevant
     277    cases (nat_of_bitvector_aux_injective … relevant)
     278    #_ #l_r_tl_refl destruct /2/
     279  |2,3:
     280    #relevant
     281    cases (nat_of_bitvector_aux_injective … relevant)
     282    #absurd destruct(absurd)
     283  ]
     284qed.
     285
     286lemma BitVector_cons_injective:
     287  ∀n: nat.
     288  ∀l_hd, r_hd: bool.
     289  ∀l_tl, r_tl: BitVector n.
     290    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
     291  #l #l_hd #r_hd #l_tl #r_tl
     292  #l_refl #r_refl destruct %
     293qed.
     294
     295lemma refl_nat_of_bitvector_to_refl:
     296  ∀n: nat.
     297  ∀l, r: BitVector n.
     298    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
     299  #n
     300  elim n
     301  [1:
     302    #l #r
     303    >(BitVector_O l)
     304    >(BitVector_O r)
     305    #_ %
     306  |2:
     307    #n' #inductive_hypothesis #l #r
     308    lapply (BitVector_Sn ? l) #l_hypothesis
     309    lapply (BitVector_Sn ? r) #r_hypothesis
     310    cases l_hypothesis #l_hd #l_tail_hypothesis
     311    cases r_hypothesis #r_hd #r_tail_hypothesis
     312    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
     313    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
     314    destruct #cons_refl
     315    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
     316    #hd_refl #tl_refl
     317    @BitVector_cons_injective try assumption
     318    @inductive_hypothesis assumption
     319  ]
    180320qed.
    181321
Note: See TracChangeset for help on using the changeset viewer.