Changeset 891 for src/utilities


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
Files:
3 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
  • src/utilities/extralib.ma

    r882 r891  
    119119
    120120lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
    121 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y);
    122 /3/; cases x; /3/; qed.
     121#x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     122/3/ whd in ⊢ (% → ??%) /3/ qed.
    123123
    124124lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
    125 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y);
    126 cases x; /3/; qed.
     125#x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     126whd in ⊢ (% → ??%) /3/ qed.
    127127
    128128theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
     
    327327  ∀A:Type[0]. ∀l1,l2:list A.
    328328    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
    329 #A #l1 #l2 cases l1;
    330 [ cases l2;
     329#A #l1 #l2 cases l1
     330[ cases l2
    331331  [ /2/
    332   | #h #t #H destruct;
    333   ]
    334 | cases l2;
    335   [ normalize; #h #t #H destruct;
    336   | normalize; #h1 #t1 #h2 #h3 #H destruct;
     332  | normalize #h #t #H destruct
     333  ]
     334| cases l2
     335  [ normalize #h #t #H destruct
     336  | normalize #h1 #t1 #h2 #h3 #H destruct
    337337  ]
    338338] qed.
Note: See TracChangeset for help on using the changeset viewer.