S-design-memo-2
Let's not have line oriented syntax, rather have semicolon separated syntax
code:s
th theorem0(A a { E b { b < a } }) {
-- axiom 1;
(1) statement_1;
-- axiom 2;
(2) statement_2;
-- use theorem0;
(3) statement_3;
}
But let's do automatic semicolon insertion in a way similar to golang
ref: https://medium.com/golangspec/automatic-semicolon-insertion-in-go-1990338f2649
A line starting with -- denotes the line is inference, not a claim.
A line not starting with -- denotes the line is a claim.
A claim line can optionally be prefixed by (N) and can be referenced as (N) in later inferences.
code:s
th ex0 (p -> r) | (q -> r) -> (p & q -> r) {
-- ax
p |- p
-- WL ^
p, q |- p
-- WR ^
p, q |- r, p
-- notR ^
(2) ~p, p, q |- r
-- ax
r |- r
-- WL
r, p |- r
-- WL
(3) r, p, q |- r
~p | r, p, q |- r =>
p -> r, p, q |- r --X
p, q |- r, q =>
~q, p, q |- r --
r, p, q |- r --
^=> ^^=>
~q | r, p, q |- r =>
q -> r, p, q |- r --
X=> ^=>
(p -> r) | (q -> r), p, q |- r =>
(p -> r) | (q -> r), p & q |- r =>
(p -> r) | (q -> r) |- p & q -> r =>
|- (p -> r) | (q -> r) -> (p & q -> r)