// Example of how we might write a conditional proof using just the
// mechanisms available in Lome 0.1.
//
// In particular, in the `assume` proof transformer, the 2nd argument
// is used to inject an arbitrary supplied term `A` into an
// `assuming(A, ...)` superterm which contains the proof.  The converse
// operation, `discharge`,
//
// Note that this is extremely low-level, in the manner of "substructural"
// proof systems; in practice we would also need to move the assumptions
// around, and possibly "bubble" them down into the term, so we would
// probably want to introduce further rules to do those operations; but
// even with those operations, this is cumbersome and tedious.
//
// Thus we are considering how to add some more mechanisms in Lome 0.2
// to handle assumptions (or more generally, context for a proof term).
// A straightforward and well-tested approach would simply be to support
// context "on the LHS of the turnstile" in the manner of sequent calculus.
// However, the exposition here encourages us to think there may be a
// simpler way, just as Lome itself is a very simple way to write proofs.

fun main() => add(1, 2)

rule pos_add(assuming(is_positive(B), assuming(is_positive(A), is_positive(add(A, B))))) =>
             assuming(is_positive(B), assuming(is_positive(A), true))
rule pos_one(is_positive(1)) => true
rule pos_two(is_positive(2)) => true

rule assume(T, A) => assuming(A, T)
rule discharge(assuming(true, T)) => T

theorem
    is_positive(add(1, 2)) => true
proof
    is_positive(add(1, 2))
    *assume(is_positive(add(1, 2)), is_positive(1))
    assuming(is_positive(1), is_positive(add(1, 2)))
    *assume(assuming(is_positive(1), is_positive(add(1, 2))), is_positive(2))
    assuming(is_positive(2), assuming(is_positive(1), is_positive(add(1, 2))))
    *pos_add(assuming(is_positive(2), assuming(is_positive(1), is_positive(add(1, 2)))))
    assuming(is_positive(2), assuming(is_positive(1), true))
    assuming(*pos_two(is_positive(2)), assuming(*pos_one(is_positive(1)), true))
    assuming(true, assuming(true, true))
    assuming(true, *discharge(assuming(true, true)))
    assuming(true, true)
    *discharge(assuming(true, true))
    true
qed