blob: bbf6dd6f84c4115ef0a02307e6384e07dbd41c40 (
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
|
module Data.Fin.Occurs
import Data.DPair
import Data.Fin
import Data.Maybe
import Data.Nat
import Syntax.PreorderReasoning
-- Thinning --------------------------------------------------------------------
export
thin : Fin (S n) -> Fin n -> Fin (S 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 (S n)) -> {y, z : Fin 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 (S n)) -> (y : Fin n) -> Not (thin x y = x)
thinSkips FZ y prf = absurd prf
thinSkips (FS x) (FS y) prf = thinSkips x y (injective prf)
-- Thickening ------------------------------------------------------------------
export
thick : {n : Nat} -> Fin (S n) -> Fin (S n) -> Maybe (Fin n)
thick FZ FZ = Nothing
thick FZ (FS y) = Just y
thick {n = S n} (FS x) FZ = Just FZ
thick {n = S n} (FS x) (FS y) = FS <$> thick x y
public export
data ThickProof : Fin (S n) -> Fin (S n) -> Maybe (Fin n) -> Type where
Equal : res = Nothing -> ThickProof x x res
Thinned : (y : Fin n) -> res = Just y -> ThickProof x (thin x y) res
%name ThickProof prf
export
thickProof : {n : Nat} -> (x, y : Fin (S n)) -> ThickProof x y (thick x y)
thickProof FZ FZ = Equal Refl
thickProof FZ (FS y) = Thinned y Refl
thickProof {n = S n} (FS x) FZ = Thinned FZ Refl
thickProof {n = S n} (FS x) (FS y) with (thickProof x y)
thickProof (FS x) (FS x) | Equal prf = Equal (cong (map FS) prf)
thickProof (FS x) (FS _) | Thinned y prf = Thinned (FS y) (cong (map FS) prf)
thickRefl' :
(x, y : Fin (S n)) ->
(0 _ : x = y) ->
ThickProof x y (thick x y) ->
thick x y = Nothing
thickRefl' x x _ (Equal prf) = prf
thickRefl' x (thin x z) prf (Thinned z _) = absurd $ thinSkips x z (sym prf)
export
thickRefl : {n : Nat} -> (x : Fin (S n)) -> thick x x = Nothing
thickRefl x = thickRefl' x x Refl (thickProof x x)
export
thickThin : {n : Nat} -> (x : Fin (S n)) -> (y : Fin n) -> thick x (thin x y) = Just y
thickThin x y with (thin x y) proof prf
_ | z with (thickProof x z)
thickThin x y | x | Equal prf' = absurd $ thinSkips x y prf
thickThin x y | _ | Thinned z prf' = Calc $
|~ thick x (thin x z)
~~ Just z ...(prf')
~~ Just y ..<(cong Just $ thinInjective x prf)
|
