Changeset 891 for src/utilities/binary


Ignore:
Timestamp:
Jun 7, 2011, 4:53:53 PM (9 years ago)
Author:
campbell
Message:

Revise proofs affected by recent matita change.

Location:
src/utilities/binary
Files:
2 edited

Legend:

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

    r697 r891  
    333333|#n cases y;
    334334   [@nmk #H elim (not_eq_OZ_pos n);#H2 /2/;
    335    |#m @eqb_elim
     335   |#m normalize @eqb_elim
    336336      [//
    337337      | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
     
    341341   [@nmk #H elim (not_eq_OZ_neg n);#H /2/;
    342342   |#m @nmk #H destruct
    343    |#m @eqb_elim
     343   |#m normalize @eqb_elim
    344344      [//
    345345      | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
     
    458458
    459459theorem sym_Zplus : ∀x,y:Z. x+y = y+x.
    460 #x #y cases x;
    461 [>(Zplus_z_OZ ?) (*XXX*) //
     460#x #y cases x
     461[>Zplus_z_OZ //
    462462|#p cases y
    463463   [//
    464    |normalize;//
    465    |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*)
     464   |//
     465   |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n
    466466      cases (pos_compare q p);//]
    467467|#p cases y
    468468   [//;
    469    |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*)
     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 normalize;
     505whd in ⊢ (??%%)
    506506<(pos_compare_S_S …)
    507 >(partialminus_S_S …)
    508 >(partialminus_S_S …) //;
     507>(minus_S_S …)
     508>(minus_S_S …) //;
    509509qed.
    510510
     
    521521#n #m @(pos_cases … n) @(pos_cases … m)
    522522[ //;
    523 | #m' >(Zpred_pos_succ …)
    524     >(?:pos (succ m') = Zsucc (pos m')) //;
    525 | #m' normalize; >(pos_compare_S_one …) normalize;
    526     >(partial_minus_S_one …) normalize; >(pos_nonzero …)
    527     <(pred_succ_n …) //;
    528 | #m' #n' normalize; <(pos_compare_S_S …)
    529     >(partialminus_S_S …)
    530     >(partialminus_S_S …)
    531     >(pos_nonzero …)
    532     >(pos_nonzero …)
    533     <(pred_succ_n …)
    534     <(pred_succ_n …)
     523| #m' >Zpred_pos_succ
     524    change in ⊢ (??(??%)?) with (Zsucc (pos m'))
     525    <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
     526| #m' whd in ⊢ (??%%) >pos_compare_S_one normalize;
     527    >partial_minus_S_one normalize; >pos_nonzero
     528    <pred_succ_n //
     529| #m' #n' whd in ⊢ (??%%) <pos_compare_S_S
     530    >minus_S_S
     531    >minus_S_S normalize
     532    >pos_nonzero
     533    >pos_nonzero
     534    <pred_succ_n
     535    <pred_succ_n
    535536    normalize; //;
    536537] qed.
     
    600601
    601602lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
    602 #n #m normalize; <(pos_compare_S_S …)
    603 >(partialminus_S_S …)
    604 >(partialminus_S_S …)
     603#n #m whd in ⊢ (??%%) <pos_compare_S_S
     604>minus_S_S >minus_S_S
    605605 //; qed.
    606606
     
    676676#x #y cases x
    677677[cases y;//
    678 |*:#n cases y;//;#m normalize;@pos_compare_elim normalize;//]
     678|*:#n cases y;//;#m whd in ⊢ (??(?%)%) @pos_compare_elim normalize;//]
    679679qed.
    680680
     
    686686#x cases x
    687687[//
    688 |*:#n normalize;>(pos_compare_n_n ?) //]
     688|*:#n whd in ⊢ (??%?) >pos_compare_n_n //]
    689689qed.
    690690
  • src/utilities/binary/positive.ma

    r697 r891  
    10951095  [ LT ⇒ n < m
    10961096  | EQ ⇒ n = m
    1097   | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *)
     1097  | GT ⇒ m < n ]))
    10981098[1,2:@pos_cases
    10991099  [ 1,3: /2/;
    11001100  | 2,4: #m' cases m'; //;
    11011101  ]
    1102 |#n1 #m1 normalize;<(pos_compare_S_S …) cases (pos_compare n1 m1);
    1103    [1,3:normalize;#IH @le_succ_succ //;
    1104    |normalize;#IH >IH //]
     1102|#n1 #m1 <pos_compare_S_S cases (pos_compare n1 m1)
     1103   [1,3: #IH @le_succ_succ //
     1104   | #IH >IH //
     1105   ]
     1106]
    11051107qed.
    11061108
Note: See TracChangeset for help on using the changeset viewer.