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
|
module Data.Fin.Occurs
import Data.DPair
import Data.Fin
import Data.Maybe.Properties
-- Utilities -------------------------------------------------------------------
predInjective : {n : Nat} -> pred n = S k -> n = S (S k)
predInjective {n = S n} prf = cong S prf
indexIsSuc : Fin n -> Exists (\k => n = S k)
indexIsSuc FZ = Evidence _ Refl
indexIsSuc (FS x) = Evidence _ Refl
%inline %tcinline
zero : (0 _ : Fin n) -> Fin n
zero x = rewrite snd (indexIsSuc x) in FZ
%inline %tcinline
suc : (_ : Fin (pred n)) -> Fin n
suc x =
replace {p = Fin}
(sym $ predInjective $ snd $ indexIsSuc x)
(FS $ rewrite sym $ snd $ indexIsSuc x in x)
-- Thinning --------------------------------------------------------------------
export
thin : Fin n -> Fin (pred n) -> Fin n
thin FZ y = FS y
thin (FS x) FZ = FZ
thin (FS x) (FS y) = FS (thin x y)
-- Properties
export
thinInjective : (x : Fin n) -> {y, z : Fin (pred n)} -> thin x y = thin x z -> y = z
thinInjective FZ prf = injective prf
thinInjective (FS x) {y = FZ, z = FZ} prf = Refl
thinInjective (FS x) {y = FS y, z = FS z} prf = cong FS $ thinInjective x $ injective prf
export
thinSkips : (x : Fin n) -> (y : Fin (pred n)) -> Not (thin x y = x)
thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)
thinSucZero : (x : Fin n) -> thin (FS x) (zero x) = FZ
thinSucZero FZ = Refl
thinSucZero (FS x) = Refl
thinSucSuc : (x : Fin n) -> (z : Fin (pred n)) -> thin (FS x) (suc z) = FS (thin x z)
thinSucSuc FZ FZ = Refl
thinSucSuc FZ (FS x) = Refl
thinSucSuc (FS x) FZ = Refl
thinSucSuc (FS x) (FS y) = Refl
export
thinInverse : (x, y : Fin n) -> Not (x = y) -> (z ** thin x z = y)
thinInverse FZ FZ neq = void (neq Refl)
thinInverse FZ (FS y) neq = (y ** Refl)
thinInverse (FS x) FZ neq = (zero x ** thinSucZero x)
thinInverse (FS x) (FS y) neq =
let (z ** prf) = thinInverse x y (\eq => neq $ cong FS eq) in
(suc z ** trans (thinSucSuc x z) (cong FS prf))
-- Thickening ------------------------------------------------------------------
export
thick : Fin n -> Fin n -> Maybe (Fin (pred n))
thick FZ FZ = Nothing
thick FZ (FS y) = Just y
thick (FS x) FZ = Just (zero x)
thick (FS x) (FS y) = [| suc (thick x y) |]
export
thickIsNothing : (x, y : Fin n) -> (x = y) <=> (thick x y = Nothing)
thickIsNothing FZ FZ = MkEquivalence (const Refl) (const Refl)
thickIsNothing FZ (FS y) = MkEquivalence absurd absurd
thickIsNothing (FS x) FZ = MkEquivalence absurd absurd
thickIsNothing (FS x) (FS y) =
let rec = thickIsNothing x y in
MkEquivalence
(cong (Just suc <*>) . rec.leftToRight . injective)
(cong FS . rec.rightToLeft . appNothingRight suc (thick x y))
export
thickIsJust : (x, y : Fin n) -> Not (x = y) <=> (z ** (thick x y = Just z, thin x z = y))
thickIsJust FZ FZ = MkEquivalence (\f => absurd $ f Refl) (\p => absurd $ fst $ snd p)
thickIsJust FZ (FS y) = MkEquivalence (const (y ** (Refl, Refl))) (const absurd)
thickIsJust (FS x) FZ =
MkEquivalence
(const (zero x ** (Refl, thinSucZero x)))
(const absurd)
thickIsJust (FS x) (FS y) =
let rec = thickIsJust x y in
MkEquivalence
(\neq =>
let (z ** (prf1, prf2)) = rec.leftToRight (neq . cong FS) in
(suc z ** (rewrite prf1 in Refl, trans (thinSucSuc x z) (cong FS prf2))))
(\(z ** (prf1, prf2)), prf => thinSkips (FS x) z $ trans prf2 (sym prf))
|
