Changeset 855 for src/ASM/AssemblyProof.ma

Timestamp:

May 27, 2011, 6:11:37 PM (10 years ago)

Author:

mulligan

Message:

changes from today

File:

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

src/ASM/AssemblyProof.ma

@@ -44 +44 @@
 (* RUSSEL **)
 
+definition bit_elim: ∀P: bool → bool. bool ≝
+  λP.
+    P true ∧ P false.
+
 let rec bitvector_elim_internal
   (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝
@@ -73 +77 @@
 lemma subvector_hd_tl:
   ∀A: Type[0].
-  ∀
-  ∀hd: A.
-  ∀
+  ∀n: nat.
+  ∀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 ⊢ (% → ?)
+  ]
 
 let rec list_addressing_mode_tags_elim