# Changeset 1892 for src/ASM/ASMCosts.ma

Ignore:
Timestamp:
Apr 19, 2012, 6:09:01 PM (8 years ago)
Message:

Lots of work from today

File:
1 edited

Unmodified
Removed
• ## src/ASM/ASMCosts.ma

 r1891 nat_of_bitvector (S n) (hd:::tl) = (2 ^ n) * nat_of_bool hd + nat_of_bitvector n tl. axiom plus_refl_to_refl_lor_refl: ∀m, m', n, n': nat. m + m' = n + n' → (m = n ∧ m' = n') ∨ (m = n' ∧ m' = n). axiom mult_refl_to_refl_lor_refl: ∀m, m', n, n': nat. m * m' = n * n' → (m = n ∧ m' = n') ∨ (m = n' ∧ n = m'). axiom Vector_inv_ind_2: ∀a: Type[0]. (* lemma BitVector_inv_ind_2: ∀n: nat. ∀left: Vector a n. ∀right: Vector a n. ∀P: (∀m: nat. Vector a m → Vector a m → Prop). (n ≃ 0 → (left ≃ VEmpty a) → (right ≃ VEmpty a) → (P 0 [[ ]] [[ ]])) → ∀left: Vector bool n. ∀right: Vector bool n. ∀P: (∀m: nat. Vector bool m → Vector bool m → Prop). (n ≃ O → left ≃ VEmpty bool → right ≃ VEmpty bool → (P 0 [[ ]] [[ ]])) → (∀m: nat. ∀hd, hd': a. ∀tl, tl': Vector a m. ∀hd, hd': bool. ∀tl, tl': Vector bool m. (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') → (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) → P n left right. #n #left elim left [1: #right #P #base #step >(BitVector_O right) @base try % >(BitVector_O right) % |2: #n' #hd #tl #inductive_hypothesis #right #P #base #step cases (BitVector_Sn … right) #hd' #right_tail_exists_assm cases right_tail_exists_assm #right_tl #right_tl_refl destruct @step try % #n_refl' #left_refl #right_refl destruct @inductive_hypothesis *) include "arithmetics/div_and_mod.ma". lemma n_plus_1_n_to_False: ∀n: nat. n + 1 = n → False. #n elim n [1: normalize #absurd destruct(absurd) |2: #n' #inductive_hypothesis normalize #absurd @inductive_hypothesis /2/ ] qed. lemma one_two_times_n_to_False: ∀n: nat. 1=2*n→False. #n cases n [1: normalize #absurd destruct(absurd) |2: #n' normalize #absurd lapply (injective_S … absurd) -absurd #absurd /2/ ] qed. lemma generalized_nat_cases: ∀n: nat. n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m). #n cases n [1: @or_introl @or_introl % |2: #n' cases n' [1: @or_introl @or_intror % |2: #n'' @or_intror %{n''} % ] ] qed. lemma blah: ∀m, n: nat. 2 * m + 1 = 2 * n → False. #m #n elim m elim n normalize [1: #absurd destruct(absurd) |2,3: #m' #inductive_hypothesis (BitVector_O r) normalize /2/ |2: #hd #tl #inductive_hypothesis #r #acc_l #acc_r normalize normalize in inductive_hypothesis; cases (BitVector_Sn … r) #r_hd * #r_tl #r_refl destruct normalize cases hd cases r_hd normalize [1: #relevant cases (inductive_hypothesis … relevant) #acc_assm #tl_assm destruct % // lapply (injective_plus_l ? ? ? acc_assm) -acc_assm #acc_assm change with (2 * acc_l = 2 * acc_r) in acc_assm; lapply (injective_times_r ? ? ? ? acc_assm) /2/ |4: #relevant cases (inductive_hypothesis … relevant) #acc_assm #tl_assm destruct % // change with (2 * acc_l = 2 * acc_r) in acc_assm; lapply(injective_times_r ? ? ? ? acc_assm) /2/ |2: #relevant change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) = (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant; cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r)) [1: #eqb_true_assm lapply (eqb_true_to_refl … eqb_true_assm) #refl_assm cases (blah … refl_assm) |2: #eqb_false_assm lapply (eqb_false_to_not_refl … eqb_false_assm) #not_refl_assm cases not_refl_assm #absurd_assm cases (inductive_hypothesis … relevant) #absurd cases (absurd_assm absurd) ] |3: #relevant change with ((nat_of_bitvector_aux r (2 * acc_l) tl) = (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant; cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1)) [1: #eqb_true_assm lapply (eqb_true_to_refl … eqb_true_assm) #refl_assm lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm) -refl_assm #refl_assm cases (blah … refl_assm) |2: #eqb_false_assm lapply (eqb_false_to_not_refl … eqb_false_assm) #not_refl_assm cases not_refl_assm #absurd_assm cases (inductive_hypothesis … relevant) #absurd cases (absurd_assm absurd) ] ] ] qed. lemma nat_of_bitvector_destruct: l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl. #n #l_hd #r_hd #l_tl #r_tl @(Vector_inv_ind_2 bool n l_tl r_tl) [1: #length_refl #l_tl_refl #r_tl_refl destruct cases l_hd cases r_hd normalize try (#absurd destruct(absurd)) @conj % |2: #m #l_hd' #r_hd' #l_tl' #r_tl' #inductive_hypothesis #n_refl #l_tl_refl #r_tl_refl destruct elim l_tl [1: #r_tl >(BitVector_O r_tl) normalize cases l_hd cases r_hd normalize try (#absurd destruct(absurd)) @conj % |2: #n' #hd #tl #inductive_hypothesis #r_tl cases (BitVector_Sn … r_tl) #hd' #tl_hypothesis' cases tl_hypothesis' #tl' #tl_refl' >tl_refl' cases daemon ] qed. axiom Vector_inv_ind_2: ∀a: Type[0]. ∀n: nat. ∀left: Vector a n. ∀right: Vector a n. ∀P: (∀m: nat. Vector a m → Vector a m → Prop). (n ≃ 0 → (left ≃ VEmpty a) → (right ≃ VEmpty a) → (P 0 [[ ]] [[ ]])) → (∀m: nat. ∀hd, hd': a. ∀tl, tl': Vector a m. (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') → (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) → P n left right. normalize cases l_hd cases r_hd normalize [4: /2/ |1: #relevant cases (nat_of_bitvector_aux_injective … relevant) #_ #l_r_tl_refl destruct /2/ |2,3: #relevant cases (nat_of_bitvector_aux_injective … relevant) #absurd destruct(absurd) ] qed. lemma BitVector_cons_injective:
Note: See TracChangeset for help on using the changeset viewer.