Ignore:
Timestamp:
Jun 8, 2011, 10:09:06 AM (9 years ago)
Author:
sacerdot
Message:

Bug more evident.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r893 r894  
    684684 ∀pc.
    685685 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
    686 *)
     686 
    687687axiom bitvector_elim_complete:
    688688 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
     
    693693 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
    694694qed.
     695*)
     696
     697
     698
    695699
    696700(*
     
    711715
    712716axiom eq_bv_refl: ∀n,v. eq_bv n v v = true.
     717
     718axiom bitvector_3_elim_prop:
     719 ∀P: BitVector 3 → Prop.
     720  P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
     721  P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
     722  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
    713723
    714724lemma test:
     
    735745 normalize in ⊢ (???% → ?)
    736746 [42,93,95: @split_elim #vl #vm #E >E -E; normalize in ⊢ (???% → ?)
    737  |92,94: cases daemon ]
     747 |92,94: @split_elim #v1 #v2 #E >E -E; @(bitvector_3_elim_prop … v1) normalize in ⊢ (???% → ?)
     748   #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
     749   try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
     750   change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
     751   whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
     752   <H2 whd BUGHERE
     753 ]
    738754 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
    739755 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
Note: See TracChangeset for help on using the changeset viewer.