Changeset 241


Ignore:
Timestamp:
Nov 15, 2010, 10:26:20 AM (9 years ago)
Author:
mulligan
Message:

Also needed an updated List.ma.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r237 r241  
    33(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    44
    5 include "Maybe.ma".
    6 include "Nat.ma".
    75include "Util.ma".
     6
     7include "Universes/Universes.ma".
     8
     9include "Datatypes/Nat/Nat.ma".
     10include "Datatypes/Nat/Addition.ma".
     11
     12include "Datatypes/Maybe.ma".
    813
    914include "Plogic/equality.ma".
     
    1621  Empty: List A
    1722| Cons: A → List A → List A.
     23
     24(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     25(* Syntax.                                                                    *)
     26(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    1827
    1928notation "hvbox(hd break :: tl)"
     
    2837  for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
    2938 
     39notation "hvbox(l break !! break n)"
     40  non associative with precedence 90
     41  for @{ 'get_index $l $n }.
     42 
    3043(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3144(* Lookup.                                                                    *)
    3245(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    33 
    34 nlet rec null (A: Type[0]) (l: List A) on l ≝
    35   match l with
    36     [ Empty ⇒ True
    37     | Cons hd tl ⇒ False
    38     ].
    39    
    40 ndefinition head ≝
    41   λA: Type[0].
    42   λl: List A.
    43     match l with
    44       [ Empty ⇒ Nothing A
    45       | Cons hd tl ⇒ Just A hd
    46       ].
    47    
    48 ndefinition tail ≝
    49   λA: Type[0].
    50   λl: List A.
    51     match l with
    52       [ Empty ⇒ Nothing (List A)
    53       | Cons hd tl ⇒ Just (List A) tl
    54       ].
    55        
    56    
    57 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    58 (* Folds and builds.                                                          *)
    59 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    60 
    61 nlet rec fold_right (A: Type[0]) (B: Type[0])
    62                     (f: A → B → B) (x: B) (l: List A) on l ≝
    63   match l with
    64     [ Empty ⇒ x
    65     | Cons hd tl ⇒ f hd (fold_right A B f x tl)
    66     ].
    67    
    68 nlet rec fold_left (A: Type[0]) (B: Type[0])
    69                    (f: A → B → A) (x: A) (l: List B) on l ≝
    70   match l with
    71     [ Empty ⇒ x
    72     | Cons hd tl ⇒ f (fold_left A B f x tl) hd
    73     ].
    74 
    75 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    76 (* Maps and zips.                                                             *)
    77 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    78 
    79 nlet rec map (A: Type[0]) (B: Type[0])
    80              (f: A → B) (l: List A) on l ≝
    81   match l with
    82     [ Empty ⇒ Empty B
    83     | Cons hd tl ⇒ f hd :: map A B f tl
    84     ].
    85 
     46     
     47nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝
     48  match n with
     49    [ Z ⇒
     50      match l with
     51        [ Empty ⇒ Nothing A
     52        | Cons hd tl ⇒ Just A hd
     53        ]
     54    | S o ⇒
     55      match l with
     56        [ Empty ⇒ Nothing A
     57        | Cons hd tl ⇒ get_index A tl o
     58        ]
     59    ].
     60   
     61interpretation "List get_index" 'get_index l n = (get_index ? l n).
     62
     63nlet rec set_index (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝
     64  match n with
     65    [ Z ⇒
     66      match l with
     67        [ Empty ⇒ Nothing (List A)
     68        | Cons hd tl ⇒ Just (List A) (Cons A a tl)
     69        ]
     70    | S o ⇒
     71      match l with
     72        [ Empty ⇒ Nothing (List A)
     73        | Cons hd tl ⇒
     74            let settail ≝ set_index A tl o a in
     75              match settail with
     76                [ Nothing ⇒ Nothing (List A)
     77                | Just j ⇒ Just (List A) (Cons A hd j)
     78                ]
     79        ]
     80    ].
     81
     82nlet rec drop (A: Type[0]) (l: List A) (n: Nat) on n ≝
     83  match n with
     84    [ Z ⇒ Just (List A) l
     85    | S o ⇒
     86        match l with
     87          [ Empty ⇒ Nothing (List A)
     88          | Cons hd tl ⇒ drop A tl o
     89          ]
     90    ].
     91   
    8692(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    8793(* Building lists from scratch                                                *)
     
    104110  for @{ 'append $l $r }.   
    105111 
    106 interpretation "List append" 'append = (append ?).
     112interpretation "List append" 'append = (append ?).   
    107113
    108114(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    121127    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
    122128    ].
     129
     130(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     131(* Deletions.                                                                 *)
     132(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     133
     134nlet rec remove_first_with_aux (A: Type[0]) (f: A → A → Bool) (a: A)
     135                               (l: List A) (b: List A) on l ≝
     136  match l with
     137    [ Empty ⇒ reverse A b
     138    | Cons hd tl ⇒
     139      match f hd a with
     140        [ True ⇒ (reverse A b) @ tl
     141        | False ⇒ remove_first_with_aux A f a tl (hd :: b)
     142        ]
     143    ].
     144
     145ndefinition remove_first_with ≝
     146  λA: Type[0].
     147  λf: A → A → Bool.
     148  λa: A.
     149  λl: List A.
     150    remove_first_with_aux A f a l (Empty A).
     151   
     152nlet rec remove_all_with_aux (A: Type[0]) (f: A → A → Bool) (a: A)
     153                             (l: List A) (b: List A) on l ≝
     154  match l with
     155    [ Empty ⇒ reverse A b
     156    | Cons hd tl ⇒
     157      match f hd a with
     158        [ True ⇒ remove_all_with_aux A f a tl b
     159        | False ⇒ remove_all_with_aux A f a tl (hd :: b)
     160        ]
     161    ].
     162   
     163ndefinition remove_all_with ≝
     164  λA: Type[0].
     165  λf: A → A → Bool.
     166  λa: A.
     167  λl: List A.
     168    remove_all_with_aux A f a l (Empty A).
     169   
     170ncheck remove_all_with.
     171
     172nlet rec drop_while (A: Type[0]) (f: A → Bool) (l: List A) on l ≝
     173  match l with
     174    [ Empty ⇒ Empty A
     175    | Cons hd tl ⇒
     176      match f hd with
     177        [ True ⇒ drop_while A f tl
     178        | False ⇒ Cons A hd tl
     179        ]
     180    ].
     181   
     182(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     183(* Folds and builds.                                                          *)
     184(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     185
     186nlet rec fold_right (A: Type[0]) (B: Type[0])
     187                    (f: A → B → B) (x: B) (l: List A) on l ≝
     188  match l with
     189    [ Empty ⇒ x
     190    | Cons hd tl ⇒ f hd (fold_right A B f x tl)
     191    ].
     192   
     193nlet rec fold_left (A: Type[0]) (B: Type[0])
     194                   (f: A → B → A) (x: A) (l: List B) on l ≝
     195  match l with
     196    [ Empty ⇒ x
     197    | Cons hd tl ⇒ f (fold_left A B f x tl) hd
     198    ].
     199   
     200(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     201(* Filters and existence tests.                                               *)
     202(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     203
     204nlet rec filter (A: Type[0]) (f: A → Bool) (l: List A) on l ≝
     205  match l with
     206    [ Empty ⇒ Empty A
     207    | Cons hd tl ⇒
     208      match f hd with
     209        [ True ⇒ hd :: (filter A f tl)
     210        | False ⇒ filter A f tl
     211        ]
     212    ].
     213   
     214nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l ≝
     215  match l with
     216    [ Empty ⇒ False
     217    | Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl)
     218    ].
     219   
     220nlet rec nub_with (A: Type[0]) (f: A → A → Bool) (l: List A) on l ≝
     221  match l with
     222    [ Empty ⇒ Empty A
     223    | Cons hd tl ⇒
     224      match member_with A hd f tl with
     225        [ True ⇒ nub_with A f tl
     226        | False ⇒ hd :: (nub_with A f tl)
     227        ]
     228    ].
     229
     230(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     231(* Maps and zips.                                                             *)
     232(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     233
     234nlet rec map (A: Type[0]) (B: Type[0])
     235             (f: A → B) (l: List A) on l ≝
     236  match l with
     237    [ Empty ⇒ Empty B
     238    | Cons hd tl ⇒ f hd :: map A B f tl
     239    ].
     240   
     241nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝
     242  match l with
     243    [ Empty ⇒ Empty A
     244    | Cons hd tl ⇒ hd @ (flatten A tl)
     245    ].
     246   
     247ndefinition map_flatten ≝
     248  λA: Type[0].
     249  λf: A → List A.
     250  λl: List A.
     251    flatten A (map A (List A) f l).
     252
     253(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     254(* Set-like operations.                                                       *)
     255(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     256
     257nlet rec intersection_with (A: Type[0]) (f: A → A → Bool)
     258                           (l: List A) (m: List A) on l ≝
     259  match l with
     260    [ Empty ⇒ Empty A
     261    | Cons hd tl ⇒
     262      match member_with A hd f m with
     263        [ True ⇒ hd :: (intersection_with A f tl m)
     264        | False ⇒ intersection_with A f tl m
     265        ]
     266    ].
    123267
    124268(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     
    256400  //.
    257401nqed.
     402
     403nlemma empty_get_index_nothing:
     404  ∀A: Type[0].
     405  ∀n: Nat.
     406    ((Empty A) !! n) = Nothing A.
     407  #A n.
     408  nelim n.
     409  //.
     410  #N H.
     411  //.
     412nqed.
     413
     414nlemma rotate_right_empty:
     415  ∀A: Type[0].
     416  ∀n: Nat.
     417    rotate_right A (Empty A) n = Empty A.
     418  #A n.
     419  nelim n.
     420  //.
     421  #N H.
     422  //.
     423nqed.
     424
     425nlemma rotate_left_empty:
     426  ∀A: Type[0].
     427  ∀n: Nat.
     428    rotate_left A (Empty A) n = Empty A.
     429  #A n.
     430  nelim n.
     431  //.
     432  #N H.
     433  //.
     434nqed.
     435
     436nlemma reverse_singleton:
     437  ∀A: Type[0].
     438  ∀a: A.
     439    reverse A (Cons A a (Empty A)) = Cons A a (Empty A).
     440  #A a.
     441  //.
     442nqed.
  • Deliverables/D4.1/Matita/Vector.ma

    r240 r241  
    66include "Util.ma".
    77
    8 include "Universes/Universes.ma".
    9 
    10 include "Datatypes/Nat/Nat.ma".
    11 include "Datatypes/Nat/Addition.ma".
    12 include "Datatypes/Nat/Order.ma".
    13 
    14 include "Datatypes/Listlike/List/List.ma".
    15 
    16 include "Datatypes/Cartesian.ma".
     8include "logic/pts.ma".
     9
     10include "Nat.ma".
     11
     12include "List.ma".
     13
     14include "Cartesian.ma".
    1715
    1816include "Plogic/equality.ma".
Note: See TracChangeset for help on using the changeset viewer.