feat(logic): make some decidability proofs [inline]

[fpvandoorn]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/sanity.20check

@digama0: do we need to make more declarations inline?

For reviewers: code review check list

[semorrison]

Perhaps we should add a test that demonstrates that inlining is working?

It may be hard to do this without generating output, I'm not sure.

[khoek]

A little bit crazy, but the test could have (in the expression a and b) a just evaluate to true, and b create a file called sadness.txt or something, and then the test could be decided by whether the file exists at the end.

[semorrison]

Let's not have the standard test suite play with the local file system, please. :-)

…

On Mon, Sep 9, 2019 at 7:48 PM Keeley Hoek ***@***.***> wrote: A little bit crazy, but the test could have (in the expression a and b) a just evaluate to true, and b create a file called sadness.txt or something, and then the test could be decided by whether the file exists at the end. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#1393?email_source=notifications&email_token=AADUWBFZ3GT7DKE3LDZEL7DQIYLWNA5CNFSM4ITI72D2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD6G5VRQ#issuecomment-529390278>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AADUWBELBVF6LCJI4DTHJBDQIYLWNANCNFSM4ITI72DQ> .

[khoek]

Not to fear, @semorrison, the following line suffices as a test

#eval if ff ∧ (@undefined_core bool "uh-oh") then tt else tt

It fails without the inlining.

[khoek]

I mean, I guess we could also just check whether those defns have the inline attribute...

But I've pushed a test for and and or which is solution-agnostic

[khoek]

All of the other logical connectives don't eagerly evaluate (or there is no notion of such), as far as I could see (the only interesting case is implies I think, and it was fine)

[fpvandoorn]

Travis successfully checked that your test fails without inlining. :)
Now I added logic/basic as an import.

EDIT: Thanks for adding a test, that is useful to have indeed.

If Travis succeeds now: I think this PR is good to go.