blob: d292a9613e94a92004cd03b3fc0d66a31a9ea7c9 (
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
|
module Core.Term.Environment
import Core.Context
import Core.Term
import Core.Thinning
import Core.Var
import Syntax.PreorderReasoning
%prefix_record_projections off
-- Definition ------------------------------------------------------------------
public export
data Env : Context -> Type where
Lin : Env [<]
Add : Env sx -> sy `Thins` sx -> Term sy -> Env (sx :< n)
%name Env env
-- Constructors ----------------------------------------------------------------
public export
(:<) : Env sx -> Term sx -> Env (sx :< n)
env :< t = Add env (id _) t
-- Operations ------------------------------------------------------------------
record IndexResult (sx : Context) where
constructor MkRes
{0 sy : Context}
val : Term sy
thin : sy `Thins` sx
shift : IndexResult sx -> IndexResult (sx :< n)
shift (MkRes val thin) = MkRes val (drop thin n)
expand : IndexResult sx -> Term sx
expand (MkRes val thin) = wkn val thin
doIndex : Env sx -> {0 i : Var sx} -> View i -> IndexResult sx
doIndex (Add env thin t) Here = shift $ MkRes t thin
doIndex (Add env thin t) (There i) = shift $ doIndex env $ view i
export
index : Env sx -> Var sx -> Term sx
index env i = expand $ doIndex env $ view i
-- Equality --------------------------------------------------------------------
namespace Eq
public export
data EnvEq : Env sx -> Env sx -> Type where
Lin : EnvEq [<] [<]
(:<) :
EnvEq env1 env2 ->
Term.wkn t thin1 = wkn u thin2 ->
EnvEq (Add env1 thin1 t) (Add env2 thin2 u)
%name EnvEq prf
expandShift : (val : IndexResult sx) -> expand (shift val) = wkn (expand val) (drop (id sx) n)
expandShift (MkRes val thin) = sym $ Calc $
|~ wkn (wkn val thin) (drop (id sx) n)
~~ wkn val (drop (id sx) n . thin) ...(wknHomo val thin $ drop (id sx) n)
~~ wkn val (drop (id sx . thin) n) ...(cong (wkn val) $ compLeftDrop (id sx) thin n)
~~ wkn val (drop thin n) ...(cong (\thin => wkn val (drop thin n)) $ compLeftIdentity thin)
doIndexEqIsEq :
-- {env1, env2 : _} ->
EnvEq env1 env2 ->
{0 i : Var sx} ->
(view : View i) ->
expand (doIndex env1 view) = expand (doIndex env2 view)
doIndexEqIsEq {sx = sx :< n} ((:<) {t, u, thin1, thin2} prf eq) Here = Calc $
|~ wkn t (drop thin1 n)
~~ wkn (wkn t thin1) (drop (id sx) n) ...(expandShift (MkRes t thin1))
~~ wkn (wkn u thin2) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ eq)
~~ wkn u (drop thin2 n) ...(sym $ expandShift (MkRes u thin2))
doIndexEqIsEq {sx = sx :< n} ((:<) {env1, env2} prf eq) (There i) = Calc $
|~ expand (shift $ doIndex env1 $ view i)
~~ wkn (expand $ doIndex env1 $ view i) (drop (id sx) n) ...(expandShift $ doIndex env1 $ view i)
~~ wkn (expand $ doIndex env2 $ view i) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ doIndexEqIsEq prf (view i))
~~ expand (shift $ doIndex env2 $ view i) ...(sym $ expandShift $ doIndex env2 $ view i)
export
indexEqIsEq : EnvEq env1 env2 -> (i : Var sx) -> index env1 i = index env2 i
indexEqIsEq prf i = doIndexEqIsEq prf $ view i
|
