-
Notifications
You must be signed in to change notification settings - Fork 0
/
BoxMp.idr
74 lines (51 loc) · 1.51 KB
/
BoxMp.idr
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
-- Minimal implicational modal logic, PHOAS approach, initial encoding
module Pi.BoxMp
%default total
-- Types
infixr 0 :=>
data Ty : Type where
UNIT : Ty
(:=>) : Ty -> Ty -> Ty
BOX : Ty -> Ty
-- Context and truth judgement with modal depth
Cx : Type
Cx = Nat -> Ty -> Type
isTrue : Ty -> Nat -> Cx -> Type
isTrue a d tc = tc d a
-- Terms
infixl 1 :$
data Tm : Nat -> Cx -> Ty -> Type where
var : isTrue a d tc -> Tm d tc a
lam' : (isTrue a d tc -> Tm d tc b) -> Tm d tc (a :=> b)
(:$) : Tm d tc (a :=> b) -> Tm d tc a -> Tm d tc b
box : Tm (succ d) tc a -> Tm d tc (BOX a)
unbox' : Tm d tc (BOX a) -> (isTrue a gd tc -> Tm d tc b) -> Tm d tc b
lam'' : (Tm d tc a -> Tm d tc b) -> Tm d tc (a :=> b)
lam'' f = lam' $ \x => f (var x)
unbox'' : Tm d tc (BOX a) -> (Tm gd tc a -> Tm d tc b) -> Tm d tc b
unbox'' x' f = unbox' x' $ \x => f (var x)
syntax "lam" {a} ":=>" [b] = lam'' (\a => b)
syntax "unbox" [a'] as {a} ":=>" [b] = unbox'' a' (\a => b)
Thm : Ty -> Type
Thm a = {d : Nat} -> {tc : Cx} -> Tm d tc a
-- Example theorems
rNec : Thm a -> Thm (BOX a)
rNec x =
box x
aK : Thm (BOX (a :=> b) :=> BOX a :=> BOX b)
aK =
lam f' :=>
lam x' :=>
unbox f' as f :=>
unbox x' as x :=> box (f :$ x)
aT : Thm (BOX a :=> a)
aT =
lam x' :=>
unbox x' as x :=> x
a4 : Thm (BOX a :=> BOX (BOX a))
a4 =
lam x' :=>
unbox x' as x :=> box (box x)
t1 : Thm (a :=> BOX (a :=> a))
t1 =
lam x :=> box (lam y :=> y)