Zulip Chat Archive

Stream: maths

Topic: is there any better way?


view this post on Zulip Truong Nguyen (Sep 03 2018 at 17:36):

Hi Everybody,
I this this way of proving 1 < 4 is not a smart way. Do you have any better way for doing this. Thanks

theorem oiooo : 1 < 4 :=
begin
have thh: 1 < nat.succ 1, from nat.lt_succ_self 1,
have hht6: nat.succ 1 < 3, from nat.lt_succ_self 2,
have ht5: 3 < 4, from nat.lt_succ_self 3,
have tg: 1 < 3, from nat.lt_trans thh hht6,
show 1 < 4, from nat.lt_trans tg ht5
end

view this post on Zulip Johan Commelin (Sep 03 2018 at 17:37):

You can format code by putting three backticks before and after it:

```lean
Your code goes here
```

view this post on Zulip Kenny Lau (Sep 03 2018 at 17:38):

theorem oiooo : 1 < 4 := dec_trivial

view this post on Zulip Kenny Lau (Sep 03 2018 at 17:38):

theorem oiooo : 1 < 4 :=
by repeat {constructor}

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 17:38):

rofl

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 17:38):

that's some obscure proof

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 17:39):

@Truong Nguyen the correct proof is dec_trivial -- inequalities are decidable on the naturals

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 17:40):

Unfortunately the reals do not have decidable equality, so for them you have to prove stuff like 1 < 4 using norm_num

view this post on Zulip Johan Commelin (Sep 03 2018 at 17:42):

import tactic.tidy

theorem oiooo : 1 < 4 := {! _ !}

view this post on Zulip Kenny Lau (Sep 03 2018 at 17:42):

theorem oiooo : 1 < 4 :=
nat.one_lt_bit0 $ ne.symm $ nat.zero_ne_bit0 $ nat.one_ne_zero

view this post on Zulip Johan Commelin (Sep 03 2018 at 17:43):

The {! _ !} is called a goal. You can fill it in in two ways: (1) Click the light bulb. (2) Put your cursor in the goal and hit Ctrl-.

view this post on Zulip Johan Commelin (Sep 03 2018 at 17:43):

Choose the option "Use tidy to fill in the goal."

view this post on Zulip Johan Commelin (Sep 03 2018 at 17:43):

theorem oiooo : 1 < 4 := by tidy

will also work.

view this post on Zulip Truong Nguyen (Sep 03 2018 at 18:29):

Oh, Thank you.
How about this one:

theorem tyyy (a b:  ):
(a + b) % 4 = (a % 4 + b % 4) % 4 :=
sorry

view this post on Zulip Bryan Gin-ge Chen (Sep 03 2018 at 18:46):

This is part of the way there:

import data.zmod, tactic.ring

theorem tyyy0 (a b:  ):
((a + b) : zmod 4) = (a : zmod 4) + (b : zmod 4) := by ring

There should be some way to use zmod.cast_mod_nat but I'm stuck.

view this post on Zulip Truong Nguyen (Sep 03 2018 at 18:51):

I am stuck too.

view this post on Zulip Reid Barton (Sep 03 2018 at 18:53):

I think the original tyyy is a lemma somewhere in mathlib

view this post on Zulip Reid Barton (Sep 03 2018 at 18:57):

There's int.add_mod_mod and int.mod_add_mod

view this post on Zulip Reid Barton (Sep 03 2018 at 19:00):

Which you can combine to get what you want

view this post on Zulip Chris Hughes (Sep 03 2018 at 19:01):

I think this should work

theorem tyyy (a b:  ):
(a + b) % 4 = (a % 4 + b % 4) % 4 :=
nat.modeq.modeq_add (eq.symm (nat.mod_mod _ _)) (eq.symm (nat.mod_mod _ _))

Last updated: May 10 2021 at 07:15 UTC