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

Revise proofs affected by recent matita change.

File:
1 edited

Legend:

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