Zulip Chat Archive

Stream: new members

Topic: quantifier exercises


view this post on Zulip Olli (Sep 08 2018 at 09:10):

could I get a hint how to make progress here:

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

view this post on Zulip Reid Barton (Sep 08 2018 at 09:11):

You can't make progress without some classical axiom.

view this post on Zulip Kenny Lau (Sep 08 2018 at 09:12):

please provide a minimum working example (MWE).

view this post on Zulip Reid Barton (Sep 08 2018 at 09:13):

Most directly, classical.by_contradiction

view this post on Zulip Reid Barton (Sep 08 2018 at 09:14):

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

view this post on Zulip Olli (Sep 08 2018 at 09:15):

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

view this post on Zulip Kenny Lau (Sep 08 2018 at 09:16):

please provide a minimum working example (MWE).

view this post on Zulip Olli (Sep 08 2018 at 09:18):

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

view this post on Zulip Kenny Lau (Sep 08 2018 at 09:20):

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

view this post on Zulip Reid Barton (Sep 08 2018 at 09:22):

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

view this post on Zulip Olli (Sep 08 2018 at 09:22):

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

view this post on Zulip Olli (Sep 08 2018 at 09:23):

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, _)

view this post on Zulip Olli (Sep 08 2018 at 09:24):

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

view this post on Zulip Kenny Lau (Sep 08 2018 at 09:24):

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.

view this post on Zulip Kenny Lau (Sep 08 2018 at 09:25):

your example is neither the second nor the last two

view this post on Zulip Reid Barton (Sep 08 2018 at 09:25):

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

view this post on Zulip Reid Barton (Sep 08 2018 at 09:26):

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

view this post on Zulip Reid Barton (Sep 08 2018 at 09:28):

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

view this post on Zulip Olli (Sep 08 2018 at 09:29):

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

view this post on Zulip Olli (Sep 08 2018 at 09:30):

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

view this post on Zulip Olli (Sep 08 2018 at 09:30):

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

view this post on Zulip Olli (Sep 08 2018 at 09:33):

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

view this post on Zulip Kenny Lau (Sep 08 2018 at 09:34):

You don't need variable a : α

view this post on Zulip Olli (Sep 08 2018 at 09:35):

I think I need it, because p uses it

view this post on Zulip Olli (Sep 08 2018 at 09:36):

oh sorry, I now realize what you meant

view this post on Zulip Olli (Sep 08 2018 at 09:42):

got it, thanks for the help

view this post on Zulip Wojciech Nawrocki (Sep 09 2018 at 00:27):

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?

view this post on Zulip Kevin Buzzard (Sep 09 2018 at 00:30):

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

view this post on Zulip Mario Carneiro (Sep 09 2018 at 00:30):

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

view this post on Zulip Mario Carneiro (Sep 09 2018 at 00:31):

(aka classical.prop_decidable)

view this post on Zulip Wojciech Nawrocki (Sep 09 2018 at 00:31):

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

view this post on Zulip Wojciech Nawrocki (Sep 09 2018 at 00:32):

@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

view this post on Zulip Mario Carneiro (Sep 09 2018 at 00:33):

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

view this post on Zulip Kevin Buzzard (Sep 09 2018 at 00:34):

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

view this post on Zulip Kevin Buzzard (Sep 09 2018 at 00:34):

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.

view this post on Zulip Mario Carneiro (Sep 09 2018 at 00:35):

is priority 0 problematic?

view this post on Zulip Wojciech Nawrocki (Sep 09 2018 at 00:37):

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

view this post on Zulip Kevin Buzzard (Sep 09 2018 at 00:49):

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

view this post on Zulip Olli (Sep 11 2018 at 02:13):

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

view this post on Zulip Mario Carneiro (Sep 11 2018 at 02:19):

yes

view this post on Zulip Olli (Sep 11 2018 at 02:20):

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

view this post on Zulip Mario Carneiro (Sep 11 2018 at 02:21):

hint: solve exercise 3.7.2

view this post on Zulip Mario Carneiro (Sep 11 2018 at 02:21):

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

view this post on Zulip Olli (Sep 11 2018 at 02:23):

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)

view this post on Zulip Mario Carneiro (Sep 11 2018 at 02:23):

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

view this post on Zulip Eduardo Cavazos (Nov 08 2019 at 00:29):

hint: solve exercise 3.7.2

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

view this post on Zulip Eduardo Cavazos (Nov 08 2019 at 00:34):

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.


Last updated: May 15 2021 at 00:39 UTC