Ignore:
Timestamp:
May 11, 2012, 2:38:55 PM (8 years ago)
Author:
mulligan
Message:

Some holes filled in AssemblyProof?.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1668 r1936  
    99 
    1010let rec bitvector_elim_prop_internal
    11   (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝
     11  (n: nat) (P: BitVector n → Prop) (m: nat)
     12    on m:
     13      m ≤ n → BitVector (n - m) → Prop ≝
    1214  match m return λm. m ≤ n → BitVector (n - m) → Prop with
    1315  [ O    ⇒ λprf1. λprefix. P ?
    14   | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?)
     16  | S n' ⇒ λprf2. λprefix.
     17      bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …)
    1518  ].
    16   [ applyS prefix
    17   | letin res ≝ (bit ::: prefix)
    18     < (minus_S_S ? ?)
    19     > (minus_Sn_m ? ?)
    20   [ @ res
    21   | @ prf2
     19  [1:
     20    applyS prefix
     21  |2:
     22    letin res ≝ (bit ::: prefix)
     23    <minus_S_S
     24    >minus_Sn_m
     25    [1:
     26      @res
     27    |2:
     28      assumption
     29    ]
     30  |3:
     31    @le_S_to_le
     32    assumption
    2233  ]
    23   | /2/
    24   ].
    2534qed.
    2635
     
    2938  λP: BitVector n → Prop.
    3039    bitvector_elim_prop_internal n P n ? ?.
    31   [ @ (le_n ?)
    32   | < (minus_n_n ?)
    33     @ [[ ]]
     40  [ @(le_n ?)
     41  | <(minus_n_n ?)
     42    @[[ ]]
    3443  ]
    3544qed.
     
    4049  #b #c
    4150  cases b
    42   [ normalize //
    43   | normalize
     51  [1:
     52    normalize //
     53  |2:
     54    normalize
    4455    cases c
    45     [ normalize //
    46     | normalize //
     56    [1:
     57      normalize //
     58    |2:
     59      normalize //
    4760    ]
    4861  ]
     
    5467
    5568let rec bitvector_elim_internal
    56   (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
     69  (n: nat) (P: BitVector n → bool) (m: nat)
     70    on m:
     71      m ≤ n → BitVector (n - m) → bool ≝
    5772  match m return λm. m ≤ n → BitVector (n - m) → bool with
    5873  [ O    ⇒ λprf1. λprefix. P ?
    5974  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
    6075  ].
    61   [ applyS prefix
    62   | letin res ≝ (bit ::: prefix)
    63     < (minus_S_S ? ?)
    64     > (minus_Sn_m ? ?)
    65     [ @ res
    66     | @ prf2
    67     ]
    68   | /2/
     76  [1:
     77    applyS prefix
     78  |2:
     79    letin res ≝ (bit ::: prefix)
     80    <(minus_S_S ? ?)
     81    >(minus_Sn_m ? ?)
     82    [1:
     83      @res
     84    |2:
     85      @prf2
     86    ]
     87  |3:
     88    /2/
    6989  ].
    7090qed.
     
    7494  λP: BitVector n → bool.
    7595    bitvector_elim_internal n P n ? ?.
    76   [ @ (le_n ?)
    77   | < (minus_n_n ?)
    78     @ [[ ]]
     96  [ @(le_n ?)
     97  | <(minus_n_n ?)
     98    @[[ ]]
    7999  ]
    80100qed.
    81101
    82102lemma super_rewrite2:
    83  ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
     103  ∀A:Type[0].
     104  ∀n, m: nat.
     105  ∀v1: Vector A n.
     106  ∀v2: Vector A m.
    84107  ∀P: ∀m. Vector A m → Prop.
    85    n=m → v1 ≃ v2 → P n v1 → P m v2.
    86  #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
     108    n = m → v1 ≃ v2 → P n v1 → P m v2.
     109  #A #n #m #v1 #v2 #P #EQ
     110  <EQ in v2; #V #JMEQ
     111  >JMEQ //
    87112qed.
    88113
     
    93118  ∀v: Vector A n.
    94119    e ::: v = [[ e ]] @@ v.
    95   # A # N # E # V
    96   elim V
    97   [ normalize %
    98   | # NN # AA # VV # IH
     120  #A #n #e #v
     121  elim v
     122  [1:
     123    normalize %
     124  |2:
     125    #NN #AA #VV #IH
    99126    normalize
    100127    %
    101 qed.
     128  ]
     129qed.
    102130
    103131lemma vector_cons_append2:
     
    110138  #A #n #m #v #q
    111139  elim v
    112   [ #hd %
    113   | #n' #hd' #tl' #ih #hd' <ih %
     140  [1:
     141    #hd %
     142  |2:
     143    #n' #hd' #tl' #ih #hd'
     144    <ih %
    114145  ]
    115146qed.
     
    125156  #A #m #n #v #q #prf #hd #E
    126157  @(super_rewrite2 A … E)
    127   [ assumption | % ]
     158  try assumption %
    128159qed.
    129160
     
    134165  ∀q: Vector A m.
    135166  ∀r: Vector A o.
    136     ((v @@ q) @@ r)
    137     ≃
    138     (v @@ (q @@ r)).
     167    (v @@ q) @@ r ≃ v @@ (q @@ r).
    139168  #A #n #m #o #v #q #r
    140   elim v
    141   [ %
    142   | #n' #hd #tl #ih
    143     <(vector_cons_append2 A … hd)
    144     @jmeq_cons_vector_monotone
    145     //
    146   ]
     169  elim v try %
     170  #n' #hd #tl #ih
     171  <(vector_cons_append2 A … hd)
     172  @jmeq_cons_vector_monotone
     173  try assumption
     174  @associative_plus
    147175qed.
    148176
     
    156184  ∀r: Vector A o.
    157185    mem A eq ? (p@@(a:::r)) a = true.
    158   # A # M # O # EQ # REFLEX # P # A
    159   elim P
    160   [ normalize
    161     > (REFLEX A)
     186  #A #m #o #eq #reflex #p #a
     187  elim p
     188  [1:
    162189    normalize
    163     # H
    164     %
    165   | # NN # AA # PP # IH
     190    >reflex
     191    #H %
     192  |2:
     193    #m' #hd #tl #inductive_hypothesis
    166194    normalize
    167     cases (EQ A AA) //
    168      @ IH
     195    cases (eq ??) normalize nodelta
     196    [1:
     197      #_ %
     198    |2:
     199      @inductive_hypothesis
     200    ]
    169201  ]
    170202qed.
     
    179211  ∀r: Vector A o.
    180212    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
    181   # A # M # O # EQ # REFLEX # P # A
    182   elim P
    183   [ #R #H @H
    184   | #NN #AA # PP # IH #R #H
     213  #A #m #o #eq #reflex #p #a
     214  elim p
     215  [1:
     216    #r #assm assumption
     217  |2:
     218    #m' #hd #tl #inductive_hypothesis #r #assm
    185219    normalize
    186     cases (EQ A AA)
    187     [ normalize %
    188     | @ IH @ H
    189     ]
     220    cases (eq ??) try %
     221    @inductive_hypothesis assumption
    190222  ]
    191223qed.
     
    201233  ∀q: Vector A m.
    202234    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
    203   # A # O # N # EQ # REFLEX # H # V
    204   elim V
    205   [ normalize
    206     # M # V %
    207   | # NN # AA # VV # IH # MM # QQ
     235  #A #o #n #eq #reflex #h #v
     236  elim v
     237  [1:
     238    normalize #m #_ @I
     239  |2:
     240    #m' #hd #tl #inductive_hypothesis #m #q
    208241    change with (bool_to_Prop (andb ??))
    209     cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
    210     [
    211     | # HH > HH
    212       > (vector_cons_append ? ? AA VV)
     242    cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
     243    [1:
     244      @mem_monotonic_wrt_append try assumption
     245      @mem_monotonic_wrt_append try assumption
     246      normalize >reflex %
     247    |2:
     248      #assm >assm
     249      >vector_cons_append
    213250      change with (bool_to_Prop (subvector_with ??????))
    214       @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
    215         (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
    216         ?
    217         (vector_associative_append A ? ? ? QQ [[AA]] VV))
    218       [ >associative_plus //
    219       | @IH ]
    220     ]
    221     @(mem_monotonic_wrt_append)
    222     [ @ REFLEX
    223     | @(mem_monotonic_wrt_append)
    224       [ @ REFLEX
    225       | normalize
    226         > REFLEX
    227         normalize
    228         %
    229       ]
    230     ]
     251      @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
     252      try @associative_plus
     253      @inductive_hypothesis
     254    ]
     255  ]
    231256qed.
    232257
     
    236261  ∀v: Vector A n.
    237262    [[ ]] @@ v = v.
    238   # A # N # V
    239   elim V
    240   [ normalize %
    241   | # NN # HH # VV #H %
    242   ]
     263  #A #n #v
     264  cases v try %
     265  #n' #hd #tl %
    243266qed.
    244267
     
    251274  ∀v: Vector A o.
    252275    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
    253   # A # O # EQ # REFLEX # H # V
    254   > (vector_cons_append A ? H V)
    255   < (vector_cons_empty A ? ([[H]] @@ V))
    256   @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]])
     276  #A #o #eq #reflex #h #v
     277  >(vector_cons_append … h v)
     278  <(vector_cons_empty … ([[h]] @@ v))
     279  @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]])
    257280qed.
    258281
    259282lemma eq_a_reflexive:
    260283  ∀a. eq_a a a = true.
    261   # A
    262   cases A
    263   %
     284  #a cases a %
    264285qed.
    265286
     
    270291  ∀to_search: addressing_mode.
    271292    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
    272   # M # N # P # Q # TO_SEARCH
    273   # H
    274   elim Q
    275   [ normalize
    276     @ H
    277   | # NN # PP # QQ # IH
    278     normalize
    279     cases (is_a PP TO_SEARCH)
    280     [ normalize
    281       %
    282     | normalize
    283       normalize in IH;
    284       @ IH
    285     ]
    286   ]
     293  #m #n #p #q #to_search #assm
     294  elim q try assumption
     295  #n' #hd #tl #inductive_hypothesis
     296  normalize
     297  cases (is_a ??) try @I
     298  >inductive_hypothesis @I
    287299qed.
    288300
     
    293305  ∀v: Vector addressing_mode_tag n.
    294306    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
    295   # TO_SEARCH # HD # N # V
    296   elim V
    297   [ # H
    298     normalize in H;
    299     cases H
    300   | # NN # HHD # VV # IH # HH
    301     > vector_cons_append
    302     > (vector_cons_append ? ? HHD VV)
    303     @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
    304     @ HH
     307  #to_search #hd #n #v
     308  elim v
     309  [1:
     310    #absurd
     311    normalize in absurd; cases absurd
     312  |2:
     313    #n' #hd' #tl #inductive_hypothesis #assm
     314    >vector_cons_append >(vector_cons_append … hd' tl)
     315    @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
     316    assumption
    305317  ]
    306318qed.
    307319 
    308320let rec list_addressing_mode_tags_elim
    309   (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
    310   match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
    311    (l → bool) → bool ] with
     321  (n: nat) (l: Vector addressing_mode_tag (S n))
     322    on l: (l → bool) → bool ≝
     323  match l return λx.
     324    match x with
     325    [ O ⇒ λl: Vector … O. bool
     326    | S x' ⇒ λl: Vector addressing_mode_tag (S x'). (l → bool) → bool
     327    ] with
    312328  [ VEmpty      ⇒  true 
    313329  | VCons len hd tl ⇒ λP.
     
    341357  ].
    342358  try %
    343   [ 2: cases (sym_eq ??? prf); @tl
    344   | generalize in match H; generalize in match tl; cases prf;
    345     (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
    346     #tl
     359  [2:
     360    cases (sym_eq ??? prf); assumption
     361  |1:
     362    generalize in match H; generalize in match tl;
     363    destruct #tl
    347364    normalize in ⊢ (∀_: %. ?);
    348     # H
    349     whd
    350     normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]);
    351     cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
     365    #H
     366    whd normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]);
     367    cases (is_a hd (subaddressing_modeel y tl H))
     368    whd try @I normalize nodelta //
     369  ]
    352370qed.
    353371
     
    535553lemma eq_addressing_mode_refl:
    536554  ∀a. eq_addressing_mode a a = true.
    537   #a cases a try #arg1 try #arg2 try @eq_bv_refl try @eq_b_refl
     555  #a
     556  cases a try #arg1 try #arg2
     557  try @eq_bv_refl try @eq_b_refl
    538558  try normalize %
    539559qed.
    540560 
    541 definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
     561definition eq_sum:
     562    ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
    542563  λlt, rt, leq, req, left, right.
    543564    match left with
     
    782803    eq_sum A B leq req s s = true.
    783804  #A #B #leq #req #s #leq_refl #req_refl
    784   cases s whd in ⊢ (? → ??%?); //
     805  cases s
     806  whd in ⊢ (? → ??%?);
     807  assumption
    785808qed.
    786809
     
    793816    eq_prod A B leq req s s = true.
    794817  #A #B #leq #req #s #leq_refl #req_refl
    795   cases s whd in ⊢ (? → ? → ??%?); #l #r >leq_refl normalize @req_refl
     818  cases s
     819  whd in ⊢ (? → ? → ??%?);
     820  #l #r
     821  >leq_refl @req_refl
    796822qed.
    797823
     
    835861    whd in ⊢ (??%?);
    836862    cases arg1
    837     [ #arg1_left normalize nodelta
     863    [1:
     864      #arg1_left normalize nodelta
    838865      @eq_sum_refl
    839       [1: #arg @eq_sum_refl
    840         [1: #arg @eq_sum_refl
    841           [1: #arg @eq_sum_refl
    842             [1: #arg @eq_prod_refl
    843               [*: @eq_addressing_mode_refl ]
    844             |2: #arg @eq_prod_refl
    845               [*: #arg @eq_addressing_mode_refl ]
     866      [1:
     867        #arg @eq_sum_refl
     868        [1:
     869          #arg @eq_sum_refl
     870          [1:
     871            #arg @eq_sum_refl
     872            [1:
     873              #arg @eq_prod_refl
     874              [*:
     875                @eq_addressing_mode_refl
     876              ]
     877            |2:
     878              #arg @eq_prod_refl
     879              [*:
     880                #arg @eq_addressing_mode_refl
     881              ]
    846882            ]
    847           |2: #arg @eq_prod_refl
    848             [*: #arg @eq_addressing_mode_refl ]
     883          |2:
     884            #arg @eq_prod_refl
     885            [*:
     886              #arg @eq_addressing_mode_refl
     887            ]
    849888          ]
    850         |2: #arg @eq_prod_refl
    851           [*: #arg @eq_addressing_mode_refl ]
     889        |2:
     890          #arg @eq_prod_refl
     891          [*:
     892            #arg @eq_addressing_mode_refl
     893          ]
    852894        ]
    853       |2: #arg @eq_prod_refl
    854         [*: #arg @eq_addressing_mode_refl ]
     895      |2:
     896        #arg @eq_prod_refl
     897        [*:
     898          #arg @eq_addressing_mode_refl
     899        ]
    855900      ]
    856     |2: #arg1_right normalize nodelta
    857         @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
     901    |2:
     902      #arg1_right normalize nodelta
     903      @eq_prod_refl
     904      [*:
     905        #arg @eq_addressing_mode_refl
     906      ]
    858907    ]
    859908  |*:
    860909    whd in ⊢ (??%?);
    861910    cases arg1
    862     [*: #arg1 >eq_sum_refl
    863       [1,4: normalize @eq_addressing_mode_refl
    864       |2,3,5,6: #arg @eq_prod_refl
    865         [*: #arg @eq_addressing_mode_refl ]
     911    [*:
     912      #arg1 >eq_sum_refl
     913      [1,4:
     914        @eq_addressing_mode_refl
     915      |2,3,5,6:
     916        #arg @eq_prod_refl
     917        [*:
     918          #arg @eq_addressing_mode_refl
     919        ]
    866920      ]
    867921    ]
     
    917971  ∀i. eq_instruction i i = true.
    918972  #i cases i
    919   [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl
    920   |7: #arg1 #arg2
    921       whd in ⊢ (??%?);
    922       >eq_addressing_mode_refl
    923       >eq_addressing_mode_refl
    924       %
    925   |8: #arg @eq_preinstruction_refl
     973  [1,2,3,4,5,6:
     974    #arg1 @eq_addressing_mode_refl
     975  |7:
     976    #arg1 #arg2
     977    whd in ⊢ (??%?);
     978    >eq_addressing_mode_refl
     979    >eq_addressing_mode_refl %
     980  |8:
     981    #arg @eq_preinstruction_refl
    926982  ]
    927983qed.
    928984
    929985let rec vect_member
    930   (A: Type[0]) (n: nat) (eq: A → A → bool)
    931   (v: Vector A n) (a: A) on v: bool ≝
     986  (A: Type[0]) (n: nat) (eq: A → A → bool) (v: Vector A n) (a: A)
     987    on v: bool ≝
    932988  match v with
    933989  [ VEmpty          ⇒ false
    934990  | VCons len hd tl ⇒
    935     eq hd a ∨ (vect_member A ? eq tl a)
     991      eq hd a ∨ (vect_member A ? eq tl a)
    936992  ].
    937993
     
    10741130    〈[[]], v〉 = split A 0 m v.
    10751131  #A #m #v
    1076   elim v
    1077   [ %
    1078   | #n #hd #tl #ih
    1079     normalize in ⊢ (???%); %
     1132  cases v try %
     1133  #n #hd #tl %
     1134qed.
     1135
     1136lemma Vector_O:
     1137  ∀A: Type[0].
     1138  ∀v: Vector A 0.
     1139    v ≃ VEmpty A.
     1140 #A #v
     1141 generalize in match (refl … 0);
     1142 cases v in ⊢ (??%? → ?%%??); //
     1143 #n #hd #tl #absurd
     1144 destruct(absurd)
     1145qed.
     1146
     1147lemma Vector_Sn:
     1148  ∀A: Type[0].
     1149  ∀n: nat.
     1150  ∀v: Vector A (S n).
     1151    ∃hd: A. ∃tl: Vector A n.
     1152      v ≃ VCons A n hd tl.
     1153  #A #n #v
     1154  generalize in match (refl … (S n));
     1155  cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
     1156  [1:
     1157    #absurd destruct(absurd)
     1158  |2:
     1159    #m #hd #tl #eq
     1160    <(injective_S … eq)
     1161    %{hd} %{tl} %
    10801162  ]
    1081 qed.
    1082 
    1083 lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
    1084  #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
    1085  #n #hd #tl #abs @⊥ destruct (abs)
    1086 qed.
    1087 
    1088 lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
    1089  ∃hd.∃tl.v ≃ VCons A n hd tl.
    1090  #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
    1091  [ #abs @⊥ destruct (abs)
    1092  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    10931163qed.
    10941164
     
    11251195  #A #n #q #r
    11261196  generalize in match (Vector_O A q …);
    1127   #hyp
    1128   >hyp in ⊢ (??%?);
    1129   %
    1130 qed.
    1131 
    1132 axiom split_succ:
    1133   ∀A, m, n.
     1197  #hyp >hyp in ⊢ (??%?); %
     1198qed.
     1199
     1200lemma tail_head:
     1201  ∀a: Type[0].
     1202  ∀m, n: nat.
     1203  ∀hd: a.
     1204  ∀l: Vector a m.
     1205  ∀r: Vector a n.
     1206    tail a ? (hd:::(l@@r)) = l@@r.
     1207  #a #m #n #hd #l #r
     1208  cases l try %
     1209  #m' #hd' #tl' %
     1210qed.
     1211
     1212lemma head_head':
     1213  ∀a: Type[0].
     1214  ∀m: nat.
     1215  ∀hd: a.
     1216  ∀l: Vector a m.
     1217    hd = head' … (hd:::l).
     1218  #a #m #hd #l cases l try %
     1219  #m' #hd' #tl %
     1220qed.
     1221
     1222lemma split_succ:
     1223  ∀A: Type[0].
     1224  ∀m, n: nat.
    11341225  ∀l: Vector A m.
    11351226  ∀r: Vector A n.
     
    11371228  ∀hd: A.
    11381229    v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)).
    1139 (*
    11401230  #A #m
    11411231  elim m
    1142   [ #n #l #r #v #hd #equal #hyp
    1143     normalize >(Vector_O A l) >equal
    1144     >(Vector_O A l) %
    1145   | #n' #ih #n #l #r #v #hd
    1146     #equal #hyp
    1147     cases(Vector_Sn A n' l)
    1148     #hd' #exists
    1149     cases exists #tl #jmeq
    1150     >jmeq *)
     1232  [1:
     1233    #n #l #r #v #hd #eq #hyp
     1234    destruct
     1235    >(Vector_O … l) %
     1236  |2:
     1237    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
     1238    destruct
     1239    cases (Vector_Sn … l) #hd' #tl'
     1240    whd in ⊢ (???%);
     1241    >tail_head
     1242    <(? : split A (S m') n (l@@r) = split' A (S m') n (l@@r))
     1243    [1:
     1244      <hyp <head_head' %
     1245    |2:
     1246      elim l normalize //
     1247    ]
     1248  ]
     1249qed.
    11511250
    11521251lemma split_prod:
    1153   ∀A,m,n.
     1252  ∀A: Type[0].
     1253  ∀m, n: nat.
    11541254  ∀p: Vector A (m + n).
    11551255  ∀v: Vector A m.
    11561256  ∀q: Vector A n.
    11571257    p = v@@q → 〈v, q〉 = split A m n p.
    1158   #A #m
    1159   elim m
    1160   [ #n #p #v #q #hyp
     1258  #A #m elim m
     1259  [1:
     1260    #n #p #v #q #hyp
    11611261    >hyp <(vector_append_zero A n q v)
    11621262    >(prod_vector_zero_eq_left A …)
    11631263    @split_zero
    1164   | #r #ih #n #p #v #q #hyp
     1264  |2:
     1265    #r #ih #n #p #v #q #hyp
    11651266    >hyp
    1166     cases (Vector_Sn A r v)
    1167     #hd #exists
    1168     cases exists
    1169     #tl #jmeq >jmeq
    1170     @split_succ [1: % |2: @ih % ]
     1267    cases (Vector_Sn A r v) #hd #exists
     1268    cases exists #tl #jmeq
     1269    >jmeq
     1270    @split_succ try %
     1271    @ih %
    11711272  ]
    11721273qed.
     
    11901291*)
    11911292
    1192 axiom split_elim:
    1193  ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
    1194   (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
    1195 (*  #A #l #m #v #P #hyp
    1196   normalize
    1197   <(split_prod A l m v ? ? ?)
    1198 *)
    1199 
     1293lemma split_elim:
     1294  ∀A: Type[0].
     1295  ∀l, m: nat.
     1296  ∀v: Vector A (l + m).
     1297  ∀P: (Vector A l) × (Vector A m) → Prop.
     1298    (∀vl: Vector A l.
     1299     ∀vm: Vector A m.
     1300      v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
     1301  cases daemon (* XXX: problem with dependent types *)
     1302qed.
     1303
     1304(* XXX: this looks almost certainly wrong *)
    12001305example half_add_SO:
    12011306 ∀pc.
     
    12301335*)
    12311336
    1232 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
    1233                        (encoding: list Byte) on encoding: Prop ≝
     1337let rec encoding_check
     1338  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
     1339    (encoding: list Byte)
     1340      on encoding: Prop ≝
    12341341  match encoding with
    12351342  [ nil ⇒ final_pc = pc
     
    12391346  ].
    12401347
    1241 lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
    1242  encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
    1243   let intermediate_pc ≝ pc + length … l1 in
    1244    encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
    1245     encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
    1246  #code_memory #final_pc #l1 elim l1
    1247   [ #pc #l2 whd in ⊢ (????% → ?); #H <plus_n_O whd whd in ⊢ (?%?); /2/
    1248   | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
    1249     #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
     1348lemma encoding_check_append:
     1349  ∀code_memory: BitVectorTrie Byte 16.
     1350  ∀final_pc: nat.
     1351  ∀l1: list Byte.
     1352  ∀pc: nat.
     1353  ∀l2: list Byte.
     1354    encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
     1355      let intermediate_pc ≝ pc + length … l1 in
     1356        encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
     1357          encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
     1358  #code_memory #final_pc #l1 elim l1
     1359  [1:
     1360    #pc #l2
     1361    whd in ⊢ (????% → ?); #H
     1362    <plus_n_O
     1363    whd whd in ⊢ (?%?); /2/
     1364  |2:
     1365    #hd #tl #IH #pc #l2 * #H1 #H2
     1366    >half_add_SO in H2; #H2
     1367    cases (IH … H2) <plus_n_Sm
     1368    #K1 #K2 % [2: @K2 ] whd % //
     1369    >half_add_SO @K1
     1370  ]
    12501371qed.
    12511372
    12521373axiom bitvector_3_elim_prop:
    1253  ∀P: BitVector 3 → Prop.
    1254   P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
    1255   P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
    1256   P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
     1374  ∀P: BitVector 3 → Prop.
     1375    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
     1376    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
     1377    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
    12571378
    12581379definition ticks_of_instruction ≝
    1259  λi.
    1260   let trivial_code_memory ≝ assembly1 i in
    1261   let trivial_status ≝ load_code_memory trivial_code_memory in
    1262    \snd (fetch trivial_status (zero ?)).
     1380  λi.
     1381    let trivial_code_memory ≝ assembly1 i in
     1382    let trivial_status ≝ load_code_memory trivial_code_memory in
     1383      \snd (fetch trivial_status (zero ?)).
    12631384
    12641385lemma fetch_assembly:
    1265   ∀pc,i,code_memory,assembled.
     1386  ∀pc: nat.
     1387  ∀i: instruction.
     1388  ∀code_memory: BitVectorTrie Byte 16.
     1389  ∀assembled: list Byte.
    12661390    assembled = assembly1 i →
    12671391      let len ≝ length … assembled in
    1268       encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
    1269       let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
    1270       let 〈instr_pc, ticks〉 ≝ fetched in
    1271       let 〈instr,pc'〉 ≝ instr_pc in
    1272        (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
    1273  #pc #i #code_memory #assembled cases i [8: *]
     1392        encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
     1393        let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
     1394        let 〈instr_pc, ticks〉 ≝ fetched in
     1395        let 〈instr,pc'〉 ≝ instr_pc in
     1396         (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
     1397  #pc #i #code_memory #assembled cases i [8: *]
    12741398 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
    12751399 [47,48,49:
     
    12891413 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
    12901414 [ whd in match fetch; normalize nodelta <H1 ] cases daemon
    1291  (*XXX
    1292    
    1293  whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
     1415(*
     1416 whd in ⊢ (let ? ≝ ??% in ?); <H1 whd in ⊢ (let fetched ≝ % in ?)
    12941417 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
    12951418 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
    12961419  30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
    12971420  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
    1298  whd >eq_instruction_refl >H4 @eq_bv_refl*)
    1299 qed.
    1300 
    1301 let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
    1302  match expected with
     1421 whd >eq_instruction_refl >H4 @eq_bv_refl
     1422*) (* XXX: not working! *)
     1423qed.
     1424
     1425let rec fetch_many
     1426  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
     1427    (expected: list instruction)
     1428      on expected: Prop ≝
     1429  match expected with
    13031430  [ nil ⇒ eq_bv … pc final_pc = true
    13041431  | cons i tl ⇒
    1305      let fetched ≝ fetch code_memory pc in
    1306      let 〈instr_pc, ticks〉 ≝ fetched in
    1307      let 〈instr,pc'〉 ≝ instr_pc in
     1432    let fetched ≝ fetch code_memory pc in
     1433    let 〈instr_pc, ticks〉 ≝ fetched in
     1434    let 〈instr,pc'〉 ≝ instr_pc in
    13081435      eq_instruction instr i = true ∧
    1309       ticks = (ticks_of_instruction i) ∧
    1310       fetch_many code_memory final_pc pc' tl].
    1311 
    1312 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
    1313  #A #a #b #EQ destruct //
     1436        ticks = (ticks_of_instruction i) ∧
     1437        fetch_many code_memory final_pc pc' tl
     1438  ].
     1439
     1440lemma option_destruct_Some:
     1441  ∀A: Type[0].
     1442  ∀a, b: A.
     1443    Some A a = Some A b → a = b.
     1444  #A #a #b #EQ
     1445  destruct %
    13141446qed.
    13151447
    13161448axiom eq_instruction_to_eq:
    1317   ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
    1318                
     1449  ∀i1, i2: instruction.
     1450    eq_instruction i1 i2 = true → i1 = i2.
     1451         
     1452(*     
    13191453lemma fetch_assembly_pseudo':
    1320  ∀lookup_labels.∀pol:policy_type lookup_labels.∀ppc,lookup_datalabels.
    1321   ∀pi,code_memory,len,assembled,instructions,pc.
    1322    let expansion ≝ pol ppc in
    1323    instructions = expand_pseudo_instruction lookup_labels ppc expansion lookup_datalabels pi →
    1324     〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels pol ppc lookup_datalabels pi →
    1325      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
    1326       fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
    1327  #lookup_labels #pol #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
    1328  #EQ1 whd in ⊢ (???% → ?); <EQ1 whd in ⊢ (???% → ?); #EQ2
    1329  cases (pair_destruct ?????? EQ2) -EQ2; #EQ2a #EQ2b
    1330  >EQ2a >EQ2b -EQ2a -EQ2b;
     1454  ∀lookup_labels.
     1455  ∀pol: policy_type lookup_labels.
     1456  ∀ppc.
     1457  ∀lookup_datalabels.
     1458  ∀pi.
     1459  ∀code_memory.
     1460  ∀len.
     1461  ∀assembled.
     1462  ∀instructions.
     1463  ∀pc.
     1464    let expansion ≝ pol ppc in
     1465      instructions = expand_pseudo_instruction lookup_labels ppc expansion lookup_datalabels pi →
     1466        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels pol ppc lookup_datalabels pi →
     1467        encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
     1468          fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
     1469  #lookup_labels #pol #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
     1470  #EQ1 whd in ⊢ (???% → ?); <EQ1 whd in ⊢ (???% → ?); #EQ2
     1471  cases (pair_destruct ?????? EQ2) -EQ2; #EQ2a #EQ2b
     1472  >EQ2a >EQ2b -EQ2a -EQ2b;
    13311473  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
    13321474  generalize in match pc; elim instructions
    1333   [ #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
    1334   | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
     1475  [1:
     1476    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
     1477  |2:
     1478    #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
    13351479    generalize in match (fetch_assembly pc i code_memory … (refl …) H1);
    13361480    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %);
    13371481    cases newi_pc #newi #newpc whd in ⊢ (% → %); #K cases (conjunction_true … K) -K; #K1
    13381482    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
    1339     [ @K1 | @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 | >(eq_bv_eq … K3) @IH @H2 ]
    1340 qed.
     1483    [1:
     1484      @K1
     1485    |2:
     1486      @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2
     1487    |3:
     1488      >(eq_bv_eq … K3) @IH @H2
     1489    ]
     1490  ]
     1491qed.
     1492*)
    13411493
    13421494axiom bitvector_of_nat_nat_of_bitvector:
     
    13461498(* CSC: soo long next one; can we merge with previous one now? *)
    13471499lemma fetch_assembly_pseudo:
    1348   ∀program:pseudo_assembly_program.
    1349   ∀pol:policy program.
     1500  ∀program: pseudo_assembly_program.
     1501  ∀pol: policy program.
    13501502  let lookup_labels ≝ λx:Identifier.sigma … pol (address_of_word_labels_code_mem (\snd  program) x) in
    13511503  ∀ppc.∀code_memory.
Note: See TracChangeset for help on using the changeset viewer.