Changeset 2443 for src/utilities/lists.ma
 Timestamp:
 Nov 8, 2012, 2:27:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.