Simple deduced steps
Adding several deduced steps and simplifications to make proofs easier one by one.
Current additions:
-
PartialCut
: Perform a cut if the pivot is inside a conjunction in the conclusion -
Left{And, Or, Implies, Iff, Not, Exists, ExistsOne}
: Allow usage without an argument list to infer all the parameters, given the conclusion sequent -
Right{And, Or, Implies, Iff, Not, Forall, ExistsOne}
: as above ^^ -
LeftForall
: In lieu of a unification algorithm, reduced usage toLeftForall(termToBind: Term)
-
RightExists
: as above ^^
Structural steps:
-
{Left, Right}Refl
: Allow usage without argument list
They may be used in proofs, for example, as (sequents omitted for readability and replaced with ...
):
THEOREM("example") of "..." NPROOF {
val s0 = andThen(...) by Weakening
have(...) by Trivial
val s1 = andThen(...) by InstantiateForall(z)
have(...) by Cut(s0, s1)
val s2 = andThen(...) by Weakening
have(...) by LeftAnd(s2)
andThen(...) by LeftNot()
andThen(...) by LeftForall(z)
andThen(...) by RightImplies
andThen(...) by RightNot
}
As in the example, if an argument list is not required, the usages by LeftNot
and by LeftNot()
are equivalent.