Ignore:
Timestamp:
Jun 19, 2012, 4:43:50 PM (7 years ago)
Author:
boender
Message:
  • renamed medium to absolute jump
  • revised proofs of policy, some daemons removed
  • reverted earlier change in extralib, bounded quantification now again uses lt
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r2006 r2101  
    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  [ 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
    8986 | #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)
    9289       [ #H @(Hk … (le_S_S_to_le … H))
    93        | #H >H @HPk
     90       | #H >(injective_S … H) @HPk
    9491       ]
    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 ]
    9693     ]
    97    | #Hk %2 @nmk #Habs @(absurd (∀n.nk→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 ]
    9895   ]
    9996 ]
     
    10198
    10299lemma 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).
    104101 #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
    110103 | #k #Hind cases Hind
    111104   [ #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 ]
    114107     | #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) @conj
     108       [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj
    116109         [ @(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 ]
    118111       ] 
    119112     ]
     
    138131
    139132lemma 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.
    141134 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x)
    142135 @conj [ @Hx | @Habs ]
     
    144137
    145138lemma 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.
    147140 #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)
    153143   [ #HP elim (Hind ?)
    154144     [ -Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx) | @(proj2 ?? Hx) ]
    155145     | @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx)
    156146       [ #H2 @H @(le_S_S_to_le … H2)
    157        | #H2 >H2 @HP
     147       | #H2 >(injective_S … H2) @HP
    158148       ]
    159149     ]
    160    | #HP @(ex_intro … (S k)) @conj [ @le_n | @HP ]
     150   | #HP @(ex_intro … k) @conj [ @le_n | @HP ]
    161151   ]
    162152 ]
Note: See TracChangeset for help on using the changeset viewer.