Changeset 1516 for src/ASM


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

Ported to syntax of Matita 0.99.1.

Location:
src/ASM
Files:
6 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  ]

  • src/ASM/BitVectorTrie.ma

    r1479 r1516  
    6161  (P → Q) → (∀a,t',P,Q.(P → Q) → f a t' P → f a t' Q) → fold A ? n f t P → fold A ? n f t Q.
    6262 #A #n #f #t #P #Q #H
    63  generalize in match (refl ? n) generalize in match H -H; generalize in match Q -Q; generalize in match P -P;
    64  elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?)
     63 generalize in match (refl ? n); generalize in match H; -H; generalize in match Q; -Q; generalize in match P; -P;
     64 elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?);
    6565 [ #a #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(Hf (zero 0) a P Q HPQ HP)
    6666 | #h #l #r #Hl #Hr #f #P #Q #HPQ #_ #Hf #HP normalize normalize in HP; @(Hl ? (fold A Prop h (λx.f (true:::x)) r P) (fold A Prop h (λx.f (true:::x)) r Q) ? (refl ? h) ?)
    … …  
    7979  ∀P: Prop.
    8080  (∀a,t',P.f a t' P → P) → fold A Prop n f t P → P.
    81  #A #n #f #t #P #H generalize in match (refl ? n) generalize in match H -H; generalize in match P -P;
    82  elim t in f ⊢ (? → ? → ???% → ???%%%? → ?) -t
     81 #A #n #f #t #P #H generalize in match (refl ? n); generalize in match H; -H; generalize in match P; -P;
     82 elim t in f ⊢ (? → ? → ???% → ???%%%? → ?); -t
    8383 [ #a #f #P #Hf #_ normalize @(Hf [[]])
    8484 | #h #l #r #Hl #Hr #f #P #Hf #_ normalize #HP @(Hr (λx.f (true:::x)))
    … …  
    107107 | #n #t' #X #Y #HXY #HX %1
    108108   [ @(proj1 ? ? HX) | @HXY @(proj2 ? ? HX) ]
    109  | whd in Hl @Hl ]
     109 | whd in Hl; @Hl ]
    110110qed.
    111111 
    … …  
    170170  ∀P:BitVector n → A → Prop.
    171171  forall A n t P → ∀a:A.∀b.lookup_opt A n b t = Some ? a → P b a.
    172  #A #n #t #P generalize in match (refl ? n) elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?)
     172 #A #n #t #P generalize in match (refl ? n); elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?);
    173173 [ #x #f #_ #Hf #a #b whd in Hf; #Hb normalize in Hb; destruct >(BitVector_O b) @(proj1 ? ? Hf)
    174174 | #h #l #r #Hl #Hr #f #_ #Hf #a #b #Hb cases (BitVector_Sn h b)
    … …  
    306306lemma BitVectorTrie_O:
    307307 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
    308  #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
     308 #A #v generalize in match (refl … O); cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??));
    309309  [ #w #_ %1 %[@w] %
    310310  | #n #l #r #abs @⊥ destruct(abs)
    … …  
    314314lemma BitVectorTrie_Sn:
    315315 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
    316  #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
     316 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%);
    317317  [ #m #abs @⊥ destruct(abs)
    318318  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
    … …  
    350350  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
    351351 #A #a #v #n #c elim c -c -n
    352   [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     352  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF; //
    353353  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    354354    #t cases(BitVectorTrie_Sn … t)
    355355    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    356      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     356     [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
    357357    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    358      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     358     [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize
    359359     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
    360360qed.
    … …  
    363363 ∀A.∀n.∀b.∀a.
    364364 lookup A n b (Stub A ?) a = a.
    365  #A #n #b #a cases n in b ⊢ (??(??%%%?)?)
     365 #A #n #b #a cases n in b ⊢ (??(??%%%?)?);
    366366 [ #b >(BitVector_O b) normalize @refl
    367367 | #h #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
    … …  
    375375  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
    376376  lookup_opt A n b t = None A → ∀x.lookup A n b t x = x.
    377  #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)
     377 #A #n #b #t #a generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?);
    378378 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct
    379379 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb
    … …  
    389389  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
    390390  lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a.
    391  #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)
     391 #A #n #b #t #a generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?);
    392392 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl
    393393 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb
    … …  
    403403  ∀A.∀n.∀b.∀t.∀x,a.
    404404  lookup A n b t x = a → x ≠ a → lookup_opt A n b t = Some A a.
    405  #A #n #b #t #x #a generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ?)
     405 #A #n #b #t #x #a generalize in match (refl ? n); elim t in b ⊢ (???% → ? → ?);
    406406 [ #z #B #_ #H #Hx >(BitVector_O B) in H; normalize #H >H @refl
    407407 | #h #l #r #Hl #Hr #B #_ #H #Hx cases (BitVector_Sn h B) #hd #X elim X; -X #tl #HB
    … …  
    436436 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
    437437  lookup_opt … b (insert … b v t) = Some A v.
    438  #A #v #n #b #t elim t in b ⊢ (??(??%%%)?)
     438 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?);
    439439 [ #x #b >(BitVector_O b) normalize @refl
    440440 | #h #l #r #Hl #Hr #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
    … …  
    442442   | normalize @Hl
    443443   ]
    444  | #n' #b cases n' in b ⊢ ?
     444 | #n' #b cases n' in b ⊢ ?;
    445445   [ #b >(BitVector_O b) normalize @refl
    446446   | #m #b cases (BitVector_Sn m b) #hd #X elim X -X; #tl #Hb >Hb cases hd
    … …  
    454454  (notb (eq_bv ? b c)) → lookup_opt … b (insert … c v t) = lookup_opt … b t.
    455455 #A #v #n #c elim c -c -n
    456   [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     456  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF; //
    457457  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    458458    #t cases(BitVectorTrie_Sn … t)
    459459    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    460      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     460     [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
    461461    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    462      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     462     [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize
    463463     [3,4: cases tl' // | *: @lookup_opt_prepare_trie_for_insertion_miss //]]]
    464464qed.
    … …  
    476476     ]
    477477   | #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
    478      [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %) #Heq3
     478     [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %); #Heq3
    479479       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X) %2 //
    480        |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H
     480       |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H;
    481481         [1,3: #X %1 //
    482482         |2,4: >Heq3 //
    … …  
    499499  ∀A:Type[0].∀n:nat.∀b.∀a.∀t.∀P.
    500500  lookup_opt A n b t = (None A)  → forall A n (insert A n b a t) P → forall A n t P.
    501  #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%)
     501 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%);
    502502 [ #x #b #_ #P >(BitVector_O b) normalize #H destruct
    503503 | #h #l #r #Hl #Hr #b #_ #P cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #Hlookup #H
    … …  
    527527  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P:(BitVector n → A → Prop).
    528528  (∀x.(lookup_opt A n b t = Some A x) → P b x) → forall A n (insert A n b a t) P → forall A n t P.
    529  #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ? → ??%%% → ?)
     529 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → % → ? → ??%%% → ?);
    530530 [ #x #b #_ #P >(BitVector_O b) normalize #HP #Hf %1 [ @HP @refl | @(proj2 ? ? Hf) ]
    531531 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #HP #Hf
    … …  
    565565  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P.
    566566  forall A n t P → P b a → forall A n (insert A n b a t) P.
    567  #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%)
     567 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%);
    568568 [ #x #b #_ #P >(BitVector_O b) normalize #H1 #H2 /2/
    569569 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #Hf #HP
    … …  
    587587     ]
    588588   ]
    589  | #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%)
     589 | #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%);
    590590   [ #b #P #Hf #HP normalize %1 [ @HP | // ]
    591591   | #h #hd #tl #H #b #P #Hf cases hd #HP normalize @(forall_prepare_tree_for_insertion A h tl a ? HP)
    … …  
    603603  ]
    604604| #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t)
    605   [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?)
     605  [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?);
    606606    #X lapply (option_map_none … X) @IH
    607607  | #E >E normalize //
    … …  
    622622  cases (BitVectorTrie_Sn … t)
    623623  [ * #t1 * #t2 #E' >E'
    624     whd in ⊢ (??%? → ??%?) cases bhd #U
     624    whd in ⊢ (??%? → ??%?); cases bhd #U
    625625    cases (option_map_some ????? U)
    626626    #tn' * #U' #E'' <E''
    627     whd in ⊢ (??%?) whd in ⊢ (??(???%%)?)
     627    whd in ⊢ (??%?); whd in ⊢ (??(???%%)?);
    628628    @(IH … U')
    629629  | #E >E normalize #E' destruct
    … …  
    642642  @(vector_inv_n … b) #bhd #btl
    643643  cases (BitVectorTrie_Sn … t)
    644   [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?) cases bhd
     644  [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?); cases bhd
    645645    #U cases (option_map_some ????? U) #tn' * #U' #E' <E'
    646646    #b' @(vector_inv_n … b') #bhd' #btl'
    647647    cases bhd'
    648648    [ 2,3: #_ @refl
    649     | *: #NE whd in ⊢ (??%%) whd in ⊢ (??(???%%)(???%%))
    650          @(IH … U') % #E'' >E'' in NE * #H @H @refl
     649    | *: #NE whd in ⊢ (??%%); whd in ⊢ (??(???%%)(???%%));
     650         @(IH … U') % #E'' >E'' in NE; * #H @H @refl
    651651    ]
    652   | #E >E whd in ⊢ (??%? → ?) #NE destruct
     652  | #E >E whd in ⊢ (??%? → ?); #NE destruct
    653653  ]
    654654] qed.

  • src/ASM/BitVectorZ.ma

    r891 r1516  
    5858#n #bv elim bv
    5959[ //
    60 | #m * #t #IH whd in ⊢ (??%) //
     60| #m * #t #IH whd in ⊢ (??%); //
    6161] qed.
    6262
    … …  
    109109| #tl #_ normalize @le_S_S
    110110  change with (? ≤ pos_length one + m)
    111   generalize in ⊢ (?(?(?????%?))(?(?%)?)) elim tl
     111  generalize in ⊢ (?(?(?????%?))(?(?%)?)); elim tl
    112112  [ // | #o * #t normalize #IH #p <plus_n_Sm
    113113    change with (? ≤ pos_length (p1 p) + o)
    … …  
    145145theorem bv_Z_signed_max : ∀n. ∀bv:BitVector (S n). Z_of_signed_bitvector (S n) bv < Z_two_power_nat n.
    146146#n #bv @(vector_inv_n ? (S n) ? bv) *
    147 [ #t whd in ⊢ (?%%) lapply (bv_Z_unsigned_min … (negation_bv n t))
     147[ #t whd in ⊢ (?%%); lapply (bv_Z_unsigned_min … (negation_bv n t))
    148148  cases (Z_of_unsigned_bitvector n (negation_bv n t)) //
    149149  #p *
    150 | #t whd in ⊢ (?%?) //
     150| #t whd in ⊢ (?%?); //
    151151] qed.

  • src/ASM/Status.ma

    r1515 r1516  
    916916  @ le_S_S
    917917  lapply (le_n n)
    918   generalize in ⊢ (?%? → ?(??%?)?)
    919   elim n in ⊢ (∀_:?. ??% → ?(?%??)?)
     918  generalize in ⊢ (?%? → ?(??%?)?);
     919  elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
    920920  [ normalize
    921921    #n
    … …  
    924924    [ //
    925925    | #H #K
    926       inversion K
     926      @(le_inv_ind ?? K …)
    927927      [ # H1
    928928        < H1
    … …  
    946946      # x # K1
    947947      lapply (le_S_S_to_le … K1)
    948       generalize in match m
     948      generalize in match m;
    949949      elim x
    950950      normalize
    … …  
    955955      //
    956956      # q # K2
    957       apply H
     957      @H
    958958      /3/
    959959    ]

  • src/ASM/Util.ma

    r1323 r1516  
    219219    #ABSURD
    220220    elim (ABSURD nil_absurd)
    221   | normalize in cons_proof
     221  | normalize in cons_proof;
    222222    @le_S_S_to_le
    223223    assumption
    … …  
    275275  | 3: normalize
    276276       generalize in match (sig2 … (reduce_strong A B tl tl1));
    277        >p2 >p3 >p4 normalize in ⊢ (% → ?)
     277       >p2 >p3 >p4 normalize in ⊢ (% → ?);
    278278       #HYP //
    279279  ]
    … …  
    377377  ∀a:A.
    378378  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    379   #A #a #P #H #x #p
    380   generalize in match H
    381   generalize in match P
    382   cases p
    383   //
     379  #A #a #P #H #x #p lapply H lapply P cases p //
    384380qed.
    385381 
    … …  
    400396    @ p
    401397  | 4:
    402     normalize in prf2
     398    normalize in prf2;
    403399    normalize
    404400    @ le_S_S_to_le
    … …  
    562558 #A #B #H #acc #suff elim suff
    563559  [ #pre >append_nil %
    564   | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
     560  | #hd #tl #IH #pre whd in ⊢ (???%); <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
    565561qed.
    566562

  • src/ASM/Vector.ma

    r1330 r1516  
    6060    ]) lt.
    6161    [ cases (not_le_Sn_O O)
    62       normalize in absd1
     62      normalize in absd1;
    6363      # H
    6464      cases (H absd1)
    6565    | cases (not_le_Sn_O (S o))
    66       normalize in prf
     66      normalize in prf;
    6767      # H
    6868      cases (H prf)
    6969    | normalize
    70       normalize in prf
     70      normalize in prf;
    7171      @ le_S_S_to_le
    7272      assumption
    … …  
    474474  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
    475475  ] P v.
    476 #A #n #P #v generalize in match P cases v normalize //
     476#A #n #P #v lapply P cases v normalize //
    477477qed.
    478478
    … …  
    487487  normalize /2/
    488488| #m #h #t #IH #y @(vector_inv_n … y)
    489   #h' #t' #Ht #Hf whd in ⊢ (?%)
     489  #h' #t' #Ht #Hf whd in ⊢ (?%);
    490490  @(f_elim ? h h') #Eh
    491491  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
    … …  
    497497#A #f #f_true #n #v elim v
    498498[ //
    499 | #m #h #t #IH whd in ⊢ (??%%) >f_true >IH @refl
     499| #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl
    500500] qed.
    501501
    … …  
    508508[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
    509509| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
    510   #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE /2/
     510  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
    511511] qed.
    512512
Note: See TracChangeset for help on using the changeset viewer.