Changeset 1516


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

Ported to syntax of Matita 0.99.1.

Location:
src
Files:
30 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
  • src/Clight/Cexec.ma

    r1244 r1516  
    3636lemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.
    3737#v #ty #r #H elim H; #v #t #H' elim H';
    38   [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?) >(eq_bv_false … ne) //
     38  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
    3939  | #r #b #pc #i #i0 #s %{ true} % //
    4040  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
  • src/Clight/CexecComplete.ma

    r1510 r1516  
    3030
    3131lemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'.
    32 #A #a #v' cases a; // #m whd in ⊢ (% → ?) *;
     32#A #a #v' cases a; // #m whd in ⊢ (% → ?); *;
    3333qed.
    3434
     
    6565inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 #e16
    6666inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 #e26
    67 >e11 in e21 #e1 >(?:ge1 = ge2) in e13 e14
     67>e11 in e21; #e1 >(?:ge1 = ge2) in e13 e14;
    6868[ 2: destruct (e1) skip (e11); @refl ]
    6969#e13 #e14
    7070
    71 >e12 in e22 #e2 destruct (e2) skip (e12);
    72 
    73 >e13 in e23 #e3 >(?:b1 = b2) in e14
     71>e12 in e22; #e2 destruct (e2) skip (e12);
     72
     73>e13 in e23; #e3 >(?:b1 = b2) in e14;
    7474[ >e24 #e4 >(?:f2 = f1)
    7575  [ //;
     
    8888>e2
    8989whd in ⊢ (??%?);
    90 change in e1:(??%?) with (make_global (mk_program ?? globs fns main))
     90change in e1:(??%?); with (make_global (mk_program ?? globs fns main))
    9191>e1
    9292>e3
     
    100100#m #v #ty #ty' #v' #H
    101101elim H;
    102 [ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
     102[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    103103| #m #f #sz #szi #sg @refl
    104 | #m #sz #sz' #sg #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
     104| #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    105105| #m #f #sz #sz' @refl
    106106| #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
    107     elim H1 in pc ⊢ % [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
    108     whd in ⊢ (??%?)
    109     [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?) ]
     107    elim H1 in pc ⊢ %; [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
     108    whd in ⊢ (??%?);
     109    [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?); ]
    110110    elim H2 in pc' ⊢ %; [ 1,4,7: #sp2 #ty2 | 2,5,8: #sp2 #ty2 #n2 | 3,6,9: #tys2 #ty2 letin sp2 ≝ Code ]
    111     #pc' whd in ⊢ (??%?)
     111    #pc' whd in ⊢ (??%?);
    112112    @(dec_true ? (pointer_compat_dec b sp2) pc') //
    113 | #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?)
    114   >intsize_eq_elim_true whd in ⊢ (??%?) cases sz //;
     113| #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?);
     114  >intsize_eq_elim_true whd in ⊢ (??%?); cases sz //;
    115115| #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
    116116    whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
     
    132132lemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ? (exec_bool_of_val v ty) b.
    133133#v #ty #r #H elim H; #v #t #H' elim H';
    134   [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true
     134  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true
    135135    >(eq_bv_false … ne) //
    136136  | #r #b #pc #i #i0 #s %{ true} % //
    137137  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
    138   | #sz #sg %{ false} % // whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //
     138  | #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //
    139139  | #r #r' #t %{ false} % //;
    140140  | #s %{ false} % //; whd; >(Feq_zero_true …) //;
     
    144144lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
    145145#v #ty #H elim H;
    146   [ #i #is #s #ne whd in ⊢ (??%?) >intsize_eq_elim_true >(eq_bv_false … ne) //;
     146  [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //;
    147147  | #p #b #i #i0 #s //
    148148  | #f #s #ne whd; >(Feq_zero_false … ne) //;
     
    152152lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
    153153#v #ty #H elim H;
    154   [ #sz #sg whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //;
     154  [ #sz #sg whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //;
    155155  | #r #r' #t //;
    156156  | #s whd; >(Feq_zero_true …) //;
     
    165165  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
    166166  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
    167 [ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl
     167[ #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl
    168168| #f #ty @refl
    169169| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
    170170    [ #id | #e' | #e' #id ] #H3
    171     whd in ⊢ (??%?)
    172     [ change in H3:(??%?) with (exec_lvalue' ge env m (Evar id) ty)
    173     | change in H3:(??%?) with (exec_lvalue' ge env m (Ederef e') ty)
    174     | change in H3:(??%?) with (exec_lvalue' ge env m (Efield e' id) ty)
     171    whd in ⊢ (??%?);
     172    [ change in H3:(??%?); with (exec_lvalue' ge env m (Evar id) ty)
     173    | change in H3:(??%?); with (exec_lvalue' ge env m (Ederef e') ty)
     174    | change in H3:(??%?); with (exec_lvalue' ge env m (Efield e' id) ty)
    175175    ]
    176176    >(yields_eq ??? H3)
    177     whd in ⊢ (??%?) change in H2:(??%?) with (load_value_of_type' ty m 〈l,off〉)
     177    whd in ⊢ (??%?); change in H2:(??%?); with (load_value_of_type' ty m 〈l,off〉)
    178178    >H2 @refl
    179179| #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
    180     >(yields_eq ??? H2) whd in ⊢ (??%?)
     180    >(yields_eq ??? H2) whd in ⊢ (??%?);
    181181    @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
    182182    @refl
     
    326326[ #env'' #m'' %
    327327| #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3
    328   < H3 whd in H1:(??%?) ⊢ (??%?)
     328  < H3 whd in H1:(??%?) ⊢ (??%?);
    329329  < (pair_eq1 ?????? H1) < (pair_eq2 ?????? H1)
    330330  @refl
     
    337337[ //;
    338338| #env1 #m1 #id #ty #l #v #tl #loc #m2 #m3 #H1 #H2 #H3 #H4
    339     whd in ⊢ (??%?)
     339    whd in ⊢ (??%?);
    340340    >H1 whd in ⊢ (??%?);
    341341    >H2 whd in ⊢ (??%?);
     
    345345lemma eventval_match_complete': ∀ev,ty,v.
    346346  eventval_match ev ty v → yields ? (check_eventval' v ty) ev.
    347 #ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl qed.
     347#ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl qed.
    348348
    349349lemma eventval_list_match_complete: ∀vs,tys,evs.
     
    351351#vs #tys #evs #H elim H;
    352352[ //
    353 | #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?)
    354     >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?)
    355     >(yields_eq ??? H3) whd in ⊢ (??%?) //
     353| #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?);
     354    >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?);
     355    >(yields_eq ??? H3) whd in ⊢ (??%?); //
    356356] qed.
    357357
     
    360360#ge #s #tr #s' #H elim H;
    361361[ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
    362     >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?)
    363     >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?)
    364     change in H3:(??%?) with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v)
     362    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
     363    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
     364    change in H3:(??%?); with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v)
    365365    >H3 @refl
    366366| #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
     
    446446    //
    447447| #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?);
    448     inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2
     448    inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2;
    449449    #H1 #H2
    450450    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
     
    453453| #v #f #env #k #m @refl
    454454| #v #f #env #k #m1 #m2 #loc #ofs #ty
    455     change in ⊢ (??%? → ?) with (store_value_of_type' ty m1 〈loc,ofs〉 v)
    456     #H whd in ⊢ (??%?) >H @refl
     455    change in ⊢ (??%? → ?); with (store_value_of_type' ty m1 〈loc,ofs〉 v)
     456    #H whd in ⊢ (??%?); >H @refl
    457457| #f #l #s #k #env #m @refl
    458458] qed.
  • src/Clight/CexecEquiv.ma

    r1510 r1516  
    5555P (is_final s).
    5656#s #P #F #NF lapply (refl ? (is_final s))
    57 cases (is_final s) in ⊢ (???% → %)
    58 [ #E @NF % * #r #H whd in E:(??%?) > (is_final_complete … H) in E #H destruct
     57cases (is_final s) in ⊢ (???% → %);
     58[ #E @NF % * #r #H whd in E:(??%?); > (is_final_complete … H) in E; #H destruct
    5959| #r #E @F @is_final_sound @E
    6060] qed.
     
    7272>(exec_inf_aux_unfold …) cases x;
    7373[ #o #k #EXEC whd in EXEC:(??%?); destruct
    74 | #y cases y #tr' #s' whd in ⊢ (??%? → ?)
     74| #y cases y #tr' #s' whd in ⊢ (??%? → ?);
    7575  @is_final_elim'
    7676  [ #r #FINAL | #FINAL ]
     
    9898>(exec_inf_aux_unfold …) cases x;
    9999[ #o #k #EXEC whd in EXEC:(??%?); destruct
    100 | #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
     100| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    101101  @is_final_elim' [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
    102102| #msg #EXEC whd in EXEC:(??%?); destruct
     
    120120  cases (se_step_eq … E) * #E1 #E2 #E3 #E4 >E1 >E2 >E3
    121121    >(exec_e_step_inv … H2)
    122     <(exec_e_step … H2) in H1 #H1 % //
     122    <(exec_e_step … H2) in H1; #H1 % //
    123123| #msg #_ #E destruct
    124124| #o #k #i #se #H1 #H2 #E destruct
     
    142142        [ #tr #r #m #E1 #E2 destruct
    143143        | #tr' #s' #e' #se' #H2 #H3 #E2 #_ destruct (E2);
    144             <(exec_e_step … H3) in H2 #H2 % [ 2: @H2 ]
     144            <(exec_e_step … H3) in H2; #H2 % [ 2: @H2 ]
    145145            lapply (STEP i);
    146146            >(exec_e_step_inv … H3)
     
    178178            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    179179                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
    180                 change in match (is_final ?????) with (is_final s2)
     180                change in match (is_final ?????); with (is_final s2)
    181181                @IFE
    182182                [ #r' #FINAL #E whd in E:(??%??);
     
    371371[ #tr #r #m #EXEC #E destruct (E)
    372372| #tr #s' #e #e' #H #EXEC #E destruct (E)
    373 | #msg #EXEC #H #_ generalize in match H -H; generalize in match EXEC -EXEC;
    374   generalize in match msg -msg; >(exec_inf_aux_unfold …)
     373| #msg #EXEC #H #_ generalize in match H; -H; generalize in match EXEC; -EXEC;
     374  generalize in match msg; -msg; >(exec_inf_aux_unfold …)
    375375    cases (exec_step ge s);
    376376  [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct
    377   | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?) @is_final_elim'
     377  | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?); @is_final_elim'
    378378      [ #r ] #F #EXEC whd in EXEC:(??%??); destruct
    379379  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%??); destruct @refl
     
    391391    cases (exec_step ge s);
    392392    [ #o #k #EXEC whd in EXEC:(??%??); destruct
    393     | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?) @is_final_elim'
     393    | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?); @is_final_elim'
    394394        [ #r ] #F #E whd in E:(??%??); destruct @F
    395395    | #msg #E whd in E:(??%??); destruct
     
    420420            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    421421                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
    422                 change in match (is_final ?????) with (is_final s2)
     422                change in match (is_final ?????); with (is_final s2)
    423423                @IFE [ #r ] #F #EXECK
    424424                whd in EXECK:(??%??); destruct;
     
    535535| #f #args #kk #m cases f;
    536536  [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
    537     #x1 #x2 whd in ⊢ (???%) @err_does_not_interact //
     537    #x1 #x2 whd in ⊢ (???%); @err_does_not_interact //
    538538  (* This is the only case that actually matters! *)
    539539  | #fn #argtys #rty whd in ⊢ (???%);
     
    637637[ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO);
    638638| #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?);
    639   [ <(E0_right tr) in ⊢ (?%????)
     639  [ <(E0_right tr) in ⊢ (?%????);
    640640      @isteps_one @isteps_none
    641641  | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *)
     
    643643      @(show_divergence s')
    644644      [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1)
    645         change in ⊢ (?%????) with (Eapp E0 tr1); @isteps_one
     645        change in ⊢ (?%????); with (Eapp E0 tr1); @isteps_one
    646646        @S
    647       | #tr2 #s2 #e2 #S >TR in UNREACTIVE #UNREACTIVE @(UNREACTIVE tr2 s2 e2)
    648           change in ⊢ (?%????) with (Eapp E0 tr2);
     647      | #tr2 #s2 #e2 #S >TR in UNREACTIVE; #UNREACTIVE @(UNREACTIVE tr2 s2 e2)
     648          change in ⊢ (?%????); with (Eapp E0 tr2);
    649649          @isteps_one @S
    650650      | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i)
    651           change in ⊢ (?%????) with (Eapp E0 tr2);
     651          change in ⊢ (?%????); with (Eapp E0 tr2);
    652652          @(isteps_one … S)
    653653      ]
     
    659659    @False_ind @(absurd ?? NOTSILENT)
    660660    @(UNREACTIVE … s' e')
    661     <(E0_right tr') in ⊢ (?%????)
     661    <(E0_right tr') in ⊢ (?%????);
    662662    >EXEC
    663663    @isteps_interact //;
     
    689689    *; #E1 #E2 #H1 destruct (E1);
    690690    lapply (H i); *; #tr' *; #s'' *; #K' #TR
    691     >E2 in H1 #H1 whd in H1:(?%?); >K' in H1
     691    >E2 in H1; #H1 whd in H1:(?%?); >K' in H1;
    692692    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
    693     change in match (is_final ?????) with (is_final s'')
     693    change in match (is_final ?????); with (is_final s'')
    694694    @is_final_elim
    695695    [ #r #F whd in ⊢ (?%? → ?); #S
     
    698698        *; #E1 #E2 #S' <E1 @TR
    699699    ]
    700 | #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?)
     700| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?);
    701701    @is_final_elim' [ #r ] #F #E whd in E:(?%?);
    702702    inversion E;
     
    885885            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    886886                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    887                 cases (H i); #tr1 *; #s1 *; #K #E >K in H2
     887                cases (H i); #tr1 *; #s1 *; #K #E >K in H2;
    888888                >(exec_inf_aux_unfold …)
    889                 whd in ⊢ (?%? → ?) @is_final_elim [ #r ]
     889                whd in ⊢ (?%? → ?); @is_final_elim [ #r ]
    890890                #F #S whd in S:(?%?); cases (se_inv … S);
    891             | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
     891            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
    892892                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    893893                cases (se_inv … S);
     
    902902            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    903903                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    904                 cases (H i); #tr1 *; #s1 *; #K #E >K in H2
     904                cases (H i); #tr1 *; #s1 *; #K #E >K in H2;
    905905                >(exec_inf_aux_unfold …)
    906                 whd in ⊢ (?%? → ?) @is_final_elim [ #r ]
     906                whd in ⊢ (?%? → ?); @is_final_elim [ #r ]
    907907                #F #S whd in S:(?%?); cases (se_inv … S);
    908             | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
     908            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
    909909                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    910910                cases (se_inv … S);
     
    987987  ∃e'.e = e_step ??? E0 s e'.
    988988#ge #s #e >(exec_inf_aux_unfold …)
    989 whd in ⊢ (??%? → ?) @is_final_elim'
     989whd in ⊢ (??%? → ?); @is_final_elim'
    990990[ #r #FINAL #EXEC #NOTFINAL
    991991    @False_ind @(absurd ?? NOTFINAL)
     
    10031003lapply (make_initial_state_sound p)
    10041004lapply (the_initial_state p)
    1005 whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?)
     1005whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?);
    10061006cases (make_initial_state p)
    10071007[ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    10081008    >exec_inf_aux_unfold
    1009     whd in ⊢ (?%? → ?)
     1009    whd in ⊢ (?%? → ?);
    10101010    @is_final_elim'
    10111011    [ #r #F @False_ind
     
    10201020        #ge #Ege
    10211021        inversion MATCHES;
    1022         [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM
     1022        [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM;
    10231023            #TERM
    10241024            lapply (exec_state_terminates … TERM); #E1
    1025             >E1 in TERM #TERM #_
     1025            >E1 in TERM; #TERM #_
    10261026            @(program_terminates (mk_transrel … step) ?? ge s)
    10271027            [ 2: @INITIAL
     
    10301030            | //;
    10311031            ]
    1032         | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES #DIVERGES
     1032        | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES; #DIVERGES
    10331033            lapply (exec_state_diverges … DIVERGES);
    1034             #E1 >E1 in DIVERGES #DIVERGES #_
     1034            #E1 >E1 in DIVERGES; #DIVERGES #_
    10351035            inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6
    1036             <E4 in INITSTEPS ⊢ % <E5 in E6 ⊢ % #E6 #INITSTEPS
     1036            <E4 in INITSTEPS ⊢ %; <E5 in E6 ⊢ %; #E6 #INITSTEPS
    10371037            cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
    1038             #E7 <E7 in INITSTEPS #INITSTEPS
     1038            #E7 <E7 in INITSTEPS; #INITSTEPS
    10391039            cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV #_
    10401040            @(program_diverges (mk_transrel … step) ?? ge s … INITIAL)
     
    10421042            | 3: <Ege @(silent_sound … DIVERGING EXECDIV)
    10431043            ]
    1044         | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS
     1044        | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS; #REACTS
    10451045            lapply (exec_state_reacts … REACTS);
    1046             #E1 >E1 in REACTS #REACTS #_
     1046            #E1 >E1 in REACTS; #REACTS #_
    10471047            inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5
    1048             <E4 in REACTING ⊢ % <E5 #REACTING #E6
     1048            <E4 in REACTING ⊢ %; <E5 #REACTING #E6
    10491049            cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
    1050             #E7 <E7 in REACTING #REACTING #_
     1050            #E7 <E7 in REACTING; #REACTING #_
    10511051            @(program_reacts (mk_transrel … step) ?? ge s … INITIAL)
    10521052            <Ege @(reacts_sound … REACTING EXEC')
    1053         | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG
     1053        | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG; #WRONG
    10541054            lapply (exec_state_wrong … WRONG);
    1055             #E1 >E1 in WRONG #WRONG #_
     1055            #E1 >E1 in WRONG; #WRONG #_
    10561056            inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7
    1057             <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG
     1057            <E4 in GOESWRONG ⊢ %; <E5 <E7 #GOESWRONG
    10581058            cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ]
    1059             #E8 <E8 in GOESWRONG #GOESWRONG
     1059            #E8 <E8 in GOESWRONG; #GOESWRONG
    10601060            elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL
    10611061            <Ege #_
  • src/Clight/CexecSound.ma

    r1510 r1516  
    66cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ]
    77cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
    8 whd in ⊢ (??%? → ?)
     8whd in ⊢ (??%? → ?);
    99[ 2: @intsize_eq_elim_elim
    1010  [ #NE #H destruct
     
    1515  ]
    1616| 8: #H cases (eq_dec f Fzero)
    17   [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
    18   | #ne >Feq_zero_false in H // #E destruct @bool_of_val_true @is_true_float @ne
     17  [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
     18  | #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne
    1919  ]
    2020| 14: #H destruct @bool_of_val_false @is_false_pointer
     
    3535lemma try_cast_null_sound: ∀m,sz,i,ty,ty',v'. try_cast_null m sz i ty ty' = OK ? v' → cast m (Vint sz i) ty ty' v'.
    3636#m #sz #i #ty #ty' #v'
    37 whd in ⊢ (??%? → ?)
     37whd in ⊢ (??%? → ?);
    3838@eq_bv_elim
    3939[ #e >e
     
    5555  | 7,8,9: #a #b #H whd in H:(??%?); destruct;
    5656  | #sz1 #si1 cases ty';
    57     [ whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     57    [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    5858      [ #NE #H destruct
    5959      | *; whd #H whd in H:(??%?); destruct;
    6060      ]
    61     | 3: #a whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     61    | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6262      [ #E #H whd in H:(??%?); destruct
    6363      | *; whd #H whd in H:(??%?); destruct; @cast_if
    6464      ]
    65     | 2,7,8,9: #a #b whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     65    | 2,7,8,9: #a #b whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6666      [ 1,3,5,7: #NE #H destruct
    6767      | *: *; whd #H whd in H:(??%?); destruct; //
     
    7070                 | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
    7171                 | #args #rty letin t ≝ (Tfunction args rty) ]
    72         whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     72        whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    7373        [ 1,3,5: #NE #H destruct
    7474        | *: *; whd
     
    100100    cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
    101101    @cast_pp_z //;
    102 | #r #b #pc #of whd in ⊢ (??%? → ?) #e
     102| #r #b #pc #of whd in ⊢ (??%? → ?); #e
    103103    elim (bind_inversion ????? e) #s * #es #e'
    104104    elim (bind_inversion ????? e') #u * #eu #e'' -e';
     
    113113        | #Hty'
    114114            cut (s = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct.
    115             #e >e in Hty #Hty
    116             cases (pointer_compat_dec b s') in e'''
     115            #e >e in Hty; #Hty
     116            cases (pointer_compat_dec b s') in e''';
    117117            #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
    118118        ]
     
    190190(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
    191191#ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
    192 [ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%)
     192[ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%);
    193193  @eq_intsize_elim #E try @I <E whd %
    194194| #ty #c whd //
     
    197197    @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
    198198    @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
    199     >H in He' #He' @He'
     199    >H in He'; #He' @He'
    200200| #v #ty
    201201    whd in ⊢ (???%);
    202202    lapply (refl ? (lookup SymbolTag block en v))
    203     cases (lookup SymbolTag block en v) in ⊢ (???% → %)
     203    cases (lookup SymbolTag block en v) in ⊢ (???% → %);
    204204    [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
    205205        whd; @(eval_Evar_global … eget efind)
    206206    | #loc #eget @(eval_Evar_local … eget)
    207207    ]
    208 | #ty #e #He whd in ⊢ (???%)
     208| #ty #e #He whd in ⊢ (???%);
    209209    @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
    210     >Hv in He #He
     210    >Hv in He; #He
    211211    @eval_Ederef [ 3: @He | *: skip ]
    212212| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
    213213  cases ty // * #pty
    214   cases loc in H ⊢ % * #loc' #H
     214  cases loc in H ⊢ %; * #loc' #H
    215215  whd try @I
    216   @eval_Eaddrof whd in H:(??%?) >H in He'' #He'' @He''
     216  @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He''
    217217| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
    218218    @opt_bind_OK #v #ev
    219219    @(eval_Eunop … ev)
    220     >Hv1 in He1 #He1 @He1
     220    >Hv1 in He1; #He1 @He1
    221221| #ty #op #e1 #e2 #He1 #He2
    222     @bind2_OK #v1 #tr1 #ev1 >ev1 in He1 #He1
    223     @bind2_OK #v2 #tr2 #ev2 >ev2 in He2 #He2
     222    @bind2_OK #v1 #tr1 #ev1 >ev1 in He1; #He1
     223    @bind2_OK #v2 #tr2 #ev2 >ev2 in He2; #He2
    224224    @opt_bind_OK #v #ev whd in He1 He2; whd;
    225225    @(eval_Ebinop … He1 He2 ev)
    226226| #ty #ty' #e' #He'
    227     @bind2_OK #v #tr #Hv >Hv in He' #He'
     227    @bind2_OK #v #tr #Hv >Hv in He'; #He'
    228228    @bind_OK #v' #ev'
    229229    @(eval_Ecast … He' ?)
     
    231231    @(exec_cast_sound … ev')
    232232| #ty #e1 #e2 #e3 #He1 #He2 #He3
    233     @bind2_OK #vb #tr1 #Hvb >Hvb in He1 #He1
     233    @bind2_OK #vb #tr1 #Hvb >Hvb in He1; #He1
    234234    @bind_OK #b
    235235    cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
    236     @bind2_OK #v #tr #Hv whd in Hv:(??%?)
    237     [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;
     236    @bind2_OK #v #tr #Hv whd in Hv:(??%?);
     237    [ >Hv in He2; #He2 whd in He2 Hv:(??%?) ⊢%;
    238238        @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
    239     | >Hv in He3 #He3 whd in He3 Hv:(??%?) ⊢%;
     239    | >Hv in He3; #He3 whd in He3 Hv:(??%?) ⊢%;
    240240        @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb)
    241241    ]
    242242| #ty #e1 #e2 #He1 #He2
    243     @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
     243    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    244244    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
    245     [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
     245    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    246246        @bind_OK #b2 #eb2
    247247        @(eval_Eandbool_2 … He1 … He2)
     
    250250    ]
    251251| #ty #e1 #e2 #He1 #He2
    252     @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
     252    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    253253    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
    254254    [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1)
    255     | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
     255    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    256256        @bind_OK #b2 #eb2
    257257        @(eval_Eorbool_2 … He1 … He2)
     
    261261| #ty #e' #ty' #i cases ty'; //;
    262262    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
    263         @bind_OK #delta #Hdelta whd in H:(??%?) >H in He' #He'
     263        @bind_OK #delta #Hdelta whd in H:(??%?); >H in He'; #He'
    264264        @(eval_Efield_struct …  He' (refl ??) Hdelta)
    265     | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?)
    266         >H in He' #He'
     265    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?);
     266        >H in He'; #He'
    267267        @(eval_Efield_union … He' (refl ??))
    268268    ]
    269 | #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He' #He'
     269| #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He'; #He'
    270270    @(eval_Ecost … He')
    271271(* exec_lvalue fails on non-lvalues. *)
     
    280280#ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
    281281[ 1,2,5: #a #b #c #H @False_ind destruct (H);
    282 | #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1 #H1 @False_ind
     282| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind
    283283    @(eval_lvalue_inv_ind … H1)
    284284    [ #a #b #c #d #bad destruct (bad);
     
    304304exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
    305305exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉.
    306 #ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?)
    307 >H whd in ⊢ (??%?) cases r @refl
     306#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
     307>H whd in ⊢ (??%?); cases r @refl
    308308qed.
    309309
     
    312312#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
    313313cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    314 [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H
     314[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H
    315315    @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ]
    316316    lapply (addrof_exec_lvalue … H) #H'
     
    350350| * #id #ty #t #IH #en #m #en' #m'
    351351  lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
    352   whd in EXEC:(??%?) ALLOC:(???%)
     352  whd in EXEC:(??%?) ALLOC:(???%);
    353353 @(alloc_variables_cons … ALLOC)
    354354 @IH @EXEC
     
    365365      @opt_bind_OK #m' #STORE
    366366      lapply (refl ? (exec_bind_parameters en m' ps' vs))
    367       cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #msg #_ %]
     367      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %); [2: #msg #_ %]
    368368      #m'' #BIND
    369369      @(bind_parameters_cons … GET STORE)
    370       lapply (IH vs en m') whd in ⊢ (% → ?) >BIND //
     370      lapply (IH vs en m') whd in ⊢ (% → ?); >BIND //
    371371    ]
    372372] qed.
     
    378378| #v #vs #IH *
    379379  [ //
    380   | #ty #tys whd in ⊢ (???%)
     380  | #ty #tys whd in ⊢ (???%);
    381381    cases ty [ #sz #sg | #sz | #r ] cases v //
    382     [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?)
     382    [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);
    383383      @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
    384384    | #v ] @bind_OK #evs #CHECKevs
     
    498498  ]
    499499| #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
    500   [ #fn whd in ⊢ (?????%)
     500  [ #fn whd in ⊢ (?????%);
    501501    lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)))
    502     cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %)
    503     #en' #m' #ALLOC whd in ⊢ (?????%)
     502    cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %);
     503    #en' #m' #ALLOC whd in ⊢ (?????%);
    504504    @res_bindIO_OK #m2 #BIND
    505505    whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
  • src/Clight/casts.ma

    r1489 r1516  
    5454<add_with_carries_unfold
    5555cases (add_with_carries n x y c)
    56 #rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?) >bool_eta //
     56#rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?); >bool_eta //
    5757qed.
    5858
     
    6060  tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y.
    6161#n #hx #hy #x #y
    62 whd in ⊢ (??(???%)%)
     62whd in ⊢ (??(???%)%);
    6363<(add_with_carries_extend n hx hy x y false)
    6464cases (add_with_carries (S n) (hx:::x) (hy:::y) false)
     
    9595#m elim m
    9696[ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs
    97   whd in ⊢ (??%?) >truncate_eq >truncate_eq  @refl
     97  whd in ⊢ (??%?); >truncate_eq >truncate_eq  @refl
    9898| #m' #IH #n #x #y #c
    9999  >(hdtl … x) >(hdtl … y)
    100100  >truncate_head >truncate_head <IH
    101101  <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y))
    102   cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%)
     102  cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%);
    103103  <truncate_tail <truncate_tail @refl
    104104] qed.
     
    106106lemma truncate_plus : ∀m,n,x,y.
    107107  truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y).
    108 #m #n #x #y whd in ⊢ (??(???%)%) <truncate_add_with_carries
     108#m #n #x #y whd in ⊢ (??(???%)%); <truncate_add_with_carries
    109109cases (add_with_carries ????) //
    110110qed.
     
    114114#m0 elim m0
    115115[ #n #x >truncate_eq //
    116 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
     116| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
    117117] qed.
    118118
    119119theorem zero_plus_reduce : ∀m,n,x,y.
    120120  truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y.
    121 #m #n #x #y <(truncate_pad m n x) in ⊢ (???%) <(truncate_pad m n y) in ⊢ (???%)
     121#m #n #x #y <(truncate_pad m n x) in ⊢ (???%); <(truncate_pad m n y) in ⊢ (???%);
    122122@truncate_plus
    123123qed.
     
    130130#m0 elim m0
    131131[ #n #x >truncate_eq //
    132 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
     132| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
    133133] qed.
    134134
    135135theorem sign_plus_reduce : ∀m,n,x,y.
    136136  truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y.
    137 #m #n #x #y <(truncate_sign m n x) in ⊢ (???%) <(truncate_sign m n y) in ⊢ (???%)
     137#m #n #x #y <(truncate_sign m n x) in ⊢ (???%); <(truncate_sign m n y) in ⊢ (???%);
    138138@truncate_plus
    139139qed.
     
    171171  <add_with_carries_unfold
    172172  cases (add_with_carries n x y c)
    173   #lb #cs whd in ⊢ (??%%) >bool_eta
     173  #lb #cs whd in ⊢ (??%%); >bool_eta
    174174  //
    175175| *: skip
     
    181181#m #n #x @(vector_inv_n … x) #h #t elim n
    182182[ @refl
    183 | #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
     183| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?); >IH @refl
    184184] qed.
    185185
     
    201201lemma zero_negate_reduce : ∀m,n,x.
    202202  truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x.
    203 #m #n #x whd in ⊢ (??(???%)%)
     203#m #n #x whd in ⊢ (??(???%)%);
    204204lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
    205205cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
    206 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     206#rs #cs whd in ⊢ (??%? → ??(???%)?);
    207207>truncate_negation_bv
    208208>truncate_pad >truncate_zero cases (add_with_carries ????)
     
    212212lemma sign_negate_reduce : ∀m,n,x.
    213213  truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x.
    214 #m #n #x whd in ⊢ (??(???%)%)
     214#m #n #x whd in ⊢ (??(???%)%);
    215215>sign_bitflip <(zero_sign (S n) m)
    216216lapply (truncate_add_with_carries m (S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
    217217cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
    218 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     218#rs #cs whd in ⊢ (??%? → ??(???%)?);
    219219>truncate_sign >truncate_sign cases (add_with_carries ????)
    220220#rs' #cs' #E destruct //
     
    224224  truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y.
    225225#m #n #x #y
    226 whd in ⊢ (??(???%)%)
     226whd in ⊢ (??(???%)%);
    227227lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
    228228cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
    229 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     229#rs #cs whd in ⊢ (??%? → ??(???%)?);
    230230>zero_negate_reduce >truncate_pad
    231231cases (add_with_carries ????)
     
    236236  truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y.
    237237#m #n #x #y
    238 whd in ⊢ (??(???%)%)
     238whd in ⊢ (??(???%)%);
    239239lapply (truncate_add_with_carries m (S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
    240240cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
    241 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     241#rs #cs whd in ⊢ (??%? → ??(???%)?);
    242242>sign_negate_reduce >truncate_sign
    243243cases (add_with_carries ????)
  • src/Clight/toCminor.ma

    r1515 r1516  
    122122  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
    123123#var #id #r #id'
    124 whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
     124whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
    125125cases (identifier_eq ? id id')
    126 [ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
     126[ #E >E >lookup_add_hit whd in ⊢ (% → ?); *
    127127| #NE >lookup_add_miss /2/
    128128] qed.
     
    131131  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
    132132#vars #id #t #id' #NE
    133 whd in ⊢ (% → %)
    134 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
     133whd in ⊢ (% → %);
     134whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
    135135>lookup_add_miss
    136136[ #H @H | /2/ ]
     
    142142      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
    143143#globals #f
    144 whd in ⊢ (∀_.∀_.??%? → ?)
     144whd in ⊢ (∀_.∀_.??%? → ?);
    145145elim (fn_params f @ fn_vars f)
    146 [ #vars #n whd in ⊢ (??%? → ?) #E destruct #i #H @False_ind
    147   elim globals in H
     146[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H @False_ind
     147  elim globals in H;
    148148  [ normalize //
    149   | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
     149  | * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ???? H)
    150150  ]
    151 | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
     151| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
    152152  cases (identifier_eq ? id i)
    153153  [ #E' <E' #H % @refl
    154154  | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
    155     whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
    156     cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
     155    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     156    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    157157    #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    158158    @(IH m0 n0)
    159     [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
     159    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
    160160    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
    161161    ]
     
    348348  expr_vars ? e P.
    349349#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
    350 whd in ⊢ (??%? → ?)
     350whd in ⊢ (??%? → ?);
    351351[ cases (classify_add ty1 ty2)
    352   [ 3,4: #z ] whd in ⊢ (??%? → ?)
    353   [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     352  [ 3,4: #z ] whd in ⊢ (??%? → ?);
     353  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    354354    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    355355    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
    356   | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     356  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    357357    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    358358    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
     
    360360  ]
    361361| cases (classify_sub ty1 ty2)
    362   [ 3,4: #z] whd in ⊢ (??%? → ?)
    363   [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     362  [ 3,4: #z] whd in ⊢ (??%? → ?);
     363  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    364364    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    365365    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
     
    737737  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
    738738#tmp #g #g' #vars #q
    739 whd in ⊢ (???% → ?) #E
     739whd in ⊢ (???% → ?); #E
    740740#id #H
    741741cases (identifier_eq ? id tmp)
    742742destruct #E
    743 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
     743whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
    744744[ >E >lookup_add_hit @I
    745745| cases E #NE >lookup_add_miss [ @H | /2/
     
    765765lemma local_id_add_local_oblivious : ∀vars,id,id'.
    766766  local_id vars id → local_id (add ?? vars id' Local) id.
    767 #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     767#vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    768768cases (identifier_eq ? id id')
    769769[ #E >E >lookup_add_hit @I
     
    791791  〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
    792792#tmp #u #q #u0 #vars
    793 whd in ⊢ (???% → ?) #E
     793whd in ⊢ (???% → ?); #E
    794794destruct
    795 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
     795whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
    796796@I
    797797qed.
     
    987987lemma lookup_label_add : ∀lbls,l,l'.
    988988  lookup_label (add … lbls l l') l = OK ? l'.
    989 #lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl
     989#lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl
    990990qed.
    991991
     
    994994  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
    995995#lbls #l #l' #l0 #NE
    996 whd in ⊢ (??%%)
     996whd in ⊢ (??%%);
    997997>lookup_add_miss
    998998[ @refl | @NE ]
     
    10121012].
    10131013[ #l #l' #H %2 @H
    1014 | cases lbls1 #lbls' #I whd in ⊢ (??%?)
     1014| cases lbls1 #lbls' #I whd in ⊢ (??%?);
    10151015  #l1 #l1' #E1 @(eq_identifier_elim … l l1)
    10161016  [ #E %1 %1 @E
    10171017  | #NE cases (I l1 l1' E1)
    10181018    [ #H %1 %2 @H
    1019     | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H
     1019    | #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H
    10201020    ]
    10211021  ]
     
    10271027  OK ? «lbls, ?».
    10281028#l #l' #E cases (H l l' E) //
    1029 whd in ⊢ (??%? → ?) #H destruct
     1029whd in ⊢ (??%? → ?); #H destruct
    10301030qed.
    10311031
     
    10341034  local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
    10351035#vars #tmpgen #i
    1036 whd in ⊢ (?%? → ?)
     1036whd in ⊢ (?%? → ?);
    10371037elim (tmp_env tmpgen)
    10381038[ #H %1 @H
     
    10861086  #l * #l' #LOOKUP
    10871087  lapply (Ilbls l' l LOOKUP) #DEFINED
    1088   cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
     1088  cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex)
    10891089  #H @H
    10901090] qed.
  • src/Cminor/initialisation.ma

    r1401 r1516  
    5555| elim init
    5656  [ % //
    57   | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
     57  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
    5858] qed.
    5959
     
    6666lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
    6767#s elim s //
    68 [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
     68[ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
    6969  >(IH1 H1) >(IH2 H2) @refl
    70 | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
     70| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
    7171  >(IH1 H1) >(IH2 H2) @refl
    7272| #s #IH * * #_ #_ #H @(IH H)
     
    103103  ]
    104104  ]
    105 | whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f)
     105| whd in ⊢ (?(λ_.??(?(λ_.???%)?))?); >(no_labels … H) @(f_inv f)
    106106] qed.
    107107
  • src/Cminor/semantics.ma

    r1369 r1516  
    185185#l #s elim s
    186186try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) )
    187 [ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
     187[ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
    188188  lapply (IH1 (Kseq s2 k) f en (π2 (π1 Inv)) (conj ?? (π2 Inv) kInv))
    189189  cases (find_label l s1 (Kseq s2 k) f en ??)
    190   [ #H1 whd in ⊢ (??%? → ?)
     190  [ #H1 whd in ⊢ (??%? → ?);
    191191    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
    192192    [ #H2 #_ % #H cases (Exists_append … H)
     
    198198  | #sk #_ #E whd in E:(??%?); destruct
    199199  ]
    200 | #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
     200| #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
    201201  lapply (IH1 k f en (π2 (π1 Inv)) kInv)
    202202  cases (find_label l s1 k f en ??)
    203   [ #H1 whd in ⊢ (??%? → ?)
     203  [ #H1 whd in ⊢ (??%? → ?);
    204204    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
    205205    [ #H2 #_ % #H cases (Exists_append … H)
     
    214214| #s1 #IH #k #f #en #Inv #kInv @IH
    215215| #E whd in i:(??%?); cases (identifier_eq Label l a) in i;
    216   whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
     216  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
    217217| whd in i:(??%?); cases (identifier_eq Label l a) in i;
    218   whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ]
     218  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ]
    219219| #cl #s1 #IH #k #f #en #Inv #kInv @IH
    220220] qed.
  • src/Cminor/toRTLabs.ma

    r1515 r1516  
    2323[ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
    2424| * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
    25   * [ whd in ⊢ (??%? → ?) #E1 <E1
    26       generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
    27       whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
     25  * [ whd in ⊢ (??%? → ?); #E1 <E1
     26      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z
     27      whd in ⊢ (??%? → ?); elim (fresh RegisterTag z) #r #gen' #E
    2828      whd in E:(??%?); destruct;
    2929      whd >lookup_add_hit % #A destruct
    30     | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
     30    | #H change in E:(??(match % with [ _ ⇒ ? ])?); with (populate_env e u tl)
    3131      lapply (refl ? (populate_env e u tl))
    32       cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)
    33       * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
    34       whd in ⊢ (??%? → ?) #E destruct
     32      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
     33      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?); cases (fresh RegisterTag u1) #r #u''
     34      whd in ⊢ (??%? → ?); #E destruct
    3535      @lookup_add_oblivious
    3636      @(IH … E1 ? H)
     
    4444[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
    4545| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
    46   change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl)
     46  change in E:(??(match % with [ _ ⇒ ?])?); with (populate_env e u tl)
    4747  lapply (refl ? (populate_env e u tl))
    48   cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0
    49   >E0 in E; whd in ⊢ (??%? → ?) #E
     48  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
     49  >E0 in E; whd in ⊢ (??%? → ?); #E
    5050  destruct
    5151  #i #H @lookup_add_oblivious @(IH … E0) @H
     
    6464#ls elim ls
    6565[ #lbls #u #lbls' #u' #E #l *
    66 | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
    67   change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
     66| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
     67  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
    6868  lapply (refl ? (populate_label_env lbls u t))
    69   cases (populate_label_env lbls u t) in ⊢ (???% → %)
    70   #lbls1 #u1 #E1 whd in ⊢ (??%? → ?)
     69  cases (populate_label_env lbls u t) in ⊢ (???% → %);
     70  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
    7171  #E destruct
    7272  #l *
     
    8181#ls elim ls
    8282[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
    83 | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
    84   change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
     83| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
     84  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
    8585  lapply (refl ? (populate_label_env lbls u t))
    86   cases (populate_label_env lbls u t) in ⊢ (???% → %)
    87   #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) 
     86  cases (populate_label_env lbls u t) in ⊢ (???% → %);
     87  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
    8888  #E destruct
    8989  #l #H cases (identifier_eq ? l h)
    9090  [ #El %1 %1 @El
    9191  | #NE cases (IH … E1 l ?)
    92     [ #H' %1 %2 @H' | #H' %2 @H' | whd in H >lookup_add_miss in H //  ]
     92    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H; >lookup_add_miss in H; //  ]
    9393  ]
    9494] qed.
     
    149149#le #l #s #f #p
    150150#l' #s' #H cases (identifier_eq … l l')
    151 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     151[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
    152152  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
    153153| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
    154154  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    155   | >lookup_add_miss in H /2/
     155  | >lookup_add_miss in H; /2/
    156156  ]
    157157] qed.
     
    205205#le #l #s #f #p
    206206#l' #s' #H cases (identifier_eq … l l')
    207 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     207[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
    208208  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    209209| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
    210210  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    211   | >lookup_add_miss in H /2/
     211  | >lookup_add_miss in H; /2/
    212212  ]
    213213] qed.
     
    273273#le #env #es #f elim es
    274274[ #p #rs #f normalize #E destruct @refl
    275 | * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
     275| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?); #E
    276276  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
    277277  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
     
    453453#lenv #l #l' #p
    454454cut (∃lx. lookup ?? lenv l = Some ? lx)
    455 [ whd in p; cases (lookup ?? lenv l) in p ⊢ %
     455[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
    456456  [ * #H cases (H (refl ??))
    457457  | #lx #_ %{lx} @refl
    458458  ]
    459 | * #lx #E whd in ⊢ (??%? → ?) cases p >E #q whd in ⊢ (??%? → ?) #E' >E' @refl
     459| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
    460460] qed.
    461461
     
    478478  labels_of s = labels_of s' → Cminor_labels_added le s' f →
    479479  Cminor_labels_added le s f.
    480 #le #s #s' #f #E whd in ⊢ (% → %) > E #H @H
     480#le #s #s' #f #E whd in ⊢ (% → %); > E #H @H
    481481qed.
    482482
     
    621621try (#l #H @H)
    622622[ -f @(choose_regs_length … (sym_eq … Eregs))
    623 | whd in Env @(π1 (π1 (π1 Env)))
     623| whd in Env; @(π1 (π1 (π1 Env)))
    624624| -f @(choose_regs_length … (sym_eq … Eregs))
    625625| #l #H cases (Exists_append … H)
     
    709709  | cases (label_env_contents … (sym_eq ??? El) l ?)
    710710    [ #H @H
    711     | whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) * #H cases (H (refl ??))
     711    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
    712712    | whd >H % #E' destruct (E')
    713713    ]
     
    716716| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
    717717  [ * #E1 #E2 >E2 @I
    718   | whd in ⊢ (??%? → ?) #E' destruct (E')
     718  | whd in ⊢ (??%? → ?); #E' destruct (E')
    719719  ]
    720720| *: whd >lookup_add_hit % #E destruct
  • src/RTL/RTLToERTL.ma

    r1481 r1516  
    359359  let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
    360360   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
    361 whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
     361whd in match ertl_params; (* CSC: Matita's bug here; not enough/too much reduction
    362362                                 makes the next application fail. Why? *)   
    363363%
  • src/common/AST.ma

    r1465 r1516  
    145145lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
    146146  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
    147 * * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct
     147* * #P #Hne #Heq whd in ⊢ (?%); try (@Heq @refl) @Hne % #E destruct
    148148qed.
    149149
     
    175175  (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d).
    176176#A * * #P #p #f #d #Q #Hne #Heq
    177 [ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))
    178 | *: whd in ⊢ (?%) @Hne % #E destruct
     177[ 1,5,9: whd in ⊢ (?%); @(Heq (refl ??))
     178| *: whd in ⊢ (?%); @Hne % #E destruct
    179179] qed.
    180180
     
    351351 #A #B #C #f #l elim l
    352352  [ #l' #E normalize in E; destruct %
    353   | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)
     353  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?);
    354354    [2: #err #E destruct
    355355    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
    356       cases (map_partial … f tl) in IH ⊢ %
    357       #x #IH normalize in ⊢ (??%? → ?) #ABS destruct normalize
     356      cases (map_partial … f tl) in IH ⊢ %;
     357      #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize
    358358      >(IH x) // ]]
    359359qed.
     
    487487 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
    488488 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
    489    #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct normalize in e1 ⊢ % >e0 //
     489   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 //
    490490   >e0 in e1; normalize #H @H ]
    491491qed.
     
    498498  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
    499499  (*CSC: interactive mode because of dependent types *)
    500   generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p))
     500  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
    501501  cases (map_partial … transf_partial_variable (prog_vars … p))
    502502  [ #vl #EQ
  • src/common/Events.ma

    r961 r1516  
    155155  ].
    156156[ *; #NE @False_rect_Type0 @NE @refl
    157 | % #E' >E' in E #E whd in E:(??%%); destruct (E);
     157| % #E' >E' in E; #E whd in E:(??%%); destruct (E);
    158158] qed.
    159159
  • src/common/FrontEndOps.ma

    r1410 r1516  
    139139  val_typ v' t'.
    140140#t #t' #op elim op
    141 [ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?)
    142   cases sg whd in ⊢ (??%? → ?) #E' destruct %
    143 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E' destruct %
     141[ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?);
     142  cases sg whd in ⊢ (??%? → ?); #E' destruct %
     143| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E' destruct %
    144144| #t'' #sz #sg cases t''
    145   [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?) #E' destruct cases (eq_bv ???) whd in ⊢ (?%?) %
     145  [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?); #E' destruct cases (eq_bv ???) whd in ⊢ (?%?); %
    146146  | #r #H #v #v' #H1 @(elim_val_typ … H1) whd %
    147     [ whd in ⊢ (??%? → ?) #E' destruct; %
    148     | #b #c #o whd in ⊢ (??%? → ?) #E' destruct %
     147    [ whd in ⊢ (??%? → ?); #E' destruct; %
     148    | #b #c #o whd in ⊢ (??%? → ?); #E' destruct %
    149149    ]
    150150  | #f *
    151151  ]
    152 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %
    153 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
    154 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
    155 | #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
    156 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %
    157 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %
    158 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2
    159 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2
    160 | #t'' #v #v' #H whd in ⊢ (??%? → ?) #E destruct @H
    161 | #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) cases (eq_bv ???)
    162   whd in ⊢ (??%? → ?) #E destruct //
     152| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %
     153| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     154| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     155| #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     156| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
     157| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
     158| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
     159| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
     160| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
     161| #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
     162  whd in ⊢ (??%? → ?); #E destruct //
    163163| #sz #sg #r #v #v' #H @(elim_val_typ … H) %
    164   [ whd in ⊢ (??%? → ?) #E destruct %
    165   | #b #c #o whd in ⊢ (??%? → ?) #E destruct
     164  [ whd in ⊢ (??%? → ?); #E destruct %
     165  | #b #c #o whd in ⊢ (??%? → ?); #E destruct
    166166  ]
    167167] qed.
  • src/common/GenMem.ma

    r1395 r1516  
    5353  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    5454  update_block … x v f x = v.
    55 #A * * #ix #v #f whd in ⊢ (??%?)
     55#A * * #ix #v #f whd in ⊢ (??%?);
    5656>eq_block_b_b //
    5757qed.
  • src/common/Identifiers.ma

    r1515 r1516  
    5656
    5757lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true.
    58 #tag * #id whd in ⊢ (??%?) >eqb_n_n @refl
     58#tag * #id whd in ⊢ (??%?); >eqb_n_n @refl
    5959qed.
    6060
     
    6464
    6565definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
    66 #tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %)
     66#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %);
    6767#E [ % | %2 ]
    6868lapply E @eqb_elim
     
    184184  ] (refl ? u').
    185185cases l in p E; cases m; -l' -m' #m' #l'
    186 whd in ⊢ (% → ?)
    187  whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?)
     186whd in ⊢ (% → ?);
     187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?);
    188188#NL #U cases NL #H @H @(update_fail … U)
    189189qed.
     
    194194  present tag A (update_present tag A m id' H' a) id.
    195195#tag #A * #m * #id #a * #id' #H #H'
    196 whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
     196whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta
    197197cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
    198 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ????? U)
     198[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U)
    199199  % #E' destruct
    200 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(??%%)?))
     200| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?));
    201201  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
    202202] qed.
  • src/common/Integers.ma

    r1512 r1516  
    124124
    125125lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y).
    126 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?) #E
     126#x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?); #E
    127127[ %1 lapply E @(eq_bv_elim … x y) [ // | #_ #X destruct ]
    128128| %2 lapply E @(eq_bv_elim … x y) [ #_ #X destruct | /2/ ]
  • src/common/Mem.ma

    r891 r1516  
    6666  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    6767  update_block … x v f x = v.
    68 #A * * #ix #v #f whd in ⊢ (??%?)
     68#A * * #ix #v #f whd in ⊢ (??%?);
    6969>eq_block_b_b //
    7070qed.
     
    192192lemma align_size_chunk_divides:
    193193  ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
    194 #chunk cases chunk;[8:#r cases r ]normalize;/3/;
     194#chunk cases chunk;[8:#r cases r ]normalize;/3 by witness/;
    195195qed.
    196196
     
    735735lemma valid_not_valid_diff:
    736736  ∀m,b,b'. valid_block m b →  ¬(valid_block m b') → b ≠ b'.
    737 #m #b #b' #H #H' @nmk #e >e in H #H
     737#m #b #b' #H #H' @nmk #e >e in H; #H
    738738@(absurd ? H H')
    739739qed.
     
    759759#m #chunk #chunk2 #r #b #ofs #H1 #H2
    760760elim H2;#H3 #H4 #H5 #H6 #H7
    761 >H1 in H5 #H5
     761>H1 in H5; #H5
    762762% //;
    763763<(align_chunk_compat … H1) //;
     
    807807#b' cases (store_inv … STORE)
    808808#H1 #H2 >H2
    809 whd in ⊢ (??(?%?)?) whd in ⊢ (??%?)
    810 whd in ⊢ (??(?%)?) @eq_block_elim #E
     809whd in ⊢ (??(?%?)?); whd in ⊢ (??%?);
     810whd in ⊢ (??(?%)?); @eq_block_elim #E
    811811normalize //
    812812qed.
     
    864864#chunk #m1 #r #b #ofs #v #m2 #STORE
    865865#chunk' #r' #b' #ofs'
    866 * Hv;
     866* as Hv
    867867#Hvb #Hl #Hr #Halign #Hptr
    868868% //;
     
    878878#chunk #m1 #r #b #ofs #v #m2 #STORE
    879879#chunk' #r' #b' #ofs'
    880 * Hv;
     880* as Hv
    881881#Hvb #Hl #Hr #Halign #Hcompat
    882882% //;
     
    35143514  ∀m,a,v.
    35153515  storev Mint8signed m a v = storev Mint8unsigned m a v.
    3516 #m #a #v whd in ⊢ (??%%) elim a //
    3517 #r #b #p #ofs whd in ⊢ (??%%)
     3516#m #a #v whd in ⊢ (??%%); elim a //
     3517#r #b #p #ofs whd in ⊢ (??%%);
    35183518>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
    35193519qed.
     
    35223522  ∀m,a,v.
    35233523  storev Mint16signed m a v = storev Mint16unsigned m a v.
    3524 #m #a #v whd in ⊢ (??%%) elim a //
    3525 #r #b #p #ofs whd in ⊢ (??%%)
     3524#m #a #v whd in ⊢ (??%%); elim a //
     3525#r #b #p #ofs whd in ⊢ (??%%);
    35263526>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
    35273527qed.
  • src/common/Pointers.ma

    r1215 r1516  
    3434  P (eq_block b1 b2).
    3535#P * #r1 #i1 * #r2 #i2 #H1 #H2
    36 whd in ⊢ (?%) @eq_region_elim #H3
    37 [ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
     36whd in ⊢ (?%); @eq_region_elim #H3
     37[ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
    3838| @H2 % #E destruct elim H3 /2/
    3939] qed.
    4040
    4141lemma eq_block_b_b : ∀b. eq_block b b = true.
    42 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl
     42* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
    4343qed.
    4444
     
    7171
    7272lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
    73  whd in match eq_offset /2/
     73 whd in match eq_offset; /2/
    7474qed.
    7575
     
    109109
    110110lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true.
    111  #p whd in ⊢ (??%?) >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
     111 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
    112112qed.
  • src/common/PositiveMap.ma

    r1515 r1516  
    6262[ * //
    6363| #tl #IH *
    64   [ whd in ⊢ (??%%) @IH
     64  [ whd in ⊢ (??%%); @IH
    6565  | #x #l #r @IH
    6666  ]
    6767| #tl #IH *
    68   [ whd in ⊢ (??%%) @IH
     68  [ whd in ⊢ (??%%); @IH
    6969  | #x #l #r @IH
    7070  ]
     
    8080| #b' #IH *
    8181  [ * [ #NE @refl | #x #l #r #NE @refl ]
    82   | #c' * [ #NE whd in ⊢ (??%%) @IH /2/
    83           | #x #l #r #NE whd in ⊢ (??%%) @IH /2/
     82  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
     83          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
    8484          ]
    8585  | #c' * //
     
    8888  [ * [ #NE @refl | #x #l #r #NE @refl ]
    8989  | #c' * //
    90   | #c' * [ #NE whd in ⊢ (??%%) @IH /2/
    91           | #x #l #r #NE whd in ⊢ (??%%) @IH /2/
     90  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
     91          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
    9292          ]
    9393  ]
     
    110110[ * [ // | * // #x #l #r normalize #E destruct ]
    111111| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
    112                    cases (update A b' a r) in U ⊢ %
     112                   cases (update A b' a r) in U ⊢ %;
    113113                   [ // | normalize #t #E destruct ]
    114114            ]
    115115| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
    116                    cases (update A b' a l) in U ⊢ %
     116                   cases (update A b' a l) in U ⊢ %;
    117117                   [ // | normalize #t #E destruct ]
    118118            ]
     
    124124#A #b #a elim b
    125125[ * [ #t' normalize #E destruct
    126     | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?)
     126    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?);
    127127      #E destruct //
    128128    ]
    129129| #b' #IH *
    130130  [ #t' normalize #E destruct
    131   | #x #l #r #t' whd in ⊢ (??%? → ??%?)
     131  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
    132132    lapply (IH r)
    133133    cases (update A b' a r)
     
    138138| #b' #IH *
    139139  [ #t' normalize #E destruct
    140   | #x #l #r #t' whd in ⊢ (??%? → ??%?)
     140  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
    141141    lapply (IH l)
    142142    cases (update A b' a l)
  • src/joint/BEValues.ma

    r1395 r1516  
    7474  [ O ⇒ λ_.[]
    7575  | S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n).
    76 /3/ qed.
     76/3/ (*Andrea: by _ cannot be re-parsed*) qed.
    7777
    7878definition bevals_of_pointer: pointer → list beval ≝
     
    8484* * #pbl #pok #poff
    8585try %
    86 whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]
    87 whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 2) %
     86whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]
     87whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 2) %
    8888qed.
    8989
  • src/joint/TranslateUtils.ma

    r1515 r1516  
    2121 #pars0 #globals #def #n elim n
    2222  [ %
    23   | #m whd in ⊢ (? → ??(??%)?) whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?)
     23  | #m whd in ⊢ (? → ??(??%)?); whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) ;
    2424    cases (fresh_regs pars0 globals def m) normalize nodelta
    25     #def' #regs #EQ change in EQ with (|regs| = m) <EQ
     25    #def' #regs #EQ change in EQ; with (|regs| = m) <EQ
    2626    @refl
    2727 ]
  • src/utilities/extralib.ma

    r1515 r1516  
    120120
    121121lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
    122 #x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     122#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
    123123/3/ qed.
    124124
    125125lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
    126 #x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
    127 whd in ⊢ (% → ??%) /3/ qed.
     126#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     127whd in ⊢ (% → ??%); /3/ qed.
    128128
    129129theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
     
    224224
    225225theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
    226 #n #m #H % #H' >(Zle_to_Zleb_true … H') in H #H destruct;
     226#n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct;
    227227qed.
    228228
     
    244244
    245245theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
    246 #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H #H destruct;
     246#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct;
    247247qed.
    248248
     
    540540          lapply (partial_minus_to_Prop md'' n);
    541541          cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
    542           #lt #e destruct % [ normalize /3/ | *: normalize /2/ ] @plt_pos
     542          #lt #e destruct % [ normalize /3 by le_to_le_to_eq, le_n, eq_f/ | *: normalize /2 by plt_zero, plt_pos/ ] @plt_pos
    543543          [ 1,3,5,7: @double_lt1 /2/;
    544544          | 2,4: @double_lt3 /2/;
     
    583583cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ]
    584584cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
    585 >DIV in ⊢ (% → ?) #H #lt destruct;
     585>DIV in ⊢ (% → ?); #H #lt destruct;
    586586[ lapply (plus_to_minus … e0);
    587587    >(commutative_times …) >(commutative_times dv'' …)
  • src/utilities/extranat.ma

    r1515 r1516  
    2424#n elim n
    2525[ @refl
    26 | #m #IH whd in ⊢ (??%?) > IH @refl
     26| #m #IH whd in ⊢ (??%?); >IH @refl
    2727] qed.
    2828
     
    3030#n #m elim n
    3131[ //
    32 | #n' #IH whd in ⊢ (??%?) > IH @refl
     32| #n' #IH whd in ⊢ (??%?); >IH @refl
    3333] qed.
    3434
     
    3636#n #m elim m
    3737[ //
    38 | #m' #IH whd in ⊢ (??%?) > IH @refl
     38| #m' #IH whd in ⊢ (??%?); >IH @refl
    3939] qed.
    4040
     
    5252
    5353lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.
    54 #m #n #o #H whd in ⊢ (??%) @leb_elim #H'
     54#m #n #o #H whd in ⊢ (??%); @leb_elim #H'
    5555[ @(transitive_le ? m ? H H')
    5656| @H
     
    5858
    5959lemma max_r : ∀m,n,o:nat. o ≤ n → o ≤ max m n.
    60 #m #n #o #H whd in ⊢ (??%) @leb_elim #H'
     60#m #n #o #H whd in ⊢ (??%); @leb_elim #H'
    6161[ @H
    6262| @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) //
  • src/utilities/lists.ma

    r1451 r1516  
    2929| #m #IH *
    3030  [ #_ #a #E whd in E:(??%?); destruct
    31   | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?) @IH
     31  | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
    3232  ]
    3333] qed.
Note: See TracChangeset for help on using the changeset viewer.