source: src/utilities/extralib.ma @ 1593

Last change on this file since 1593 was 1593, checked in by boender, 8 years ago
  • cleaned up Assembly, moved some definitions elsewhere
File size: 4.7 KB
Line 
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
15include "basics/types.ma".
16include "basics/list.ma".
17include "basics/logic.ma".
18include "utilities/pair.ma".
19include "ASM/Util.ma".
20
21lemma eq_rect_Type0_r:
22 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
23 #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption.
24qed.
25
26lemma eq_rect_r2:
27 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
28 #A #a #x #p cases p; #P #H assumption.
29qed.
30
31lemma eq_rect_Type2_r:
32 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
33 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption.
34qed.
35
36lemma eq_rect_CProp0_r:
37 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
38 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption.
39qed.
40
41lemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.
42#A #x #y *;#H @nmk #H' /2/;
43qed.
44
45interpretation "logical iff" 'iff x y = (iff x y).
46
47(* bool *)
48
49definition xorb : bool → bool → bool ≝
50  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
51 
52 
53 
54
55(* should be proved in nat.ma, but it's not! *)
56lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
57#n elim n;
58[ #m cases m; //;
59| #n' #IH #m cases m; [ /2/; | #m' whd in match (eqb (S n') (S m')) in ⊢ %;
60  lapply (IH m'); cases (eqb n' m'); /2/; ]
61] qed.
62
63(* datatypes/list.ma *)
64
65theorem nil_append_nil_both:
66  ∀A:Type[0]. ∀l1,l2:list A.
67    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
68#A #l1 #l2 cases l1
69[ cases l2
70  [ /2/
71  | normalize #h #t #H destruct
72  ]
73| cases l2
74  [ normalize #h #t #H destruct
75  | normalize #h1 #t1 #h2 #h3 #H destruct
76  ]
77] 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 TracBrowser for help on using the repository browser.