Changeset 2277


Ignore:
Timestamp:
Jul 30, 2012, 4:54:33 PM (7 years ago)
Author:
tranquil
Message:
  • replaced incorrect use of subvector_with
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues_paolo.ma

    r2275 r2277  
    66include "ASM/I8051.ma".
    77include "ASM/BitVectorTrie.ma".
     8include "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   Leibniz-equal *)
     13let rec vprefix A n m (test : A → A → bool) (v1 : Vector A n) (v2 : Vector A m) on v1 : bool ≝
     14match 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
     23let rec vsuffix A n m test (v1 : Vector A n) (v2 : Vector A m) on v2 : bool ≝
     24If 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  ] ?
     29else (if eqb n m then
     30  vprefix A n m test v1 v2
     31else
     32  false).
     33@hide_prf
     34lapply prf cases m [*] #m' #_ % qed.
     35
     36include alias "arithmetics/nat.ma".
     37
     38lemma 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'
     43whd in ⊢ (?%→?);
     44elim (test ??) [2: *]
     45whd in ⊢ (?%→?);
     46#H @le_S_S @(IH … H)
     47qed.
     48
     49lemma 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 ⊢ (?%→?);
     57elim (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]
     69qed.
     70
     71lemma vector_append_empty : ∀A,n.∀v : Vector A n.v @@ [[ ]] ≃ v.
     72#A #n #v elim v -n [%]
     73#n #hd #tl change with (?→?:::(?@@?)≃?)
     74lapply (tl@@[[ ]])
     75<plus_n_O #v #EQ >EQ %
     76qed.
     77
     78lemma 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]
     87qed.
     88
     89lemma 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]
     99qed.
     100
     101lemma 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
     105lemma 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]
     121qed.
     122 
     123lemma 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
     128elim 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]
     155qed.
     156
     157lemma 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]
     181qed.
    8182
    9183record part (*r: region*): Type[0] ≝
     
    45219        eq_block … b1 b2 ∧ eqb p1 p2 ∧
    46220          (* equivalent to equality if p1 = p2 *)
    47           subvector_with … (eq_bv 8) o1 o2
     221          vprefix … (eq_bv 8) o1 o2
    48222      | _ ⇒ false
    49223      ]
     
    104278        if eq_block b b' ∧
    105279           eqb part part' ∧
    106            subvector_with ??? eq_b acc acc' then
     280           vsuffix … eq_b acc acc' then
    107281           pointer_of_bevals_aux b (S part') acc' tl
    108282         else
     
    191365qed.
    192366
    193 
    194367lemma pointer_of_bevals_bevals_of_pointer:
    195368 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
     
    206379>eq_block_b_b >eqb_n_n
    207380>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 % ]
    209383normalize nodelta %
    210384qed.
     
    297471        eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧
    298472          (* equivalent to equality if p1 = p2 *)
    299           subvector_with … (eq_bv 8) o1 o2 ∧
    300           subvector_with … (eq_bv 8) by1 by2
     473          vprefix … (eq_bv 8) o1 o2 ∧
     474          vprefix … (eq_bv 8) by1 by2
    301475      | _ ⇒ false
    302476      ]
     
    351525      match carry with
    352526      [ 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 then
     527        if eq_b is_add is_add' ∧ eq_block b b' ∧ vsuffix … (eq_bv 8) o' o then
    354528          If eqb k p' then with prf do
    355529            let by' ≝ by' ⌈Vector ?? ↦ Vector Byte (S k)⌉ in
     
    429603      | Xor ⇒
    430604        if eq_block bl1 bl2 ∧ eqb p1 p2 then
    431           if subvector_with … (eq_bv 8) o1 o2 (* equivalent to equality *) then
     605          if vprefix … (eq_bv 8) o1 o2 (* equivalent to equality *) then
    432606            return 〈BVByte (bv_zero …), carry〉
    433607          else
Note: See TracChangeset for help on using the changeset viewer.