Theory meeting, Nov. 28th

[Lyle Kopnicky]

We'll discuss Chapter 18, "The Natural Numbers and Induction in Lean", of Logic and Proof (https://leanprover.github.io/logic_and_proof/). Please read the material beforehand and try your hand at the exercises. At the meeting anyone will be able to present and contribute to the discussion.

In contrast to the last chapter, where there were 19 exercise, this one only has one: To select and prove theorems from sections 17.4 and 17.5. So, we may end up proving different ones. We could even work exercises that we skipped in Chapter 17, by doing them formally. I look forward to seeing what you come up with.

November 28th, 2018, 6:30-8:30pm

Location:

Collective Agency

3050 SE Division, Suite 245 · Portland, OR

We'll be in the second floor conference room, not in the Collective Agency suite. It's just off the lobby area in the middle of the second floor. Elevator access is available.

RSVP at:

https://www.meetup.com/Portland-Functional-Programming-Study-Group/events/mpwwbqyxpblc/

[Lyle Kopnicky]

I was able to prove all the remaining theorems from section 17.4, but had trouble with the ones from 17.5. We can discuss tonight.

Here are my solutions for 17.4: https://gist.github.com/lylek/2b1d9adb2ddc69bb314ebc50e23859df

[Matt Rice]

ditto, except i couldn't figure out 0 != 1.
I got started on 17.5 but 0 != 1 was needed to make any more progress.
(it's definitely not as clean as yours!)

https://gist.github.com/ratmice/52f74e0957e2e4da9df7215bf936c3de

> --
> You received this message because you are subscribed to the Google Groups "pdxfunc" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to pdxfunc+u...@googlegroups.com.
> To post to this group, send email to pdx...@googlegroups.com.
> Visit this group at https://groups.google.com/group/pdxfunc.
> For more options, visit https://groups.google.com/d/optout.