blob: 09ba2c9462b07844b778e8abdb377782732e11b8 (
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
|
module Data.Term.Zipper
import Data.DPair
import Data.Fin.Occurs
import Data.Vect.Properties.Insert
import Data.Vect.Properties.Map
import Data.Term
import Syntax.PreorderReasoning
-- Definition ------------------------------------------------------------------
public export
data Zipper : Signature -> Nat -> Type where
Top : Zipper sig n
Op : sig.Operator (S k) -> Fin (S k) -> Vect k (Term sig n) -> Zipper sig n -> Zipper sig n
%name Zipper zip
-- Monoid ----------------------------------------------------------------------
export
(++) : Zipper sig n -> Zipper sig n -> Zipper sig n
Top ++ zip2 = zip2
Op op i ts zip1 ++ zip2 = Op op i ts (zip1 ++ zip2)
-- Properties
export
leftUnit : (zip : Zipper sig n) -> Top ++ zip = zip
leftUnit zip = Refl
export
rightUnit : (zip : Zipper sig n) -> zip ++ Top = zip
rightUnit Top = Refl
rightUnit (Op op i ts zip) = cong (Op op i ts) (rightUnit zip)
export
assoc : (zip1, zip2, zip3 : Zipper sig n) -> (zip1 ++ zip2) ++ zip3 = zip1 ++ (zip2 ++ zip3)
assoc Top zip2 zip3 = Refl
assoc (Op op i ts zip1) zip2 zip3 = cong (Op op i ts) (assoc zip1 zip2 zip3)
-- Action ----------------------------------------------------------------------
export
(+) : Zipper sig n -> Term sig n -> Term sig n
Top + t = t
Op op i ts zip + t = Op op (insertAt i (zip + t) ts)
-- Properties
export
actionAssoc :
(zip1, zip2 : Zipper sig n) ->
(t : Term sig n) ->
(zip1 ++ zip2) + t = zip1 + (zip2 + t)
actionAssoc Top zip2 t = Refl
actionAssoc (Op op i ts zip1) zip2 t =
cong (\t => Op op (insertAt i t ts)) $ actionAssoc zip1 zip2 t
-- Substitution ----------------------------------------------------------------
export
(<$>) : (Fin k -> Term sig n) -> Zipper sig k -> Zipper sig n
f <$> Top = Top
f <$> Op op i ts zip = Op op i (map (f <$>) ts) (f <$> zip)
-- Properties
export
actionHomo :
(0 f : Fin k -> Term sig n) ->
(zip : Zipper sig k) ->
(0 t : Term sig k) ->
f <$> zip + t = (f <$> zip) + (f <$> t)
actionHomo f Top t = Refl
actionHomo f (Op op i ts zip) t = cong (Op op) $ Calc $
|~ map (f <$>) (insertAt i (zip + t) ts)
~~ insertAt i (f <$> zip + t) (map (f <$>) ts) ...(mapInsertAt (f <$>) i (zip + t) ts)
~~ insertAt i ((f <$> zip) + (f <$> t)) (map (f <$>) ts) ...(cong (\t => insertAt i t (map (f <$>) ts)) $ actionHomo f zip t)
-- Cycles ----------------------------------------------------------------------
pivotAt : sig.Operator k -> Fin k -> Vect k (Term sig n) -> Zipper sig n
pivotAt op i ts =
let op' = replace {p = sig.Operator} (snd prf) op in
let i' = replace {p = Fin} (snd prf) i in
let ts' = replace {p = flip Vect (Term sig n)} (snd prf) ts in
Op op' i' (deleteAt i' ts') Top
where
prf : Exists (\j => k = S j)
prf = indexIsSuc i
actionPivotAt :
(op : sig.Operator k) ->
(i : Fin k) ->
(ts : Vect k (Term sig n)) ->
pivotAt op i ts + index i ts = Op op ts
actionPivotAt op i@FZ ts = cong (Op op) $ insertAtIndex i ts
actionPivotAt op i@(FS _) ts = cong (Op op) $ insertAtIndex i ts
pivotNotTop : (zip : Zipper sig k) -> Not (zip ++ pivotAt op i ts = Top)
pivotNotTop (Op op' j us zip) prf impossible
export
noCycles : (zip : Zipper sig k) -> (t : Term sig k) -> zip + t = t -> zip = Top
noCycles Top t prf = Refl
noCycles (Op {k} op i ts zip') t@(Op {k = j} op' us) prf =
void $ pivotNotTop zip' prf''
where
I : Fin j
I = replace {p = Fin} (opInjectiveLen prf) i
prf' : ((zip' ++ pivotAt op' I us) + index I us = index I us)
prf' = Calc $
|~ (zip' ++ pivotAt op' I us) + index I us
~~ zip' + (pivotAt op' I us + index I us) ...(actionAssoc zip' (pivotAt op' I us) (index I us))
~~ zip' + Op op' us ...(cong (zip' +) $ actionPivotAt op' I us)
~~ index i (insertAt i (zip' + Op op' us) ts) ..<(indexInsertAt i (zip' + Op op' us) ts)
~~ index i (rewrite opInjectiveLen prf in us) ...(cong (index i) $ opInjectiveTs prf)
~~ index I us ...(rewrite opInjectiveLen prf in Refl)
prf'' : zip' ++ pivotAt op' I us = Top
prf'' = noCycles (zip' ++ pivotAt op' I us) (assert_smaller t (index I us)) prf'
|
