Changeset 1593 for src/utilities
 Timestamp:
 Dec 7, 2011, 3:48:32 PM (9 years ago)
 Location:
 src/utilities
 Files:

 2 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. 
src/utilities/extranat.ma
r1516 r1593 63 63 ] qed. 64 64 65 lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m. 66 /2/ qed. 67 68 lemma le_plus_k: 69 ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k. 70 #n #m elim m m; 71 [ #Hn % [ @O  <(le_n_O_to_eq n Hn) // ] 72  #m #Hind #Hn cases (le_to_or_lt_eq … Hn) Hn; #Hn 73 [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k)  >Hk // ] 74  % [ @O  <Hn // ] 75 ] 76 ] 77 qed. 78 79 lemma eq_plus_S_to_lt: 80 ∀n,m,p:ℕ.n = m + (S p) → m < n. 81 #n #m #p /2 by lt_plus_to_lt_l/ 82 qed. 65 83 66 84 (* "Fast" proofs: some proofs get reduced during normalization (in particular,
Note: See TracChangeset
for help on using the changeset viewer.