[3] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
[487] | 15 | include "basics/types.ma". |
---|
[1599] | 16 | include "basics/lists/list.ma". |
---|
[487] | 17 | include "basics/logic.ma". |
---|
[1593] | 18 | include "ASM/Util.ma". |
---|
[3] | 19 | |
---|
[487] | 20 | lemma eq_rect_Type0_r: |
---|
[3] | 21 | ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
[487] | 22 | #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption. |
---|
| 23 | qed. |
---|
[3] | 24 | |
---|
[487] | 25 | lemma eq_rect_r2: |
---|
[3] | 26 | ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p. |
---|
[487] | 27 | #A #a #x #p cases p; #P #H assumption. |
---|
| 28 | qed. |
---|
[3] | 29 | |
---|
[487] | 30 | lemma eq_rect_Type2_r: |
---|
[3] | 31 | ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
[487] | 32 | #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption. |
---|
| 33 | qed. |
---|
[3] | 34 | |
---|
[487] | 35 | lemma eq_rect_CProp0_r: |
---|
[16] | 36 | ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
[487] | 37 | #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption. |
---|
| 38 | qed. |
---|
[16] | 39 | |
---|
[487] | 40 | lemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x. |
---|
| 41 | #A #x #y *;#H @nmk #H' /2/; |
---|
| 42 | qed. |
---|
[3] | 43 | |
---|
| 44 | interpretation "logical iff" 'iff x y = (iff x y). |
---|
| 45 | |
---|
| 46 | (* bool *) |
---|
| 47 | |
---|
[487] | 48 | definition xorb : bool → bool → bool ≝ |
---|
[3] | 49 | λx,y. match x with [ false ⇒ y | true ⇒ notb y ]. |
---|
| 50 | |
---|
[1523] | 51 | |
---|
| 52 | |
---|
[3] | 53 | |
---|
| 54 | (* should be proved in nat.ma, but it's not! *) |
---|
[487] | 55 | lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. |
---|
| 56 | #n elim n; |
---|
| 57 | [ #m cases m; //; |
---|
| 58 | | #n' #IH #m cases m; [ /2/; | #m' whd in match (eqb (S n') (S m')) in ⊢ %; |
---|
| 59 | lapply (IH m'); cases (eqb n' m'); /2/; ] |
---|
| 60 | ] qed. |
---|
[3] | 61 | |
---|
| 62 | (* datatypes/list.ma *) |
---|
| 63 | |
---|
[487] | 64 | theorem nil_append_nil_both: |
---|
| 65 | ∀A:Type[0]. ∀l1,l2:list A. |
---|
[3] | 66 | l1 @ l2 = [] → l1 = [] ∧ l2 = []. |
---|
[891] | 67 | #A #l1 #l2 cases l1 |
---|
| 68 | [ cases l2 |
---|
[487] | 69 | [ /2/ |
---|
[891] | 70 | | normalize #h #t #H destruct |
---|
[487] | 71 | ] |
---|
[891] | 72 | | cases l2 |
---|
| 73 | [ normalize #h #t #H destruct |
---|
| 74 | | normalize #h1 #t1 #h2 #h3 #H destruct |
---|
[487] | 75 | ] |
---|
| 76 | ] qed. |
---|
[1593] | 77 | |
---|
| 78 | (* some useful stuff for quantifiers *) |
---|
| 79 | |
---|
| 80 | lemma dec_bounded_forall: |
---|
| 81 | ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n). |
---|
| 82 | #P #HP_dec #k elim k -k |
---|
| 83 | [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O |
---|
| 84 | | #k #Hind cases Hind |
---|
| 85 | [ #Hk cases (HP_dec k) |
---|
| 86 | [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn) |
---|
| 87 | [ #H @(Hk … (le_S_S_to_le … H)) |
---|
| 88 | | #H >(injective_S … H) @HPk |
---|
| 89 | ] |
---|
| 90 | | #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k))) | @HPk ] |
---|
| 91 | ] |
---|
| 92 | | #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ] |
---|
| 93 | ] |
---|
| 94 | ] |
---|
| 95 | qed. |
---|
| 96 | |
---|
| 97 | lemma dec_bounded_exists: |
---|
| 98 | ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n). |
---|
| 99 | #P #HP_dec #k elim k -k |
---|
| 100 | [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O |
---|
| 101 | | #k #Hind cases Hind |
---|
| 102 | [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn) | @(proj2 … Hn) ] |
---|
| 103 | | #Hk cases (HP_dec k) |
---|
| 104 | [ #HPk %1 @(ex_intro … k) @conj [ @le_n | @HPk ] |
---|
| 105 | | #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn)) |
---|
| 106 | [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj |
---|
| 107 | [ @(le_S_S_to_le … H) | @(proj2 … Hn) ] | @Hk ] |
---|
| 108 | | #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn) | @HPk ] |
---|
| 109 | ] |
---|
| 110 | ] |
---|
| 111 | ] |
---|
| 112 | ] |
---|
| 113 | qed. |
---|
| 114 | |
---|
| 115 | lemma not_exists_forall: |
---|
| 116 | ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x. |
---|
| 117 | #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) |
---|
| 118 | @conj [ @Hx | @Habs ] |
---|
| 119 | qed. |
---|
| 120 | |
---|
| 121 | lemma not_forall_exists: |
---|
| 122 | ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x. |
---|
| 123 | #k #P #Hdec elim k |
---|
| 124 | [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O |
---|
| 125 | | -k #k #Hind #Hfa cases (Hdec k) |
---|
| 126 | [ #HP elim (Hind ?) |
---|
| 127 | [ -Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx) | @(proj2 ?? Hx) ] |
---|
| 128 | | @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx) |
---|
| 129 | [ #H2 @H @(le_S_S_to_le … H2) |
---|
| 130 | | #H2 >(injective_S … H2) @HP |
---|
| 131 | ] |
---|
| 132 | ] |
---|
| 133 | | #HP @(ex_intro … k) @conj [ @le_n | @HP ] |
---|
| 134 | ] |
---|
| 135 | ] |
---|
| 136 | qed. |
---|