quantifier exercises

Stream: new members

[Olli]

could I get a hint how to make progress here:

https://gist.github.com/luxbock/853bdcdde0f333502055c6913fc91e9c

[Reid Barton]

You can't make progress without some classical axiom.

[Kenny Lau]

please provide a minimum working example (MWE).

[Reid Barton]

Most directly, classical.by_contradiction

[Reid Barton]

Or, wait. Also what Kenny said. Where did a come from?

[Olli]

sorry, I'll edit to include the full context and also my attempt with by_contradiction where I got stuck

[Kenny Lau]

please provide a minimum working example (MWE).

[Olli]

https://gist.github.com/luxbock/853bdcdde0f333502055c6913fc91e9c updated

[Kenny Lau]

I don't think that's what you want to prove.

[Reid Barton]

This variable a : α isn't doing what you want--now you have to prove p a for every a

[Olli]

this is one of the exercises from here:
https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html

[Olli]

so my attempt is clearly wrong (it does not work after all), but I don't know how to make progress beyond by_contradiction (λ ha, _)

[Olli]

I don't know how to go about getting a p a from what I have:

nanpx : (∀ (x : α), p x → false) → false,
hnpa : ¬p a
⊢ false

[Kenny Lau]

Notice that the declaration variable a : α amounts to the assumption that there is at least one element of type α. This assumption is needed in the second example, as well as in the last two.

[Kenny Lau]

your example is neither the second nor the last two

[Reid Barton]

You can never get p a, because a is an arbitrary member of α, and it might not be one for which p holds.

[Reid Barton]

So line 11 suffices hpa : p a, from ... is already the wrong way to go.

[Reid Barton]

The way to do this is to use by_contradiction at the top level--suppose ¬ (∃ x, p x), then what?

[Olli]

thanks, I'll try to see where backtracking to beginning gets me. although now that @Kenny Lau commented about the variable declaration, I'm a little bit confused about if I need to change anything outside this example

[Olli]

oh I think I understand what you mean, I don't need the variable declaration for this particular example

[Olli]

I just copy/pasted the exercises from the page and I'm filling in the sorry's

[Olli]

actually that can't be the case, so yeah I am confused about what you meant @Kenny Lau

[Kenny Lau]

You don't need variable a : α

[Olli]

I think I need it, because p uses it

[Olli]

oh sorry, I now realize what you meant

[Olli]

got it, thanks for the help

[Wojciech Nawrocki]

I'm doing the same exercise atm!
I found some disparities in mathlib's intuitionist and classical namespaces, namely in intuitionist we have this:

theorem not_forall {p : α → Prop}
    [decidable (∃ x, ¬ p x)] [∀ x, decidable (p x)] :
  (¬ ∀ x, p x) ↔ ∃ x, ¬ p x :=
⟨not.imp_symm $ λ nx x, nx.imp_symm $ λ h, ⟨x, h⟩,
 not_forall_of_exists_not⟩

@[simp] theorem not_forall_not [decidable (∃ x, p x)] :
  (¬ ∀ x, ¬ p x) ↔ ∃ x, p x :=
by haveI := decidable_of_iff (¬ ∃ x, p x) not_exists;
exact not_iff_comm.1 not_exists

but in classical only this:

protected theorem not_forall : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := not_forall

So from classical.not_forall.mp h with h: ¬ ∀ x, ¬ p x we get a double negation. Now, I know that ¬¬p ↔ p is easy to prove from classical axioms, but despite how common its usage seems to be, there is no theorem for it built into the library. Is there some reason why double-negation is redundant, or should I make a PR to add it?

[Kevin Buzzard]

lean and mathlib are pretty huge, it would surprise me if ¬¬p ↔ p were not there already.

[Mario Carneiro]

The idea is that you should use the "intuitionist" theorem and use classical.dec to fulfill the decidability assumptions

[Mario Carneiro]

(aka classical.prop_decidable)

[Wojciech Nawrocki]

@Kevin Buzzard #find tells me that there are versions for decidable p, but not for generic propositions in classical reasoning

[Wojciech Nawrocki]

@Mario Carneiro oh i see, so i should use all the decidable stuff with classical reasoning and then that one axiom to make it work? Ok

[Mario Carneiro]

This is why you often see local attribute [instance] classical.prop_decidable at the top of files that do classical reasoning

[Kevin Buzzard]

I've taken to using local attribute [instance, priority 1] classical.prop_decidable

[Kevin Buzzard]

because I ran into situations where this local attribute clobbered some decidability result which type class inference had given me and I ended up with typeclass problems.

[Mario Carneiro]

is priority 0 problematic?

[Wojciech Nawrocki]

I see, this attribute is indeed used in classical.lean

[Kevin Buzzard]

is priority 0 problematic?

my bad, I just went back to the file where some undergrads were having trouble and indeed I fixed it with priority 0

[Olli]

is it possible to solve the barber paradox exercise without using classical?https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html

[Mario Carneiro]

yes

[Olli]

can I have a hint? this is what I have so far:

example (h : ∀ x : α, S x x ↔ ¬ S x x) : false :=
have saa : S a a → ¬S a a, from (h a).mp,
have nsaa : ¬ S a a → S a a, from (h a).mpr,
sorry

[Mario Carneiro]

hint: solve exercise 3.7.2

[Mario Carneiro]

also your problem statement isn't quite right for the barber paradox

[Olli]

thanks, looks like I actually overlooked 3.7.2, so I'll go back to that and try to figure it out from there (and also fix what you mentioned)

[Mario Carneiro]

example {α} (b : α) (r : α → α → Prop)
  (H : ∀ x : α, r b x ↔ ¬ r x x) : false := sorry

[Eduardo Cavazos]

hint: solve exercise 3.7.2

@Mario Carneiro, Your hint here helped me. Thanks again!

[Eduardo Cavazos]

For any folks who come back to this thread by searching for "barber"...

In 4.6.3 (the barber paradox) we're given the following to start:

h : ∀ x : men, shaves barber x ↔ ¬ shaves x x

But I kept thinking, what can I apply this to??? We'll, barber is a men so... this is valid:

h barber

It gives us a value of type:

shaves barber barber ↔ ¬shaves barber barber

And for the rest, as @Mario Carneiro mentions, consider 3.7.2.