-
Notifications
You must be signed in to change notification settings - Fork 0
/
C.idr
109 lines (79 loc) · 2.84 KB
/
C.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
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
-- Classical logic, PHOAS approach, initial encoding
module Pi.C
%default total
-- Types
data Indiv : Type where
TODO : Indiv
Ty : Type
Pred : Type
Pred = Indiv -> Ty
infixl 2 :&&
infixl 1 :||
infixr 0 :=>
data Ty : Type where
UNIT : Ty
(:=>) : Ty -> Ty -> Ty
(:&&) : Ty -> Ty -> Ty
(:||) : Ty -> Ty -> Ty
FALSE : Ty
FORALL : Pred -> Ty
EXISTS : Pred -> Ty
infixr 0 :<=>
(:<=>) : Ty -> Ty -> Ty
(:<=>) a b = (a :=> b) :&& (b :=> a)
NOT : Ty -> Ty
NOT a = a :=> FALSE
TRUE : Ty
TRUE = FALSE :=> FALSE
-- Context and truth judgement
data El : Type where
mkTrue : Ty -> El
mkIndiv : Indiv -> El
Cx : Type
Cx = El -> Type
isTrue : Ty -> Cx -> Type
isTrue a tc = tc (mkTrue a)
isIndiv : Indiv -> Cx -> Type
isIndiv x tc = tc (mkIndiv x)
-- Terms
infixl 2 :$$
infixl 1 :$
data Tm : Cx -> Ty -> Type where
var : isTrue a tc -> Tm tc a
lam' : (isTrue a tc -> Tm tc b) -> Tm tc (a :=> b)
(:$) : Tm tc (a :=> b) -> Tm tc a -> Tm tc b
pair : Tm tc a -> Tm tc b -> Tm tc (a :&& b)
fst : Tm tc (a :&& b) -> Tm tc a
snd : Tm tc (a :&& b) -> Tm tc b
left : Tm tc a -> Tm tc (a :|| b)
right : Tm tc b -> Tm tc (a :|| b)
case' : Tm tc (a :|| b) -> (isTrue a tc -> Tm tc c) -> (isTrue b tc -> Tm tc c) -> Tm tc c
pi' : ({x : Indiv} -> isIndiv x tc -> Tm tc (p x)) -> Tm tc (FORALL p)
(:$$) : Tm tc (FORALL p) -> isIndiv x tc -> Tm tc (p x)
sig : isIndiv x tc -> Tm tc (p x) -> Tm tc (EXISTS p)
split' : Tm tc (EXISTS p) -> (isTrue (p x) tc -> Tm tc a) -> Tm tc a
abort' : (isTrue (NOT a) tc -> Tm tc FALSE) -> Tm tc a
lam'' : (Tm tc a -> Tm tc b) -> Tm tc (a :=> b)
lam'' f = lam' $ \x => f (var x)
case'' : Tm tc (a :|| b) -> (Tm tc a -> Tm tc c) -> (Tm tc b -> Tm tc c) -> Tm tc c
case'' xy f g = case' xy (\x => f (var x)) (\y => g (var y))
split'' : Tm tc (EXISTS p) -> (Tm tc (p x) -> Tm tc a) -> Tm tc a
split'' x f = split' x $ \y => f (var y)
abort'' : (Tm tc (NOT a) -> Tm tc FALSE) -> Tm tc a
abort'' f = abort' $ \na => f (var na)
syntax "lam" {a} ":=>" [b] = lam'' (\a => b)
syntax "[" [a] "," [b] "]" = pair a b
syntax "case" [ab] "of" {a} ":=>" [c1] or {b} ":=>" [c2] = case'' ab (\a => c1) (\b => c2)
syntax "pi" {x} ":=>" [y] = pi' (\x => y)
syntax "[" [x] ",," [y] "]" = sig x y
syntax "split" [x] as {y} ":=>" [z] = split'' x (\y => z)
syntax "abort" {a} ":=>" [b] = abort'' (\a => b)
Thm : Ty -> Type
Thm a = {tc : Cx} -> Tm tc a
-- Example theorems
t214 : Thm (NOT (FORALL (\x => NOT (p x))) :=> EXISTS p)
t214 =
lam f :=>
abort g :=>
f :$ (pi x :=>
lam p :=> g :$ [ x ,, p ])