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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
|
module Soat.FirstOrder.Term
import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Soat.Data.Product
import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Signature
import Syntax.PreorderReasoning.Setoid
%default total
public export
data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
Done : (i : v t) -> Term sig v t
Call : (op : Op sig t) -> (ts : Term sig v ^ op.arity) -> Term sig v t
public export
bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> {t : _} -> Term sig v t -> a.U t
public export
bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts
bindTerm env (Done i) = env _ i
bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts)
bindTerms env [] = []
bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts
public export
bindTermsIsMap : {auto a : RawAlgebra sig}
-> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts)
-> bindTerms (\tm => env tm) tms = map (\t => bindTerm (\tm => env tm)) tms
bindTermsIsMap env [] = Refl
bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts)
-- FIXME: these names shouldn't be public. Indication of bad API design
namespace Rel
public export
data (~=~) : forall v . (0 r : IRel v) -> IRel (Term sig v)
where
Done' : {0 v : sig.T -> Type} -> {0 r : IRel v}
-> {t : sig.T} -> {i, j : v t}
-> r t i j
-> (~=~) {sig} {v} r t (Done i) (Done j)
Call' : {0 v : sig.T -> Type} -> {0 r : IRel v}
-> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig v ^ op.arity}
-> Pointwise ((~=~) {sig} {v} r) tms tms'
-> (~=~) {sig} {v} r t (Call op tms) (Call op tms')
public export
tmRelEqualIsEqual : (~=~) (\_ => Equal) t tm tm' -> tm = tm'
public export
tmsRelEqualIsEqual : Pointwise ((~=~) (\_ => Equal)) tms tms' -> tms = tms'
tmRelEqualIsEqual (Done' eq) = cong Done eq
tmRelEqualIsEqual (Call' op eqs) = cong (Call op) $ tmsRelEqualIsEqual eqs
tmsRelEqualIsEqual [] = Refl
tmsRelEqualIsEqual (eq :: eqs) = cong2 (::) (tmRelEqualIsEqual eq) (tmsRelEqualIsEqual eqs)
public export
tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
-> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm
public export
tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
-> {ts : List sig.T} -> (tms : Term sig V ^ ts) -> Pointwise ((~=~) rel) tms tms
tmRelRefl refl (Done i) = Done' reflexive
tmRelRefl refl (Call op ts) = Call' op (tmsRelRefl refl ts)
tmsRelRefl refl [] = []
tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts
public export
tmRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
-> {t : sig.T} -> {tm, tm' : Term sig V t} -> tm = tm' -> (~=~) rel t tm tm'
tmRelReflexive refl Refl = tmRelRefl refl _
public export
tmsRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
-> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
-> tms = tms' -> Pointwise ((~=~) rel) tms tms'
tmsRelReflexive refl Refl = tmsRelRefl refl _
public export
tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
-> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm
public export
tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
-> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
-> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms
tmRelSym sym (Done' i) = Done' (symmetric i)
tmRelSym sym (Call' op ts) = Call' op (tmsRelSym sym ts)
tmsRelSym sym [] = []
tmsRelSym sym (t :: ts) = tmRelSym sym t :: tmsRelSym sym ts
public export
tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
-> {t : sig.T} -> {tm, tm', tm'' : Term sig V t}
-> (~=~) rel t tm tm' -> (~=~) rel t tm' tm'' -> (~=~) rel t tm tm''
public export
tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
-> {ts : List sig.T} -> {tms, tms', tms'' : Term sig V ^ ts}
-> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms''
-> Pointwise ((~=~) rel) tms tms''
tmRelTrans trans (Done' i) (Done' j) = Done' (transitive i j)
tmRelTrans trans (Call' op ts) (Call' _ ts') = Call' op (tmsRelTrans trans ts ts')
tmsRelTrans trans [] [] = []
tmsRelTrans trans (t :: ts) (t' :: ts') = tmRelTrans trans t t' :: tmsRelTrans trans ts ts'
export
tmRelEq : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IEquivalence V rel
-> IEquivalence _ ((~=~) {sig = sig} {v = V} rel)
tmRelEq eq t = MkEquivalence
(MkReflexive $ tmRelRefl (\t => (eq t).refl) _)
(MkSymmetric $ tmRelSym (\t => (eq t).sym))
(MkTransitive $ tmRelTrans (\t => (eq t).trans))
public export
Free : (0 V : sig.T -> Type) -> RawAlgebra sig
Free v = MkRawAlgebra (Term sig v) Call
public export
FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.relation)
FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call'
public export
FreeAlgebra : ISetoid sig.T -> Algebra sig
FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
public export
bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
-> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y))
-> {t : sig.T} -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm'
-> a.relation t (bindTerm {a = a.raw} env tm) (bindTerm {a = a.raw} env' tm')
public export
bindTermsCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
-> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y))
-> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms'
-> Pointwise a.relation (bindTerms {a = a.raw} env tms) (bindTerms {a = a.raw} env' tms')
bindTermCong' cong (Done' i) = cong _ i
bindTermCong' {a = a} cong (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong ts)
bindTermsCong' cong [] = []
bindTermsCong' cong (t :: ts) = bindTermCong' cong t :: bindTermsCong' cong ts
public export
bindTermCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
-> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm'
-> a.relation t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
bindTermCong env = bindTermCong' env.cong
public export
bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
-> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms'
-> Pointwise a.relation
(bindTerms {a = a.raw} env.func tms)
(bindTerms {a = a.raw} env.func tms')
bindTermsCong env = bindTermsCong' env.cong
public export
bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid)
-> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func)
bindIsHomo a env = MkIsHomomorphism
(\t, eq => bindTermCong env eq)
(\op, tms =>
a.algebra.semCong op $
map (\t => (a.algebra.equivalence t).equalImpliesEq) $
equalImpliesPwEq $
bindTermsIsMap {a = a.raw} env.func tms)
public export
bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (FreeAlgebra v) a
bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
public export
bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
-> (f, g : Homomorphism (FreeAlgebra v) a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
-> {t : sig.T} -> (tm : Term sig v.U t)
-> a.relation t (f.func t tm) (g.func t tm)
public export
bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
-> (f, g : Homomorphism (FreeAlgebra v) a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
-> Pointwise a.relation (map f.func tms) (map g.func tms)
bindUnique' f g cong (Done i) = cong i
bindUnique' f g cong (Call op ts) = CalcWith (a.setoid.index _) $
|~ f.func _ (Call op ts)
~~ a.raw.sem op (map f.func ts) ...( f.homo.semHomo op ts )
~~ a.raw.sem op (map g.func ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
~~ g.func _ (Call op ts) ..<( g.homo.semHomo op ts )
bindsUnique' f g cong [] = []
bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts
public export
bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
-> (f : Homomorphism (FreeAlgebra v) a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
-> {t : sig.T} -> (tm : Term sig v.U t)
-> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm)
bindUnique env f = bindUnique' f (bindHomo env)
public export
bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
-> (f : Homomorphism (FreeAlgebra v) a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
-> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms)
bindsUnique env f cong ts = CalcWith (pwSetoid a.setoid _) $
|~ map f.func ts
~~ map (\_ => bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts )
~~ bindTerms {a = a.raw} env.func ts .=<( bindTermsIsMap {a = a.raw} env.func ts )
|
