2 include "tutorial/chapter2.ma".
3 include "basics/bool.ma".
5 inductive list (A:Type[0]) : Type[0] :=
7 | cons: A -> list A -> list A.
9 notation "hvbox(hd break :: tl)"
10 right associative with precedence 47
13 notation "[ list0 x sep ; ]"
14 non associative with precedence 90
15 for ${fold right @'nil rec acc @{'cons $x $acc}}.
17 notation "hvbox(l1 break @ l2)"
18 right associative with precedence 47
19 for @{'append $l1 $l2 }.
21 interpretation "nil" 'nil = (nil ?).
22 interpretation "cons" 'cons hd tl = (cons ? hd tl).
24 definition not_nil: ∀A:Type[0].
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A → Prop ≝
25 λA.λl.match l with [ nil ⇒
\ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"
\ 6True
\ 5/a
\ 6| cons hd tl ⇒
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6].
28 ∀A:Type[0].∀l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.∀a:A. a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6].
29 #A #l #a @
\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"
\ 6nmk
\ 5/a
\ 6 #Heq (change with (
\ 5a href="cic:/matita/tutorial/chapter3/not_nil.def(1)"
\ 6not_nil
\ 5/a
\ 6 ? (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l))) >Heq //
32 let rec append A (l1:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) l2 on l1 ≝
35 | cons hd tl ⇒ hd
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6: append A tl l2 ].
37 definition hd ≝ λA.λl:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.λd:A.
38 match l with [ nil ⇒ d | cons a _ ⇒ a].
40 definition tail ≝ λA.λl:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
41 match l with [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6] | cons hd tl ⇒ tl].
43 interpretation "append" 'append l1 l2 = (append ? l1 l2).
45 theorem append_nil: ∀A.∀l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.l
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 l.
46 #A #l (elim l) normalize // qed.
48 theorem associative_append:
49 ∀A.
\ 5a href="cic:/matita/basics/relations/associative.def(1)"
\ 6associative
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) (
\ 5a href="cic:/matita/tutorial/chapter3/append.fix(0,1,1)"
\ 6append
\ 5/a
\ 6 A).
50 #A #l1 #l2 #l3 (elim l1) normalize // qed.
52 (* qualcosa di strano qui theorem append_cons:∀A.∀a:A.∀l,l1:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.l
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6(a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l1)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 (l
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 \ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6a])
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 l1.
55 theorem nil_append_elim: ∀A.∀l1,l2:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.∀P:?→?→Prop.
56 l1
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6l2
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6] → P
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6] → P l1 l2.
57 #A #l1 #l2 #P (cases l1) normalize //
61 theorem nil_to_nil: ∀A.∀l1,l2:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 \ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6A.
62 l1
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6l2
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6] → l1
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 l2
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6].
63 #A #l1 #l2 #isnil @(
\ 5a href="cic:/matita/tutorial/chapter3/nil_append_elim.def(3)"
\ 6nil_append_elim
\ 5/a
\ 6 A l1 l2) /2/
68 let rec map (A,B:Type[0]) (f: A → B) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) on l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 B ≝
69 match l with [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6] | cons x tl ⇒ f x
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6: (map A B f tl)].
71 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) on l :B ≝
72 match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
75 λT.λp:T →
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6.
76 \ 5a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"
\ 6foldr
\ 5/a
\ 6 T (
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 T) (λx,l0.
\ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"
\ 6if_then_else
\ 5/a
\ 6 ? (p x) (x
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l0) l0)
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6].
78 lemma filter_true : ∀A,l,a,p. p a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 →
79 \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:
\ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p l.
80 #A #l #a #p #pa (elim l) normalize >pa // qed.
82 lemma filter_false : ∀A,l,a,p. p a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 →
83 \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p l.
84 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
87 theorem eq_map : ∀A,B,f,g,l. (∀x.f x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 g x) →
\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"
\ 6map
\ 5/a
\ 6 A B f l
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"
\ 6map
\ 5/a
\ 6 A B g l.
88 #A #B #f #g #l #eqfg (elim l) normalize // qed.
92 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
95 | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
98 (**************************** length ******************************)
100 let rec length (A:Type[0]) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) on l ≝
102 [ nil ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6
103 | cons a tl ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (length A tl)].
105 let rec nth n (A:Type[0]) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) (d:A) ≝
107 [O ⇒
\ 5a href="cic:/matita/tutorial/chapter3/hd.def(1)"
\ 6hd
\ 5/a
\ 6 A l d
108 |S m ⇒ nth m A (
\ 5a href="cic:/matita/tutorial/chapter3/tail.def(1)"
\ 6tail
\ 5/a
\ 6 A l) d].
110 (**************************** fold *******************************)
112 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6) (f:A→B) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) on l :B ≝
115 | cons a l ⇒
\ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"
\ 6if_then_else
\ 5/a
\ 6 ? (p a) (op (f a) (fold A B op b p f l))
116 (fold A B op b p f l)].
118 notation "\fold [ op , nil ]_{ ident i ∈ l | p} f"
120 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
122 notation "\fold [ op , nil ]_{ident i ∈ l } f"
124 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
126 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
129 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 →
130 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l| p i} (f i)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6
131 op (f a)
\ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ l| p i} (f i).
132 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
135 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
136 p a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 →
\ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l| p i} (f i)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6
137 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ l| p i} (f i).
138 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
141 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
142 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ l| p i} (f i)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6
143 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ (
\ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p l)} (f i).
144 #A #B #a #l #p #op #nil #f elim l //
145 #a #tl #Hind cases(
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (p a)) #pa
146 [ >
\ 5a href="cic:/matita/tutorial/chapter3/filter_true.def(3)"
\ 6filter_true
\ 5/a
\ 6 // >
\ 5a href="cic:/matita/tutorial/chapter3/fold_true.def(3)"
\ 6fold_true
\ 5/a
\ 6 // >
\ 5a href="cic:/matita/tutorial/chapter3/fold_true.def(3)"
\ 6fold_true
\ 5/a
\ 6 //
147 | >
\ 5a href="cic:/matita/tutorial/chapter3/filter_false.def(3)"
\ 6filter_false
\ 5/a
\ 6 // >
\ 5a href="cic:/matita/tutorial/chapter3/fold_false.def(3)"
\ 6fold_false
\ 5/a
\ 6 // ]
150 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
152 nill:∀a. op nil a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a;
153 nilr:∀a. op a nil
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a;
154 assoc: ∀a,b,c.op a (op b c)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 op (op a b) c
157 theorem fold_sum: ∀A,B. ∀I,J:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.∀nil.∀op:
\ 5a href="cic:/matita/tutorial/chapter3/Aop.ind(1,0,2)"
\ 6Aop
\ 5/a
\ 6 B nil.∀f.
158 op (
\ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i∈I} (f i)) (
\ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i∈J} (f i))
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6
159 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i∈(I
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6J)} (f i).
160 #A #B #I #J #nil #op #f (elim I) normalize
161 [>
\ 5a href="cic:/matita/tutorial/chapter3/nill.fix(0,2,2)"
\ 6nill
\ 5/a
\ 6 //|#a #tl #Hind <
\ 5a href="cic:/matita/tutorial/chapter3/assoc.fix(0,2,2)"
\ 6assoc
\ 5/a
\ 6 //]