Changeset 2126


Ignore:
Timestamp:
Jun 27, 2012, 4:56:52 PM (5 years ago)
Author:
sacerdot
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r2124 r2126  
    236236    String.
    237237
    238 definition bitvector_3_cases:
    239   ∀b: BitVector 3.
    240     ∃l, c, r: bool.
    241       b ≃ [[l; c; r]].
    242   #b
    243   @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
    244   [1:
    245     #absurd @⊥ -b @(destruct_bug_fix_1 2)
    246     >absurd %
    247   |2:
    248     #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
    249     cut (n = 2)
    250     [1:
    251       @destruct_bug_fix_2
    252       >size_refl %
    253     |2:
    254       #n_refl >n_refl in tl; #V
    255       @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))
    256       [1:
    257         #absurd @⊥ -V @(destruct_bug_fix_1 1)
    258         >absurd %
    259       |2:
    260         #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}
    261         cut (n' = 1)
    262         [1:
    263           @destruct_bug_fix_2 >size_refl' %
    264         |2:
    265           #n_refl' >n_refl' in tl'; #V'
    266           @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))
    267           [1:
    268             #absurd @⊥ -V' @(destruct_bug_fix_1 0)
    269             >absurd %
    270           |2:
    271             #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}
    272             cut (n'' = 0)
    273             [1:
    274               @destruct_bug_fix_2 >size_refl'' %
    275             |2:
    276               #n_refl'' >n_refl'' in tl''; #tl'''
    277               >(Vector_O … tl''') %
    278             ]
    279           ]
    280         ]
    281       ]
    282     ]
    283   ]
     238lemma bitvector_3_cases:
     239  ∀w: BitVector 3.
     240   ∃b0,b1,b2: bool.
     241    w ≃ [[b0;b1;b2]].
     242  #w
     243 repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
     244 >(BitVector_O … w) %
     245qed.
     246
     247lemma bitvector_11_cases:
     248  ∀w: BitVector 11.
     249    ∃b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10: bool.
     250      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7;b8;b9;b10]].
     251 #w
     252 repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
     253 >(BitVector_O … w) %
    284254qed.
    285255
Note: See TracChangeset for help on using the changeset viewer.