Changeset 1516 for src/utilities


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/utilities
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • 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.