Changeset 864 for src

Timestamp:

May 31, 2011, 11:27:13 AM (10 years ago)

Author:

mulligan

Message:

resolved conflict

File:

• src/ASM/AssemblyProof.ma (modified) (3 diffs)

src/ASM/AssemblyProof.ma

@@ -174 +174 @@
 qed.
 
-lemma subvector_hd_tl:
+lemma subvector_multiple_append:
   ∀A: Type[0].
   ∀o, n: nat.
@@ -213 +213 @@
     ]
 qed.
-(*
+
 lemma subvector_hd_tl:
   ∀A: Type[0].
-  ∀n: nat.
+  ∀o: nat.
+  ∀eq: A → A → bool.
+  ∀refl: ∀a. eq a a = true.
   ∀h: A.
-  ∀eq: A → A → bool.
-  ∀v: Vector A n.
-  ∀m: nat.
-  ∀q: Vector A m.
-    bool_to_Prop (subvector_with A ? ? eq v (h ::: q @@ v)).
-  # A
-  # N
-  # H
-  # EQ
-  # V
-  elim V
-  [ normalize
-    # M
-    # Q
-    %
-  | # NN
-    # AA
-    # VV
-    # IH
-    # MM
-    # QQ
-    whd
-    whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
-    change in ⊢ (match (match ? with [_ ⇒ % | _ ⇒ ?]) with [_ ⇒ ? | _ ⇒ ?])
-     with (subvector_with ??????)
-    change in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]) with (andb ??)
-    change with (bool_to_Prop ?);
-    cut ((mem A EQ (S MM+S NN) (H:::QQ@@AA:::VV) AA) = true)
-    [
-    | # H
-      > H
-      applyS (IH ? (QQ@@[[AA]]))
-    ]
-    generalize in match (IH ? (QQ@@[[AA]]))
-    whd in ⊢ (% → ?)
-  ]
-  *)
-
+  ∀v: Vector A o.
+    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
+
+axiom eq_a_reflexive:
+  ∀a. eq_a a a = true.
+  
 (*
 let rec list_addressing_mode_tags_elim
@@ -293 +263 @@
   [1: @ (execute_1_technical ? ? tl)
       [ //
-      | 
+      | @ (subvector_hd_tl addressing_mode_tag (S y) (S len) eq_a eq_a_reflexive)
       ]
   ].