blob: 4caa089ec28f8ef31384952a817af0ecd417f29e (
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 Data.Term.Occurs
import Data.Fin.Occurs
import Data.Maybe.Properties
import Data.Term
import Data.Term.Zipper
import Syntax.PreorderReasoning
-- Check -----------------------------------------------------------------------
export
check : Fin k -> Term sig k -> Maybe (Term sig (pred k))
checkAll : Fin k -> Vect n (Term sig k) -> Maybe (Vect n (Term sig (pred k)))
check x (Var y) = Var <$> thick x y
check x (Op op ts) = Op op <$> checkAll x ts
checkAll x [] = Just []
checkAll x (t :: ts) = [| check x t :: checkAll x ts |]
-- Properties
export
checkOccurs : (x : Fin k) -> (zip : Zipper sig k) -> IsNothing (check x (zip + Var x))
checkAllOccurs :
(x : Fin k) ->
(i : Fin (S n)) ->
(ts : Vect n (Term sig k)) ->
(zip : Zipper sig k) ->
IsNothing (checkAll x (insertAt i (zip + Var x) ts))
checkOccurs x Top = mapNothing Var (thickRefl x)
checkOccurs x (Op op i ts zip) = mapNothing (Op op) (checkAllOccurs x i ts zip)
checkAllOccurs x FZ ts zip =
appLeftNothingIsNothing
(appRightNothingIsNothing (Just (::)) (checkOccurs x zip))
(checkAll x ts)
checkAllOccurs x (FS i) (t :: ts) zip =
appRightNothingIsNothing
(Just (::) <*> check x t)
(checkAllOccurs x i ts zip)
export
checkNothing :
(x : Fin k) ->
(t : Term sig k) ->
(0 _ : IsNothing (check x t)) ->
(zip : Zipper sig k ** t = zip + Var x)
checkAllNothing :
(x : Fin k) ->
(t : Term sig k) ->
(ts : Vect n (Term sig k)) ->
(0 _ : IsNothing (checkAll x (t :: ts))) ->
(i ** ts' ** zip : Zipper sig k ** t :: ts = insertAt i (zip + Var x) ts')
checkNothing x (Var y) prf =
(Top ** sym (cong Var (thickNothing x y (mapNothingInverse Var (thick x y) prf))))
checkNothing x (Op op (t :: ts)) prf =
let (i ** ts' ** zip ** prf) = checkAllNothing x t ts (mapNothingInverse (Op op) _ prf) in
(Op op i ts' zip ** cong (Op op) prf)
checkAllNothing x t ts prf with (appNothingInverse (Just (::) <*> check x t) (checkAll x ts) prf)
_ | Left prf' = case appNothingInverse (Just (::)) (check x t) prf' of
Right prf =>
let (zip ** prf) = checkNothing x t prf in
(FZ ** ts ** zip ** cong (:: ts) prf)
checkAllNothing x t (t' :: ts) prf | Right prf' =
let (i ** ts ** zip ** prf) = checkAllNothing x t' ts prf' in
(FS i ** t :: ts ** zip ** cong (t ::) prf)
export
checkThin : (x : Fin k) -> (t : Term sig (pred k)) -> IsJust (check x (pure (thin x) <$> t))
checkAllThin :
(x : Fin k) ->
(ts : Vect n (Term sig (pred k))) ->
IsJust (checkAll x (map (pure (thin x) <$>) ts))
checkThin x (Var y) = mapIsJust Var (thickNeq x (thin x y) (\prf => thinSkips x y $ sym prf))
checkThin x (Op op ts) = mapIsJust (Op op) (checkAllThin x ts)
checkAllThin x [] = ItIsJust
checkAllThin x (t :: ts) =
appIsJust
(appIsJust ItIsJust (checkThin x t))
(checkAllThin x ts)
export
checkJust :
(x : Fin k) ->
(t : Term sig k) ->
(0 _ : check x t = Just u) ->
t = pure (thin x) <$> u
checkAllJust :
(x : Fin k) ->
(ts : Vect n (Term sig k)) ->
(0 _ : checkAll x ts = Just us) ->
ts = map (pure (thin x) <$>) us
checkJust x (Var y) prf =
let 0 z = mapJustInverse Var (thick x y) prf in
let 0 prf = thickJust x y (fst z.snd) in
sym $ Calc $
|~ pure (thin x) <$> u
~~ pure (thin x) <$> Var z.fst ...(cong (pure (thin x) <$>) $ snd z.snd)
~~ Var y ...(cong Var prf)
checkJust x (Op op ts) prf =
let 0 z = mapJustInverse (Op op) (checkAll x ts) prf in
let 0 prf = checkAllJust x ts (fst z.snd) in
Calc $
|~ Op op ts
~~ pure (thin x) <$> Op op z.fst ...(cong (Op op) prf)
~~ pure (thin x) <$> u ...(sym $ cong (pure (thin x) <$>) $ snd z.snd)
checkAllJust x [] Refl = Refl
checkAllJust x (t :: ts) prf =
let 0 z = appJustInverse (Just (::) <*> check x t) (checkAll x ts) prf in
let 0 w = appJustInverse (Just (::)) (check x t) (fst z.snd.snd) in
Calc $
|~ t :: ts
~~ map (pure (thin x) <$>) (w.snd.fst :: z.snd.fst) ...(cong2 (::) (checkJust x t (fst $ snd w.snd.snd)) (checkAllJust x ts (fst $ snd z.snd.snd)))
~~ map (pure (thin x) <$>) (w.fst w.snd.fst z.snd.fst) ...(cong (\f => map (pure (thin x) <$>) (f w.snd.fst z.snd.fst)) $ injective $ fst w.snd.snd)
~~ map (pure (thin x) <$>) (z.fst z.snd.fst) ...(sym $ cong (\f => map (pure (thin x) <$>) (f z.snd.fst)) $ snd $ snd w.snd.snd)
~~ map (pure (thin x) <$>) us ...(sym $ cong (map (pure (thin x) <$>)) $ snd $ snd z.snd.snd)
|
