-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtest_itt.elpi
79 lines (61 loc) · 2.4 KB
/
test_itt.elpi
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
accumulate itp.
accumulate itt/theory.
interactive TestName OutputTerm :-
interactive TestName [] OutputTerm.
interactive TestName InScript OutputTerm :-
TestName Type,
prove X Type InScript ProofTerm _,
print "raw out" ProofTerm "::" Type,
print_pt ProofTerm Type OutputTerm.
print_pt Term Type S :-
pp Term TermPP, pp Type TypePP, !,
S is TermPP ^ " :: " ^ TypePP.
identity (@arrow a a).
test_mapp (@arrow (@arrow a (@arrow b c)) (@arrow a (@arrow b c))).
% ---------------------- %
% ---- K combinator ---- %
% ---------------------- %
% [intro x, intro y, mapp x]
comb_K (@arrow a (@arrow b a)).
% ---------------------- %
% ---- S combinator ---- %
% ---------------------- %
% [intro g, intro f, intro x, mapp g, mapp x, mapp f, mapp x]
comb_S (@arrow (@arrow a (@arrow b c)) (@arrow (@arrow a b) (@arrow a c))).
% axioms of conjunction
% [intro x, intro y, andI, mapp x, mapp y]
andIntro (@arrow a (@arrow b (@times a b))).
% [intro p, andEL p]
andElimL (@arrow (@times a b) a).
% [intro p, andER p]
andElimR (@arrow (@times a b) b).
%
superAnd (@arrow a (@arrow b (@arrow c (@arrow d (@times (@times a b) (@times c d)))))).
% [intro f, intro p, andE p y z, mapp f, mapp x, mapp y]
implAnd (@arrow (@arrow a (@arrow b c)) (@arrow (@times a b) c)).
% [intro f, andI, maptac (intro x) [3, 4], andEL, mapp f, mapp x, andER, mapp f, mapp x]
choice (@arrow (prod a (x\ sum b (y\ c))) (sum (prod a (x\ b)) (f\ prod a (x\ c)))).
% [intro x, idIntro]
intro_id_axiom (prod a (x\ id a x x)).
elim_id_axiom (prod a (x\ prod a (y\ @arrow (id a x y) (@arrow (B x) (B y))))).
test_all L :-
print "start",
interactive identity [intro x, mapp x] S1,
print "1/9",
interactive comb_K [intro x, intro y, mapp x] S2,
print "2/9",
interactive comb_S [intro g, intro f, intro x, mapp g, mapp x, mapp f, mapp x] S3,
print "3/9",
interactive andIntro [intro x, intro y, andI, mapp x, mapp y] S4,
print "4/9",
interactive andElimL [intro p, andEL p] S5,
print "5/9",
interactive andElimR [intro p, andER p] S6,
print "6/9",
interactive implAnd [intro f, intro p, andE p x y, mapp f, mapp x, mapp y] S7,
print "7/9",
interactive choice [intro f, andI, maptac (intro x) [3, 4], andEL, mapp f, mapp x, andER, mapp f, mapp x] S8,
print "8/9",
interactive intro_id_axiom [intro x, idIntro] S9,
print "9/9",
L = [S1, S2, S3, S4, S5, S6, S7, S8, S9].