# Changeset 1894

Ignore:
Timestamp:
Apr 20, 2012, 12:52:31 PM (7 years ago)
Message:

Closed a hole in the proof by deriving a contradiction using even_p and odd_p

File:
1 edited

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

 r1892 qed. lemma blah: let rec odd_p (n: nat) on n ≝ match n with [ O ⇒ False | S n' ⇒ even_p n' ] and even_p (n: nat) on n ≝ match n with [ O ⇒ True | S n' ⇒ odd_p n' ]. let rec n_even_p_to_n_plus_2_even_p (n: nat) on n: even_p n → even_p (n + 2) ≝ match n with [ O ⇒ ? | S n' ⇒ ? ] and n_odd_p_to_n_plus_2_odd_p (n: nat) on n: odd_p n → odd_p (n + 2) ≝ match n with [ O ⇒ ? | S n' ⇒ ? ]. [1,3: normalize #assm assumption |2: normalize @n_odd_p_to_n_plus_2_odd_p |4: normalize @n_even_p_to_n_plus_2_even_p ] qed. let rec two_times_n_even_p (n: nat) on n: even_p (2 * n) ≝ match n with [ O ⇒ ? | S n' ⇒ ? ] and two_times_n_plus_one_odd_p (n: nat) on n: odd_p ((2 * n) + 1) ≝ match n with [ O ⇒ ? | S n' ⇒ ? ]. [1,3: normalize @I |2: normalize >plus_n_Sm <(associative_plus n' n' 1) >(plus_n_O (n' + n')) cut(n' + n' + 0 + 1 = 2 * n' + 1) [1: // |2: #refl_assm >refl_assm @two_times_n_plus_one_odd_p ] |4: normalize >plus_n_Sm cut(n' + (n' + 1) + 1 = (2 * n') + 2) [1: normalize /2/ |2: #refl_assm >refl_assm @n_even_p_to_n_plus_2_even_p @two_times_n_even_p ] ] qed. let rec even_p_to_not_odd_p (n: nat) on n: even_p n → ¬ odd_p n ≝ match n with [ O ⇒ ? | S n' ⇒ ? ] and odd_p_to_not_even_p (n: nat) on n: odd_p n → ¬ even_p n ≝ match n with [ O ⇒ ? | S n' ⇒ ? ]. [1: normalize #_ @nmk #assm assumption |3: normalize #absurd cases absurd |2: normalize @odd_p_to_not_even_p |4: normalize @even_p_to_not_odd_p ] qed. lemma even_p_odd_p_cases: ∀n: nat. even_p n ∨ odd_p n. #n elim n [1: normalize @or_introl @I |2: #n' #inductive_hypothesis normalize cases inductive_hypothesis #assm try (@or_introl assumption) try (@or_intror assumption) ] qed. lemma two_times_n_plus_one_refl_two_times_n_to_False: ∀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 assm @conj @two_times_n_even_p |2: * #_ #absurd cases (even_p_to_not_odd_p … absurd) #assm @assm @two_times_n_plus_one_odd_p ] qed. lapply (eqb_true_to_refl … eqb_true_assm) #refl_assm cases (blah … refl_assm) cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm) |2: #eqb_false_assm lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm) -refl_assm #refl_assm cases (blah … refl_assm) cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm) |2: #eqb_false_assm
Note: See TracChangeset for help on using the changeset viewer.