Changeset 905 for src/ASM

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

work from today

File:
1 edited

Unmodified
Added
Removed
• src/ASM/AssemblyProof.ma

 r904 (* END RUSSELL **) definition bit_elim_prop: ∀P: bool → Prop. Prop ≝ λP. P true ∧ P false. let rec bitvector_elim_prop_internal (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝ match m return λm. m ≤ n → BitVector (n - m) → Prop with [ O    ⇒ λprf1. λprefix. P ? | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?) ]. [ applyS prefix | letin res ≝ (bit ::: prefix) < (minus_S_S ? ?) > (minus_Sn_m ? ?) [ @ res | @ prf2 ] | /2/ ]. qed. definition bitvector_elim_prop ≝ λn: nat. λP: BitVector n → Prop. bitvector_elim_prop_internal n P n ? ?. [ @ (le_n ?) | < (minus_n_n ?) @ [[ ]] ] qed. lemma eq_b_eq: ∀b, c. eq_b b c = true → b = c. #b #c cases b cases c normalize // qed. lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // #n #hd #tl #abs @⊥ // qed. lemma BitVector_Sn: ∀n.∀v:BitVector (S n). ∃hd.∃tl.v ≃ VCons bool n hd tl. #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) [ #abs @⊥ // | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] qed. lemma eq_bv_eq: ∀n, v, q. eq_bv n v q = true → v = q. #n #v #q generalize in match v elim q [ #v #h @BitVector_O | #n #hd #tl #ih #v' #h cases (BitVector_Sn ? v') #hd' * #tl' #jmeq >jmeq in h; #new_h change in new_h with ((andb ? ?) = ?); cases(conjunction_true … new_h) #eq_heads #eq_tails whd in eq_heads:(??(??(%))?); cases(eq_b_eq … eq_heads) whd in eq_tails:(??(?????(%))?); change in eq_tails with (eq_bv ??? = ?); <(ih tl') // ] qed. lemma bool_eq_internal_eq: ∀b, c. (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c. #b #c cases b [ normalize // | normalize cases c [ normalize // | normalize // ] ] qed. lemma eq_bv_refl: ∀n,v. eq_bv n v v = true. #n #v elim v [ // | #n #hd #tl #ih normalize cases hd [ normalize @ ih | normalize @ ih ] ] qed. lemma eq_eq_bv: ∀n, v, q. v = q → eq_bv n v q = true. #n #v elim v [ #q #h h // ] qed. let rec foldl_strong_internal qed. lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // #n #hd #tl #abs @⊥ // qed. lemma BitVector_Sn: ∀n.∀v:BitVector (S n). ∃hd.∃tl.v ≃ VCons bool n hd tl. #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) [ #abs @⊥ // | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] qed. coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
Note: See TracChangeset for help on using the changeset viewer.