source: src/utilities/extralib.ma

Last change on this file was 2796, checked in by tranquil, 7 years ago
  • added global notation for existence in Type[1] (\exists[1] x.P)
  • in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
  • in joint_semantics, moved out and around some parameters in primitive semantics functions
  • fixed all back end semantics
  • added skeleton files for single passes correctness proofs
File size: 7.9 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 
49lemma xorb_neg : ∀a,b. notb (xorb a b) = xorb a (notb b). * * @refl qed.
50lemma xorb_false : ∀a. xorb a false = a. * @refl qed.
51lemma xorb_true : ∀a. xorb a true = (¬a). * @refl qed.
52lemma xorb_comm : ∀a,b. xorb a b = xorb b a. * * @refl qed.
53lemma xorb_assoc : ∀a,b,c. xorb a (xorb b c) = xorb (xorb a b) c. * * * @refl qed.
54lemma xorb_lneg : ∀a,b. xorb (¬a) b = (¬xorb a b). * * @refl qed.
55lemma xorb_rneg : ∀a,b. xorb a (¬b) = (¬xorb a b). * * @refl qed.
56lemma xorb_inj : ∀a,b,c. xorb a b = xorb a c ↔ b = c. * * * @conj try // normalize try // qed. 
57 
58 
59 
60(* should be proved in nat.ma, but it's not! *)
61(* Paolo: there is eqb_elim which does something very similar *)
62lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
63#n elim n;
64[ #m cases m; //;
65| #n' #IH #m cases m; [ /2/; | #m' whd in match (eqb (S n') (S m')) in ⊢ %;
66  lapply (IH m'); cases (eqb n' m'); /2/; ]
67] qed.
68
69(* datatypes/list.ma *)
70
71theorem nil_append_nil_both:
72  ∀A:Type[0]. ∀l1,l2:list A.
73    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
74#A #l1 #l2 cases l1
75[ cases l2
76  [ /2/
77  | normalize #h #t #H destruct
78  ]
79| cases l2
80  [ normalize #h #t #H destruct
81  | normalize #h1 #t1 #h2 #h3 #H destruct
82  ]
83] qed.
84
85(* some useful stuff for quantifiers *)
86
87lemma dec_bounded_forall:
88  ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n).
89 #P #HP_dec #k elim k -k
90 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O
91 | #k #Hind cases Hind
92   [ #Hk cases (HP_dec k)
93     [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn)
94       [ #H @(Hk … (le_S_S_to_le … H))
95       | #H >(injective_S … H) @HPk
96       ]
97     | #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k))) | @HPk ]
98     ]
99   | #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ]
100   ]
101 ]
102qed.
103
104lemma dec_bounded_exists:
105  ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n).
106 #P #HP_dec #k elim k -k
107 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O
108 | #k #Hind cases Hind
109   [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn) | @(proj2 … Hn) ]
110   | #Hk cases (HP_dec k)
111     [ #HPk %1 @(ex_intro … k) @conj [ @le_n | @HPk ]
112     | #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn))
113       [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj
114         [ @(le_S_S_to_le … H) | @(proj2 … Hn) ] | @Hk ]
115       | #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn) | @HPk ]
116       ] 
117     ]
118   ]
119 ]
120qed.
121
122(* Replace decision functions by result. *)
123
124lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
125#P #f #p #Q #H cases f;
126[ @H
127| #np cut False [ @(absurd ? p np) | * ]
128] qed.
129
130lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
131#P #f #p #Q #H cases f;
132[ #np cut False [ @(absurd ? np p) | * ]
133| @H
134] qed.
135
136
137lemma not_exists_forall:
138  ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x.
139 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x)
140 @conj [ @Hx | @Habs ]
141qed.
142
143lemma not_forall_exists:
144  ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x.
145 #k #P #Hdec elim k
146 [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O
147 | -k #k #Hind #Hfa cases (Hdec k)
148   [ #HP elim (Hind ?)
149     [ -Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx) | @(proj2 ?? Hx) ]
150     | @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx)
151       [ #H2 @H @(le_S_S_to_le … H2)
152       | #H2 >(injective_S … H2) @HP
153       ]
154     ]
155   | #HP @(ex_intro … k) @conj [ @le_n | @HP ]
156   ]
157 ]
158qed.
159
160lemma associative_orb : associative ? orb.
161*** // qed.
162
163lemma commutative_orb : commutative ? orb.
164** // qed.
165
166lemma associative_andb : associative ? andb.
167*** // qed.
168
169lemma commutative_andb : commutative ? andb.
170** // qed.
171
172
173lemma notb_false : ∀b.(¬b) = false → b = true.
174* [#_ % | normalize #EQ destruct]
175qed.
176
177lemma notb_true : ∀b.(¬b) = true → b = false.
178* [normalize #EQ destruct | #_ %]
179qed.
180
181
182
183notation > "Σ 〈 ident x : tyx, ident y : tyy 〉 . P" with precedence 20 for
184  @{'sigma (λ${fresh p}.
185    match ${fresh p} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P])}.
186notation > "Σ 〈 ident x, ident y 〉 . P" with precedence 20 for
187  @{'sigma (λ${fresh p}.
188    match ${fresh p} with [mk_Prod ${ident x} ${ident y} ⇒ $P])}.
189notation > "Σ 〈 ident x : tyx, ident y : tyy, ident z : tyz 〉 . P" with precedence 20 for
190  @{'sigma (λ${fresh p1}.
191    match ${fresh p1} with [mk_Prod ${fresh p2} (${ident z} : $tyz) ⇒
192      match ${fresh p2} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P]])}.
193notation > "Σ 〈 ident x , ident y , ident z 〉 . P" with precedence 20 for
194  @{'sigma (λ${fresh p1}.
195    match ${fresh p1} with [mk_Prod ${fresh p2} ${ident z} ⇒
196      match ${fresh p2} with [mk_Prod ${ident x} ${ident y} ⇒ $P]])}.
197
198
199notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10
200  for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }.
201
202notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)"
203 with precedence 10
204for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒
205        λ${ident E}.$s ] (refl ? $t) }.
206
207inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
208    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
209
210interpretation "exists in Type[1]" 'exists_Type1 x = (ex_Type1 ? x).
211
212notation < "hvbox(∃\sub 1 ident i : ty break . p)"
213 right associative with precedence 20
214for @{'exists_Type1 (\lambda ${ident i} : $ty. $p) }.
215
216notation > "\exists[1] list1 ident x sep , opt (: T). term 19 Px"
217  with precedence 20
218  for ${ default
219          @{ ${ fold right @{$Px} rec acc @{'exists_Type1 (λ${ident x}:$T.$acc)} } }
220          @{ ${ fold right @{$Px} rec acc @{'exists_Type1 (λ${ident x}.$acc)} } }
221       }.
Note: See TracBrowser for help on using the repository browser.