int.mod

Stream: new members

[petercommand]

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]

there should be a theorem called int.mod_lt for this

[Mario Carneiro]

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

[petercommand]

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

[petercommand]

There is nat.mod_lt though

[Johan Commelin]

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

[petercommand]

no

[Johan Commelin]

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

[Johan Commelin]

So something of the form

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

[petercommand]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[petercommand]

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

[petercommand]

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

[petercommand]

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

[Johan Commelin]

I guess it is some sort of inductive definition

[Kevin Buzzard]

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]

Which, in int.of_nat a_1, is of_nat

[Kevin Buzzard]

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.

[petercommand]

True

[Kevin Buzzard]

If you post a MWE I can try to help.

[petercommand]

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

[petercommand]

Thanks

[petercommand]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Well, that's my amateur diagnosis anyway.

[Kenny Lau]

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]

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

[Kenny Lau]

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]

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

[petercommand]

@Kenny Lau thanks

[Kenny Lau]

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

[Kenny Lau]

it is

[Kenny Lau]

oh, and it isn't def

[Kenny Lau]

it's theorem

[Kenny Lau]

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]

aren't they synonyms?

[Kenny Lau]

no

[petercommand]

what's different between def and thoerem?

[Kenny Lau]

def is data

[Kenny Lau]

theorem is proof

[petercommand]

I mean, semantically, are they different?

[Kenny Lau]

yes

[petercommand]

proof irrelevance?

[petercommand]

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]

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

[Kenny Lau]

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]

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]

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]

@Kevin Buzzard lol the conditions keep changing

[Kevin Buzzard]

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

[Kenny Lau]

@petercommand can you make up your mind?

[Kevin Buzzard]

I never changed anything, I just copied his MWE.

[Kenny Lau]

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]

Did you look at my tactic mode post?

[Kevin Buzzard]

There's an extra nat

[Kevin Buzzard]

-- ??

[Kenny Lau]

I don't know why you have 4 intros

[Kevin Buzzard]

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

[Kenny Lau]

what do you mean Lean is asking for 4

[Kevin Buzzard]

What do you mean? The function wants 4 inputs

[Kenny Lau]

that's spooky

[Kevin Buzzard]

Must be Halloween.

[Kenny Lau]

oh!

[petercommand]

o.o

[Kenny Lau]

lol

[Kenny Lau]

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

[Kenny Lau]

> is a binder or something

[Kevin Buzzard]

right

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[petercommand]

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]

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]

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

[petercommand]

anyway

[Kevin Buzzard]

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]

@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]

because Kenny (intentionally) wrote bad code

[Kenny Lau]

because test is now a definition so it has definitional equations

[Kenny Lau]

just write any old definition

[Kevin Buzzard]

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

[Kevin Buzzard]

because they were not designed to be used in these circumstances

[Kenny Lau]

undocumented behaviour... lul

[Kevin Buzzard]

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

[AHan]

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

[Kenny Lau]

you don't really use it

[Kenny Lau]

it's internal mechanism

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

unfold X is simp only [equation lemmas for X]

[Kevin Buzzard]

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

[AHan]

Are they the beta reduction rules?