/
thatexproof.tex
90 lines (79 loc) · 2.2 KB
/
thatexproof.tex
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
%{{{ [vim]
% vim:foldmarker=%{{{,%}}}
% vim:foldmethod=marker
% vim:foldcolumn=4
%}}}
%% thatexproof.tex
%% author: Thanos Tsouanas <thanos@tsouanas.org>
% You must first load bussproofs.sty and string.sty
% If used outside of thatex, you must define
% \let\IfStrContains=\IfSubStr\relax
% \def\WhenStrContains#1#2#3{\IfStrContains {#1} {#2} {#3} {}}
\def\Assumption#1{\AxiomC{#1}}
\def\InfFromBy#1#2#3#4{% #1: arity; #2: style; #3: label; #4: conclusion
% write \RightLabel{#3} only for non-0 case
\ifcase #1
\AxiomC{}
\fi
% write \RightLabel{#3} in all cases
\RightLabel{#3}
% set style
\WhenStrContains {#2} {**} {\noLine} % no line
\WhenStrContains {#2} {--} {\singleLine\solidLine} % single solid
\WhenStrContains {#2} {==} {\doubleLine\solidLine} % double solid
\WhenStrContains {#2} {..} {\singleLine\dottedLine} % single dotted
\WhenStrContains {#2} {::} {\doubleLine\dottedLine} % double dotted
\WhenStrContains {#2} {''} {\singleLine\dashedLine} % single dashed
\WhenStrContains {#2} {""} {\doubleLine\dashedLine} % double dashed
% infer conclusion
\ifcase #1 \UnaryInfC{#4} % 0
\or \UnaryInfC{#4} % 1
\or \BinaryInfC{#4} % 2
\or \TrinaryInfC{#4} % 3
\or \QuaternaryInfC{#4} % 4
\or \QuinaryInfC{#4} % 5
\fi
}
% PROOF{,m,r,mn,mr,mrw}:
% m = assume math mode for nodes
% r = put rule labels in \rulelabel{...}
% w = space-delimited args (words)
% n = naked (no labels)
\def\PROOF#1{
\def\A{\Assumption}
\def\I##1##2 ##3##4{\InfFromBy##1{##2}{##3}{##4}}
#1
\DisplayProof
}
\def\PROOFm#1{
\def\A##1{\Assumption{$##1$}}
\def\I##1##2 ##3##4{\InfFromBy##1{##2}{##3}{$##4$}}
#1
\DisplayProof
}
\def\PROOFmn#1{
\def\A##1{\Assumption{$##1$}}
\def\I##1##2 ##3{\InfFromBy##1{##2}{}{$##3$}}
#1
\DisplayProof
}
\def\PROOFr#1{
\def\A{\Assumption}
\def\I##1##2 ##3##4{\InfFromBy##1{##2}{\rulelabel{##3}}{##4}}
#1
\DisplayProof
}
\def\PROOFmr#1{
\def\A##1{\Assumption{$##1$}}
\def\I##1##2 ##3##4{\InfFromBy##1{##2}{\rulelabel{##3}}{$##4$}}
#1
\DisplayProof
}
\def\PROOFmrw#1{
\def\A##1 {\Assumption{$##1$}}
\def\I##1##2 ##3 ##4 {\InfFromBy##1{##2}{\rulelabel{##3}}{$##4$}}
#1
\DisplayProof
}
\def\infered#1\endinfered{\PROOF{#1}}
\def\infer#1\endinfer{\math#1\endmath}