Changeset 864


Ignore:
Timestamp:
May 31, 2011, 11:27:13 AM (8 years ago)
Author:
mulligan
Message:

resolved conflict

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r863 r864  
    174174qed.
    175175
    176 lemma subvector_hd_tl:
     176lemma subvector_multiple_append:
    177177  ∀A: Type[0].
    178178  ∀o, n: nat.
     
    213213    ]
    214214qed.
    215 (*
     215
    216216lemma subvector_hd_tl:
    217217  ∀A: Type[0].
    218   ∀n: nat.
     218  ∀o: nat.
     219  ∀eq: A → A → bool.
     220  ∀refl: ∀a. eq a a = true.
    219221  ∀h: A.
    220   ∀eq: A → A → bool.
    221   ∀v: Vector A n.
    222   ∀m: nat.
    223   ∀q: Vector A m.
    224     bool_to_Prop (subvector_with A ? ? eq v (h ::: q @@ v)).
    225   # A
    226   # N
    227   # H
    228   # EQ
    229   # V
    230   elim V
    231   [ normalize
    232     # M
    233     # Q
    234     %
    235   | # NN
    236     # AA
    237     # VV
    238     # IH
    239     # MM
    240     # QQ
    241     whd
    242     whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    243     change in ⊢ (match (match ? with [_ ⇒ % | _ ⇒ ?]) with [_ ⇒ ? | _ ⇒ ?])
    244      with (subvector_with ??????)
    245     change in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]) with (andb ??)
    246     change with (bool_to_Prop ?);
    247     cut ((mem A EQ (S MM+S NN) (H:::QQ@@AA:::VV) AA) = true)
    248     [
    249     | # H
    250       > H
    251       applyS (IH ? (QQ@@[[AA]]))
    252     ]
    253     generalize in match (IH ? (QQ@@[[AA]]))
    254     whd in ⊢ (% → ?)
    255   ]
    256   *)
    257 
     222  ∀v: Vector A o.
     223    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
     224
     225axiom eq_a_reflexive:
     226  ∀a. eq_a a a = true.
     227 
    258228(*
    259229let rec list_addressing_mode_tags_elim
     
    293263  [1: @ (execute_1_technical ? ? tl)
    294264      [ //
    295       |
     265      | @ (subvector_hd_tl addressing_mode_tag (S y) (S len) eq_a eq_a_reflexive)
    296266      ]
    297267  ].
Note: See TracChangeset for help on using the changeset viewer.