Zulip Chat Archive
Stream: new members
Topic: Help with proving with contradiction
Dev-Indra (Apr 28 2020 at 18:40):
Here is my code, along with some definitions and helper theorems (I know its long, but my main issue is at the very end where I have the comment -- Help here ---)
def dvd (m n: ℕ): Prop := ∃ k, n = m * k
def prime (p : ℕ) : Prop := p ≥ 2 ∧ ∀ n, dvd n p → n = 1 ∨ n = p
def composite (d : ℕ): Prop:= ∃ (a b: ℕ), d = a*b ∧ a ≤ b ∧ b < d
lemma greater_than_not_zero (n : ℕ)(n ≥ 2): n ≠ 0:=
begin
exact lattice.ne_bot_of_gt H,
end
lemma dvd_n_less_than_n (u n : ℕ) (ha: dvd u n) (hb: u ≠ 1) (hc: u ≠ n) (hn : n ≠ 0) : u < n :=
begin
refine lt_of_le_of_ne _ hc,
rcases ha with ⟨k, rfl⟩,
simpa using nat.mul_le_mul_left _ (_:1≤_),
refine nat.pos_iff_ne_zero.2 (mt _ hn),
rintro rfl, refl,
end
lemma either_prime_or_composite (n:ℕ ) (ge: n≥ 2): (¬ (prime n) ↔ composite n) :=
begin
split,
{
intros h,
rw prime at h,
rw composite,
push_neg at h,
cases h,
{
linarith,
} ,
{
cases h with u hu,
let hu_left:= hu.1,
rw dvd at hu_left,
cases hu_left with k hk,
have u_g_k : (u≤ k)∨ (u>k),
{
-- by library_search,
exact le_or_lt u k,
},
cases u_g_k,
{
use u,
use k,
split,
exact hk,
split,
exact u_g_k,
let hu_mid:= hu.2.1,
have u_ge_1 : (u≥ 1),
{
by_contradiction,
have u_zero: u=0,
{
linarith,
},
have n_zero: n=0,
{
subst u_zero,
simp at hk,
exact hk,
},
linarith,
},
have u_ge_2 : (u≥ 2),
{
by_contradiction,
have u_less_2 : u<2,
{
linarith,
},
have u_eq_1: u=1,
{
linarith,
},
-- by library_search,
exact hu_mid u_eq_1,
},
by_contradiction,
have k_ge_n: k≥ n,
{
linarith,
},
have uk_ge_2n: u*k≥ 2* n,
{
-- by library_search,
exact canonically_ordered_semiring.mul_le_mul u_ge_2 k_ge_n,
},
have n_ge_2n: n≥ 2*n,
{
linarith,
},
have twon_gt_n: 2*n > n,
{
linarith,
},
linarith,
},
{
use k,
use u,
split,
rw mul_comm at hk,
exact hk,
split,
--exact u_g_k,
let hu_mid:= hu.2.1,
have u_ge_1 : (u≥ 1),
{
by_contradiction,
have u_zero: u=0,
{
linarith,
},
have n_zero: n=0,
{
subst u_zero,
simp at hk,
exact hk,
},
linarith,
},
have u_ge_2 : (u≥ 2),
{
by_contradiction,
have u_less_2 : u<2,
{
linarith,
},
have u_eq_1: u=1,
{
linarith,
},
-- by library_search,
exact hu_mid u_eq_1,
},
by_contradiction,
have k_ge_n: k≥ n,
{
linarith,
},
have uk_ge_2n: u*k≥ 2* n,
{
-- by library_search,
exact canonically_ordered_semiring.mul_le_mul u_ge_2 k_ge_n,
},
have n_ge_2n: n≥ 2*n,
{
linarith,
},
have twon_gt_n: 2*n > n,
{
linarith,
},
linarith,
have ha: dvd u n, from and.left hu,
have h2: u ≠ 1 ∧ u ≠ n, from and.right hu,
have hc: u ≠ n, from and.right h2,
have hb: u ≠ 1, from and.left h2,
have hn: n ≠ 0,
{
exact lattice.ne_bot_of_gt ge,
},
apply dvd_n_less_than_n,
have h4: dvd u n, from and.left hu,
apply h4,
apply hb,
apply hc,
apply hn,
},
}
},
{
intros h,
rw composite at h,
by_contradiction,
rw prime at a,
cases h with a1 ha1,
cases ha1 with b hb,
have h1: n = a1*b, from and.left hb,
have temp: a1 ≤ b ∧ b < n, from and.right hb,
have h2: a1 ≤ b, from and.left temp,
have h3: b < n, from and.right temp,
have hc := a.right b,
have b_isnt_one: b ≠ 1,
{
by_contradiction,
push_neg at a_1,
subst a_1,
rw mul_one at h1,
linarith,
},
have b_divides_n: dvd b n,
{
rw dvd,
rw mul_comm at h1,
use a1,
rw h1,
},
have b_is_trivial: b = 1 ∨ b = n,
{
exact hc b_divides_n,
},
--Help here--
},
end
So basically, I have the statements: b_is_trivial : b = 1 \or b = n, b_isnt_one: b \neq 1 andh3: b < n. I want to get a contradiction, but I cant. I tried using linarith and by library search, but nothing worked. Any suggestions?
Reid Barton (Apr 28 2020 at 18:43):
A huge block of code is not useful without the correct imports.
Reid Barton (Apr 28 2020 at 18:43):
That said, use cases on b_is_trivial.
Patrick Massot (Apr 28 2020 at 18:54):
@Dev-Indra Why do you post this huge pile of code (without import) if your question if how to prove example (n b) (b_is_trivial : b = 1 ∨ b = n) (b_isnt_one: b ≠ 1) (h3: b < n) : false?
Patrick Massot (Apr 28 2020 at 18:56):
Alternative to Reid's method: by linarith [or_iff_not_imp_left.mp b_is_trivial b_isnt_one]. Of course you can also write the proof term by hand.
Dev-Indra (Apr 28 2020 at 18:59):
@Patrick Massot Sometimes when I asked questions in the past, people wanted me to put in the code so that they can run it on their laptops. As for imports I only had import tactic at the top, and I assumed everyone has this import statement. But thanks for the help. My code works now.
Reid Barton (Apr 28 2020 at 19:01):
With just import tactic already lattice.ne_bot_of_gt is not in scope.
Reid Barton (Apr 28 2020 at 19:01):
But why omit one or two lines out of a hundred?
Patrick Massot (Apr 28 2020 at 19:02):
What I posted is a MWE. You can copy the file I posted in an empty Lean file and it works.
Patrick Massot (Apr 28 2020 at 19:03):
I mean before I posted the proof, which does use import tactic
Jalex Stark (Apr 29 2020 at 13:58):
Dev-Indra said:
Patrick Massot Sometimes when I asked questions in the past, people wanted me to put in the code so that they can run it on their laptops. As for imports I only had
import tacticat the top, and I assumed everyone has this import statement. But thanks for the help. My code works now.
"minimum working example" means that I can copy your code block, paste into a new file in my lean project, and see what the problem is. The "working" part means I shouldn't have to add any code myself, and you can test this by... copying your code block into a new lean file! The "minimum" part means that there aren't unnecessary bits that will distract me before I see what's wrong.
I know it sounds annoying, but if you don't post a mwe then you are implicitly valuing your time over the time of people that might help you.
Jalex Stark (Apr 29 2020 at 14:00):
do we have a standard linkpost for the definition of MWE yet?
Reid Barton (Apr 29 2020 at 14:01):
I also endorse the edit. In particular, there is only one of you but there may be multiple people who could help you, so even if you valued all people's time equally it would still make sense to put in the effort yourself.
Johan Commelin (Apr 29 2020 at 14:02):
Maybe we can use the Zulip linkifier so that #mwe links to something useful
Kenny Lau (Apr 29 2020 at 14:03):
macro time... maybe not
Kenny Lau (Apr 29 2020 at 14:04):
does Zulip even have macros?
Johan Commelin (Apr 29 2020 at 14:04):
https://en.wikipedia.org/wiki/Minimal_working_example
Johan Commelin (Apr 29 2020 at 14:05):
@Kenny Lau lean#251
Rob Lewis (Apr 29 2020 at 14:05):
If there's a place to link to, that's very easy to do. Maybe even better: posting #mwe or #codebackticks or whatever could summon a bot to make a prerecorded post.
Rob Lewis (Apr 29 2020 at 14:05):
Zulip bot scripting is pretty easy.
Kenny Lau (Apr 29 2020 at 14:05):
your wiki link doesn't emphasize on "working"
Reid Barton (Apr 29 2020 at 14:06):
It also doesn't explain the why
Rob Lewis (Apr 29 2020 at 14:06):
The bigger challenge is automatically identifying posts that are missing a mwe or backticks.
Reid Barton (Apr 29 2020 at 14:07):
I think we could train an AI for the backticks one.
Reid Barton (Apr 29 2020 at 14:07):
Once Sebastien formalizes the sigmoid function.
Jalex Stark (Apr 29 2020 at 14:07):
Rob Lewis said:
The bigger challenge is automatically identifying posts that are missing a mwe or backticks.
That would be great, too, but having a macro for humans to type is already a big step forward
Reid Barton (Apr 29 2020 at 14:08):
I'm not sure but I think there's some way a human can trigger a bot manually, using a / command or something? Now that I think about it I'm not sure how it is supposed to work
Rob Lewis (Apr 29 2020 at 14:09):
I think bots can scan the contents of posts. It should be easy to write a bot that watches for #mwe.
Jalex Stark (Apr 29 2020 at 14:09):
I think the documentation here is enough for anyone willing to give it a go:
https://zulipchat.com/api/running-bots
Reid Barton (Apr 29 2020 at 14:11):
Right, I was just wondering whether the extra noise of someone typing #mwe could be avoided
Reid Barton (Apr 29 2020 at 14:12):
maybe that's not even a good idea though
Johan Commelin (Apr 29 2020 at 14:12):
I was thinking we would just write
please provide an #mwe
Johan Commelin (Apr 29 2020 at 14:12):
And then Zulip would linkify #mwe
Jalex Stark (Apr 29 2020 at 14:12):
Gotcha.
My model of how this works i based off of chatbots in twitch streams.
Kenny Lau (Apr 29 2020 at 14:12):
what is linkify? is it something admins can edit?
Johan Commelin (Apr 29 2020 at 14:12):
And then user clicks and gets enlightened
Jalex Stark (Apr 29 2020 at 14:13):
Do we have a "server meta" stream?
Reid Barton (Apr 29 2020 at 14:13):
Johan Commelin said:
And then Zulip would linkify
#mwe
This might be better, since we can put more text on the page linked to than we would want to see a bot write out over and over.
Jalex Stark (Apr 29 2020 at 14:13):
I think the bot should say two-ish sentences to convince the user to click the link
Johan Commelin (Apr 29 2020 at 14:13):
Kenny Lau said:
what is linkify? is it something admins can edit?
yes
Johan Commelin (Apr 29 2020 at 14:14):
We only need to ping @Mario Carneiro and it will be done before you can say #mwe
Kenny Lau (Apr 29 2020 at 14:14):
but what do we want to link it to?
Rob Lewis (Apr 29 2020 at 14:15):
Yeah, I was thinking the bot post would be more visible. We don't have to trust people to click #mwe instead of posting "what's a #mwe?"
Johan Commelin (Apr 29 2020 at 14:15):
If we are lazy: wiki, and otherwise a custom page hosted on leanprover-community.github.io
Rob Lewis (Apr 29 2020 at 14:15):
But either way is an improvement!
Kenny Lau (Apr 29 2020 at 14:17):
https://github.com/leanprover-community/mathlib/wiki/Minimum-Working-Example-(MWE)
Jalex Stark (Apr 29 2020 at 14:18):
I think this discussion could profitably move here
https://leanprover.zulipchat.com/#narrow/stream/236604-server-meta/topic/.23mwe.20bot
Mario Carneiro (Apr 29 2020 at 14:27):
Just clarifying that the reason I was summoned is not the way people are planning to implement this, yes?
Johan Commelin (Apr 29 2020 at 14:28):
Well...
Kenny Lau (Apr 29 2020 at 14:29):
I don't see anything wrong with having #mwe link to the wiki page
Johan Commelin (Apr 29 2020 at 14:29):
You are an admin, so you can help us avoid it that way
Last updated: Dec 20 2023 at 11:08 UTC