 Timestamp:
 Jul 30, 2012, 4:54:33 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/ByteValues_paolo.ma
r2275 r2277 6 6 include "ASM/I8051.ma". 7 7 include "ASM/BitVectorTrie.ma". 8 include "utilities/hide.ma". 9 10 (* move *) 11 (* n.b.: if n = m this is equivalent to equality, without n and m needing to be 12 Leibnizequal *) 13 let rec vprefix A n m (test : A → A → bool) (v1 : Vector A n) (v2 : Vector A m) on v1 : bool ≝ 14 match v1 with 15 [ VEmpty ⇒ true 16  VCons n' hd1 tl1 ⇒ 17 match v2 with 18 [ VEmpty ⇒ false 19  VCons m' hd2 tl2 ⇒ test hd1 hd2 ∧ vprefix … test tl1 tl2 20 ] 21 ]. 22 23 let rec vsuffix A n m test (v1 : Vector A n) (v2 : Vector A m) on v2 : bool ≝ 24 If leb (S n) m then with prf do 25 match v2 return λm.λv2:Vector A m.not_zero m → bool with 26 [ VEmpty ⇒ Ⓧ 27  VCons m' hd2 tl2 ⇒ λ_.vsuffix ?? m' test v1 tl2 28 ] ? 29 else (if eqb n m then 30 vprefix A n m test v1 v2 31 else 32 false). 33 @hide_prf 34 lapply prf cases m [*] #m' #_ % qed. 35 36 include alias "arithmetics/nat.ma". 37 38 lemma prefix_to_le : ∀A,n,m,test,v1,v2. 39 vprefix A n m test v1 v2 → n ≤ m. 40 #A #n #m #test #v1 lapply m m elim v1 n [//] 41 #n #hd #tl #IH #m * m [*] 42 #m #hd' #tl' 43 whd in ⊢ (?%→?); 44 elim (test ??) [2: *] 45 whd in ⊢ (?%→?); 46 #H @le_S_S @(IH … H) 47 qed. 48 49 lemma vprefix_ok : ∀A,n,m,test,v1,v2. 50 vprefix A n m test v1 v2 → 51 ∃pre.∃post : Vector A (m  n).v2 ≃ pre @@ post ∧ 52 bool_to_Prop (eq_v … test v1 pre). 53 #A #n #m #test #v1 lapply m m elim v1 n 54 [ #m #v2 * <minus_n_O %{[[ ]]} %{v2} % % ] 55 #n #hd1 #tl1 #IH #m * m [*] 56 #m #hd2 #tl2 whd in ⊢ (?%→?); 57 elim (true_or_false_Prop (test hd1 hd2)) #H >H normalize nodelta [2: *] 58 #G elim (IH … G) #pre * #post * #EQ #EQ' 59 %{(hd2:::pre)} %{post} % 60 [ change with (?≃hd2 ::: (? @@ ?)) lapply EQ lapply (pre @@ post) 61 <(minus_to_plus m … (refl …)) 62 [ #V #EQ'' >EQ'' % 63  @(prefix_to_le … G) 64 ] 65  whd in ⊢ (?%); 66 whd in match (head' ???); >H 67 @EQ' 68 ] 69 qed. 70 71 lemma vector_append_empty : ∀A,n.∀v : Vector A n.v @@ [[ ]] ≃ v. 72 #A #n #v elim v n [%] 73 #n #hd #tl change with (?→?:::(?@@?)≃?) 74 lapply (tl@@[[ ]]) 75 <plus_n_O #v #EQ >EQ % 76 qed. 77 78 lemma vprefix_to_eq : ∀A,n,test,v1,v2. 79 vprefix A n n test v1 v2 = eq_v … test v1 v2. 80 #A #n #test #v1 elim v1 n 81 [ #v2 >(Vector_O … v2) % 82  #n #hd1 #tl1 #IH 83 #v2 elim (Vector_Sn … v2) #hd2 * #tl2 #EQ destruct(EQ) 84 normalize elim (test ??) [2: %] 85 normalize @IH 86 ] 87 qed. 88 89 lemma vprefix_true : ∀A,n,m,test.∀v1,pre : Vector A n.∀post : Vector A m. 90 eq_v … test v1 pre → bool_to_Prop (vprefix … test v1 (pre @@ post)). 91 #A #n #m #test #v1 lapply m m elim v1 n 92 [ #m #pre #post #_ % 93  #n #hd #tl #IH #m #pre elim (Vector_Sn … pre) #hd' * #tl' #EQpre >EQpre 94 #post 95 whd in ⊢ (?%→?%); whd in match (head' ???); 96 elim (test hd hd') [2: *] normalize nodelta whd in match (tail ???); 97 @IH 98 ] 99 qed. 100 101 lemma If_elim : ∀A.∀P : A → Prop.∀b : bool.∀f : b → A.∀g : Not (bool_to_Prop b) → A. 102 (∀prf.P (f prf)) → (∀prf.P (g prf)) → P (If b then with prf do f prf else with prf do g prf). 103 #A #P * #f #g #H1 #H2 normalize // qed. 104 105 lemma vsuffix_to_le : ∀A,n,m,test,v1,v2. 106 vsuffix A n m test v1 v2 → n ≤ m. 107 #A #n #m #test #v1 #v2 lapply v1 lapply n n elim v2 m 108 [ #n * n 109 [ * % 110  #n #hd #tl * 111 ] 112  #m #hd2 #tl2 #IH 113 #n #v1 change with (bool_to_Prop (If ? then with prf do ? else ?) → ?) 114 @If_elim normalize nodelta @leb_elim #H * 115 [ #_ @(transitive_le … H) %2 %1 116  #ABS elim (ABS I) 117  #_ @eqb_elim #G normalize nodelta [2: *] 118 destruct #_ % 119 ] 120 ] 121 qed. 122 123 lemma vsuffix_ok : ∀A,n,m,test,v1,v2. 124 vsuffix A n m test v1 v2 → 125 ∃pre : Vector A (m  n).∃post.v2 ≃ pre @@ post ∧ 126 bool_to_Prop (eq_v … test v1 post). 127 #A #n #m #test #v1 #v2 lapply v1 lapply n n 128 elim v2 m 129 [ #n #v1 130 whd in ⊢ (?%→?); 131 @eqb_elim #EQ1 [2: *] 132 normalize nodelta lapply v1 v1 >EQ1 #v1 133 >(Vector_O … v1) * %{[[ ]]} %{[[ ]]} % % 134  #m #hd2 #tl2 #IH #n #v1 135 change with (bool_to_Prop (If ? then with prf do ? else ?) → ?) 136 @If_elim normalize nodelta #H 137 [ #G elim (IH … G) #pre * #post * #EQ1 #EQ2 138 >minus_Sn_m 139 [ %{(hd2:::pre)} %{post} %{EQ2} 140 change with (?≃?:::(?@@?)) 141 lapply EQ1 lapply (pre@@post) 142 <plus_minus_m_m 143 [ #v #EQ >EQ %] 144 ] 145 @(vsuffix_to_le … G) 146  @eqb_elim #EQn [2: *] normalize nodelta 147 generalize in match (hd2:::tl2); 148 <EQn in ⊢ (%→%→??(λ_.??(λ_.?(?%%??)?))); 149 #v2' >vprefix_to_eq #G 150 <EQn in ⊢ (?%(λ_:%.??(λ_.?(???%%)?))); 151 <minus_n_n %{[[ ]]} %{v2'} %{G} 152 % 153 ] 154 ] 155 qed. 156 157 lemma vsuffix_true : ∀A,n,m,test.∀pre : Vector A n.∀v1,post : Vector A m. 158 eq_v … test v1 post → bool_to_Prop (vsuffix … test v1 (pre @@ post)). 159 #A #n #m #test #pre lapply m m elim pre n 160 [ #m #v1 #post lapply v1 v1 cases post m 161 [ #v1 >(Vector_O … v1) * % 162  #m #hd #tl #v1 #G 163 change with (bool_to_Prop (If ? then with prf do ? else ?)) 164 @If_elim normalize nodelta 165 [ @leb_elim #H * @⊥ @(absurd ? H ?) normalize // ] 166 #_ >eqb_n_n normalize nodelta 167 >vprefix_to_eq assumption 168 ] 169  #n #hd2 #tl2 #IH 170 #m #v1 #post #G 171 change with (bool_to_Prop (If ? then with prf do ? else ?)) 172 @If_elim normalize nodelta 173 [ #H @IH @G 174  @leb_elim [ #_ * #ABS elim (ABS I) ] 175 #H #_ @eqb_elim #K 176 [ @⊥ @(absurd ? K) @lt_to_not_eq // ] 177 normalize elim H H #H @H normalize 178 >plus_n_Sm_fast // 179 ] 180 ] 181 qed. 8 182 9 183 record part (*r: region*): Type[0] ≝ … … 45 219 eq_block … b1 b2 ∧ eqb p1 p2 ∧ 46 220 (* equivalent to equality if p1 = p2 *) 47 subvector_with… (eq_bv 8) o1 o2221 vprefix … (eq_bv 8) o1 o2 48 222  _ ⇒ false 49 223 ] … … 104 278 if eq_block b b' ∧ 105 279 eqb part part' ∧ 106 subvector_with ???eq_b acc acc' then280 vsuffix … eq_b acc acc' then 107 281 pointer_of_bevals_aux b (S part') acc' tl 108 282 else … … 191 365 qed. 192 366 193 194 367 lemma pointer_of_bevals_bevals_of_pointer: 195 368 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p. … … 206 379 >eq_block_b_b >eqb_n_n 207 380 >vflatten_rvsplit >vflatten_rvsplit 208 >(subvector_with_refl0 … post ? pre) [2: * %] 381 >vsuffix_true 382 [2: change with (bool_to_Prop (eq_bv ???)) >eq_bv_refl % ] 209 383 normalize nodelta % 210 384 qed. … … 297 471 eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧ 298 472 (* equivalent to equality if p1 = p2 *) 299 subvector_with… (eq_bv 8) o1 o2 ∧300 subvector_with… (eq_bv 8) by1 by2473 vprefix … (eq_bv 8) o1 o2 ∧ 474 vprefix … (eq_bv 8) by1 by2 301 475  _ ⇒ false 302 476 ] … … 351 525 match carry with 352 526 [ BBptrcarry is_add' b' p' o' by' ⇒ 353 if eq_b is_add is_add' ∧ eq_block b b' ∧ subvector_with… (eq_bv 8) o' o then527 if eq_b is_add is_add' ∧ eq_block b b' ∧ vsuffix … (eq_bv 8) o' o then 354 528 If eqb k p' then with prf do 355 529 let by' ≝ by' ⌈Vector ?? ↦ Vector Byte (S k)⌉ in … … 429 603  Xor ⇒ 430 604 if eq_block bl1 bl2 ∧ eqb p1 p2 then 431 if subvector_with… (eq_bv 8) o1 o2 (* equivalent to equality *) then605 if vprefix … (eq_bv 8) o1 o2 (* equivalent to equality *) then 432 606 return 〈BVByte (bv_zero …), carry〉 433 607 else
Note: See TracChangeset
for help on using the changeset viewer.