source: src/utilities/extralib.ma @ 2006

Last change on this file since 2006 was 2006, checked in by boender, 7 years ago
  • added alias for bitvector zero
  • changed extralib bounded forall/exists to use le instead of lt
File size: 6.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/lists/list.ma".
17include "basics/logic.ma".
18include "ASM/Util.ma".
19
20lemma eq_rect_Type0_r:
21 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
22 #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption.
23qed.
24
25lemma eq_rect_r2:
26 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
27 #A #a #x #p cases p; #P #H assumption.
28qed.
29
30lemma eq_rect_Type2_r:
31 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
32 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption.
33qed.
34
35lemma eq_rect_CProp0_r:
36 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
37 #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption.
38qed.
39
40lemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.
41#A #x #y *;#H @nmk #H' /2/;
42qed.
43
44(* Paolo: already in library, generates ambiguity
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! *)
56(* Paolo: there is eqb_elim which does something very similar *)
57lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
58#n elim n;
59[ #m cases m; //;
60| #n' #IH #m cases m; [ /2/; | #m' whd in match (eqb (S n') (S m')) in ⊢ %;
61  lapply (IH m'); cases (eqb n' m'); /2/; ]
62] qed.
63
64(* datatypes/list.ma *)
65
66theorem nil_append_nil_both:
67  ∀A:Type[0]. ∀l1,l2:list A.
68    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
69#A #l1 #l2 cases l1
70[ cases l2
71  [ /2/
72  | normalize #h #t #H destruct
73  ]
74| cases l2
75  [ normalize #h #t #H destruct
76  | normalize #h1 #t1 #h2 #h3 #H destruct
77  ]
78] qed.
79
80(* some useful stuff for quantifiers *)
81
82lemma dec_bounded_forall:
83  ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n ≤ k → P n) + ¬(∀n.n ≤ k → P n).
84 #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   ]
89 | #k #Hind cases Hind
90   [ #Hk cases (HP_dec (S k))
91     [ #HPk %1 #n #Hn elim (le_to_or_lt_eq … Hn)
92       [ #H @(Hk … (le_S_S_to_le … H))
93       | #H >H @HPk
94       ]
95     | #HPk %2 @nmk #Habs @(absurd (P (S k))) [ @(Habs … (le_n (S k))) | @HPk ]
96     ]
97   | #Hk %2 @nmk #Habs @(absurd (∀n.n≤k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ]
98   ]
99 ]
100qed.
101
102lemma dec_bounded_exists:
103  ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n ≤ k ∧ P n) + ¬(∃n.n ≤ k ∧ P n).
104 #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   ]
110 | #k #Hind cases Hind
111   [ #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 ]
114     | #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
116         [ @(le_S_S_to_le … H) | @(proj2 … Hn) ] | @Hk ]
117       | #H @(absurd (P (S k))) [ <H @(proj2 … Hn) | @HPk ]
118       ] 
119     ]
120   ]
121 ]
122qed.
123
124(* Replace decision functions by result. *)
125
126lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
127#P #f #p #Q #H cases f;
128[ @H
129| #np cut False [ @(absurd ? p np) | * ]
130] qed.
131
132lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
133#P #f #p #Q #H cases f;
134[ #np cut False [ @(absurd ? np p) | * ]
135| @H
136] qed.
137
138
139lemma not_exists_forall:
140  ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x ≤ k ∧ P x) → ∀x.x ≤ k → ¬P x.
141 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x)
142 @conj [ @Hx | @Habs ]
143qed.
144
145lemma not_forall_exists:
146  ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x ≤ k → P x) → ∃x.x ≤ k ∧ ¬P x.
147 #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))
153   [ #HP elim (Hind ?)
154     [ -Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx) | @(proj2 ?? Hx) ]
155     | @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx)
156       [ #H2 @H @(le_S_S_to_le … H2)
157       | #H2 >H2 @HP
158       ]
159     ]
160   | #HP @(ex_intro … (S k)) @conj [ @le_n | @HP ]
161   ]
162 ]
163qed.
164
165lemma associative_orb : associative ? orb.
166*** // qed.
167
168lemma commutative_orb : commutative ? orb.
169** // qed.
170
171lemma associative_andb : associative ? andb.
172*** // qed.
173
174lemma commutative_andb : commutative ? andb.
175** // qed.
176
177
178lemma notb_false : ∀b.(¬b) = false → b = true.
179* [#_ % | normalize #EQ destruct]
180qed.
181
182lemma notb_true : ∀b.(¬b) = true → b = false.
183* [normalize #EQ destruct | #_ %]
184qed.
185
186
187
188notation > "Σ 〈 ident x : tyx, ident y : tyy 〉 . P" with precedence 20 for
189  @{'sigma (λ${fresh p}.
190    match ${fresh p} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P])}.
191notation > "Σ 〈 ident x, ident y 〉 . P" with precedence 20 for
192  @{'sigma (λ${fresh p}.
193    match ${fresh p} with [mk_Prod ${ident x} ${ident y} ⇒ $P])}.
194notation > "Σ 〈 ident x : tyx, ident y : tyy, ident z : tyz 〉 . P" with precedence 20 for
195  @{'sigma (λ${fresh p1}.
196    match ${fresh p1} with [mk_Prod ${fresh p2} (${ident z} : $tyz) ⇒
197      match ${fresh p2} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P]])}.
198notation > "Σ 〈 ident x , ident y , ident z 〉 . P" with precedence 20 for
199  @{'sigma (λ${fresh p1}.
200    match ${fresh p1} with [mk_Prod ${fresh p2} ${ident z} ⇒
201      match ${fresh p2} with [mk_Prod ${ident x} ${ident y} ⇒ $P]])}.
202
Note: See TracBrowser for help on using the repository browser.