Ignore:
Timestamp:
Nov 10, 2010, 5:26:08 PM (10 years ago)
Author:
mulligan
Message:

Lots of work from today.

File:
1 edited

Legend:

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

    r229 r230  
    22include "Nat.ma".
    33include "Util.ma".
     4
     5include "Plogic/equality.ma".
    46
    57ninductive List (A: Type[0]): Type[0] ≝
     
    1113  for @{ 'Cons $hd $tl }.
    1214
    13 interpretation "Empty" 'Empty = (Empty ?).
    14 interpretation "Cons" 'Cons = (Cons ?).
     15interpretation "List empty" 'Empty = (Empty ?).
     16interpretation "List cons" 'Cons = (Cons ?).
    1517 
    1618notation "[ list0 x sep ; ]"
     
    2729  match l with
    2830    [ Empty ⇒ m
    29     | Cons hd tl ⇒ hd :: (append A tl l)
     31    | Cons hd tl ⇒ hd :: (append A tl m)
    3032    ].
    3133   
     
    3436  for @{ 'append $l $r }.
    3537 
    36 interpretation "Append" 'append = (append ?).
     38interpretation "List append" 'append = (append ?).
    3739 
    3840nlet rec fold_right (A: Type[0]) (B: Type[0])
     
    9092    | S o ⇒ a :: replicate A o a
    9193    ].
     94   
     95nlemma append_empty:
     96  ∀A: Type[0].
     97  ∀l: List A.
     98    l @ (Empty A) = l.
     99  #A l.
     100  nelim l.
     101  nnormalize.
     102  @.
     103  #H L H2.
     104  nnormalize.
     105  nrewrite > H2.
     106  @.
     107nqed.
     108
     109nlemma append_associative:
     110  ∀A: Type[0].
     111  ∀l,m,n: List A.
     112    l @ (m @ n) = (l @ m) @ n.
     113  #A l m n.
     114  nelim l.
     115  nnormalize.
     116  @.
     117  #H L H2.
     118  nnormalize.
     119  nrewrite > H2.
     120  @.
     121nqed.
     122   
     123nlemma reverse_append:
     124  ∀A: Type[0].
     125  ∀l, m: List A.
     126    reverse A (l @ m) = reverse A m @ reverse A l.
     127  #A l m.
     128  nelim l.
     129  nnormalize.
     130  napplyS append_empty.
     131  #H L A.
     132  nnormalize.
     133  nrewrite > A.
     134  napplyS append_associative.
     135nqed.
     136
     137nlemma length_append:
     138  ∀A: Type[0].
     139  ∀l, m: List A.
     140    length A (l @ m) = length A l + length A m.
     141  #A l m.
     142  nelim l.
     143  nnormalize.
     144  @.
     145  #H L H2.
     146  nnormalize.
     147  nrewrite > H2.
     148  @.
     149nqed.
     150
     151(* 
     152nlemma length_reverse:
     153  ∀A: Type[0].
     154  ∀l: List A.
     155    length A (reverse A l) = length A l.
     156  #A l.
     157  nelim l.
     158  nnormalize.
     159  @.
     160  #H L H2.
     161  nnormalize.
     162  napplyS length_append.
     163   
     164nlemma reverse_reverse:
     165  ∀A: Type[0].
     166  ∀l: List A.
     167    reverse A (reverse A l) = l.
     168  #A l.
     169  nelim l.
     170  nnormalize.
     171  @.
     172  #H L H2.
     173  nnormalize.
     174*)
Note: See TracChangeset for help on using the changeset viewer.