Changeset 905


Ignore:
Timestamp:
Jun 8, 2011, 6:07:20 PM (8 years ago)
Author:
mulligan
Message:

work from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r904 r905  
    4848
    4949(* END RUSSELL **)
     50
     51
     52definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
     53  λP.
     54    P true ∧ P false.
     55 
     56let rec bitvector_elim_prop_internal
     57  (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
     58  match m return λm. m ≤ n → BitVector (n - m) → Prop with
     59  [ O    ⇒ λprf1. λprefix. P ?
     60  | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
     61  ].
     62  [ applyS prefix
     63  | letin res ≝ (bit ::: prefix)
     64    < (minus_S_S ? ?)
     65    > (minus_Sn_m ? ?)
     66  [ @ res
     67  | @ prf2
     68  ]
     69  | /2/
     70  ].
     71qed.
     72
     73definition bitvector_elim_prop ≝
     74  λn: nat.
     75  λP: BitVector n → Prop.
     76    bitvector_elim_prop_internal n P n ? ?.
     77  [ @ (le_n ?)
     78  | < (minus_n_n ?)
     79    @ [[ ]]
     80  ]
     81qed.
     82
     83lemma eq_b_eq:
     84  ∀b, c.
     85    eq_b b c = true → b = c.
     86  #b #c
     87  cases b
     88  cases c
     89  normalize //
     90qed.
     91
     92lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
     93 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     94 #n #hd #tl #abs @⊥ //
     95qed.
     96
     97lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
     98 ∃hd.∃tl.v ≃ VCons bool n hd tl.
     99 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     100 [ #abs @⊥ //
     101 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     102qed.
     103
     104lemma eq_bv_eq:
     105  ∀n, v, q.
     106    eq_bv n v q = true → v = q.
     107  #n #v #q generalize in match v
     108  elim q
     109  [ #v #h @BitVector_O
     110  | #n #hd #tl #ih #v' #h
     111    cases (BitVector_Sn ? v')
     112    #hd' * #tl' #jmeq >jmeq in h;
     113    #new_h
     114    change in new_h with ((andb ? ?) = ?);
     115    cases(conjunction_true … new_h)
     116    #eq_heads #eq_tails
     117    whd in eq_heads:(??(??(%))?);
     118    cases(eq_b_eq … eq_heads)
     119    whd in eq_tails:(??(?????(%))?);
     120    change in eq_tails with (eq_bv ??? = ?);
     121    <(ih tl') //
     122  ]
     123qed.
     124
     125lemma bool_eq_internal_eq:
     126  ∀b, c.
     127    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
     128  #b #c
     129  cases b
     130  [ normalize //
     131  | normalize
     132    cases c
     133    [ normalize //
     134    | normalize //
     135    ]
     136  ]
     137qed.
     138
     139lemma eq_bv_refl:
     140  ∀n,v. eq_bv n v v = true.
     141  #n #v
     142  elim v
     143  [ //
     144  | #n #hd #tl #ih
     145    normalize
     146    cases hd
     147    [ normalize
     148      @ ih
     149    | normalize
     150      @ ih
     151    ]
     152  ]
     153qed.
     154
     155lemma eq_eq_bv:
     156  ∀n, v, q.
     157    v = q → eq_bv n v q = true.
     158  #n #v
     159  elim v
     160  [ #q #h <h normalize %
     161  | #n #hd #tl #ih #q #h >h //
     162  ]
     163qed.
    50164
    51165let rec foldl_strong_internal
     
    625739qed.
    626740
    627 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
    628  #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
    629  #n #hd #tl #abs @⊥ //
    630 qed.
    631 
    632 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
    633  ∃hd.∃tl.v ≃ VCons bool n hd tl.
    634  #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
    635  [ #abs @⊥ //
    636  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    637 qed.
    638 
    639741coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    640742
Note: See TracChangeset for help on using the changeset viewer.