is there any better way?

Stream: maths

[Truong Nguyen]

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]

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

```lean
Your code goes here
```

[Kenny Lau]

theorem oiooo : 1 < 4 := dec_trivial

[Kenny Lau]

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

[Kevin Buzzard]

rofl

[Kevin Buzzard]

that's some obscure proof

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

import tactic.tidy

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

[Kenny Lau]

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

[Johan Commelin]

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]

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

[Johan Commelin]

theorem oiooo : 1 < 4 := by tidy

will also work.

[Truong Nguyen]

Oh, Thank you.
How about this one:

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

[Bryan Gin-ge Chen]

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.

[Truong Nguyen]

I am stuck too.

[Reid Barton]

I think the original tyyy is a lemma somewhere in mathlib

[Reid Barton]

There's int.add_mod_mod and int.mod_add_mod

[Reid Barton]

Which you can combine to get what you want

[Chris Hughes]

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