Theorem for ¬(p ↔ ¬p) missing?

[MatteoGaetzner]

Dear lean4 maintainers,

Thanks for your work, I love playing with lean4. Unfortunately I got stuck with proving one of the exercise theorems in Propositions and Proofs ,¬(p ↔ ¬p), and couldn't find a proof in the source code either. Most likely I'm looking at the wrong place or just can't recognize it because. I'd appreciate any help.

Cheers, Matteo

[timotree3]

If you're looking for help with the exercise, the Lean Community Zulip Chat would be a better place. I can post a solution here though:

Solution (Spoiler)

```lean example (p : Prop) : ¬(p ↔ ¬p) := fun h : p ↔ ¬p => have hnp : ¬p := fun hp : p => have hnp : ¬p := h.mp hp show False from hnp hp have hp : p := h.mpr hnp show False from hnp hp ```

[MatteoGaetzner]

Hey timotree3, thanks for the pointer to the community chat and the solution! Will ask in the community chat next time I have a similar question.

I was thinking about adding a solution.lean file (or a file for each chapter) to this repository. I think many people use this resource kind of like a textbook and use the exercises for practice. Many likely get stuck like me and look in this repo for solutions. If we would solutions here, they could get unstuck faster.

An alternative to this could also be to provide a disclaimer somewhere in the document that they could ask for solutions in the community chat. However, this could lead to someone having to answer the same question over and over again.

What do you think? I could add solutions for the first four chapters if wanted.

[timotree3]

Both ideas (solutions or Zulip pointer) seem reasonable to me! I don't know if there's a reason that solutions haven't already been included, so it might be worth proposing to a wider audience. Maybe make a thread in the Zulip on the topic of adding solutions to TPIL?

[MatteoGaetzner]

Sounds good, will do 👍