Changeset 1515 for src/utilities
 Timestamp:
 Nov 18, 2011, 1:03:14 PM (9 years ago)
 Location:
 src/utilities
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/binary/positive.ma
r1330 r1515 656 656 definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p  _ ⇒ one ]. 657 657 658 interpretation " naturalminus" 'minus x y = (minus x y).658 interpretation "positive minus" 'minus x y = (minus x y). 659 659 660 660 lemma partialminus_S: ∀n,m:Pos. … … 942 942 ]. 943 943 944 theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop.944 theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Type[0]. 945 945 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 946 946 #n elim n; … … 1159 1159 1160 1160 definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p). 1161 1162 1163 1164 definition max : Pos → Pos → Pos ≝ 1165 λn,m. match leb n m with [ true ⇒ m  _ ⇒ n]. 
src/utilities/extralib.ma
r1350 r1515 389 389 definition mod ≝ λm,n. snd ?? (divide m n). 390 390 391 lemma pred_minus: ∀n,m . pred n  m = pred (nm).391 lemma pred_minus: ∀n,m:Pos. pred n  m = pred (nm). 392 392 @pos_elim /3/; 393 393 qed. 
src/utilities/extranat.ma
r961 r1515 1 include "basics/types.ma". 1 2 include "arithmetics/nat.ma". 2 3 … … 36 37 [ // 37 38  #m' #IH whd in ⊢ (??%?) > IH @refl 39 ] qed. 40 41 42 let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝ 43 match n return λn.Sum (n=m) (n≠m) with 44 [ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??)  S m' ⇒ inr ??? ] 45  S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ???  S m' ⇒ 46 match eq_nat_dec n' m' with [ inl E ⇒ inl ???  inr NE ⇒ inr ??? ] ] 47 ]. 48 [ 1,2: % #E destruct 49  >E @refl 50  % #E destruct cases NE /2/ 38 51 ] qed. 39 52
Note: See TracChangeset
for help on using the changeset viewer.