Logic and Proof Chapter 4 exercises

[Lyle Kopnicky]

Happy New Year!

I've read Chapter 4 and worked the exercises. I found that reading the chapter took a lot of time, but most of the proofs in the exercises were simpler than the ones from Chapter 3. I'll post my solutions if people want them now, or else I'll wait until closer to the meeting.

One thing that threw me off was that there are confusingly similar, but different sorts of brackets. Tuples are enclosed with brackets like this: ⟨h1, h2⟩. Those are neither parentheses (as in Haskell) nor are they to be confused with less than < and greater than > signs. They can be typed in VS Code (and probably Emacs) with \< and \>. Then there are French quotes that are used to indicate the implicit proof in scope for a proposition, as in ‹A›. The book doesn't say how to type them, but I looked in the source code for the Lean VS code extension and found that you can type \f< and \f> to get those. At first I thought they might be less than/greater than signs, and then tried the tuple brackets, until I realized they really were a separate delimiter. It is a bit annoying that you have to type space following each of those abbreviations, which inserts a space, but with delimiters, you don't want a space. I might make a suggestion to improve the extension.

I found myself varying my style as I went through the examples: sometimes using h1, h2, sometimes using h₁, h₂, sometimes using hA, hB, sometimes using ‹A›, ‹B›. I think the French quote form is convenient when the proposition term is small, so you don't introduce the confusion of an extra label. But as it gets longer, it becomes more worth introducing a label. I'd be interested to see what styles people develop.

The last exercise was the trickiest. I thought at first I would have to use classical logic, with proof by contradiction, and I successfully proved it with that. Then I found that I was able to do it without using proof by contradiction, so there was no need to import the classical library.

As a reminder, we will meet on January 10th, 2018, at the same place (3050 SE Division 2nd floor conference room), same time (6:30-8:30pm). This time we'll cover Chapter 4 in depth, on natural deduction in the theorem prover Lean. I'll be out of town, but Leif will be hosting.

- Lyle

[Lyle Kopnicky]

And, here are my solutions:

https://gist.github.com/lylek/11c9b6c9accbfede745d21cb6fe801f9

I also made an attempt at translating them to Haskell:

https://gist.github.com/lylek/872c134f988adacd964b26ebcd0b3402

The trick is implementing not. There is a wonderful wiki page here that explains how it can be done:

https://en.wikibooks.org/wiki/Haskell/The_Curry–Howard_isomorphism

[Matt Rice]

Here are mine,
thought the last one was trickiest too,
i also did constructive, and classical variation as well as a 3rd variation (which i don't can be done constructively)
https://gist.github.com/ratmice/dcbed57a934b253eda0b1a0474801748

I think you can also hit arrow keys instead of space to avoid inserting the space when \< etc...
(I had thought it was escape, but trying now that seems to be for the autocomplete)

[Lyle Kopnicky]

Thanks for posting your variations, Matt.

As I commented in the gist:

I didn't realize you could get away without not.intro, just concluding false. I guess not.intro is actually a no-op, since ¬ A is an alias for A → false.

It also didn't occur to me that by partially applying elim_left to A ↔ B, we would get the desired implication A → B. I was thinking only in terms of fully applying it by passing A as well. I like the symmetry you create by deriving both A → ¬ A and ¬ A → A.