Mechanics of Proof Exercise 5.3.6.3

Stream: maths

[Jonatas Miguel]

Ahoy all!

I feel like I had to do something weird to be able to solve this exercise, and was hoping to know if others had to do the same or have come up with something else.

For reference, the exercise can be found by clicking this link.

Here's the answer I came up with:

example (P : α → Prop) : ¬ (∀ x, P x) ↔ ∃ x, ¬ P x := by
  constructor
  · intro hnaxPx
    by_cases hxPx : ∃ (x : α), ¬P x
    · apply hxPx
    · -- NOTE: this obtain pattern is kinda weird... I tried an alternative I had used elsewhere, but, it didn't work...
      obtain ⟨li, _ri⟩ :=
        calc
          (¬∃ (x : α), ¬P x) ↔ (∀ (x : α), ¬¬P x) := by rel [not_exists]
          _ ↔ ∀ (x : α), P x := by rel [not_not]
      have haxPx := li hxPx
      -- NOTE: the above lines are necessary because the following two aren't working:
      -- rw [not_exists] at hxPx
      -- NOTE: issue starts here, ¬¬ replacement seems to be impossible for some reason even though I can see it in the InfoView...
      -- rw [not_not] at hxPx
      contradiction
  · intro hexnPx haxPx
    obtain ⟨x, nPx⟩ := hexnPx
    have hPx := haxPx x
    contradiction

cc: @Heather Macbeth

[Jonatas Miguel]

Here's a screenshot of the issue:

Screenshot-2024-08-12-at-7.27.03AM.png

[Yaël Dillies]

Do you know about simp_rw?

[Jonatas Miguel]

Nope, I haven't seen that being used yet in the book, so I haven't tried to use it.

I always tend to assume that we can solve some of these exercises with what's been used in examples so far and maybe some high school level math, so I try to stick to that as much as I can (for better or worse sometimes, lol).

I have started to take a look at Mathematics in Lean to try to get a better sense of how some of this stuff is working and what other tools I may have available, but I haven't gone too far into that book just yet either.

[Jonatas Miguel]

I'm starting to wonder if it has something to do with the specific version of Lean v4 that I'm using. The version specified for the codebase seems to be v4.3.0, not sure if this is relevant or not though.

[Kim Morrison]

You can always try in the most recent Lean using the code sandbox (click the icon in the top right of any code block on zulip).

[Kim Morrison]

(Oops, you can't because you've forgotten to include your imports in your code block, and in this case it is Heather's custom tactics, which aren't available in the sandbox.)

[Kim Morrison]

@Heather Macbeth, should we make the sandbox work with your repo? I don't see why it would be difficult?

[Timo Carlin-Burns]

The error is because rw doesn't work for rewriting terms which appear "under binders", e.g. terms after ∀ x, or ∃ x, . I think the expected way to prove this exercise is using only "logic" tactics like intro, constructor, use, by_cases, have, obtain, contradiction, and apply.

[Heather Macbeth]

Kim Morrison said:

Heather Macbeth, should we make the sandbox work with your repo? I don't see why it would be difficult?

@Kim Morrison There are a few quirks, for example there are files from the repo which could not be imported, because they contain exercises with sorries in the statements.

[Heather Macbeth]

@Jonatas Miguel As Timo says, the solution I have in mind would replace this part of your proof

      obtain ⟨li, _ri⟩ :=
        calc
          (¬∃ (x : α), ¬P x) ↔ (∀ (x : α), ¬¬P x) := by rel [not_exists]
          _ ↔ ∀ (x : α), P x := by rel [not_not]
      have haxPx := li hxPx

with only "logic" tactics, i.e. no use of rel.

The proof of not_exists is in Example 5.16 and the proof of not_not is basically in Example 5.2.6, so rather than invoking those lemmas by name in your proof, you can adapt the ideas from the proofs of those lemmas.

[Heather Macbeth]

By the way, the reason your code wasn't working on standard Mathlib is because Mathlib's rel doesn't handle ↔. This is for slightly subtle reasons -- related to the reason Yael suggested the simp_rw workaround -- so in the book I cheat by extending rel to special-case ↔:
https://github.com/hrmacbeth/math2001/blob/main/Library/Tactic/Rel.lean

[Jonatas Miguel]

Aah, I see. I had wondered if that was the case or not. I think one way to make that clearer is to state that we shouldn't be using any of those lemmas instead of referring only to the ones that we'd essentially be reimplementing. I'll go back to those exercises and rewrite my solutions.

[Heather Macbeth]

I hadn't realised that there was a way of using them in this exercise! :)

[Heather Macbeth]

But now I think about it, here's how to take this idea to the extreme: :grinning:

import Mathlib

example (P : α → Prop) : ¬ (∀ x, P x) ↔ ∃ x, ¬ P x := by
  calc ¬ (∀ x, P x) ↔ ¬ (∀ x, ¬ ¬ P x) := by simp_rw [not_not]
    _ ↔ ¬ ¬ (∃ x, ¬ P x) := by simp_rw [not_exists]
    _ ↔ ∃ x, ¬ P x := by simp_rw [not_not]

(The simp_rw are standing in for rel on the math2001 repo, although I haven't tested it there.)

[Jonatas Miguel]

Ok, finally got some time and finished rewriting those two exercises in chapter 5.3 where we were supposed to avoid using the lemmas.

Exercise 5.3.6.2:

example (P Q : Prop) : ¬ (P → Q) ↔ (P ∧ ¬ Q) := by
  constructor
  · intro hnPimpQ
    -- case ¬(P → Q) → P ∧ ¬Q
    by_cases hPanQ : P ∧ ¬Q
    · apply hPanQ
    · have himp : (¬ P ∨ Q) → (P → Q)
      · intro hnPoQ hP
        obtain l | r := hnPoQ
        · contradiction
        · apply r
      have hnPoQ : (¬ P ∨ Q)
      · by_cases hQ : Q
        · right
          apply hQ
        · left
          intro hP
          have hPanQ : P ∧ ¬ Q
          · constructor
            · apply hP
            · apply hQ
          contradiction
      have hcon := himp hnPoQ
      contradiction -- between `hcon` and `hnPimpQ`
  · intro h hPiQ
    obtain ⟨hP, hnQ⟩ := h
    have hQ := hPiQ hP
    contradiction

Exercise 5.3.6.3:

example (P : α → Prop) : ¬ (∀ x, P x) ↔ ∃ x, ¬ P x := by
  constructor
  · -- case: (¬∀ (x : α), P x) → ∃ (x : α), ¬P x
    intro hnfaxPx
    by_cases h : ∃ x, ¬ P x
    · apply h
    · -- essentially, need to conclude ¬(∃ (x : α), ¬P x) → ∀ x, P x
      have himp : (∀ x, ¬¬P x) → (∀ x, P x)
      · intro hfaxnnPx x
        have hnnPx := hfaxnnPx x
        by_cases hPx : P x
        · apply hPx
        · contradiction
      have hfaxnnPx : ∀ x, ¬¬ P x
      · intro x hnPx
        have : ∃ x, ¬ P x
        · use x
          apply hnPx
        contradiction
      have hcon := himp hfaxnnPx
      contradiction -- between `hcon` and `hnfaxPx`
  · intro hexnPx hfaxPx
    obtain ⟨x, hnPx⟩ := hexnPx
    have hPx := hfaxPx x
    contradiction

I think there are a few reasons why I chose to go the route I did originally:

1. I assumed I would only need to use excluded middle once in each exercise, which led to
2. I wasn't sure what selections I should be making for the excluded middle portions as nothing I tried was working, which made me think
3. Well the exercises don't explicitly exclude the use of the other lemmas, and I can see a route where we can potentially solve them via mechanisms we've learned about related to equivalencies

When I have a tool that can achieve a result in a way that makes more sense to me, and requires less work to arrive at the desired result, I reach for that, lol. Eventually, when I understand something better, I'll try to use what I think is the more correct approach, even if it does require a bit more effort to achieve.

Part of my difficulties have been related to my inexperience in writing proofs, but, sometimes it's also my inexperience with lean. In some part it's also not being sure what some of the expectations are up front for some exercises and so I end up overcomplicating what I assume needs to be done.

I'm also curious if there are even more straightforward versions of these solutions. Are the ones I came up with sufficiently succinct? Or is there an even simpler solution given what has been presented so far?

[Jonatas Miguel]

Thanks everyone for your assistance! This was super helpful.

[Timo Carlin-Burns]

Jonatas Miguel said:

I'm also curious if there are even more straightforward versions of these solutions.

Here are some shorter solutions

Exercise 5.3.6.2

example (P Q : Prop) : ¬ (P → Q) ↔ (P ∧ ¬ Q) := by
  constructor
  · intro hnPimpQ
    by_cases hQ : Q
    · have himp : P → Q
      · intro hP
        apply hQ
      contradiction
    · by_cases hP : P
      · constructor
        · apply hP
        · apply hQ
      · have himp : P → Q
        · intro hP'
          contradiction
        contradiction
  · intro h hPiQ
    obtain ⟨hP, hnQ⟩ := h
    have hQ := hPiQ hP
    contradiction

Exercise 5.3.6.3

example (P : α → Prop) : ¬ (∀ x, P x) ↔ ∃ x, ¬ P x := by
  constructor
  · -- case: (¬∀ (x : α), P x) → ∃ (x : α), ¬P x
    intro hnfaxPx
    by_cases h : ∃ x, ¬ P x
    · apply h
    · have hfaxPx : ∀ x, P x
      · intro x
        by_cases hPx : P x
        · apply hPx
        · have hexnPx : ∃ x, ¬ P x
          · use x
            apply hPx
          contradiction
      contradiction
  · intro hexnPx hfaxPx
    obtain ⟨x, hnPx⟩ := hexnPx
    have hPx := hfaxPx x
    contradiction

[Jonatas Miguel]

Nice, I'll try to study these, hopefully what I learn from them will help unblock some of my intuitions in the future. Thanks for providing these!