Changeset 2443 for src/utilities


Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (7 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

Location:
src/utilities
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/deqsets.ma

    r2296 r2443  
    11include "basics/deqsets.ma".
     2include "basics/lists/listb.ma".
     3include "ASM/Util.ma".
    24
    35lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D.
     
    911| #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct
    1012] qed.
     13
     14
     15(* is it already there? *)
     16lemma 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]
     23qed.
  • src/utilities/lists.ma

    r2440 r2443  
    150150definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
    151151// 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   with
    157 [ 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 …).
    166152
    167153definition List ≝ MakeMonadProps
     
    379365| cons h t ⇒ ordered_insert A lt h (insert_sort A lt t)
    380366].
     367
     368(* range from 0 to n excluded with proof of minoration *)
     369
     370let 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]
     381qed.
     382
     383definition 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.