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
|
import Std.Data.List.Basic
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]
#eval length [1,2,3,4,5,6,7,8,9]
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]
#eval filter (·>5) [1,2,3,4,5,6,7,8,9]
end filter
end catamorphism
section anamorphism
partial def ana {α β : Type} (p : β → Bool) (b : β) (g : ∀ (b : β) (_ : ¬p b), α × β) := by
cases h : (p b)
have hp := ne_true_of_eq_false h
let t := g b hp
exact t.fst :: ana p t.snd g
exact []
notation:max "〖" l:10 "," r:11 "〗" => λ b => ana r b l
section zip
def p (l : List α × List β) : Bool := (List.length l.1) = 0 || (List.length l.2 = 0)
-- this si fucking ugly!!!!!!
def g (l : List α × List β) (hp : ¬p l) := by
unfold p at hp
simp at hp
rw [not_or] at hp
have left := And.left hp
rw [List.length_eq_zero] at left
have right := And.right hp
rw [List.length_eq_zero] at right
have lh := List.head l.fst left
have rh := List.head l.snd right
exact ((lh, rh), (List.tail l.fst, List.tail l.snd))
def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
def zip : List α → List β → List (α × β) := curry 〖g, p〗
#eval zip [1] [2]
end zip
end anamorphism
section hylomorphism
-- partial def hylo (c : φ) (f : β → φ → φ) (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 : β → φ → φ) (p : α → Bool) (g : (b : α) → ¬p b = true → β × α) := ⦅c,f⦆ ∘ 〖g, p〗
notation:max "⟦" "(" c:10 "," f:11 ")" "," "(" g:12 "," p:13 ")" "⟧" => hylo c f p g
section factorial
def g_1 (b : Nat) (_ : ¬decide (b = 0)) : Nat × Nat := (b, b-1)
def fac : Nat → Nat := ⟦(1, Nat.mul), (g_1, (·=0))⟧
#eval fac 8
end factorial
end hylomorphism
|
