Changeset 2006
 Timestamp:
 May 30, 2012, 6:43:02 PM (7 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r1928 r2006 50 50 definition zero: ∀n:nat. BitVector n ≝ 51 51 λn: nat. replicate bool n false. 52 52 53 alias id "bv_zero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)". 54 53 55 definition maximum: ∀n:nat. BitVector n ≝ 54 56 λn: nat. replicate bool n true. 
src/utilities/extralib.ma
r1949 r2006 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 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O 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 ] 86 89  #k #Hind cases Hind 87 [ #Hk cases (HP_dec k)88 [ #HPk %1 #n #Hn cases(le_to_or_lt_eq … Hn)90 [ #Hk cases (HP_dec (S k)) 91 [ #HPk %1 #n #Hn elim (le_to_or_lt_eq … Hn) 89 92 [ #H @(Hk … (le_S_S_to_le … H)) 90  #H > (injective_S … H)@HPk93  #H >H @HPk 91 94 ] 92  #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k)))  @HPk ]95  #HPk %2 @nmk #Habs @(absurd (P (S k))) [ @(Habs … (le_n (S k)))  @HPk ] 93 96 ] 94  #Hk %2 @nmk #Habs @(absurd (∀n.n <k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn'))  @Hk ]97  #Hk %2 @nmk #Habs @(absurd (∀n.n≤k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn'))  @Hk ] 95 98 ] 96 99 ] … … 98 101 99 102 lemma dec_bounded_exists: 100 ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n <k ∧ P n).103 ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n ≤ k ∧ P n) + ¬(∃n.n ≤ k ∧ P n). 101 104 #P #HP_dec #k elim k k 102 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O 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 ] 103 110  #k #Hind cases Hind 104 111 [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn)  @(proj2 … Hn) ] 105  #Hk cases (HP_dec k)106 [ #HPk %1 @(ex_intro … k) @conj [ @le_n  @HPk ]112  #Hk cases (HP_dec (S k)) 113 [ #HPk %1 @(ex_intro … (S k)) @conj [ @le_n  @HPk ] 107 114  #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn)) 108 [ #H @(absurd (∃n.n <k ∧ P n)) [ @(ex_intro … n) @conj115 [ #H @(absurd (∃n.n ≤ k ∧ P n)) [ @(ex_intro … n) @conj 109 116 [ @(le_S_S_to_le … H)  @(proj2 … Hn) ]  @Hk ] 110  #H @(absurd (P k)) [ <(injective_S … H)@(proj2 … Hn)  @HPk ]117  #H @(absurd (P (S k))) [ <H @(proj2 … Hn)  @HPk ] 111 118 ] 112 119 ] … … 131 138 132 139 lemma not_exists_forall: 133 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x <k → ¬P x.140 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x ≤ k ∧ P x) → ∀x.x ≤ k → ¬P x. 134 141 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) 135 142 @conj [ @Hx  @Habs ] … … 137 144 138 145 lemma not_forall_exists: 139 ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x <k ∧ ¬P x.146 ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x ≤ k → P x) → ∃x.x ≤ k ∧ ¬P x. 140 147 #k #P #Hdec elim k 141 [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O 142  k #k #Hind #Hfa cases (Hdec 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)) 143 153 [ #HP elim (Hind ?) 144 154 [ Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx)  @(proj2 ?? Hx) ] 145 155  @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx) 146 156 [ #H2 @H @(le_S_S_to_le … H2) 147  #H2 > (injective_S … H2)@HP157  #H2 >H2 @HP 148 158 ] 149 159 ] 150  #HP @(ex_intro … k) @conj [ @le_n  @HP ]160  #HP @(ex_intro … (S k)) @conj [ @le_n  @HP ] 151 161 ] 152 162 ]
Note: See TracChangeset
for help on using the changeset viewer.