blob: a0ed5dfb06a1241e0810d12c54a7a033b568fe3e (
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
|
module Data.Fin.Strong
import Data.Fin
import Decidable.Equality.Core
import Syntax.PreorderReasoning
public export
data SFin : Nat -> Type where
FZ : SFin (S n)
FS : SFin (S n) -> SFin (S (S n))
public export
0 indexPred : (0 x : Fin n) -> Nat
indexPred {n = S n} x = n
public export
0 indexPredPrf : (0 x : Fin n) -> n = S (indexPred x)
indexPredPrf {n = S n} x = Refl
public export
0 indexPred' : (0 x : SFin n) -> Nat
indexPred' {n = S n} x = n
public export
0 indexPred'Prf : (0 x : SFin n) -> n = S (indexPred' x)
indexPred'Prf {n = S n} x = Refl
public export
finToStrong : Fin n -> SFin n
finToStrong FZ = FZ
finToStrong (FS x) =
rewrite indexPredPrf x in
FS (replace {p = SFin} (indexPredPrf x) (finToStrong x))
public export
strongToFin : SFin n -> Fin n
strongToFin FZ = FZ
strongToFin (FS x) = FS (strongToFin x)
export
finToStrongToFin : (x : Fin n) -> strongToFin (finToStrong x) = x
finToStrongToFin FZ = Refl
finToStrongToFin (FS FZ) = Refl
finToStrongToFin (FS (FS x)) = cong FS $ finToStrongToFin (FS x)
export
strongToFinToStrong : (x : SFin n) -> finToStrong (strongToFin x) = x
strongToFinToStrong FZ = Refl
strongToFinToStrong (FS x) = cong FS (strongToFinToStrong x)
%inline
export
FS' : SFin n -> SFin (S n)
FS' = finToStrong . FS . strongToFin
export
Injective (FS {n}) where
injective Refl = Refl
export
Injective (FS' {n}) where
injective {x = FZ, y = FZ} prf = Refl
injective {x = FS x, y = FS y} prf = cong FS $ injective {f = FS'} $ injective prf
export
Injective (strongToFin {n}) where
injective {x, y} prf = Calc $
|~ x
~~ finToStrong (strongToFin x) ..<(strongToFinToStrong x)
~~ finToStrong (strongToFin y) ...(cong finToStrong prf)
~~ y ...(strongToFinToStrong y)
export
Uninhabited (SFin 0) where uninhabited x impossible
export
Uninhabited (Strong.FS x = FZ) where uninhabited prf impossible
export
sucNonZero : (x : SFin n) -> Not (FS' x = FZ)
sucNonZero FZ prf = absurd prf
sucNonZero (FS x) prf = absurd prf
export
sucIsFS : (x : SFin (S n)) -> FS' x = FS x
sucIsFS x = rewrite strongToFinToStrong x in Refl
export
DecEq (SFin n) where
decEq x y = viaEquivalence
(MkEquivalence (injective {f = strongToFin}) (\prf => cong strongToFin prf))
(decEq (strongToFin x) (strongToFin y))
|
