1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
section catamorphism
def cata {α β : Type} (b : β) (f : α → β → β) (x : List α) :=
match x with
| [] => b
| a :: as => f a (cata b f as)
notation:max "⦅" l:10 "," r:11 "⦆" => cata l r
-- theorem cata_fusion (h : β → β) (b : β) (f : α → β → β) : h ∘ ⦅b, f⦆ = ⦅b, h ∘ f⦆ := by
-- sorry
section length
def length := ⦅0, Function.const Nat Nat.succ⦆
theorem length_empty : length [] = Nat.zero := by
unfold length
unfold cata
rfl
theorem length_cons : length (a :: as) = Nat.succ (length as) := by
match as with
| [] =>
rw [length_empty]
unfold length
simp [cata]
| b :: bs =>
unfold length
simp [cata]
end length
section filter
def filter {α : Type} (p : α → Bool) := ⦅[],
λ (a as) => if (p a) then (a :: as) else (as)⦆
theorem filter_nil {α : Type} (p : α → Bool) : filter p [] = [] := by
unfold filter
simp [cata]
theorem filter_cons_pos {α : Type} (p : α → Bool) {a : α} (l : List α) : p a → filter p (a :: l) = a :: (filter p l) := by
intro hp
unfold filter
simp [cata]
simp [hp]
theorem filter_cons_neg {α : Type} (p : α → Bool) {a : α} (l : List α) : ¬p a → filter p (a :: l) = filter p l := by
intro hp
unfold filter
simp [cata]
simp [hp]
end filter
end catamorphism
section anamorphism
partial def ana {α β : Type} (g : β → α × β) (p : β → Bool) (b : β) :=
match p b with
| true => []
| false => let t := g b
t.fst :: ana g p t.snd
notation:max "〖" l:10 "," r:11 "〗" => ana l r
section zip
def p (l : List α × List β) := match l with
| ([], _) => true
| (_, []) => true
| _ => false
def g [Inhabited α] [Inhabited β] (l : List α × List β) := match l with
| (a :: as, b :: bs) => ((a,b),(as,bs))
-- prove this cant happen, i dont wanna handle this case
| _ => ((default,default), ([], []))
def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
def zip [Inhabited α] [Inhabited β] : List α → List β → List (α × β) := curry 〖g, p〗
-- theorem zip_nil_left {α β : Type} [Inhabited β] [Inhabited α] {l1 : List α} {l2 : List β} : l1 = [] → zip l1 l2 = [] := by
-- -- intro emp
-- -- rw [emp]
-- -- unfold zip
-- sorry
-- theorem zip_cons_cons {α β : Type} [Inhabited β] [Inhabited α] {l1 : List α} {l2 : List β} : l2 = [] → zip l1 l2 = [] := by
-- intro emp
-- rw [emp]
-- sorry
#eval zip ["hello"] ["world"]
end zip
-- def g {α : Type} (a : α) := (a, f a)
-- def iterate {α β : Type} (f : α → β) := let g := fun a => (f a, a)
-- ana g (Function.const α false)
-- theorem iterate_nonempty {α β : Type} (f : α → β) (a : α) : iterate f a ≠ [] := by
-- unfold iterate
-- sorry
-- example : List.head (iterate Nat.succ 0) = 1 := by
-- sorry
-- #eval List.head (iterate Nat.succ 0)
end anamorphism
section hylomorphism
-- partial def hylo (c : φ) (f : β → φ → φ) (g : α → β × α) (p : α → Bool) (a : α) := match p a with
-- | true => c
-- | false => let t := g a
-- f t.fst (hylo c f g p t.snd)
def hylo (c : φ) (f : β → φ → φ) (g : α → β × α) (p : α → Bool) := ⦅c,f⦆ ∘ 〖g, p〗
notation:max "⟦" "(" c:10 "," f:11 ")" "," "(" g:12 "," p:13 ")" "⟧" => hylo c f g p
section factorial
def g_1 (n : Nat) := match n with
| Nat.succ k => (n, k)
-- prove this cant happen, i dont wanna handle this case
| 0 => default
def fac := ⟦(1, Nat.mul), (g_1, λ n => n = 0)⟧
#eval fac 6
end factorial
end hylomorphism
|
