Ignore:
Timestamp:
Dec 7, 2011, 3:48:32 PM (8 years ago)
Author:
boender
Message:
  • cleaned up Assembly, moved some definitions elsewhere
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r1523 r1593  
    1717include "basics/logic.ma".
    1818include "utilities/pair.ma".
     19include "ASM/Util.ma".
    1920
    2021lemma eq_rect_Type0_r:
     
    7576  ]
    7677] qed.
     78
     79(* some useful stuff for quantifiers *)
     80
     81lemma 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 ]
     96qed.
     97
     98lemma 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 ]
     114qed.
     115
     116lemma 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 ]
     120qed.
     121
     122lemma 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 ]
     137qed.
Note: See TracChangeset for help on using the changeset viewer.