-
Notifications
You must be signed in to change notification settings - Fork 0
/
FM.ttw
131 lines (102 loc) · 3.75 KB
/
FM.ttw
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
126
127
128
129
130
131
// The type of free monoids on type A.
data FM (A : Type) : Type
| in of A
| id
| op with (l r : FM)
| id , _ => r
| op x y, z => op x (op y z)
| _ , id => l
// Convert a free monoid expression to a list.
f : FM A -> list A
| in a => [a]
| id => []
| op x y => f x ++ f y
// Convert a list to a free monoid expression.
g : list A -> FM A
| [] => id
| h :: t => op (in h) (g t)
fg : (x : FM A) -> g (f x) = x
| in a => refl
| id => refl
| op (in a) y => ap (op (in a)) (fg y)
// The `id` and `in a` cases are trivial.
// In the `op (in a) y` case:
// Note that we don't need to match the cases `op id _` or `op (op _ _) _` because
// they are not canonical forms of FM A. This is because they get computed away
// by the constructor `op`. So it suffices to consider `op (in a) y`.
// LHS: g (f (op (in a) y)) => g (f (in a) ++ f y) => g ([a] ++ f y) => g (a :: f y) => op (in a) (g (f y))
// RHS: op (in a) y
// So the goal is convertible with `op (in a) (g (f y)) = op (in a) y`.
// The recursive call tives us `fg y : g (f y) = y`.
// It suffices to prepend `op (in a)` on both sides of the equation.
gf : (l : list A) -> f (g l) = l
| [] => refl
| h :: t => ap (h ::) (gf t)
// The `[]` case is trivial.
// In the `h :: t` case:
// LHS: `f (g (h :: t)) => f (op (in h) (g t)) => f (in h) ++ f (g t) => [h] ++ f (g t) => h :: f (g t)`
// RHS: `h :: t`
// So the goal is convertible with `h :: f (g t) = h :: t`.
// The recursive call gives us `gf t : f (g t) = t`.
// It suffices to prepend `h ::` on both sides of the equation.
list-is-free-mon (A : Type) : FM A = list A :=
// by univalence, as (f, g, fg, gf) is an equivalence
// It is not possible to define the free group with this approach, because we
// encounter non-linear patterns when trying to enforce x(x^-1) = id.
// | op : FG A -> FG A -> FG A
// | op x (inv x) => id
map (f : A -> B) : FM A -> FM B
| in a => in (f a)
| id => id
| op x y => op (map x) (map y)
map-id : (x : FM A) -> map id x = x
| in a => refl
| id => refl
| op x y => path i => op (map-id x i) (map-id y i)
map-map (f : A -> B) (g : B -> C) : (x : FM A) -> map g (map f x) = map (f.g) x
| in a => refl
| id => refl
| op x y => path i => op (map-map x i) (map-map y i)
filter (p : A -> Bool) : FM A -> FM A
| in a => if p a then in a else id
| id => id
| op x y => op (filter x) (filter y)
filter-filter (p : A -> Bool) : (x : FM A) -> filter p (filter p x) = filter p x
| in a => if p a then refl else refl
| id => refl
| op x y => path i => op (filter-filter x i) (filter-filter y i)
rev : FM A -> FM A
| in a => in a
| id => id
| op x y => op (rev y) (rev x)
rev-rev : (x : FM A) -> rev (rev x) = x
| in a => refl
| id => refl
| op x y => path i => op (rev-rev x i) (rev-rev y i)
map-rev (f : A -> B) : (x : FM A) -> map f (rev x) = rev (map f x)
| in a => refl
| id => refl
| op x y => path i => op (map-rev y i) (map-rev x i)
rev-filter (p : A -> Bool) : (x : FM A) -> rev (filter p x) = filter p (rev x)
| in a => if p a then refl else refl // TODO: reconsider
| id => refl
| op x y => path i => op (rev-filter y i) (rev-filter x i)
join : FM (FM A) -> FM A
| in fma => fma
| id => id
| op x y => op (join x) (join y)
bind (f : A -> FM B) : FM A -> FM B
| in a => f a
| id => id
| op x y => op (bind x) (bind y)
pure : A -> FM A := in
bind-pure-l : (x : FM A) -> bind pure x = x
| in a => refl
| id => refl
| op x y => path i => op (bind-pure-l x i) (bind-pure-l y i)
bind-pure-r (f : A -> FM B) (a : A) : bind f (pure a) = f a := refl
bind-bind (f : A -> FM B) (g : B -> FM C)
: (x : FM A) -> bind g (bind f x) = bind (fun a : A => bind g (f a)) x
| in a => refl
| id => refl
| op x y => path i => op (bind-bind f g x i) (bind-bind f g y i)