Changeset 2006


Ignore:
Timestamp:
May 30, 2012, 6:43:02 PM (5 years ago)
Author:
boender
Message:
  • added alias for bitvector zero
  • changed extralib bounded forall/exists to use le instead of lt
Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r1928 r2006  
    5050definition zero: ∀n:nat. BitVector n ≝
    5151  λn: nat. replicate bool n false.
    52    
     52
     53alias id "bv_zero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)".
     54
    5355definition maximum: ∀n:nat. BitVector n ≝
    5456  λn: nat. replicate bool n true.
  • src/utilities/extralib.ma

    r1949 r2006  
    8181
    8282lemma 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).
    8484 #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   ]
    8689 | #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)
    8992       [ #H @(Hk … (le_S_S_to_le … H))
    90        | #H >(injective_S … H) @HPk
     93       | #H >H @HPk
    9194       ]
    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 ]
    9396     ]
    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.nk→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ]
    9598   ]
    9699 ]
     
    98101
    99102lemma 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).
    101104 #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   ]
    103110 | #k #Hind cases Hind
    104111   [ #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 ]
    107114     | #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) @conj
     115       [ #H @(absurd (∃n.n k ∧ P n)) [ @(ex_intro … n) @conj
    109116         [ @(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 ]
    111118       ] 
    112119     ]
     
    131138
    132139lemma 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.
    134141 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x)
    135142 @conj [ @Hx | @Habs ]
     
    137144
    138145lemma 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.
    140147 #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))
    143153   [ #HP elim (Hind ?)
    144154     [ -Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx) | @(proj2 ?? Hx) ]
    145155     | @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx)
    146156       [ #H2 @H @(le_S_S_to_le … H2)
    147        | #H2 >(injective_S … H2) @HP
     157       | #H2 >H2 @HP
    148158       ]
    149159     ]
    150    | #HP @(ex_intro … k) @conj [ @le_n | @HP ]
     160   | #HP @(ex_intro … (S k)) @conj [ @le_n | @HP ]
    151161   ]
    152162 ]
Note: See TracChangeset for help on using the changeset viewer.