Changeset 2126

Timestamp:

Jun 27, 2012, 4:56:52 PM (7 years ago)

Author:

sacerdot

Message:

Proof improved (for case 3) + new proof (for case 11)

File:

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

src/ASM/BitVector.ma

@@ -236 +236 @@
     String.
 
-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''') %
-            ]
-          ]
-        ]
-      ]
-    ]
-  ]
+lemma bitvector_3_cases:
+  ∀w: BitVector 3.
+   ∃b0,b1,b2: bool.
+    w ≃ [[b0;b1;b2]].
+  #w
+ repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
+ >(BitVector_O … w) %
+qed.
+
+lemma bitvector_11_cases:
+  ∀w: BitVector 11.
+    ∃b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10: bool.
+      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7;b8;b9;b10]].
+ #w
+ repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
+ >(BitVector_O … w) %
 qed.