source: Deliverables/D4.1/Matita/List.ma @ 230

Last change on this file since 230 was 230, checked in by mulligan, 9 years ago

Lots of work from today.

File size: 3.3 KB
Line 
1include "Maybe.ma".
2include "Nat.ma".
3include "Util.ma".
4
5include "Plogic/equality.ma".
6
7ninductive List (A: Type[0]): Type[0] ≝
8  Empty: List A
9| Cons: A → List A → List A.
10
11notation "hvbox(hd break :: tl)"
12  right associative with precedence 47
13  for @{ 'Cons $hd $tl }.
14
15interpretation "List empty" 'Empty = (Empty ?).
16interpretation "List cons" 'Cons = (Cons ?).
17 
18notation "[ list0 x sep ; ]"
19  non associative with precedence 90
20  for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
21 
22nlet 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   
28nlet 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   
34notation "hvbox(l break @ r)"
35  right associative with precedence 47
36  for @{ 'append $l $r }.
37 
38interpretation "List append" 'append = (append ?).
39 
40nlet 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   
47nlet 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   
54nlet 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   
61nlet rec null (A: Type[0]) (l: List A) on l ≝
62  match l with
63    [ Empty ⇒ True
64    | Cons hd tl ⇒ False
65    ].
66   
67nlet 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)
71    ].
72   
73ndefinition head ≝
74  λA: Type[0].
75  λl: List A.
76    match l with
77      [ Empty ⇒ Nothing A
78      | Cons hd tl ⇒ Just A hd
79      ].
80   
81ndefinition tail ≝
82  λA: Type[0].
83  λl: List A.
84    match l with
85      [ Empty ⇒ Nothing (List A)
86      | Cons hd tl ⇒ Just (List A) tl
87      ].
88     
89nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
90  match n with
91    [ Z ⇒ Empty A
92    | S o ⇒ a :: replicate A o a
93    ].
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 TracBrowser for help on using the repository browser.