Ignore:
Timestamp:
Dec 2, 2010, 4:36:35 PM (10 years ago)
Author:
mulligan
Message:

Added subvector_with function.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/List.ma

    r357 r364  
    5353  for @{ 'append $l $r }.   
    5454 
    55 interpretation "List append" 'append = (append ?). 
     55interpretation "List append" 'append = (append ?).
     56
     57(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     58(* Maps and zips.                                                             *)
     59(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     60
     61nlet rec map (A: Type[0]) (B: Type[0])
     62             (f: A → B) (l: List A) on l ≝
     63  match l with
     64    [ Empty ⇒ Empty B
     65    | Cons hd tl ⇒ f hd :: map A B f tl
     66    ].
     67   
     68nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝
     69  match l with
     70    [ Empty ⇒ Empty A
     71    | Cons hd tl ⇒ hd @ (flatten A tl)
     72    ].
     73   
     74ndefinition map_flatten ≝
     75  λA: Type[0].
     76  λf: A → List A.
     77  λl: List A.
     78    flatten A (map A (List A) f l).
    5679 
    5780(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    6992    [ Empty ⇒ Empty A
    7093    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
     94    ].
     95   
     96nlet rec power_list (A: Type[0]) (l: List A) on l ≝
     97  match l with
     98    [ Empty ⇒ [ [ ] ]
     99    | Cons hd tl ⇒
     100        let r ≝ power_list A tl in
     101          (map ? ? (λx. hd :: x) r) @ r
    71102    ].
    72103 
     
    284315
    285316(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    286 (* Maps and zips.                                                             *)
    287 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    288 
    289 nlet rec map (A: Type[0]) (B: Type[0])
    290              (f: A → B) (l: List A) on l ≝
    291   match l with
    292     [ Empty ⇒ Empty B
    293     | Cons hd tl ⇒ f hd :: map A B f tl
    294     ].
    295    
    296 nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝
    297   match l with
    298     [ Empty ⇒ Empty A
    299     | Cons hd tl ⇒ hd @ (flatten A tl)
    300     ].
    301    
    302 ndefinition map_flatten ≝
    303   λA: Type[0].
    304   λf: A → List A.
    305   λl: List A.
    306     flatten A (map A (List A) f l).
    307 
    308 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    309317(* Set-like operations.                                                       *)
    310318(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    340348  λm: Nat.
    341349    reverse A (rotate_left A (reverse A l) m).
     350
     351(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     352(* Decidable equality.                                                        *)
     353(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     354
     355nlet rec eq_l (A: Type[0]) (f: A → A → Bool) (l: List A) (m: List A) on l ≝
     356  match l with
     357    [ Empty ⇒
     358      match m with
     359        [ Empty ⇒ true
     360        | Cons hd tl ⇒ false
     361        ]
     362    | Cons hd tl ⇒
     363      match m with
     364        [ Empty ⇒ false
     365        | Cons hd' tl' ⇒ conjunction (f hd hd') (eq_l A f tl tl')
     366        ]
     367    ].     
    342368
    343369(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.