Ignore:
Timestamp:
Nov 29, 2010, 1:42:00 PM (10 years ago)
Author:
mulligan
Message:

Commit to restore deleted file.

File:
1 edited

Legend:

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

    r260 r329  
    77include "Bool.ma".
    88include "Nat.ma".
    9 (* include "Maybe.ma". *)
     9include "Maybe.ma".
    1010include "Plogic/equality.ma".
    1111
     
    3838 
    3939(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     40(* Building lists from scratch                                                *)
     41(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     42
     43nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
     44  match n with
     45    [ Z ⇒ Empty A
     46    | S o ⇒ a :: replicate A o a
     47    ].
     48   
     49nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
     50  match l with
     51    [ Empty ⇒ m
     52    | Cons hd tl ⇒ hd :: (append A tl m)
     53    ].
     54   
     55notation "hvbox(l break @ r)"
     56  right associative with precedence 47
     57  for @{ 'append $l $r }.   
     58 
     59interpretation "List append" 'append = (append ?). 
     60 
     61(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     62(* Other manipulations.                                                       *)
     63(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     64
     65nlet rec length (A: Type[0]) (l: List A) on l ≝
     66  match l with
     67    [ Empty ⇒ Z
     68    | Cons hd tl ⇒ S $ length A tl
     69    ].
     70   
     71nlet rec reverse (A: Type[0]) (l: List A) on l ≝
     72  match l with
     73    [ Empty ⇒ Empty A
     74    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
     75    ].
     76 
     77(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    4078(* Lookup.                                                                    *)
    4179(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    42    
    43 (*   
    44 nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝
     80
     81nlet rec get_index (A: Type[0]) (l: List A)
     82                   (n: Nat) (lt: n < length ? l) on n: A ≝
     83  match n return λx. x < length ? l → A with
     84    [ Z ⇒
     85      match l return λx. Z < length ? x → A with
     86        [ Empty ⇒ λabsd: Z < Z. ?
     87        | Cons hd tl ⇒ λp. hd
     88        ]
     89    | S o ⇒
     90      match l return λx. S o < length ? x → A with
     91        [ Empty ⇒ λabsd: S o < Z. ?
     92        | Cons hd tl ⇒ λp. get_index A tl o ?
     93        ]
     94    ] ?.
     95    ##[##1:
     96        nassumption;
     97    ##|##2:
     98        ncases (nothing_less_than_Z Z);
     99        #K;
     100        ncases (K absd);
     101    ##|##3:
     102        ncases (nothing_less_than_Z (S o));
     103        #K;
     104        ncases (K absd);
     105    ##| ncases (less_than_monoton);
     106   
     107   
     108nlet rec get_index_weak (A: Type[0]) (l: List A) (n: Nat) on n ≝
    45109  match n with
    46110    [ Z ⇒
     
    58122interpretation "List get_index" 'get_index l n = (get_index ? l n).
    59123
    60 nlet rec set_index (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝
     124nlet rec set_index_weak (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝
    61125  match n with
    62126    [ Z ⇒
     
    85149          | Cons hd tl ⇒ drop A tl o
    86150          ]
    87     ].
    88 *)
    89    
    90 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    91 (* Building lists from scratch                                                *)
    92 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    93 
    94 nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
    95   match n with
    96     [ Z ⇒ Empty A
    97     | S o ⇒ a :: replicate A o a
    98     ].
    99    
    100 nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
    101   match l with
    102     [ Empty ⇒ m
    103     | Cons hd tl ⇒ hd :: (append A tl m)
    104     ].
    105    
    106 notation "hvbox(l break @ r)"
    107   right associative with precedence 47
    108   for @{ 'append $l $r }.   
    109  
    110 interpretation "List append" 'append = (append ?).   
    111 
    112 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    113 (* Other manipulations.                                                       *)
    114 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    115 
    116 nlet rec length (A: Type[0]) (l: List A) on l ≝
    117   match l with
    118     [ Empty ⇒ Z
    119     | Cons hd tl ⇒ S $ length A tl
    120     ].
    121    
    122 nlet rec reverse (A: Type[0]) (l: List A) on l ≝
    123   match l with
    124     [ Empty ⇒ Empty A
    125     | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
    126     ].
     151    ]. 
    127152
    128153(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.