source: src/utilities/extralib.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 6.0 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
44interpretation "logical iff" 'iff x y = (iff x y).
45
46(* bool *)
47
48definition xorb : bool → bool → bool ≝
49  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
50 
51 
52 
53
54(* should be proved in nat.ma, but it's not! *)
55(* Paolo: there is eqb_elim which does something very similar *)
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.
138
139lemma associative_orb : associative ? orb.
140*** // qed.
141
142lemma commutative_orb : commutative ? orb.
143** // qed.
144
145lemma associative_andb : associative ? andb.
146*** // qed.
147
148lemma commutative_andb : commutative ? andb.
149** // qed.
150
151
152lemma notb_false : ∀b.(¬b) = false → b = true.
153* [#_ % | normalize #EQ destruct]
154qed.
155
156lemma notb_true : ∀b.(¬b) = true → b = false.
157* [normalize #EQ destruct | #_ %]
158qed.
159
160
161
162notation > "Σ 〈 ident x : tyx, ident y : tyy 〉 . P" with precedence 20 for
163  @{'sigma (λ${fresh p}.
164    match ${fresh p} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P])}.
165notation > "Σ 〈 ident x, ident y 〉 . P" with precedence 20 for
166  @{'sigma (λ${fresh p}.
167    match ${fresh p} with [mk_Prod ${ident x} ${ident y} ⇒ $P])}.
168notation > "Σ 〈 ident x : tyx, ident y : tyy, ident z : tyz 〉 . P" with precedence 20 for
169  @{'sigma (λ${fresh p1}.
170    match ${fresh p1} with [mk_Prod ${fresh p2} (${ident z} : $tyz) ⇒
171      match ${fresh p2} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P]])}.
172notation > "Σ 〈 ident x , ident y , ident z 〉 . P" with precedence 20 for
173  @{'sigma (λ${fresh p1}.
174    match ${fresh p1} with [mk_Prod ${fresh p2} ${ident z} ⇒
175      match ${fresh p2} with [mk_Prod ${ident x} ${ident y} ⇒ $P]])}.
176
Note: See TracBrowser for help on using the repository browser.