Proofs can now be written using dedicated tactics and deduced steps. Tactics can be developed as object from which a SCProof can be recomputed. Management of premises and target bottom sequent is unified, but tactics can optionally take other arguments. Tactics can be used to construct proof using a dedicated syntax and DSL. Formally, The proof is built imperatively. This means it is possible to write code in the middle of the proof (for example to print it) and it is possible to assign proof steps. The library keep track of the proof being written from start to finish. A proof may look like:
THEOREM("fixedPointDoubleApplication") of "∀'x. 'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('f('x)))" PROOF {
assume(forall(x, P(x) ==> P(f(x))))
val base = have( (P(x) ==> P(f(x)), P(f(x)) ==> P(f(f(x)))) |- P(x) ==> P(f(f(x)))) by Trivial
have(() |- P(x) ==> P(f(f(x)))) by SUBPROOF {
have(P(f(x)) ==> P(f(f(x))) |- P(x) ==> P(f(f(x))) ) by LeftForall(x)(base)
andThen(() |- P(x) ==> P(f(f(x)))) by LeftForall(f(x))
}
}
Sequent Calculus proof steps have been adapted so that they need only the minimum (often zero) explicit parameters, which are automatically inferred. Subproofs can also be used, and there is no need to do import management. Imports of Justifications and of proof steps of enclosing proofs are automatically passed through the imports.
User should not use integers anymore to refer to premises, but instead provide a previous proof step or a justification directly. On top of basic SC steps, the naive propositional solver and a tactic to instantiate forall quantifiers. Existing proof have been translated to old SC (with every step lead by SC.) to make room for the new tactics identifiers.
Proofs can now be written using dedicated tactics and deduced steps. Tactics can be developed as object from which a SCProof can be recomputed. Management of premises and target bottom sequent is unified, but tactics can optionally take other arguments. Tactics can be used to construct proof using a dedicated syntax and DSL. Formally, The proof is built imperatively. This means it is possible to write code in the middle of the proof (for example to print it) and it is possible to assign proof steps. The library keep track of the proof being written from start to finish. A proof may look like:
Sequent Calculus proof steps have been adapted so that they need only the minimum (often zero) explicit parameters, which are automatically inferred. Subproofs can also be used, and there is no need to do import management. Imports of Justifications and of proof steps of enclosing proofs are automatically passed through the imports. User should not use integers anymore to refer to premises, but instead provide a previous proof step or a justification directly. On top of basic SC steps, the naive propositional solver and a tactic to instantiate forall quantifiers. Existing proof have been translated to old SC (with every step lead by SC.) to make room for the new tactics identifiers.