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
|
module Soat.SecondOrder.Algebra.Lift
import Data.List.Sublist
import Data.Setoid.Indexed
import Data.Setoid.Pair
import Data.Setoid.Product
import Soat.FirstOrder.Algebra
import Soat.SecondOrder.Algebra
import Soat.SecondOrder.Signature.Lift
import Syntax.PreorderReasoning.Setoid
%default total
public export
project : RawAlgebra (lift sig) -> (ctx : List sig.T) -> RawAlgebra sig
project a ctx = MkRawAlgebra
(\t => a.U t ctx)
(\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))
public export
projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig
projectAlgebra sig a ctx = MkAlgebra
{ U = a.setoidAt ctx
, sem = \op =>
a.semFunc ctx (MkOp (Op op.op)) .
index (wrapFunc (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) (MkPair [])) _
}
public export
projectHomo : {a, b : Algebra (lift sig)} -> a ~> b
-> (ctx : _) -> projectAlgebra sig a ctx ~> projectAlgebra sig b ctx
projectHomo f ctx = MkHomomorphism
{ func = reindex (flip MkPair ctx) f.func
, semHomo = \op, tms => CalcWith (index b.setoid _) $
|~ f.func.H (_, ctx) (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
~~ b.raw.sem ctx (MkOp (Op op.op)) (map (\ty => f.func.H (snd ty, fst ty ++ ctx)) (wrap (MkPair []) tms))
...(f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f.func.H (t, ctx)) tms))
.=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $
mapWrap (MkPair []) {f = \ty => f.func.H (snd ty, fst ty ++ ctx)} tms)
}
public export
(.renameHomo) : (a : Algebra (lift sig)) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
-> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx'
(.renameHomo) a f = MkHomomorphism
{ func = a.renameFunc f
, semHomo = \op, tms => CalcWith (index a.setoid _) $
|~ a.raw.rename _ f (a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) tms))
~~ a.raw.sem _ (MkOp (Op op.op)) (map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms))
...(a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
~~ a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => a.raw.rename t f) tms))
...(a.algebra.semCong _ (MkOp (Op op.op)) $
CalcWith (index (Product (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid)) _) $
|~ map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms)
~~ wrap (MkPair []) (map (\t => a.raw.rename t (reflexive {x = []} ++ f)) tms)
.=.(mapWrap (MkPair []) tms)
~~ wrap (MkPair []) (map (\t => a.raw.rename t f) tms)
...(wrapIntro $
mapIntro'' (\t, tm, tm', eq =>
CalcWith (index a.setoid (t, _)) $
|~ a.raw.rename t (reflexive {x = []} ++ f) tm
~~ a.raw.rename t f tm
.=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry f)
~~ a.raw.rename t f tm'
...(a.algebra.renameCong t f eq)) $
(Product (a.setoidAt ctx)).equivalence.reflexive _ tms))
}
public export
(.substHomo1) : (a : Algebra (lift sig)) -> (ctx : List sig.T)
-> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx')
-> projectAlgebra sig a ctx' ~> projectAlgebra sig a ctx
(.substHomo1) a ctx tms = MkHomomorphism
{ func = bundle (\t =>
a.substFunc t ctx ctx' .
tuple
(id (index a.setoid (t, ctx')))
(const {b = index (Product (a.setoidAt ctx)) ctx'} tms))
, semHomo = \op, tms' => CalcWith (index a.setoid _) $
|~ a.raw.subst _ ctx (a.raw.sem ctx' (MkOp (Op op.op)) (wrap (MkPair []) tms')) tms
~~ a.raw.sem ctx (MkOp (Op op.op)) (map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms'))
...(a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
~~ a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms'))
...(a.algebra.semCong ctx (MkOp (Op op.op)) $
CalcWith (index (Product (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $
|~ map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms')
~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm (map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms)) tms')
.=.(mapWrap (MkPair []) tms')
~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms')
...(wrapIntro $
mapIntro' (\t, eq =>
a.algebra.substCong t ctx eq $
CalcWith (index (Product (a.setoidAt _)) _) $
|~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms
~~ map (\t => id) tms
...(mapIntro'' (\t, tm, tm', eq =>
CalcWith (index a.setoid (t, ctx)) $
|~ a.raw.rename t ([] {ys = []} ++ reflexive) tm
~~ a.raw.rename t reflexive tm
.=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry reflexive)
~~ tm
...(a.algebra.renameId t ctx tm)
~~ tm'
...(eq)) $
(Product (a.setoidAt _)).equivalence.reflexive _ _)
~~ tms
.=.(mapId tms)) $
(Product (a.setoidAt _)).equivalence.reflexive _ _))
}
|
