Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (8 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2024 r2032  
    6262  try @le_n
    6363  <minus_n_n @[[]]
    64 qed.
    65 
    66 lemma super_rewrite2:
    67   ∀A:Type[0].
    68   ∀n, m: nat.
    69   ∀v1: Vector A n.
    70   ∀v2: Vector A m.
    71   ∀P: ∀m. Vector A m → Prop.
    72     n = m → v1 ≃ v2 → P n v1 → P m v2.
    73   #A #n #m #v1 #v2 #P #eq #jmeq
    74   destruct #assm assumption
    75 qed.
    76 
    77 lemma vector_cons_append:
    78   ∀A: Type[0].
    79   ∀n: nat.
    80   ∀e: A.
    81   ∀v: Vector A n.
    82     e ::: v = [[ e ]] @@ v.
    83   #A #n #e #v
    84   cases v try %
    85   #n' #hd #tl %
    86 qed.
    87 
    88 lemma vector_cons_append2:
    89   ∀A: Type[0].
    90   ∀n, m: nat.
    91   ∀v: Vector A n.
    92   ∀q: Vector A m.
    93   ∀hd: A.
    94     hd:::(v@@q) = (hd:::v)@@q.
    95   #A #n #m #v #q
    96   elim v try (#hd %)
    97   #n' #hd' #tl' #ih #hd'
    98   <ih %
    99 qed.
    100 
    101 lemma jmeq_cons_vector_monotone:
    102   ∀A: Type[0].
    103   ∀m, n: nat.
    104   ∀v: Vector A m.
    105   ∀q: Vector A n.
    106   ∀prf: m = n.
    107   ∀hd: A.
    108     v ≃ q → hd:::v ≃ hd:::q.
    109   #A #m #n #v #q #prf #hd #E
    110   @(super_rewrite2 A … E)
    111   try assumption %
    112 qed.
    113 
    114 lemma vector_associative_append:
    115   ∀A: Type[0].
    116   ∀n, m, o:  nat.
    117   ∀v: Vector A n.
    118   ∀q: Vector A m.
    119   ∀r: Vector A o.
    120     (v @@ q) @@ r ≃ v @@ (q @@ r).
    121   #A #n #m #o #v #q #r
    122   elim v try %
    123   #n' #hd #tl #ih
    124   <(vector_cons_append2 A … hd)
    125   @jmeq_cons_vector_monotone
    126   try assumption
    127   @associative_plus
    12864qed.
    12965
     
    186122    >vector_cons_append
    187123    change with (bool_to_Prop (subvector_with ??????))
    188     @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
     124    @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
    189125    try @associative_plus
    190126    @inductive_hypothesis
     
    214150  <(vector_cons_empty … ([[h]] @@ v))
    215151  @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]])
    216 qed.
    217 
    218 lemma eq_a_reflexive:
    219   ∀a. eq_a a a = true.
    220   #a cases a %
    221152qed.
    222153
     
    1056987     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
    1057988
    1058 lemma split_zero:
     989lemma vsplit_zero:
    1059990  ∀A,m.
    1060991  ∀v: Vector A m.
    1061     〈[[]], v〉 = split A 0 m v.
     992    〈[[]], v〉 = vsplit A 0 m v.
    1062993  #A #m #v
    1063994  cases v try %
     
    11511082qed.
    11521083
    1153 lemma split_succ:
     1084lemma vsplit_succ:
    11541085  ∀A: Type[0].
    11551086  ∀m, n: nat.
     
    11581089  ∀v: Vector A (m + n).
    11591090  ∀hd: A.
    1160     v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)).
     1091    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
    11611092  #A #m
    11621093  elim m
     
    11701101    whd in ⊢ (???%);
    11711102    >tail_head
    1172     <(? : split A (S m') n (l@@r) = split' A (S m') n (l@@r))
     1103    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
    11731104    try (<hyp <head_head' %)
    11741105    elim l normalize //
     
    11761107qed.
    11771108
    1178 lemma split_prod:
     1109lemma vsplit_prod:
    11791110  ∀A: Type[0].
    11801111  ∀m, n: nat.
     
    11821113  ∀v: Vector A m.
    11831114  ∀q: Vector A n.
    1184     p = v@@q → 〈v, q〉 = split A m n p.
     1115    p = v@@q → 〈v, q〉 = vsplit A m n p.
    11851116  #A #m elim m
    11861117  [1:
     
    11881119    >hyp <(vector_append_zero A n q v)
    11891120    >(prod_vector_zero_eq_left A …)
    1190     @split_zero
     1121    @vsplit_zero
    11911122  |2:
    11921123    #r #ih #n #p #v #q #hyp
     
    11941125    cases (Vector_Sn A r v) #hd #exists
    11951126    cases exists #tl #jmeq
    1196     >jmeq @split_succ try %
     1127    >jmeq @vsplit_succ try %
    11971128    @ih %
    11981129  ]
     
    12001131
    12011132(*
    1202 lemma split_prod_exists:
     1133lemma vsplit_prod_exists:
    12031134  ∀A, m, n.
    12041135  ∀p: Vector A (m + n).
    12051136  ∃v: Vector A m.
    12061137  ∃q: Vector A n.
    1207     〈v, q〉 = split A m n p.
     1138    〈v, q〉 = vsplit A m n p.
    12081139  #A #m #n #p
    12091140  elim m
     
    12171148*)
    12181149
    1219 definition split_elim:
     1150definition vsplit_elim:
    12201151  ∀A: Type[0].
    12211152  ∀l, m: nat.
     
    12241155    (∀vl: Vector A l.
    12251156     ∀vm: Vector A m.
    1226       v = vl@@vm → P 〈vl,vm〉) → P (split A l m v) ≝
     1157      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
    12271158  λa: Type[0].
    12281159  λl, m: nat.
     
    14131344 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
    14141345 normalize in ⊢ (???% → ?);
    1415  [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
     1346 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
    14161347  normalize in ⊢ (???% → ?);]
    14171348 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
     
    18861817  λs: PreStatus M.
    18871818  λv: Byte.
    1888     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
     1819    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
    18891820    let bit_zero ≝ get_index_v… nu O ? in
    18901821    let bit_1 ≝ get_index_v… nu 1 ? in
     
    19221853      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    19231854      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    1924       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     1855      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
    19251856      let s ≝ write_at_stack_pointer' ? s pc_bl in
    19261857      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     
    19501881  [ #pre cases pre
    19511882     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    1952        cases (split ????) #z1 #z2 %
     1883       cases (vsplit ????) #z1 #z2 %
    19531884     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    1954        cases (split ????) #z1 #z2 %
     1885       cases (vsplit ????) #z1 #z2 %
    19551886     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    1956        cases (split ????) #z1 #z2 %
     1887       cases (vsplit ????) #z1 #z2 %
    19571888     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
    19581889       [ #x1 whd in ⊢ (??? (??%))
     
    19631894  | #label %
    19641895  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
    1965     cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
    1966     whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
     1896    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
     1897    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
    19671898    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
    19681899    (* CSC: ??? *)
     
    21732104qed.
    21742105
    2175 axiom split_append:
     2106axiom vsplit_append:
    21762107  ∀A: Type[0].
    21772108  ∀m, n: nat.
    21782109  ∀v, v': Vector A m.
    21792110  ∀q, q': Vector A n.
    2180     let 〈v', q'〉 ≝ split A m n (v@@q) in
     2111    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
    21812112      v = v' ∧ q = q'.
    21822113
    2183 lemma split_vector_singleton:
     2114lemma vsplit_vector_singleton:
    21842115  ∀A: Type[0].
    21852116  ∀n: nat.
     
    22152146  #m #s #arg #b #hyp
    22162147  whd in ⊢ (??%%)
    2217   @split_elim''
     2148  @vsplit_elim''
    22182149  #nu' #nl' #arg_nu_nl_eq
    22192150  normalize nodelta
     
    22242155  [2:
    22252156    normalize nodelta
    2226     @split_elim''
     2157    @vsplit_elim''
    22272158    #bit_one' #three_bits' #bit_one_three_bit_eq
    22282159    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
     
    22432174        |1: -carr_hyp';
    22442175            >arg_nu_nl_eq
    2245             <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
     2176            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
    22462177            [1: >get_index_v_eq in ⊢ (??%? → ?)
    22472178            |2: @le_S @le_S @le_S @le_n
     
    22542185    |3: >get_index_v_eq in ⊢ (??%?)
    22552186        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
    2256         >(split_vector_singleton … bit_one_three_bit_eq)
     2187        >(vsplit_vector_singleton … bit_one_three_bit_eq)
    22572188        <arg_nu_nl_eq
    22582189        whd in hyp:(??%?)
Note: See TracChangeset for help on using the changeset viewer.