## Stream: new members

### Topic: int.mod

#### petercommand (Nov 01 2018 at 07:47):

Trying to prove int.mod (int.of_nat a_1) ↑p < ↑p in lean, but I wasn't able to unfold int.mod.

#### Mario Carneiro (Nov 01 2018 at 07:48):

there should be a theorem called int.mod_lt for this

#### Mario Carneiro (Nov 01 2018 at 07:49):

it is int.mod_lt_of_pos and it isn't true when a_1 = 0

#### petercommand (Nov 01 2018 at 07:51):

I can't find int.mod_lt in C-c C-d

#### petercommand (Nov 01 2018 at 07:52):

There is nat.mod_lt though

#### Johan Commelin (Nov 01 2018 at 07:54):

@petercommand Welcome! Can you tell if Mario's suggestion works?

no

#### Johan Commelin (Nov 01 2018 at 07:55):

Ok, can you give a more detailed version of what you want to prove? A "minimal working example" (MWE)

#### Johan Commelin (Nov 01 2018 at 07:56):

So something of the form

lemma foobar (p : ??) (a_1 : int) : int.mod (int.of_nat a_1) ↑p < ↑p := sorry


#### petercommand (Nov 01 2018 at 07:58):

def test : Π (a b : ℤ) (p : ℕ), (a + b) % p < p := sorry

#### Johan Commelin (Nov 01 2018 at 08:01):

That isn't true if p = 0, right?

#### Mario Carneiro (Nov 01 2018 at 08:02):

Do you have mathlib? int.mod_lt_of_pos is in data.int.basic

#### petercommand (Nov 01 2018 at 08:03):

@Johan Commelin ah, it should be def test : Π (a b : ℤ) (p : ℕ) (p >= 2), (a + b) % p < p := sorry

#### petercommand (Nov 01 2018 at 08:04):

@Mario Carneiro Ah..Thanks! I didn't set up mathlib

#### petercommand (Nov 01 2018 at 08:07):

why wasn't I able to unfold int.mod though

#### Johan Commelin (Nov 01 2018 at 08:12):

I guess it is some sort of inductive definition

#### Kevin Buzzard (Nov 01 2018 at 08:12):

int is an inductive type with two constructors. int.mod eats an int, and how it unfolds depends on which constructor you use -- int.mod can't unfold unless it knows which it is.

#### petercommand (Nov 01 2018 at 08:13):

Which, in int.of_nat a_1, is of_nat

#### Kevin Buzzard (Nov 01 2018 at 08:13):

But on the other hand you probably don't want to be unfolding int.mod. The devs will have made all the infrastructure you need, at least that's the philosophy.

True

#### Kevin Buzzard (Nov 01 2018 at 08:13):

If you post a MWE I can try to help.

#### petercommand (Nov 01 2018 at 08:15):

def test : Π (a p : ℕ) (p > 0) , int.mod (int.of_nat a) ↑p < ↑p := sorry  something like this

Thanks

#### petercommand (Nov 01 2018 at 08:17):

My first MWE wasn't clear, this one should be a bit better

#### Kevin Buzzard (Nov 01 2018 at 08:18):

the answer appears to be that the exact definition of int.mod uses ↑a instead of int.of_nat a

#### Kevin Buzzard (Nov 01 2018 at 08:19):

def test : Π (a p : ℕ) (p > 0) , int.mod (int.of_nat a) ↑p < ↑p :=
begin
--  unfold int.mod, -- fails
change Π (a p : ℕ) (p > 0), int.mod (a : ℕ) ↑p < ↑p,
unfold int.mod,
sorry
end


#### Kevin Buzzard (Nov 01 2018 at 08:19):

All the more reason why you shouldn't be unfolding it ;-)

#### Kevin Buzzard (Nov 01 2018 at 08:21):

I just wrote #check int.mod and then right clicked on int.mod and peeked the actual definition.

#### Kevin Buzzard (Nov 01 2018 at 08:23):

Of course the two things are definitionally equal: example (a : ℕ) : int.of_nat a = ↑a := rfl

#### Kevin Buzzard (Nov 01 2018 at 08:23):

But under the hood unfold is using simp, and I think simp can be fussy about not changing things to definitionally equal things.

#### Kevin Buzzard (Nov 01 2018 at 08:23):

Well, that's my amateur diagnosis anyway.

#### Kenny Lau (Nov 01 2018 at 08:26):

def test (a b : ℤ) (p : ℕ) (Hp : p ≥ 2) : (a + b) % p < p :=
match a+b with
| (n:ℕ) := show ↑(n%p:ℕ) < (p:ℤ), from int.coe_nat_lt_coe_nat_of_lt
(nat.mod_lt _ (lt_of_le_of_lt dec_trivial Hp))
| -[1+ n] := show ↑p + -[1+ n%p] < ↑p, from add_lt_of_le_of_neg
(le_refl p) (int.neg_succ_lt_zero (n%p))
end


#### Kevin Buzzard (Nov 01 2018 at 08:27):

A side comment -- I think test is not quite what you want to prove (AFK)

#### Kenny Lau (Nov 01 2018 at 08:27):

def test (a b : ℤ) (p : ℕ) (Hp : p > 0) : (a + b) % p < p :=
match a+b with
| (n:ℕ) := show ↑(n%p:ℕ) < (p:ℤ), from int.coe_nat_lt_coe_nat_of_lt (nat.mod_lt _ Hp)
| -[1+ n] := show ↑p + -[1+ n%p] < ↑p, from add_lt_of_le_of_neg
(le_refl p) (int.neg_succ_lt_zero (n%p))
end


(I just noticed that you changed the condition again)

#### petercommand (Nov 01 2018 at 08:29):

hmm, this is quite annoying..I thought int.mod was directly matching on the constructor

#### petercommand (Nov 01 2018 at 08:30):

@Kenny Lau thanks

#### Kenny Lau (Nov 01 2018 at 08:31):

def test (a b : ℤ) (p : ℕ) (Hp : p > 0) : (a + b) % p < p :=
match a+b with
| (n:ℕ) := show ↑(n%p:ℕ) < (p:ℤ), from int.coe_nat_lt_coe_nat_of_lt (nat.mod_lt _ Hp)
| -[1+ n] := show ↑p + -[1+ n%p] < ↑p, from int.lt.intro (neg_add_cancel_right (p:ℤ) (n%p+1))
end


it is

#### Kenny Lau (Nov 01 2018 at 08:31):

oh, and it isn't def

#### Kenny Lau (Nov 01 2018 at 08:31):

it's theorem

#### Kenny Lau (Nov 01 2018 at 08:32):

theorem test (a b : ℤ) (p : ℕ) (Hp : p > 0) : (a + b) % p < p :=
match a+b with
| (n:ℕ) := show ↑(n%p:ℕ) < (p:ℤ), from int.coe_nat_lt_coe_nat_of_lt (nat.mod_lt _ Hp)
| -[1+ n] := show ↑p + -[1+ n%p] < ↑p, from int.lt.intro (neg_add_cancel_right (p:ℤ) (n%p+1))
end


#### petercommand (Nov 01 2018 at 08:32):

aren't they synonyms?

no

#### petercommand (Nov 01 2018 at 08:33):

what's different between def and thoerem?

def is data

theorem is proof

#### petercommand (Nov 01 2018 at 08:34):

I mean, semantically, are they different?

yes

#### petercommand (Nov 01 2018 at 08:35):

proof irrelevance?

#### petercommand (Nov 01 2018 at 08:36):

https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html
Ah, it says that
by proof irrelevance, any two proofs of that theorem are definitionally equal.

#### Kenny Lau (Nov 01 2018 at 08:36):

theorem x : nat := 5
def test : x=5 := sorry


#### Kenny Lau (Nov 01 2018 at 08:36):

https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html
Ah, it says that
by proof irrelevance, any two proofs of that theorem are definitionally equal.

that's irrelevant

#### Kevin Buzzard (Nov 01 2018 at 08:37):

Kenny, independent of that def/theorem business, what's happening below? @petercommand 's original formulation of the MWE has something wrong with it I think:

def test : Π (a p : ℕ) (p > 0) , int.mod (int.of_nat a) ↑p < ↑p :=
begin
intro a,
intro b, -- ??
intro p,
intro HP,
-- ⊢ int.mod (int.of_nat a) ↑p < ↑p
sorry
end


#### Kenny Lau (Nov 01 2018 at 08:38):

def test : 5=5 := rfl
#print prefix test
/-
test : 5 = 5
test.equations._eqn_1 : test = rfl
-/

theorem test2 : 5=5 := rfl
#print prefix test2
/-
test2 : 5 = 5
-/


#### Kenny Lau (Nov 01 2018 at 08:39):

@Kevin Buzzard lol the conditions keep changing

#### Kevin Buzzard (Nov 01 2018 at 08:39):

I think the p in forall p isn't the same as the p in p > 0.

#### Kenny Lau (Nov 01 2018 at 08:39):

@petercommand can you make up your mind?

#### Kevin Buzzard (Nov 01 2018 at 08:39):

I never changed anything, I just copied his MWE.

#### Kenny Lau (Nov 01 2018 at 08:39):

I think the p in forall p isn't the same as the p in p > 0.

I think it's the same

#### Kevin Buzzard (Nov 01 2018 at 08:40):

Did you look at my tactic mode post?

#### Kevin Buzzard (Nov 01 2018 at 08:40):

There's an extra nat

#### Kevin Buzzard (Nov 01 2018 at 08:40):

-- ??

#### Kenny Lau (Nov 01 2018 at 08:40):

I don't know why you have 4 intros

#### Kevin Buzzard (Nov 01 2018 at 08:40):

because Lean is asking for 4. That's the point I'm trying to make

#### Kenny Lau (Nov 01 2018 at 08:41):

what do you mean Lean is asking for 4

#### Kevin Buzzard (Nov 01 2018 at 08:41):

What do you mean? The function wants 4 inputs

that's spooky

#### Kevin Buzzard (Nov 01 2018 at 08:41):

Must be Halloween.

oh!

o.o

lol

#### Kenny Lau (Nov 01 2018 at 08:42):

theorem test : Π (a : ℕ) (p > 0) , int.mod (int.of_nat a) ↑p < ↑p :=


#### Kenny Lau (Nov 01 2018 at 08:42):

> is a binder or something

right

#### Kevin Buzzard (Nov 01 2018 at 08:44):

@petercommand this is fine: theorem test : ∀ (a p : ℕ), (p > 0) → int.mod (int.of_nat a) ↑p < ↑p :=

#### Kevin Buzzard (Nov 01 2018 at 08:44):

but (p > 0) before the comma gets interpreted as "and there's another variable p, different to the p you just mentioned"

#### Kenny Lau (Nov 01 2018 at 08:45):

I don't think @petercommand has tested his "MWE" before posting

#### Kevin Buzzard (Nov 01 2018 at 08:45):

def test' : Π (a : ℕ) (p > 0) , int.mod (int.of_nat a) ↑p < ↑p :=  is OK

#### Kevin Buzzard (Nov 01 2018 at 08:45):

I just made it a bit more minimal, that's all ;-)

#### petercommand (Nov 01 2018 at 08:46):

I don't think @petercommand has tested his "MWE" before posting

Yeah, I should've tested the MWEs o.o Thought that was simple enough

#### Kenny Lau (Nov 01 2018 at 08:46):

theorem test' (a : ℕ) (p > 0) : int.mod (int.of_nat a) ↑p < ↑p :=
int.coe_nat_lt_coe_nat_of_lt (nat.mod_lt _ H)


#### petercommand (Nov 01 2018 at 08:48):

Hmm, actually, I tested the MWEs, but didn't discover that I got one more variable

anyway

#### Kevin Buzzard (Nov 01 2018 at 08:54):

import data.int.basic

theorem test' (a p : ℕ) (H : p > 0) : int.mod (int.of_nat a) ↑p < ↑p :=
int.mod_lt_of_pos a (int.coe_nat_lt_coe_nat_of_lt H)


#### AHan (Nov 01 2018 at 08:54):

@Kenny Lau About the difference between "def" and "theorem", why is there test.eqations._eqn_1 appeared in your example
def test : 5=5 := rfl #print prefix test

#### Kevin Buzzard (Nov 01 2018 at 08:54):

because Kenny (intentionally) wrote bad code

#### Kenny Lau (Nov 01 2018 at 08:55):

because test is now a definition so it has definitional equations

#### Kenny Lau (Nov 01 2018 at 08:55):

just write any old definition

#### Kevin Buzzard (Nov 01 2018 at 08:55):

If you use def instead of theorem or theorem instead of def, expect random things

#### Kevin Buzzard (Nov 01 2018 at 08:55):

because they were not designed to be used in these circumstances

#### Kenny Lau (Nov 01 2018 at 08:56):

undocumented behaviour... lul

#### Kevin Buzzard (Nov 01 2018 at 08:56):

I think "garbage in, garbage out" is well documented in the literature

#### AHan (Nov 01 2018 at 08:58):

What does the definitional equations refers to here?
And how to use it in a normal def?

#### Kenny Lau (Nov 01 2018 at 09:00):

you don't really use it

#### Kenny Lau (Nov 01 2018 at 09:00):

it's internal mechanism

#### Kevin Buzzard (Nov 01 2018 at 09:00):

Every time you make a definition (especially a nice complicated one, maybe with pattern matching) Lean creates some secret "equation lemmas"

#### Kevin Buzzard (Nov 01 2018 at 09:00):

and when you try and unfold the definition, Lean uses these lemmas

#### Kevin Buzzard (Nov 01 2018 at 09:01):

As Kenny says, this is all done internally and the user is not supposed to have to worry about it. It's basically the trick which makes "unfold" work.

#### Kevin Buzzard (Nov 01 2018 at 09:01):

unfold X is simp only [equation lemmas for X]

#### Kevin Buzzard (Nov 01 2018 at 09:02):

(this is my slightly amateurish understanding of it -- I am a mathematician so shouldn't really be talking about implementation issues)

#### AHan (Nov 01 2018 at 09:03):

Are they the beta reduction rules?

Last updated: May 13 2021 at 04:21 UTC