Changeset 1517


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

Ported to syntax of Matita 0.99.1.

Location:
src/utilities/binary
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/Z.ma

    r891 r1517  
    237237   |#m cases z
    238238      [//
    239       |#p apply transitive_lt (* XXX: auto??? *)
     239      |#p @transitive_lt (* XXX: auto??? *)
    240240      |//]
    241241   |#m #Hl cases Hl]
     
    249249   |#m cases z
    250250      [1,2://
    251       |#p #Hl #Hr apply (transitive_lt … Hr Hl)]
     251      |#p #Hl #Hr @(transitive_lt … Hr Hl)]
    252252   ]
    253253]
     
    463463   [//
    464464   |//
    465    |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n
     465   |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n
    466466      cases (pos_compare q p);//]
    467467|#p cases y
    468468   [//;
    469    |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n
     469   |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n
    470470      cases (pos_compare q p);//
    471471   |normalize;//]
     
    503503  ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
    504504#n #m
    505 whd in ⊢ (??%%) 
     505whd in ⊢ (??%%);
    506506<(pos_compare_S_S …)
    507507>(minus_S_S …)
     
    522522[ //;
    523523| #m' >Zpred_pos_succ
    524     change in ⊢ (??(??%)?) with (Zsucc (pos m'))
     524    change in ⊢ (??(??%)?); with (Zsucc (pos m'))
    525525    <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
    526 | #m' whd in ⊢ (??%%) >pos_compare_S_one normalize;
     526| #m' whd in ⊢ (??%%); >pos_compare_S_one normalize;
    527527    >partial_minus_S_one normalize; >pos_nonzero
    528528    <pred_succ_n //
    529 | #m' #n' whd in ⊢ (??%%) <pos_compare_S_S
     529| #m' #n' whd in ⊢ (??%%); <pos_compare_S_S
    530530    >minus_S_S
    531531    >minus_S_S normalize
     
    601601
    602602lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
    603 #n #m whd in ⊢ (??%%) <pos_compare_S_S
     603#n #m whd in ⊢ (??%%); <pos_compare_S_S
    604604>minus_S_S >minus_S_S
    605605 //; qed.
     
    676676#x #y cases x
    677677[cases y;//
    678 |*:#n cases y;//;#m whd in ⊢ (??(?%)%) @pos_compare_elim normalize;//]
     678|*:#n cases y;//;#m whd in ⊢ (??(?%)%); @pos_compare_elim normalize;//]
    679679qed.
    680680
     
    686686#x cases x
    687687[//
    688 |*:#n whd in ⊢ (??%?) >pos_compare_n_n //]
     688|*:#n whd in ⊢ (??%?); >pos_compare_n_n //]
    689689qed.
    690690
  • src/utilities/binary/positive.ma

    r1515 r1517  
    213213#n elim n; normalize;
    214214[ //
    215 | 2,3: #n' #IH #m cases m; /3/;
    216     normalize; cases n'; //;
     215| 2,3: #n' #IH #m cases m; /3 by eq_f, sym_eq/
     216    normalize; cases n' //
    217217] qed.
    218218
     
    284284@pos_elim
    285285[ //
    286 | #n #IH #m <(times_succn_m …) <(times_succn_m …) /3/;
     286| #n #IH #m <(times_succn_m …) <(times_succn_m …) /3 by succ_injective, trans_eq/
    287287] qed.
    288288
     
    449449
    450450theorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m.
    451 @pos_elim2 /4/;
     451@pos_elim2 /4 by le_n_one_to_eq, monotonic_pred, eq_f, sym_eq/
    452452qed.
    453453
     
    913913#n #m #p #lep
    914914@transitive_le
    915   [|apply le_plus_minus_m_m
     915  [|@le_plus_minus_m_m
    916916  |@monotonic_le_plus_l //;
    917917  ]
     
    11381138
    11391139theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m.
    1140 (* sic
    1141 #n #m #H elim H
    1142 [//
    1143 |/2/] *)
    11441140/2/; qed.
    11451141
    11461142lemma cmp_nat: ∀n,m:Pos.cmp_cases n m.
    11471143#n #m lapply (pos_compare_to_Prop n m)
    1148 cases (pos_compare n m);normalize; /3/;
     1144cases (pos_compare n m);normalize; /3 by lt_times_n_to_lt_l, le_n, cmp_le, cmp_gt, lt_to_le/
    11491145qed.
    11501146
Note: See TracChangeset for help on using the changeset viewer.