blob: 959702de62975016a7233e036756a9ced5a91bab (
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
|
module Core.Thinning
import Data.Fin
-- Definition ------------------------------------------------------------------
data Thinner : Nat -> Nat -> Type where
IsBase : Thinner n (S n)
IsDrop : Thinner m n -> Thinner m (S n)
IsKeep : Thinner m n -> Thinner (S m) (S n)
export
data Thins : Nat -> Nat -> Type where
IsId : n `Thins` n
IsThinner : Thinner m n -> m `Thins` n
%name Thinner thin
%name Thins thin
-- Constructors ----------------------------------------------------------------
export
id : (0 n : Nat) -> n `Thins` n
id n = IsId
export
drop : m `Thins` n -> m `Thins` S n
drop IsId = IsThinner IsBase
drop (IsThinner thin) = IsThinner (IsDrop thin)
export
keep : m `Thins` n -> S m `Thins` S n
keep IsId = IsId
keep (IsThinner thin) = IsThinner (IsKeep thin)
-- Non-Identity ----------------------------------------------------------------
export
data IsNotId : m `Thins` n -> Type where
ItIsThinner : IsNotId (IsThinner thin)
%name IsNotId prf
-- Views -----------------------------------------------------------------------
public export
data View : m `Thins` n -> Type where
Id : (0 n : Nat) -> View (id n)
Drop : (thin : m `Thins` n) -> View (drop thin)
Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)
export
view : (thin : m `Thins` n) -> View thin
view IsId = Id m
view (IsThinner IsBase) = Drop (id _)
view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
-- Composition -----------------------------------------------------------------
comp : Thinner m n -> Thinner k m -> Thinner k n
comp IsBase thin2 = IsDrop thin2
comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) IsBase = IsDrop thin1
comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)
export
(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
IsId . thin2 = thin2
IsThinner thin1 . IsId = IsThinner thin1
IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)
-- Specific Cases
export
compRightId : (thin : m `Thins` n) -> thin . id m = thin
compRightId IsId = Refl
compRightId (IsThinner thin) = Refl
export
compKeep :
(thin1 : m `Thins` n) ->
(thin2 : k `Thins` m) ->
keep thin1 . keep thin2 = keep (thin1 . thin2)
compKeep IsId thin2 = Refl
compKeep (IsThinner thin1) IsId = Refl
compKeep (IsThinner thin1) (IsThinner thin2) = Refl
-- Weakening -------------------------------------------------------------------
wkn' : Fin m -> Thinner m n -> Fin n
wkn' i IsBase = FS i
wkn' i (IsDrop thin) = FS (wkn' i thin)
wkn' FZ (IsKeep thin) = FZ
wkn' (FS i) (IsKeep thin) = FS (wkn' i thin)
export
wkn : Fin m -> m `Thins` n -> Fin n
wkn i IsId = i
wkn i (IsThinner thin) = wkn' i thin
-- Properties
wkn'Homo :
(i : Fin k) ->
(thin2 : Thinner m n) ->
(thin1 : Thinner k m) ->
wkn' (wkn' i thin1) thin2 = wkn' i (comp thin2 thin1)
wkn'Homo i IsBase thin1 = Refl
wkn'Homo i (IsDrop thin2) thin1 = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo i (IsKeep thin2) IsBase = Refl
wkn'Homo i (IsKeep thin2) (IsDrop thin1) = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo FZ (IsKeep thin2) (IsKeep thin1) = Refl
wkn'Homo (FS i) (IsKeep thin2) (IsKeep thin1) = cong FS (wkn'Homo i thin2 thin1)
export
wknHomo :
(i : Fin k) ->
(thin1 : k `Thins` m) ->
(thin2 : m `Thins` n) ->
wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
wknHomo i IsId thin2 = sym $ cong (wkn i) $ compRightId thin2
wknHomo i (IsThinner thin1) IsId = Refl
wknHomo i (IsThinner thin1) (IsThinner thin2) = wkn'Homo i thin2 thin1
|
