Ignore:
Timestamp:
May 14, 2012, 10:37:08 AM (8 years ago)
Author:
mulligan
Message:

Changes to get things to compile and to avoid the dependency circularity between ASM/Interpret.ma and common/StructuredTraces.ma. New file ASM/AbstractStatus.ma factors out the definition (not the implementation!) of an abstract status, which both of the previously mentioned files require.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1936 r1939  
    107107  ∀P: ∀m. Vector A m → Prop.
    108108    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 //
     109  #A #n #m #v1 #v2 #P #eq #jmeq
     110  destruct #assm assumption
    112111qed.
    113112
     
    119118    e ::: v = [[ e ]] @@ v.
    120119  #A #n #e #v
    121   elim v
    122   [1:
    123     normalize %
    124   |2:
    125     #NN #AA #VV #IH
    126     normalize
    127     %
    128   ]
     120  cases v try %
     121  #n' #hd #tl %
    129122qed.
    130123
     
    137130    hd:::(v@@q) = (hd:::v)@@q.
    138131  #A #n #m #v #q
    139   elim v
    140   [1:
    141     #hd %
    142   |2:
    143     #n' #hd' #tl' #ih #hd'
    144     <ih %
    145   ]
     132  elim v try (#hd %)
     133  #n' #hd' #tl' #ih #hd'
     134  <ih %
    146135qed.
    147136
     
    185174    mem A eq ? (p@@(a:::r)) a = true.
    186175  #A #m #o #eq #reflex #p #a
    187   elim p
    188   [1:
    189     normalize
    190     >reflex
    191     #H %
    192   |2:
    193     #m' #hd #tl #inductive_hypothesis
    194     normalize
    195     cases (eq ??) normalize nodelta
    196     [1:
    197       #_ %
    198     |2:
    199       @inductive_hypothesis
    200     ]
    201   ]
     176  elim p try (normalize >reflex #H %)
     177  #m' #hd #tl #inductive_hypothesis
     178  normalize
     179  cases (eq ??) normalize nodelta
     180  try (#irrelevant %)
     181  @inductive_hypothesis
    202182qed.
    203183
     
    212192    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
    213193  #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
    219     normalize
    220     cases (eq ??) try %
    221     @inductive_hypothesis assumption
    222   ]
     194  elim p try (#r #assm assumption)
     195  #m' #hd #tl #inductive_hypothesis #r #assm
     196  normalize
     197  cases (eq ??) try %
     198  @inductive_hypothesis assumption
    223199qed.
    224200
     
    234210    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
    235211  #A #o #n #eq #reflex #h #v
    236   elim v
     212  elim v try (normalize #m #irrelevant @I)
     213  #m' #hd #tl #inductive_hypothesis #m #q
     214  change with (bool_to_Prop (andb ??))
     215  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
    237216  [1:
    238     normalize #m #_ @I
     217    @mem_monotonic_wrt_append try assumption
     218    @mem_monotonic_wrt_append try assumption
     219    normalize >reflex %
    239220  |2:
    240     #m' #hd #tl #inductive_hypothesis #m #q
    241     change with (bool_to_Prop (andb ??))
    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
    250       change with (bool_to_Prop (subvector_with ??????))
    251       @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
    252       try @associative_plus
    253       @inductive_hypothesis
    254     ]
     221    #assm >assm
     222    >vector_cons_append
     223    change with (bool_to_Prop (subvector_with ??????))
     224    @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
     225    try @associative_plus
     226    @inductive_hypothesis
    255227  ]
    256228qed.
     
    803775    eq_sum A B leq req s s = true.
    804776  #A #B #leq #req #s #leq_refl #req_refl
    805   cases s
    806   whd in ⊢ (? → ??%?);
    807   assumption
     777  cases s assumption
    808778qed.
    809779
     
    828798  try @eq_addressing_mode_refl
    829799  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
    830     whd in ⊢ (??%?);
    831     try %
     800    whd in ⊢ (??%?); try %
    832801    >eq_addressing_mode_refl
    833802    >eq_addressing_mode_refl %
     
    852821    |3:
    853822      #arg1_left normalize nodelta
    854       >(eq_sum_refl …) [1: %
    855       |2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ]
     823      >(eq_sum_refl …)
     824      [1:
     825        %
     826      |2,3:
     827        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
     828      ]
    856829    |4:
    857830      #arg1_left normalize nodelta
     
    12911264*)
    12921265
    1293 lemma split_elim:
     1266definition split_elim:
    12941267  ∀A: Type[0].
    12951268  ∀l, m: nat.
     
    12981271    (∀vl: Vector A l.
    12991272     ∀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 *)
    1302 qed.
     1273      v = vl@@vm → P 〈vl,vm〉) → P (split A l m v) ≝
     1274  λa: Type[0].
     1275  λl, m: nat.
     1276  λv: Vector a (l + m).
     1277  λP.
     1278  match v return λn: nat. λv: Vector a (n + m).
     1279    (∀vl: Vector a ?.
     1280     ∀vm: Vector a m.
     1281      v = vl@@vm → P 〈vl,vm〉) → P (split a ? m v) with
     1282  [ VEmpty ⇒ ?
     1283  | VCons v' hd tl ⇒ ?
     1284  ] ?.
    13031285
    13041286(* XXX: this looks almost certainly wrong *)
Note: See TracChangeset for help on using the changeset viewer.