Changeset 2101 for src/utilities/extralib.ma
 Timestamp:
 Jun 19, 2012, 4:43:50 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r2006 r2101 81 81 82 82 lemma dec_bounded_forall: 83 ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n ≤ k → P n) + ¬(∀n.n ≤k → P n).83 ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n). 84 84 #P #HP_dec #k elim k k 85 [ cases (HP_dec 0) 86 [ #HP %1 #n #Hn <(le_n_O_to_eq … Hn) @HP 87  #HP %2 @nmk #H cases HP #H2 @H2 @H @le_n 88 ] 85 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O 89 86  #k #Hind cases Hind 90 [ #Hk cases (HP_dec (S k))91 [ #HPk %1 #n #Hn elim(le_to_or_lt_eq … Hn)87 [ #Hk cases (HP_dec k) 88 [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn) 92 89 [ #H @(Hk … (le_S_S_to_le … H)) 93  #H > H@HPk90  #H >(injective_S … H) @HPk 94 91 ] 95  #HPk %2 @nmk #Habs @(absurd (P (S k))) [ @(Habs … (le_n (S k)))  @HPk ]92  #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k)))  @HPk ] 96 93 ] 97  #Hk %2 @nmk #Habs @(absurd (∀n.n ≤k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn'))  @Hk ]94  #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn'))  @Hk ] 98 95 ] 99 96 ] … … 101 98 102 99 lemma dec_bounded_exists: 103 ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n ≤ k ∧ P n) + ¬(∃n.n ≤k ∧ P n).100 ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n). 104 101 #P #HP_dec #k elim k k 105 [ cases (HP_dec 0) 106 [ #HP %1 @(ex_intro ?? 0) @conj [ @le_n  @HP ] 107  #HP %2 @nmk #Habs @(absurd ?? HP) elim Habs #k #Hk 108 >(le_n_O_to_eq … (proj1 ?? Hk)) @(proj2 ?? Hk) 109 ] 102 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O 110 103  #k #Hind cases Hind 111 104 [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn)  @(proj2 … Hn) ] 112  #Hk cases (HP_dec (S k))113 [ #HPk %1 @(ex_intro … (S k)) @conj [ @le_n  @HPk ]105  #Hk cases (HP_dec k) 106 [ #HPk %1 @(ex_intro … k) @conj [ @le_n  @HPk ] 114 107  #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn)) 115 [ #H @(absurd (∃n.n ≤k ∧ P n)) [ @(ex_intro … n) @conj108 [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj 116 109 [ @(le_S_S_to_le … H)  @(proj2 … Hn) ]  @Hk ] 117  #H @(absurd (P (S k))) [ <H@(proj2 … Hn)  @HPk ]110  #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn)  @HPk ] 118 111 ] 119 112 ] … … 138 131 139 132 lemma not_exists_forall: 140 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x ≤ k ∧ P x) → ∀x.x ≤k → ¬P x.133 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x. 141 134 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) 142 135 @conj [ @Hx  @Habs ] … … 144 137 145 138 lemma not_forall_exists: 146 ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x ≤ k → P x) → ∃x.x ≤k ∧ ¬P x.139 ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x. 147 140 #k #P #Hdec elim k 148 [ #Hfa @(ex_intro … 0) @conj 149 [ @le_n 150  @nmk #HP @(absurd ?? Hfa) #i #Hi <(le_n_O_to_eq … Hi) @HP 151 ] 152  k #k #Hind #Hfa cases (Hdec (S k)) 141 [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O 142  k #k #Hind #Hfa cases (Hdec k) 153 143 [ #HP elim (Hind ?) 154 144 [ Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx)  @(proj2 ?? Hx) ] 155 145  @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx) 156 146 [ #H2 @H @(le_S_S_to_le … H2) 157  #H2 > H2@HP147  #H2 >(injective_S … H2) @HP 158 148 ] 159 149 ] 160  #HP @(ex_intro … (S k)) @conj [ @le_n  @HP ]150  #HP @(ex_intro … k) @conj [ @le_n  @HP ] 161 151 ] 162 152 ]
Note: See TracChangeset
for help on using the changeset viewer.