blob: 973ff3d55da754477678d064db7b0da87e162347 (
plain)
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
|
module Data.Term
import public Data.DPair
import public Data.Vect
import Data.Vect.Properties.Map
import Syntax.PreorderReasoning
%prefix_record_projections off
-- Definition ------------------------------------------------------------------
public export
record Signature where
constructor MkSignature
Operator : Nat -> Type
%name Signature sig
public export
(.Op) : Signature -> Type
sig .Op = Exists sig.Operator
public export
interface DecOp (0 sig : Signature) where
decOp : (op, op' : sig.Op) -> Dec (op = op')
public export
data Term : Signature -> Nat -> Type where
Var : Fin n -> Term sig n
Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n
%name Term t, u, v
export
Uninhabited (Op op ts = Var x) where uninhabited prf impossible
-- Substitution ----------------------------------------------------------------
export
pure : (Fin k -> Fin n) -> Fin k -> Term sig n
pure r = Var . r
public export
(<$>) : (Fin k -> Term sig n) -> Term sig k -> Term sig n
f <$> Var i = f i
f <$> Op op ts = Op op (map (\t => f <$> assert_smaller ts t) ts)
-- Extensional Equality --------------------------------------------------------
public export
0 (.=.) : Rel (Fin k -> Term sig n)
f .=. g = (i : Fin k) -> f i = g i
export
subExtensional : {f, g : Fin k -> Term sig n} -> f .=. g -> (t : Term sig k) -> f <$> t = g <$> t
subExtensional prf (Var i) = prf i
subExtensional prf (Op op ts) =
cong (Op op) $
mapExtensional (f <$>) (g <$>) (\t => subExtensional prf (assert_smaller ts t)) ts
-- Substitution is Monadic -----------------------------------------------------
public export
(.) : (Fin k -> Term sig n) -> (Fin j -> Term sig k) -> Fin j -> Term sig n
f . g = (f <$>) . g
-- Properties
export
subUnit : (t : Term sig n) -> Var <$> t = t
subUnit (Var i) = Refl
subUnit (Op op ts) = cong (Op op) $ Calc $
|~ map (Var <$>) ts
~~ map id ts ...(mapExtensional (Var <$>) id (\t => subUnit (assert_smaller ts t)) ts)
~~ ts ...(mapId ts)
export
subAssoc :
(f : Fin k -> Term sig n) ->
(g : Fin j -> Term sig k) ->
(t : Term sig j) ->
(f . g) <$> t = f <$> g <$> t
subAssoc f g (Var i) = Refl
subAssoc f g (Op op ts) = cong (Op op) $ Calc $
|~ map ((f . g) <$>) ts
~~ map ((f <$>) . (g <$>)) ts ...(mapExtensional ((f . g) <$>) ((f <$>) . (g <$>)) (\t => subAssoc f g (assert_smaller ts t)) ts)
~~ map (f <$>) (map (g <$>) ts) ..<(mapFusion (f <$>) (g <$>) ts)
export
subComp :
(f : Fin k -> Term sig n) ->
(r : Fin j -> Fin k) ->
f . pure r .=. f . r
subComp f r i = Refl
export
compCong2 :
{0 f1, f2 : Fin k -> Term sig n} ->
{0 g1, g2 : Fin j -> Term sig k} ->
f1 .=. f2 ->
g1 .=. g2 ->
f1 . g1 .=. f2 . g2
compCong2 prf1 prf2 i = Calc $
|~ f1 <$> g1 i
~~ f1 <$> g2 i ...(cong (f1 <$>) $ prf2 i)
~~ f2 <$> g2 i ...(subExtensional prf1 (g2 i))
compCongL :
{0 f1, f2 : Fin k -> Term sig n} ->
f1 .=. f2 ->
(0 g : Fin j -> Term sig k) ->
f1 . g .=. f2 . g
compCongL prf g = compCong2 prf (\_ => Refl)
compCongR :
(0 f : Fin k -> Term sig n) ->
{0 g1, g2 : Fin j -> Term sig k} ->
g1 .=. g2 ->
f . g1 .=. f . g2
compCongR f prf = compCong2 (\_ => Refl) prf
-- Injectivity -----------------------------------------------------------------
export
opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
opInjectiveLen Refl = Refl
export
opInjectiveOp :
(prf : Op {sig, k} op ts = Op {sig, k = n} op' us) ->
the sig.Op (Evidence k op) = Evidence n op'
opInjectiveOp Refl = Refl
export
opInjectiveTs' : {0 ts, us : Vect k (Term sig n)} -> (prf : Op op ts = Op op us) -> ts = us
opInjectiveTs' Refl = Refl
export
opInjectiveTs :
{0 ts : Vect k (Term sig n)} ->
{0 us : Vect j (Term sig n)} ->
(prf : Op op ts = Op op' us) -> ts = (rewrite opInjectiveLen prf in us)
opInjectiveTs Refl = Refl
|
