Ignore:
Timestamp:
Nov 12, 2010, 11:51:18 AM (10 years ago)
Author:
mulligan
Message:

Changes from this morning: Bool / Prop division = nightmare.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D4.1/Matita/List.ma

    r230 r233  
     1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     2(* List.ma: Polymorphic lists, and routine operations on them.                *)
     3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     4
    15include "Maybe.ma".
    26include "Nat.ma".
    … …  
    59include "Plogic/equality.ma".
    610
     11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     12(* The datatype.                                                              *)
     13(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     14
    715ninductive List (A: Type[0]): Type[0] ≝
    816  Empty: List A
    … …  
    2028  for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
    2129 
    22 nlet rec length (A: Type[0]) (l: List A) on l ≝
    23   match l with
    24     [ Empty ⇒ Z
    25     | Cons hd tl ⇒ S $ length A tl
    26     ].
    27    
    28 nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
    29   match l with
    30     [ Empty ⇒ m
    31     | Cons hd tl ⇒ hd :: (append A tl m)
    32     ].
    33    
    34 notation "hvbox(l break @ r)"
    35   right associative with precedence 47
    36   for @{ 'append $l $r }.
    37  
    38 interpretation "List append" 'append = (append ?).
    39  
    40 nlet rec fold_right (A: Type[0]) (B: Type[0])
    41                     (f: A → B → B) (x: B) (l: List A) on l ≝
    42   match l with
    43     [ Empty ⇒ x
    44     | Cons hd tl ⇒ f hd (fold_right A B f x tl)
    45     ].
    46    
    47 nlet rec fold_left (A: Type[0]) (B: Type[0])
    48                    (f: A → B → A) (x: A) (l: List B) on l ≝
    49   match l with
    50     [ Empty ⇒ x
    51     | Cons hd tl ⇒ f (fold_left A B f x tl) hd
    52     ].
    53    
    54 nlet rec map (A: Type[0]) (B: Type[0])
    55              (f: A → B) (l: List A) on l ≝
    56   match l with
    57     [ Empty ⇒ Empty B
    58     | Cons hd tl ⇒ f hd :: map A B f tl
    59     ].
    60    
     30(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     31(* Lookup.                                                                    *)
     32(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     33
    6134nlet rec null (A: Type[0]) (l: List A) on l ≝
    6235  match l with
    6336    [ Empty ⇒ True
    6437    | Cons hd tl ⇒ False
    65     ].
    66    
    67 nlet rec reverse (A: Type[0]) (l: List A) on l ≝
    68   match l with
    69     [ Empty ⇒ Empty A
    70     | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
    7138    ].
    7239   
    … …  
    8653      | Cons hd tl ⇒ Just (List A) tl
    8754      ].
    88      
     55       
     56   
     57(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     58(* Folds and builds.                                                          *)
     59(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     60
     61nlet 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   
     68nlet 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
     79nlet 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
     86(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     87(* Building lists from scratch                                                *)
     88(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     89
    8990nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
    9091  match n with
    … …  
    9394    ].
    9495   
    95 nlemma append_empty:
     96nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
     97  match l with
     98    [ Empty ⇒ m
     99    | Cons hd tl ⇒ hd :: (append A tl m)
     100    ].
     101   
     102notation "hvbox(l break @ r)"
     103  right associative with precedence 47
     104  for @{ 'append $l $r }.   
     105 
     106interpretation "List append" 'append = (append ?).
     107
     108(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     109(* Other manipulations.                                                       *)
     110(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     111
     112nlet rec length (A: Type[0]) (l: List A) on l ≝
     113  match l with
     114    [ Empty ⇒ Z
     115    | Cons hd tl ⇒ S $ length A tl
     116    ].
     117   
     118nlet rec reverse (A: Type[0]) (l: List A) on l ≝
     119  match l with
     120    [ Empty ⇒ Empty A
     121    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
     122    ].
     123
     124(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     125(* Rotates and shifts.                                                        *)
     126(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     127
     128nlet rec rotate_left (A: Type[0]) (l: List A) (m: Nat) on m ≝
     129  match m with
     130    [ Z ⇒ l
     131    | S n ⇒
     132      match l with
     133        [ Empty ⇒ Empty A
     134        | Cons hd tl ⇒ hd :: rotate_left A tl n
     135        ]
     136    ].
     137
     138ndefinition rotate_right ≝
     139  λA: Type[0].
     140  λl: List A.
     141  λm: Nat.
     142    reverse A (rotate_left A (reverse A l) m).
     143
     144(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     145(* Lemmas.                                                                    *)
     146(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     147   
     148nlemma append_empty_left_neutral:
    96149  ∀A: Type[0].
    97150  ∀l: List A.
    … …  
    121174nqed.
    122175   
    123 nlemma reverse_append:
     176nlemma reverse_distributes_append:
    124177  ∀A: Type[0].
    125178  ∀l, m: List A.
    … …  
    128181  nelim l.
    129182  nnormalize.
    130   napplyS append_empty.
     183  napplyS append_empty_left_neutral.
    131184  #H L A.
    132185  nnormalize.
    … …  
    135188nqed.
    136189
    137 nlemma length_append:
     190nlemma length_distributes_append:
    138191  ∀A: Type[0].
    139192  ∀l, m: List A.
    … …  
    160213  #H L H2.
    161214  nnormalize.
    162   napplyS length_append.
    163    
     215  napply (length_distributes_append A (reverse A l) (Cons A H (Empty A))).
     216*)
     217 
     218(*   
    164219nlemma reverse_reverse:
    165220  ∀A: Type[0].
    … …  
    173228  nnormalize.
    174229*)
     230
     231nlemma map_fusion:
     232  ∀A, B, C: Type[0].
     233  ∀l: List A.
     234  ∀m: List B.
     235  ∀f: A → B.
     236  ∀g: B → C.
     237    map B C g (map A B f l) = map A C (λx. g (f x)) l.
     238  #A B C l m f g.
     239  nelim l.
     240  //.
     241  #H L H2.
     242  nnormalize.
     243  //.
     244nqed.
     245
     246nlemma map_preserves_length:
     247  ∀A, B: Type[0].
     248  ∀l: List A.
     249  ∀f: A → B.
     250    length B (map A B f l) = length A l.
     251  #A B l f.
     252  nelim l.
     253  //.
     254  #H L H2.
     255  nnormalize.
     256  //.
     257nqed.
Note: See TracChangeset for help on using the changeset viewer.