blob: 2afc7743d049bb20d3372f7e8fc3e85b1654611c (
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
|
module Data.Term
import public Data.Vect
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 : Fin n -> Term sig n
Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n
%name Term t, u, v
-- Substitution ----------------------------------------------------------------
export
pure : (Fin k -> Fin n) -> Fin k -> Term sig n
pure r = Var . r
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
-- Substitution is Monadic -----------------------------------------------------
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
-- Injectivity -----------------------------------------------------------------
export
opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
opInjectiveLen 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
|
