Changeset 1516 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r990 r1516  
    2929
    3030lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
    31  #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     31 #v lapply (refl … 0) cases v in ⊢ (??%? → ?%%??); //
    3232 #n #hd #tl #abs @⊥ destruct (abs)
    3333qed.
     
    3535lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
    3636 ∃hd.∃tl.v ≃ VCons bool n hd tl.
    37  #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     37 #n #v lapply (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
    3838 [ #abs @⊥ destruct (abs)
    3939 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     
    132132  (x ≠ y → P false) →
    133133  P (eq_bv n x y).
    134 #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)
     134#P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf)
    135135#Q * *; normalize /3/
    136136qed.
     
    177177  ∀n, v, q.
    178178    eq_bv n v q = true → v = q.
    179   #n #v #q generalize in match v
     179  #n #v #q generalize in match v;
    180180  elim q
    181181  [ #v #h @BitVector_O
     
    184184    #hd' * #tl' #jmeq >jmeq in h;
    185185    #new_h
    186     change in new_h with ((andb ? ?) = ?);
     186    change in new_h; with ((andb ? ?) = ?);
    187187    cases(conjunction_true … new_h)
    188188    #eq_heads #eq_tails
     
    190190    cases(eq_b_eq … eq_heads)
    191191    whd in eq_tails:(??(?????(%))?);
    192     change in eq_tails with (eq_bv ??? = ?);
     192    change in eq_tails; with (eq_bv ??? = ?);
    193193    <(ih tl') //
    194194  ]
Note: See TracChangeset for help on using the changeset viewer.