Changeset 1593 for src/utilities/extralib.ma
 Timestamp:
 Dec 7, 2011, 3:48:32 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r1523 r1593 17 17 include "basics/logic.ma". 18 18 include "utilities/pair.ma". 19 include "ASM/Util.ma". 19 20 20 21 lemma eq_rect_Type0_r: … … 75 76 ] 76 77 ] qed. 78 79 (* some useful stuff for quantifiers *) 80 81 lemma dec_bounded_forall: 82 ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n). 83 #P #HP_dec #k elim k k 84 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O 85  #k #Hind cases Hind 86 [ #Hk cases (HP_dec k) 87 [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn) 88 [ #H @(Hk … (le_S_S_to_le … H)) 89  #H >(injective_S … H) @HPk 90 ] 91  #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k)))  @HPk ] 92 ] 93  #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn'))  @Hk ] 94 ] 95 ] 96 qed. 97 98 lemma dec_bounded_exists: 99 ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n). 100 #P #HP_dec #k elim k k 101 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O 102  #k #Hind cases Hind 103 [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn)  @(proj2 … Hn) ] 104  #Hk cases (HP_dec k) 105 [ #HPk %1 @(ex_intro … k) @conj [ @le_n  @HPk ] 106  #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn)) 107 [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj 108 [ @(le_S_S_to_le … H)  @(proj2 … Hn) ]  @Hk ] 109  #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn)  @HPk ] 110 ] 111 ] 112 ] 113 ] 114 qed. 115 116 lemma not_exists_forall: 117 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x. 118 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) 119 @conj [ @Hx  @Habs ] 120 qed. 121 122 lemma not_forall_exists: 123 ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x. 124 #k #P #Hdec elim k 125 [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O 126  k #k #Hind #Hfa cases (Hdec k) 127 [ #HP elim (Hind ?) 128 [ Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx)  @(proj2 ?? Hx) ] 129  @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx) 130 [ #H2 @H @(le_S_S_to_le … H2) 131  #H2 >(injective_S … H2) @HP 132 ] 133 ] 134  #HP @(ex_intro … k) @conj [ @le_n  @HP ] 135 ] 136 ] 137 qed.
Note: See TracChangeset
for help on using the changeset viewer.