blob: 4b0ac3e001611d229d0d4842bb30c6dfa75e48fc (
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
|
module Data.Term
import public Data.Vect
import public Data.Fin.Strong
import Data.Vect.Properties.Map
import Syntax.PreorderReasoning
%prefix_record_projections off
-- Definition ------------------------------------------------------------------
public export
record Signature where
Operator : Nat -> Type
%name Signature sig
public export
data Term : Signature -> Nat -> Type where
Var : SFin (S n) -> Term sig (S n)
Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n
%name Term t, u, v
export
Var' : SFin n -> Term sig n
Var' x = rewrite indexPred'Prf x in Var (replace {p = SFin} (indexPred'Prf x) x)
export
varIsVar : (x : SFin (S n)) -> Var' x = Var x
varIsVar x = Refl
-- Substitution ----------------------------------------------------------------
export
pure : (SFin k -> SFin n) -> SFin k -> Term sig n
pure r = Var' . r
export
(<$>) : (SFin 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 (SFin k -> Term sig n)
f .=. g = (i : SFin k) -> f i = g i
export
subCong : {f, g : SFin k -> Term sig n} -> f .=. g -> (t : Term sig k) -> f <$> t = g <$> t
subCong prf (Var i) = prf i
subCong prf (Op op ts) =
cong (Op op) $
mapExtensional (f <$>) (g <$>) (\t => subCong prf (assert_smaller ts t)) ts
-- Substitution is Monadic -----------------------------------------------------
export
(.) : (SFin k -> Term sig n) -> (SFin j -> Term sig k) -> SFin 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 : SFin k -> Term sig n) ->
(g : SFin 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 : SFin (S k) -> Term sig n) ->
(r : SFin j -> SFin (S k)) ->
f . pure r .=. f . r
subComp f r i = Refl
-- Injectivity -----------------------------------------------------------------
export
opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
opInjectiveLen 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
|
