Stream: maths

Topic: is there any better way?

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

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



Kenny Lau (Sep 03 2018 at 17:38):

theorem oiooo : 1 < 4 := dec_trivial


Kenny Lau (Sep 03 2018 at 17:38):

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


rofl

Kevin Buzzard (Sep 03 2018 at 17:38):

that's some obscure proof

Kevin Buzzard (Sep 03 2018 at 17:39):

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

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

Johan Commelin (Sep 03 2018 at 17:42):

import tactic.tidy

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


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


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-.

Johan Commelin (Sep 03 2018 at 17:43):

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

Johan Commelin (Sep 03 2018 at 17:43):

theorem oiooo : 1 < 4 := by tidy


will also work.

Truong Nguyen (Sep 03 2018 at 18:29):

Oh, Thank you.

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


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.

I am stuck too.

Reid Barton (Sep 03 2018 at 18:53):

I think the original tyyy is a lemma somewhere in mathlib

Reid Barton (Sep 03 2018 at 18:57):

There's int.add_mod_mod and int.mod_add_mod

Reid Barton (Sep 03 2018 at 19:00):

Which you can combine to get what you want

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