Zulip Chat Archive

Stream: new members

Topic: int.mod


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 01 2018 at 07:48):

there should be a theorem called int.mod_lt for this

view this post on Zulip Mario Carneiro (Nov 01 2018 at 07:49):

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

view this post on Zulip petercommand (Nov 01 2018 at 07:51):

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

view this post on Zulip petercommand (Nov 01 2018 at 07:52):

There is nat.mod_lt though

view this post on Zulip Johan Commelin (Nov 01 2018 at 07:54):

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

view this post on Zulip petercommand (Nov 01 2018 at 07:55):

no

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip petercommand (Nov 01 2018 at 07:58):

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

view this post on Zulip Johan Commelin (Nov 01 2018 at 08:01):

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

view this post on Zulip Mario Carneiro (Nov 01 2018 at 08:02):

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

view this post on Zulip 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

view this post on Zulip petercommand (Nov 01 2018 at 08:04):

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

view this post on Zulip petercommand (Nov 01 2018 at 08:07):

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

view this post on Zulip Johan Commelin (Nov 01 2018 at 08:12):

I guess it is some sort of inductive definition

view this post on Zulip 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.

view this post on Zulip petercommand (Nov 01 2018 at 08:13):

Which, in int.of_nat a_1, is of_nat

view this post on Zulip 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.

view this post on Zulip petercommand (Nov 01 2018 at 08:13):

True

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:13):

If you post a MWE I can try to help.

view this post on Zulip 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

view this post on Zulip petercommand (Nov 01 2018 at 08:16):

Thanks

view this post on Zulip petercommand (Nov 01 2018 at 08:17):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:19):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:23):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:23):

Well, that's my amateur diagnosis anyway.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:27):

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

view this post on Zulip 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)

view this post on Zulip petercommand (Nov 01 2018 at 08:29):

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

view this post on Zulip petercommand (Nov 01 2018 at 08:30):

@Kenny Lau thanks

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:31):

it is

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:31):

oh, and it isn't def

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:31):

it's theorem

view this post on Zulip 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

view this post on Zulip petercommand (Nov 01 2018 at 08:32):

aren't they synonyms?

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:32):

no

view this post on Zulip petercommand (Nov 01 2018 at 08:33):

what's different between def and thoerem?

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:33):

def is data

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:33):

theorem is proof

view this post on Zulip petercommand (Nov 01 2018 at 08:34):

I mean, semantically, are they different?

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:34):

yes

view this post on Zulip petercommand (Nov 01 2018 at 08:35):

proof irrelevance?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:36):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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
-/

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:39):

@Kevin Buzzard lol the conditions keep changing

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:39):

@petercommand can you make up your mind?

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:39):

I never changed anything, I just copied his MWE.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:40):

Did you look at my tactic mode post?

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:40):

There's an extra nat

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:40):

-- ??

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:40):

I don't know why you have 4 intros

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:40):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:41):

what do you mean Lean is asking for 4

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:41):

What do you mean? The function wants 4 inputs

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:41):

that's spooky

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:41):

Must be Halloween.

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:42):

oh!

view this post on Zulip petercommand (Nov 01 2018 at 08:42):

o.o

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:42):

lol

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:42):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:42):

> is a binder or something

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:43):

right

view this post on Zulip 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 :=

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:45):

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

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:45):

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

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:45):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip petercommand (Nov 01 2018 at 08:48):

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

view this post on Zulip petercommand (Nov 01 2018 at 08:48):

anyway

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:54):

because Kenny (intentionally) wrote bad code

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:55):

because test is now a definition so it has definitional equations

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:55):

just write any old definition

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:55):

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

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:55):

because they were not designed to be used in these circumstances

view this post on Zulip Kenny Lau (Nov 01 2018 at 08:56):

undocumented behaviour... lul

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 08:56):

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

view this post on Zulip AHan (Nov 01 2018 at 08:58):

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

view this post on Zulip Kenny Lau (Nov 01 2018 at 09:00):

you don't really use it

view this post on Zulip Kenny Lau (Nov 01 2018 at 09:00):

it's internal mechanism

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 09:00):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 01 2018 at 09:01):

unfold X is simp only [equation lemmas for X]

view this post on Zulip 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)

view this post on Zulip AHan (Nov 01 2018 at 09:03):

Are they the beta reduction rules?


Last updated: May 13 2021 at 04:21 UTC