Changeset 2124 for src/ASM/BitVector.ma

Timestamp:

Jun 27, 2012, 4:23:54 PM (7 years ago)

Author:

sacerdot

Message:

Much more shuffling around to proper places

File:

• src/ASM/BitVector.ma (modified) (1 diff)

src/ASM/BitVector.ma

@@ -236 +236 @@
     String.
 
-example sub_minus_one_seven_eight:
-  ∀v: BitVector 7.
-  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
-  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
- cases daemon.
-qed.
-
-axiom sub16_with_carry_overflow:
-  ∀left, right, result: BitVector 16.
-  ∀flags: BitVector 3.
-  ∀upper: BitVector 9.
-  ∀lower: BitVector 7.
-    sub_16_with_carry left right false = 〈result, flags〉 →
-      vsplit bool 9 7 result = 〈upper, lower〉 →
-        get_index_v bool 3 flags 2 ? = true →
-          upper = [[true; true; true; true; true; true; true; true; true]].
-  //
-qed.
-
-axiom sub_16_to_add_16_8_0:
- ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
-  get_index' ? 2 0 flags = false →
-  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
-   v1 = add ? v2 (sign_extension (false:::v3)).
-
-axiom sub_16_to_add_16_8_1:
- ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
-  get_index' ? 2 0 flags = true →
-  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
-   v1 = add ? v2 (sign_extension (true:::v3)).
+definition bitvector_3_cases:
+  ∀b: BitVector 3.
+    ∃l, c, r: bool.
+      b ≃ [[l; c; r]].
+  #b
+  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
+  [1:
+    #absurd @⊥ -b @(destruct_bug_fix_1 2)
+    >absurd %
+  |2:
+    #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
+    cut (n = 2)
+    [1:
+      @destruct_bug_fix_2
+      >size_refl %
+    |2:
+      #n_refl >n_refl in tl; #V
+      @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))
+      [1:
+        #absurd @⊥ -V @(destruct_bug_fix_1 1)
+        >absurd %
+      |2:
+        #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}
+        cut (n' = 1)
+        [1:
+          @destruct_bug_fix_2 >size_refl' %
+        |2:
+          #n_refl' >n_refl' in tl'; #V'
+          @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))
+          [1:
+            #absurd @⊥ -V' @(destruct_bug_fix_1 0)
+            >absurd %
+          |2:
+            #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}
+            cut (n'' = 0)
+            [1:
+              @destruct_bug_fix_2 >size_refl'' %
+            |2:
+              #n_refl'' >n_refl'' in tl''; #tl'''
+              >(Vector_O … tl''') %
+            ]
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+
+lemma bitvector_3_elim_prop:
+  ∀P: BitVector 3 → Prop.
+    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
+    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
+    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
+  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
+  cases (bitvector_3_cases … H9) #l #assm cases assm
+  -assm #c #assm cases assm
+  -assm #r #assm cases assm destruct
+  cases l cases c cases r assumption
+qed.