Tests for proof tactics

[sankalpgambhir]

Adding tests for proof tactics, since it seems we currently miss some errors during changes!

Progress: :heavy_check_mark: Hypo, Rewrite (WIP to use EqvChecker test functions), Cut :heavy_check_mark: Left rules :heavy_check_mark: Right rules :heavy_check_mark: Structural rules

Other changes to facilitate things: :1st_place_medal: unwrapTactic utility to call other tactics safely

Issues: The new tests in this PR will fail till I fix these (eventually) :heavy_check_mark: LeftExists checking :heavy_check_mark: OCBSL/Weakening leniency :heavy_check_mark: InstantiateForall not working due to argument type mismatch -> changed it to accept a sequent and check against it

[sankalpgambhir]

Some interesting behavior has been discovered due to liberal checking in parameter inference:

Normally (by magic = some proof was given before) :

have(P, Q ==> S |- R ) by magic
andThen(P, Q <=> S |- R) by LeftIff

But we are lenient towards cases like this:

have(P, Q ==> S |- R ) by magic
andThen(P, Q <=> S, Q ==> S |- R) by LeftIff

And for efficiency this is internally posed as a Weakening step with OCBSL equivalence. Turns out, that allows these two cool behaviors:

have(P |- Q, R ) by magic
andThen(P, !Q |- R) by LeftIff

// and ofc in the other direction for equality :)

have(P, Q ==> S|- R ) by magic
andThen(P, Q <=> S |- R) by LeftNot

The new tests in this PR will continue to fail till I fix this with stricter checking (I will... eventually).

EDIT: IT'S OK

[sankalpgambhir]

Not cool behavior:

LeftExists parameter inference currently only checks LHS of the sequent, and thus allows this:

have(P(x) |- R(x); Q(x) by magic
andThen(P(x) |- R(x)) by LeftExists

It's caught by the proof checker but shouldn't return a ValidProofTactic in the first place!

EDIT: FIXED, added stricter checks to every tactic that could need them. They are only run in corner cases, so there should not be any extra overhead in the general usecases over the previous versions.

[sankalpgambhir]

{Left,Right}ExistsOne tests will continue to fail till alpha-equivalence is fixed in the OL checker.

EDIT: FIXED THANKS #109 !

[sankalpgambhir]

Basic tactics are now complete (except subproof, I don't know what to do for subproof).

[sankalpgambhir]

A passing build? Is this a dream? :thinking: