Changeset 2443 for src/utilities
 Timestamp:
 Nov 8, 2012, 2:27:54 PM (7 years ago)
 Location:
 src/utilities
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/deqsets.ma
r2296 r2443 1 1 include "basics/deqsets.ma". 2 include "basics/lists/listb.ma". 3 include "ASM/Util.ma". 2 4 3 5 lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D. … … 9 11  #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct 10 12 ] qed. 13 14 15 (* is it already there? *) 16 lemma All_memb : ∀A : DeqSet.∀P,l,x.All A P l → x ∈ l → P x. 17 #A #P #l elim l 18 [ #x * * 19  #hd #tl #IH #x * #Phd #Ptl 20 normalize @(eqb_elim A) #H normalize nodelta [destruct * @Phd] 21 @IH @Ptl 22 ] 23 qed. 
src/utilities/lists.ma
r2440 r2443 150 150 definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?. 151 151 // qed. 152 153 let rec range_strong_internal (start, how_many, end : ℕ)154 on how_many : start + how_many ≤ end → list (Σn : ℕ.n < end) ≝155 match how_many return λx.start + x ≤ end → ?156 with157 [ O ⇒ λ_.[ ]158  S k ⇒ λprf.«start, ?» :: range_strong_internal (S start) k end ?159 ].160 [2: //]161 >(plus_n_O start) /2 by plus_lt_to_lt/162 qed.163 164 definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝165 λend.range_strong_internal 0 end end (le_n …).166 152 167 153 definition List ≝ MakeMonadProps … … 379 365  cons h t ⇒ ordered_insert A lt h (insert_sort A lt t) 380 366 ]. 367 368 (* range from 0 to n excluded with proof of minoration *) 369 370 let rec range_strong_internal (index, how_many, end : ℕ) on how_many : 371 index + how_many = end → 372 list (Σn.n<end) ≝ 373 match how_many return λhow_many.index + how_many = end → ? with 374 [ O ⇒ λ_.[ ] 375  S k ⇒ λprf.«index, ?» :: range_strong_internal (S index) k end ? 376 ]. 377 <prf 378 [ >(plus_n_O index) in ⊢ (?%?); @monotonic_lt_plus_r @le_S_S @le_O_n 379  @plus_n_Sm 380 ] 381 qed. 382 383 definition range_strong : ∀end.list (Σn.n < end) ≝ 384 λend.range_strong_internal 0 ? end (refl …).
Note: See TracChangeset
for help on using the changeset viewer.