TPIL Chapter 4 Exercises

Stream: new members

[Rocky Kamen-Rubio]

Question 4.2: I'm getting a type mismatch errors on all the example in ch4 exercise 2, first on the iff.intro, then on the or.elim, then on the iff.intro. Any insights would be appreciated!

variables (r : Prop) (α : Type) (p q : α → Prop)

example : α → ((∀ x : α, r) ↔ r) :=
  assume a : α,
  iff.intro
    (assume h : (∀ x : α, r), show r, from h a)
    (assume hr : r,  hr)

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
assume a : α,
iff.intro
  (assume h1 : (∀ x, p x ∨ r),
    or.elim (h1 a)
      (assume hpx : p a, or.intro_left r hpx)
      (assume hr : r, or.intro_right _ hr))
  (assume h2 : (∀ x, p x) ∨ r,
    or.elim h2
      (assume hVxpx : (∀ x, p x), or.intro_left _ (hVxpx a))
      (assume hr : r, or.intro_right _ hr))

example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
assume a : α,
iff.intro
  (assume h1 : (∀ x, r → p x),
   assume hr : r, show p a, from
   ((h1 a) hr))
  (assume h2 : (r → ∀ x, p x),
  assume hr : r, show p a, from
  ((h2 hr) a))

[Reid Barton]

Is this your real code? p is not declared anywhere

[Reid Barton]

also, (assume hr : hr) is clearly wrong

[Edward Ayers]

For the first one, you need to write assume hr a, hr instead of assume hr: hr

[Rocky Kamen-Rubio]

Reid Barton said:

Is this your real code? p is not declared anywhere

Sorry! P was defined at the top of my file and I forgot to include it when I copied it over.

[Edward Ayers]

The pattern for assume is assume x : α, b where x is an identifier, α is a type or proposition and b is a term or proof. But you can skip the type and you can chain multiple identifiers.

[Rocky Kamen-Rubio]

Edward Ayers said:

For the first one, you need to write assume hr a, hr instead of assume hr: hr

Just made that correction, thank you! It's still giving me a type mismatch error on iff.intro though.

[Edward Ayers]

On the next example, take a look at the error:

type mismatch at application
  or.elim h2 (λ (hVxpx : ∀ (x : α), p x), or.intro_left ?m_1[hVxpx] (hVxpx a))
term
  λ (hVxpx : ∀ (x : α), p x), or.intro_left ?m_1[hVxpx] (hVxpx a)
has type
  ∀ (hVxpx : ∀ (x : α), p x), p a ∨ ?m_1[hVxpx]
but is expected to have type
  (∀ (x : α), p x) → ∀ (x : α), p x ∨ r

[Edward Ayers]

Try commenting out the code that is complaining and replacing it with an underscore _ and then seeing what type Lean wants you to replace the underscore with

[Edward Ayers]

In the case of the second exercise, you might want to comment out the entire proof and replace with an underscore and then slowly add lines back in.

[Edward Ayers]

Because eg there is a rogue assume a : α, at the top

[Rocky Kamen-Rubio]

Ok I was able to get 1 and 3 working. I realize now that I misunderstood the way that "assume" statements interact with universal quantifiers. I still can't figure out how to get the 'left to right' direction of 2. If I assume a specific element in the assumption to be able to or.elim, then I've lost the generality to exact on all elements in alpha on the right hand side. I feel like I'm missing something.

[Edward Ayers]

I think that (∀ x, p x ∨ r) -> (∀ x, p x) ∨ r needs to be done by contradiction.

[Patrick Massot]

There is nothing much you can try with intuitionistic logic here. The assumption cannot be broken and the only allowed moves are left and right.

[Patrick Massot]

I'm skimming through this chapter to see what seems allowed, and I'm always puzzled by this "French quotation mark" terminology. In English, do you say ' is a quotation mark? Do you ever use it alone?

[Marc Huisinga]

the problem mentions that one of the directions requires classical reasoning

[Patrick Massot]

Anyway, I guess this exercise is rather difficult in term mode, since it seems you are not allowed to use the lemmas describing the negation of quantifiers.

[Patrick Massot]

Classical reasoning yes, but why half quotation marks?

[Kevin Buzzard]

I think I'd be happy calling a quotation mark a quotation mark. Does TPIL refer to one French quotation mark? I'm a bit confused about whether you're talking about ' vs " or " vs ""

[Reid Barton]

apostrophe or single quote

[Reid Barton]

They are sometimes used to quote inside quotations

[Patrick Massot]

TPIL says ‹ is a French quotation mark, but this symbol appears nowhere in France. We do use « as an opening quotation mark.

[Rob Lewis]

Single quotes are sometimes just normal quotes in the UK, right?

[Patrick Massot]

They are sometimes used to quote inside quotations

I'm so disappointed, I thought python invented this wonderful trick.

[Rob Lewis]

Wiki says:

The single quotation marks emerged around 1800 as a means of indicating a secondary level of quotation. One could expect that the logic of using the corresponding single mark would be applied everywhere, but it was not. In some languages using the angular quotation marks, the usage of single ones (‹…›) became obsolete, being replaced by double curved ones (“…”); the single ones still survive, for instance, in Switzerland.

[Rob Lewis]

Maybe we should call them Swiss quotes instead.

[Patrick Massot]

This would be less confusing, especially since French quotation marks are also used in Lean.

[Mario Carneiro]

Given that angle quotation marks are paired, I don't see why there needs to be two different flavors anyway. Nesting FTW

[Kenny Lau]

in Hong Kong written Chinese we use 「」 for the outer quote and 『』 for the inner quote

[Kenny Lau]

(in mainland China they use '' and "")

[Reid Barton]

「」looks like the "round towards 0" operation (ceiling if negative, floor if positive)

[Rocky Kamen-Rubio]

I'm getting an error message when I try to use exp_log_eq in term mode below for Chapter 6 Exercise 6.

--6. Give a calculational proof of the theorem log_mul below.


variables (real : Type) [ordered_ring real]
variables (log exp : real → real)
variable  log_exp_eq : ∀ x, log (exp x) = x
variable  exp_log_eq : ∀ {x}, x > 0 → exp (log x) = x
variable  exp_pos    : ∀ x, exp x > 0
variable  exp_add    : ∀ x y, exp (x + y) = exp x * exp y

-- this ensures the assumptions are available in tactic proofs
include log_exp_eq exp_log_eq exp_pos exp_add

example (x y z : real) :
  exp (x + y + z) = exp x * exp y * exp z :=
by rw [exp_add, exp_add]

example (y : real) (h : y > 0)  : exp (log y) = y := exp_log_eq h

theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y :=
calc
  log(x*y) = log(x*y) : by refl
  ... = log(exp(log x) * y) : by (exp_log_eq hx) --??????????
  ... = log(exp(log x) * exp(log y)) : by (exp_log_eq hy) --??????????
  ... = log(exp(log x + log y)) : by rw exp_add
  ... = log x + log y : by rw log_exp_eq

I got it to work in tactic mode, but I want to understand what I'm doing wrong.

theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) :
  log (x * y) = log x + log y :=
begin
have h1 := exp_log_eq hx, -
rw ← h1,
have h2 := exp_log_eq hy,
rw ← h2,
rw ← exp_add,
rw h1,
rw h2,
rw log_exp_eq,
end

[Mario Carneiro]

by rw exp_log_eq hx

[Mario Carneiro]

by exp_log_eq hx doesn't work because exp_log_eq is not a tactic

[Mario Carneiro]

remember that by tac is shorthand for begin tac, end

[Lucas Teixeira]

For Russel's Paradox (Exercise 4.3) I came up with the following solution

open classical

theorem Russel's_Paradox (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) :
  false :=
  or.cases_on (em (shaves barber barber))
    (λ a: shaves barber barber, absurd a ((h barber).mp a))
    (λ b: ¬(shaves barber barber), absurd ((h barber).mpr b) b)

I was wondering if anyone knew if there was a whether there was a constructive solution to this. If so, I would love a hint, but if not, how do you know??

[Kevin Buzzard]

Can you make your spoiler into a #mwe?

[Kevin Buzzard]

If I guessed correctly the question you're asking, the answer is that there is a constructive solution and the hint is that it boils down to exactly the same "how do I do this constructively" question which gets asked on this site time and time again :-) (namely ¬ (P ↔ ¬ P))

[Kevin Buzzard]

It's the special case Q = false of https://twitter.com/XenaProject/status/1433904823947177988?s=20

Is `(P → P → Q) → ((P → Q) → P) → Q` provable constructively? [I should say that I know the answer]. Classically you just check all four cases P,Q in {T,F} and you're done, but constructively this isn't allowed.

- The Xena Project (@XenaProject)

[Lucas Teixeira]

Quick question on problem 4

Partial solution to problem 4 (Potentially)

Should we be structuring our definitions like this?

import data.nat.basic

def prime (p : ℕ ) (hn: p > 1):(¬∃ x y : ℕ , p = x * y) := sorry

or like this??

import data.nat.basic

def prime (p : ℕ ) (hn: p > 1) (hq: ¬∃ x y : ℕ , p = x * y): Prop := sorry

[Kyle Miller]

@Lucas Teixeira The first one says "When p is a natural number and hn is a proof that p > 1, then prime p hn is a proof that ¬∃ x y : ℕ , p = x * y, and that proof right now is sorry". The second one says "When p is a natural number, hn is a proof that p > 1, and hq is a proof that ¬∃ x y : ℕ , p = x * y, then prime p hn hq is a proposition, and that proposition hasn't been defined yet (it's sorry)."

Neither of these are quite what you're going for yet.

[Kyle Miller]

You want to replace the sorry in the following with a proposition that means "n is prime":

def prime (n : ℕ) : Prop := sorry

[Lucas Teixeira]

Kyle Miller said:

You want to replace the sorry in the following with a proposition that means "n is prime":

def prime (n : ℕ) : Prop := sorry

Gotcha. so something like this??

import data.nat.basic

def prime (p : ℕ ) : Prop :=
  (p > 1) ∧ (¬∃ x y : ℕ , p = x * y)

[Mario Carneiro]

Also, a reminder that primes don't satisfy ¬∃ x y : ℕ , p = x * y either

[Mario Carneiro]

because p = 1 * p

[Kyle Miller]

Yeah, something like that, but as Mario says that's not yet the definition of a prime number.

[Lucas Teixeira]

lol that's embarrassing. Thanks y'all for the help.

[Lucas Teixeira]

I think I've got it now, this is my final answer for exercise 4

Exercise 4

import data.nat.basic
import algebra.group_power

#check even

def prime (p : ℕ ) : Prop :=
  (p > 1) ∧ (¬∃ x y : ℕ ,(x ≠ 1 ∧ x ≠ p ∧ y ≠ 1 ∧ y ≠ p) ∧ p = x * y)

def infinitely_many_primes : Prop :=
  (∀ n : ℕ, ∃ p: ℕ, p > n ∧ prime p)

def Fermat_prime (p: ℕ) : Prop :=
  (prime p) ∧ (∃ n: ℕ, (p = (2 ^ (2 ^ n)) + 1) )

def infinitely_many_Fermat_primes : Prop:=
  (∀ n : ℕ, ∃ p: ℕ, p > n ∧ Fermat_prime p)

def goldbach_conjecture : Prop :=
    (∀ n: ℕ, ∃ p q : ℕ, (n > 2 ∧ (prime p ∧ prime q)) →  n = p + q)

def Goldbach's_weak_conjecture : Prop :=
  (∀ n: ℕ, ∃ x y z: ℕ, (¬(even n) ∧ (prime x ∧ prime y ∧ prime z)) → (n = x + y + z))

def Fermat's_last_theorem : Prop :=
  (∀ n: ℕ, ¬∃ a b c : ℕ, (n > 2) → ((a ^ n) + (b ^ n) = (c ^ n)))

[Mario Carneiro]

Looking good. Your answers for goldbach_conjecture, Goldbach's_weak_conjecture, Fermat's_last_theorem are wrong; hint: you almost never want to use \exists x, p -> q

[Kyle Miller]

For prime, as a small followup exercise try writing the not-exists as forall (the part in parentheses in the exists would be to the left of an implication arrow).

[Mario Carneiro]

also, it's not wrong but it is unusual to put the n > 2 inside the p,q quantifiers of goldbach_conjecture

[Lucas Teixeira]

Mario Carneiro said:

Looking good. Your answers for goldbach_conjecture, Goldbach's_weak_conjecture, Fermat's_last_theorem are wrong; hint: you almost never want to use \exists x, p -> q

Yeah I was feeling unsure about that. I'm having a hard time expressing statements which state "for all n greater than two" and the conditionals inside the quantifier was an attempt at solving that.

Does this work??

goldbach_conjecture, Goldbach's_weak_conjecture, Fermat's_last_theorem

import data.nat.basic
import algebra.group_power

#check even

def prime (p : ℕ ) : Prop :=
  (p > 1) ∧ (¬∃ x y : ℕ ,(x ≠ 1 ∧ x ≠ p ∧ y ≠ 1 ∧ y ≠ p) ∧ (p = x * y))

def goldbach_conjecture : Prop :=
  (∀ n: ℕ, (n > 2) ∧ ∃ p q : ℕ, (prime p ∧ prime q) ∧ n = p + q)

def Goldbach's_weak_conjecture : Prop :=
  (∀ n: ℕ, ¬(even n) ∧ ∃ x y z: ℕ, (prime x ∧ prime y ∧ prime z) ∧ (n = x + y + z))

def Fermat's_last_theorem : Prop :=
  (∀ n: ℕ, (n > 2) ∧ ¬∃ a b c : ℕ, (a ^ n) + (b ^ n) = (c ^ n))

[Mario Carneiro]

Almost. You usually want to pair ∀ with → and ∃ with ∧: that is, adjectives turn into assumptions like so:

• "for all reprehensible x, bla(x)" becomes ∀ x, reprehensible x → bla x
• "there is a reprehensible x such that bla(x)" becomes ∃ x, reprehensible x ∧ bla x

Using ∀ x, foo x ∧ bla x also makes sense but is less common, because it distributes into two separate assumptions ∀ x, foo x and ∀ x, bla x.

[Kyle Miller]

Here's a disproof of the Goldbach conjecture:

example : ¬goldbach_conjecture :=
assume h : goldbach_conjecture,  nat.not_lt_zero 2 (h 0).1

[Lucas Teixeira]

Kyle Miller said:

For prime, as a small followup exercise try writing the not-exists as forall (the part in parentheses in the exists would be to the left of an implication arrow).

You mean something like this??

prime'

import data.nat.basic

def prime' (p : ℕ ) : Prop :=
  (p > 1) ∧ (∀ x y : ℕ, (x = 1 ∨ x = p ∨ y = 1 ∨ y = p) ∨ (p ≠ x * y))

[Lucas Teixeira]

Mario Carneiro said:

Almost. You usually want to pair ∀ with → and ∃ with ∧: that is, adjectives turn into assumptions like so:

• "for all reprehensible x, bla(x)" becomes ∀ x, reprehensible x → bla x
• "there is a reprehensible x such that bla(x)" becomes ∃ x, reprehensible x ∧ bla x

Using ∀ x, foo x ∧ bla x also makes sense but is less common, because it distributes into two separate assumptions ∀ x, foo x and ∀ x, bla x.

Ahh! that makes total sense. So my idea of using conditionals was unto something, they were just in the wrong place.

I think this should work now right???

goldbach_conjecture, Goldbach's_weak_conjecture, Fermat's_last_theorem

import data.nat.basic
import algebra.group_power

#check even

def prime (p : ℕ ) : Prop :=
  (p > 1) ∧ (¬∃ x y : ℕ ,(x ≠ 1 ∧ x ≠ p ∧ y ≠ 1 ∧ y ≠ p) ∧ (p = x * y))

def goldbach_conjecture : Prop :=
  (∀ n: ℕ, (n > 2) → ∃ p q : ℕ, (prime p ∧ prime q) ∧ n = p + q)

def Goldbach's_weak_conjecture : Prop :=
  (∀ n: ℕ, ¬(even n) →  ∃ x y z: ℕ, (prime x ∧ prime y ∧ prime z) ∧ (n = x + y + z))

def Fermat's_last_theorem : Prop :=
  (∀ n: ℕ, (n > 2) → ¬∃ a b c : ℕ, (a ^ n) + (b ^ n) = (c ^ n))

[Kyle Miller]

Sure, that prime' works. Here's another version that can be convenient:

def prime'' (p : ℕ ) : Prop :=
  (p > 1) ∧ (∀ x y : ℕ, p = x * y → (x = 1 ∨ x = p ∨ y = 1 ∨ y = p))

[Lucas Teixeira]

Kyle Miller said:

Sure, that prime' works. Here's another version that can be convenient:

def prime'' (p : ℕ ) : Prop :=
  (p > 1) ∧ (∀ x y : ℕ, p = x * y → (x = 1 ∨ x = p ∨ y = 1 ∨ y = p))

That's pretty :sunrise:

[Mario Carneiro]

Also, you don't need all four conjuncts for prime: since p = x * y, x = 1 iff y = p and y = 1 iff x = p, so one of each works

[Kyle Miller]

(The actual thing I had in mind was

def prime'' (p : ℕ ) : Prop :=
  (p > 1) ∧ (∀ x y : ℕ, x ≠ 1 → x ≠ p → y ≠ 1 → y ≠ p → p ≠ x * y)

This uses the transformation of not-exists-and to forall-implies-not. It's not as nice, though.)

[Mario Carneiro]

it's generally easier to work with forall and implies than negated exists in lean because of how application works

[Mario Carneiro]

Your answers look correct now, except that Goldbach's_weak_conjecture is false as stated (hint: there are 3 counterexamples)

[Mario Carneiro]

goldbach_conjecture is also missing an assumption (there are an infinite number of counterexamples)

[Mario Carneiro]

Fermat's_last_theorem has a trivial case as well

[Lucas Teixeira]

Mario Carneiro said:

Fermat's_last_theorem has a trivial case as well

How about now?

prime, goldbach_conjecture, Goldbach's_weak_conjecture, Fermat's_last_theorem

import data.nat.basic
import algebra.group_power

#check even

def prime (p : ℕ ) : Prop :=
  (p > 1) ∧ (∀ x y : ℕ, (p = x * y) → (x = 1 ∨ x = p ∨ y = 1 ∨ y = p))

def goldbach_conjecture : Prop :=
  (∀ n: ℕ, (n > 2 ∧ even n) → ∃ p q : ℕ, (prime p ∧ prime q) ∧ n = p + q)

def Goldbach's_weak_conjecture : Prop :=
  (∀ n: ℕ, (¬(even n) ∧ (n > 5)) →  ∃ x y z: ℕ, (prime x ∧ prime y ∧ prime z) ∧ (n = x + y + z))

def Fermat's_last_theorem : Prop :=
  (∀ n: ℕ, (n > 2) → ¬∃ a b c : ℕ, (a > 0 ∧ b > 0 ∧ c > 0) ∧ ((a ^ n) + (b ^ n) = (c ^ n)))

[Mario Carneiro]

I think you got it

[Lucas Teixeira]

Mario Carneiro said:

I think you got it

Thank you for being so incredibly helpful! Here's the full answer to the problem. Thought it'd be important to have noted seeing as how these are the types which you can't type check

Exercise 4 Answers

import data.nat.basic
import algebra.group_power

#check even

def prime (p : ℕ ) : Prop :=
  (p > 1) ∧ (∀ x y : ℕ, (p = x * y) → (x = 1 ∨ x = p ∨ y = 1 ∨ y = p))

def infinitely_many_primes : Prop :=
  (∀ n : ℕ, ∃ p: ℕ, p > n ∧ prime p)

def Fermat_prime (p: ℕ) : Prop :=
  (prime p) ∧ (∃ n: ℕ, (p = (2 ^ (2 ^ n)) + 1) )

def infinitely_many_Fermat_primes : Prop:=
  (∀ n : ℕ, ∃ p: ℕ, p > n ∧ Fermat_prime p)

def goldbach_conjecture : Prop :=
  (∀ n: ℕ, (n > 2 ∧ even n) → ∃ p q : ℕ, (prime p ∧ prime q) ∧ n = p + q)

def Goldbach's_weak_conjecture : Prop :=
  (∀ n: ℕ, (¬(even n) ∧ (n > 5)) →  ∃ x y z: ℕ, (prime x ∧ prime y ∧ prime z) ∧ (n = x + y + z))

def Fermat's_last_theorem : Prop :=
  (∀ n: ℕ, (n > 2) → ¬∃ a b c : ℕ, (a > 0 ∧ b > 0 ∧ c > 0) ∧ ((a ^ n) + (b ^ n) = (c ^ n)))

[Mario Carneiro]

You should also compare with the mathlib "answer key", which doesn't have all of these but does have src#nat.prime and src#nat.exists_infinite_primes

[Mario Carneiro]

mathlib doesn't make a habit of defining conjectures it can't prove, which is why none of the conjectures are defined, and infinitely_many_primes is proved rather than defined

[Mario Carneiro]

Fermat_prime could conceivably be in mathlib, but I guess we don't have anything interesting to say about them

[Lucas Teixeira]

I'm having some difficulties working with negation and quantifiers.

I've gotten this far on this problem

(∀ x, p x) ↔ ¬ (∃ x, ¬ p x)

open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable r : Prop

example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
  iff.intro
    (assume h1: (∀ x, p x),
     show ¬ (∃ x, ¬ p x),
     from or.elim (em (∃ x, ¬ p x))
       (assume hnt: ∃ x, ¬ p x,
        exists.elim hnt (λ x: α, λ npx: ¬ p x, absurd (h1 x) npx)
       )
       (assume ht: ¬(∃ x, ¬ p x), ht)
    )
    (assume h2: ¬ (∃ x, ¬ p x),
     show (∀ x, p x),
     from ...
    )

but I'm kind of at a loss with how to proceed with proving the second implication

[Kevin Buzzard]

Why don't you come back to this once you've got onto chapter 5, tactic mode, and you'll be able to write code which is much less unwieldy? As for the proof, after lam x your goal will be p x and the way to make progress is to replace it with not not p x, which is a classical step.

[Lucas Teixeira]

Kevin Buzzard said:

As for the proof, after lam x your goal will be p x and the way to make progress is to replace it with not not p x, which is a classical step.

Ahh, that makes sense. I was trying to perform the classical step on the quantifier itself and getting nowhere, it didn't occur to me to do the classical step on the contents of the quantifier instead.

[Lucas Teixeira]

Kevin Buzzard said:

Why don't you come back to this once you've got onto chapter 5, tactic mode, and you'll be able to write code which is much less unwieldy?

I'll definitely take the advice and come back through these after having worked through chapter 5, but I don't think my difficulties stem from the unwieldyness of the code (for some background: I'm a functional programmer who's trying to get into pure mathematics through LEAN, rather than the other way round). The things I'm still developing an intuition around are:

1. Navigating the inference rules for quantifiers
2. Knowing when it is necessary to use the law of excluded middle
3. If it is necessary to to use the law of excluded middle, which statements would it be strategic to do this on

For example, I was able to get this far on these two problems:

(∃ x, p x → r) ↔ (∀ x, p x) → r and (∃ x, r → p x) ↔ (r → ∃ x, p x)

open classical

variables (α : Type*) (p q : α → Prop)
variable a : α
variable {r : Prop}

example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
   iff.intro
     (assume mh: (∃ x, p x → r),
       λ apx: (∀ x, p x), exists.elim mh (λ x: α, λ fpxr: p x → r, fpxr (apx x) )
     )
     (assume sh: (∀ x, p x) → r,
      show (∃ x, p x → r),
      from ...
     )

example : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
  iff.intro
    (assume h1:(∃ x, r → p x),
      λ hr: r, exists.elim h1 (λ x: α, λ frpx: r → p x, exists.intro x (frpx hr))
    )
    (assume h2: (r → ∃ x, p x),
     show (∃ x, r → p x),
     from ...
    )

But I was unable to pull the trigger with the exists.intro function because I don't have an assumption of x to work with. As a work around I tried using the a which is defined as a variable to implement exists.intro a (λ px: p a, sh (λ x: α, px) as a solution to the first problem but it led to this error

type mismatch at application sh (λ (x : α), px) term λ (x : α), px has type α → p a but is expected to have type ∀ (x : α), p x

This has led me to believe that it might not be possible to construct an existential statement from the given assumptions, so I've opted to try out a classical approach, and find statements to use em on.

I could go on to state my process of selecting candidate statements to use em on and list out some of the issues I came across when trying to implement em on said statements, but I would love to receive some feedback on the validity of the reasoning that I demonstrated above if there is anyone who is willing to offer that up.

[Mario Carneiro]

But I was unable to pull the trigger with the exists.intro function because I don't have an assumption of x to work with.

This one is sneaky: Notice the variable a : α assumption at the top

[Mario Carneiro]

But you are right that a doesn't work for the problem, because p a doesn't necessarily hold, and a classical approach is needed. You will actually need more than one application of em or by_contradiction here. Here's a hint: assume (∃ x, p x → r) is false and prove (∀ x, p x)

[Mario Carneiro]

@Lucas Teixeira

[Lucas Teixeira]

Mario Carneiro said:

But you are right that a doesn't work for the problem, because p a doesn't necessarily hold, and a classical approach is needed. You will actually need more than one application of em or by_contradiction here.

I see what you mean by p a doesn't necessarily hold, and that explains the type error that I was getting when I attempted to fit it into exists.intro.

Here's a hint: assume (∃ x, p x → r) is false and prove (∀ x, p x)

And thank you for the hint, I'll work on it for a bit and try to follow up.
I'm assuming that this is a hint for the first problem (∃ x, p x → r) ↔ (∀ x, p x) → r??

[Lucas Teixeira]

Mario Carneiro
I guess I'm having some trouble seeing how under the assumption of ¬(∃ x, p x → r) we would benefit from a proof of (∀ x, p x). The way I see it, since the current goal is (∃ x, p x → r) ,assuming¬(∃ x, p x → r) would change our goal into a derivation of a contradiction.

The statements that I see following from (∀ x, p x) are r, ¬∃ x, ¬ p x, and p a, none of them feel to have any immediate use.

You mentioned that there is another use of em that was necessary. What was your process of coming to that conclusion like??

[Mario Carneiro]

@Lucas Teixeira If you can prove r, then you can prove (∃ x, p x → r) and thus false

[Mario Carneiro]

You mentioned that there is another use of em that was necessary. What was your process of coming to that conclusion like??

That's probably too spoilerific to say, but roughly speaking there is nothing in this problem that would help prove the existential, or to prove p x from not (not (p x)), so you will need two applications of LEM around these two places.

[Mario Carneiro]

For the second problem, there is one proposition that would benefit a lot from em. Think of it this way: after applying em foo, you can simplify all statements involving foo, which might make the goal match the assumption after simplification, or make it provable outright

[Lucas Teixeira]

Mario Carneiro

Thank you for your response! I ended up getting side tracked with other projects but I do plan on coming back to it soon enough