# Zulip Chat Archive

## Stream: new members

### Topic: rw failure

#### Kenny Lau (Sep 12 2018 at 19:01):

div and mod just don't interact in Lean

#### Etienne Laurin (Sep 12 2018 at 19:03):

In this example there is no need for cases, `have : p % 4 = 3, rw [nat_eq_sub_of_add_eq (nat.mod_add_div p 4), nat_eq_sub_of_add_eq thing11]`

#### Kenny Lau (Sep 12 2018 at 19:07):

I'm talking about the 2|p/2 not giving us useful information regarding p%4

#### Kevin Buzzard (Sep 12 2018 at 19:09):

right.

#### Kevin Buzzard (Sep 12 2018 at 19:09):

` have H : 3 = p % 4 := add_right_cancel (eq.trans thing11 (nat.mod_add_div p 4).symm),`

#### Chris Hughes (Sep 12 2018 at 19:10):

I'm talking about the 2|p/2 not giving us useful information regarding p%4

my quadratic reciprocity PR contains this lemma, which can be used to deduce `(p % 4) / 2 = 0`

from `nine`

which is also a way to get a contradiction

lemma mod_mul_right_div_self (a b c : ℕ) : a % (b * c) / b = (a / b) % c

#### Kenny Lau (Sep 12 2018 at 19:12):

my Lean doesn't have your QR PR

#### Etienne Laurin (Sep 12 2018 at 19:13):

This looks like it

https://github.com/leanprover/mathlib/blob/e005c3983be832dba68972519873df3ce0a2a6bb/data/nat/basic.lean#L240-L244

#### Kevin Buzzard (Sep 12 2018 at 19:13):

How about `a | (b / c) -> b % (a * c) < a`

modulo edge cases.

#### Chris Hughes (Sep 12 2018 at 19:15):

How about

`a | (b / c) -> b % (a * c) < a`

modulo edge cases.

The trouble with these lemmas is it's still hard to find the proof, because things like this aren't in the list of standard things in my head which I expect to be in the library.

#### Kevin Buzzard (Sep 12 2018 at 19:16):

`(b / c) % a = n -> a * n <= b % (a * c)`

#### Kevin Buzzard (Sep 12 2018 at 19:16):

`(b / c) % a = n -> b % (a * c) < a * (n + 1)`

#### Kevin Buzzard (Sep 12 2018 at 19:17):

or something

#### Reid Barton (Sep 12 2018 at 19:19):

A linear arithmetic solver should also be able to solve the original problem with suitable preprocessing

#### Kevin Buzzard (Sep 12 2018 at 19:20):

`b % (a * c) = b % c + c * ((b / c) % a)`

or something

#### Kevin Buzzard (Sep 12 2018 at 19:20):

that well-known fact

#### Kevin Buzzard (Sep 12 2018 at 19:21):

Is there some standard name like `omega`

or `sledgehammer`

or something, for a linear arithmetic solver?

#### Kevin Buzzard (Sep 12 2018 at 19:22):

oh wow that well-known fact might even be true in the edge cases

#### Chris Hughes (Sep 12 2018 at 19:23):

@Reid Barton Do you know if there are "standard" algorithms powerful enough to do that sort of thing?

#### Patrick Massot (Sep 12 2018 at 19:23):

We have Rob's linear arithmetic tactic

#### Patrick Massot (Sep 12 2018 at 19:23):

And maybe Seul will come back at some point

#### Chris Hughes (Sep 12 2018 at 19:24):

I don't think that handles mod and integer division

#### Kevin Buzzard (Sep 12 2018 at 20:17):

My attempt to write some div mod stuff is `div_mod_stuff.lean`

in the cocalc repo

#### Kevin Buzzard (Sep 12 2018 at 20:17):

I have to clean the kitchen. I proved the well-known lemma

#### Kevin Buzzard (Sep 12 2018 at 20:17):

`lemma well_known (a b c : ℕ) : b % (a * c) = b % c + c * ((b / c) % a) := [done]`

#### Kevin Buzzard (Sep 12 2018 at 20:17):

I'm wondering if it makes the proof any easier

#### Kevin Buzzard (Sep 12 2018 at 20:18):

nine : 2 ∣ p / 2, thing11 : 3 + 4 * (p / 4) = p, [used] H : 3 = p % 2 + 2 * (p / 2 % 2) ⊢ false

#### Kevin Buzzard (Sep 12 2018 at 20:18):

that's after applying the lemma

#### Reid Barton (Sep 12 2018 at 21:02):

Chris the original statement can be expressed in Presburger arithmetic (natural numbers with only addition), which has a decidable theory -- that's what Seul Baek implemented in `cooper`

, I believe.

#### Johan Commelin (Sep 13 2018 at 03:52):

@Tobias Grosser Is also working on Presburger arithmetic in Lean. He told me he would like to match up with someone who knows Lean/maths to get implement a version for mathlib.

#### Xita Meyers (Sep 13 2018 at 11:26):

An additional question-- something that I have no idea how to fix. I currently have

an9 : 1 + x ^ 2 ≡ 0 [MOD p] ⊢ 1 + x ^ 2 ≡ 0 [MOD p]

and ` exact an9, `

gives the error message:

invalid type ascription, term has type nat.modeq p (@has_add.add nat nat.has_add 1 (@has_pow.pow nat nat (@monoid.has_pow nat nat.monoid) x 2)) 0 but is expected to have type nat.modeq p (@has_add.add nat nat.has_add 1 (@has_pow.pow nat nat nat.has_pow x 2)) 0

In the middle of a complicated code, so I haven't made an MWE yet. Would this be easily fixable? (Before I try a different approach)

#### Rob Lewis (Sep 13 2018 at 11:30):

Does `simpa`

or `simpa using an9`

work? I think there's a simp lemma for rewriting pow on `nat`

.

#### Xita Meyers (Sep 13 2018 at 11:31):

`simpa using an9,`

works! Thanks!

#### Chris Hughes (Sep 13 2018 at 11:32):

(deleted)

#### Tobias Grosser (Sep 13 2018 at 12:20):

@Johan Commelin , yes I am interested in Presburger arithmetic.Still learning more about lean, but I am certainly interested to chat about this. In case sb is interested in collaborating, I am open to collaborative visits or internships @ETH.

#### JIANXIONG SUN (Oct 16 2018 at 23:35):

How can I represent square or cube in Lean such as x^2?

#### Andrew Ashworth (Oct 16 2018 at 23:36):

what error does lean give you when you write `x^2`

?

#### Kenny Lau (Oct 16 2018 at 23:47):

`import algebra.group_power`

#### Paula Neeley (Feb 15 2019 at 02:00):

Hey guys,

First timer, so please be nice :)

I'm aiming to prove the example at the bottom of the long code snippet. I made the lemmas "foo" and "bar" to help. My theorem "bar" worked to prove the inductive step, but I don't understand the output that Lean gives me when I try to prove this lemma "bar" itself. The base case gives me the output:

2 goals case list.nil α : Type u_1, s : list α, a : α ⊢ length (s ++ [a]) = length (s ++ nil) + 1

Specifically, I am unsure what the [a] here means and how to work with it. Any insights would be appreciated.

section open list variable {α : Type*} variables s t : list α variable a : α theorem length_nil : length (@nil α) = 0 := rfl theorem foo (t : list α) : t ++ nil = t := begin induction t with a t ih, {refl}, rw [cons_append, ih], end theorem bar : length (s ++ a :: t) = length (s ++ t) + 1 := begin induction t with a t ih, sorry end #check foo #check nil_append #check cons_append #check length_cons #check length_nil #eval [1, 2, 3] ++ [4, 5] #eval length [1, 2, 3, 4, 5] end /- Prove the following. -/ section open list variable {α : Type*} variables s t : list α variable a : α example : length (s ++ t) = length s + length t := begin induction t with a t ih, {rw [length_nil, foo], refl}, rw [length_cons, bar, ih], refl, end end

#### Simon Hudon (Feb 15 2019 at 02:12):

`[a]`

is the same as `a :: nil`

(it's a special notation)

#### Simon Hudon (Feb 15 2019 at 02:14):

You should consider doing your induction on `s`

instead of `t`

. The reason is that `++`

is defined by recursion on `s`

: `x :: xs ++ ys = x :: (xs ++ ys)`

#### Simon Hudon (Feb 15 2019 at 02:15):

Also: welcome to Zulip Paula!

#### Paula Neeley (Feb 15 2019 at 02:15):

You should consider doing your induction on

`s`

instead of`t`

. The reason is that`++`

is defined by recursion on`s`

:`x :: xs ++ ys = x :: (xs ++ ys)`

Oh ok, I will try that! Thank you for your help!

#### Kenny Lau (Feb 15 2019 at 08:32):

namespace list variable {α : Type*} variables s t : list α variable a : α theorem length_nil : length (@nil α) = 0 := rfl theorem append_nil' : ∀ t : list α, t ++ nil = t | [] := rfl | (hd::tl) := congr_arg ((::)hd) (append_nil tl) theorem length_append' : ∀ s t : list α, length (s ++ t) = length s + length t | [] t := (zero_add _).symm | (hd::tl) t := by rw [length_cons, nat.succ_add, ← length_append' tl t]; refl theorem length_append_cons : length (s ++ a :: t) = length (s ++ t) + 1 := by rw [length_append', length_append']; refl #check append_nil' #check nil_append #check cons_append #check length_cons #check length_nil #eval [1, 2, 3] ++ [4, 5] #eval length [1, 2, 3, 4, 5] end list

#### Robert Spencer (Mar 15 2019 at 12:00):

(deleted)

#### Tony Wang (Mar 15 2019 at 12:11):

(deleted)

#### Tony Wang (Mar 15 2019 at 12:17):

Hello - I was just wondering for the bit where I have `rw succ_a_plus_b_equals_a_plus_succ_b`

below, surely there's a better way to use the definition of `add`

?

inductive xnat | zero : xnat | succ : xnat → xnat open xnat def add : xnat → xnat → xnat | n zero := n | a (succ b) := succ (add a b) notation a + b := add a b theorem succ_a_plus_b_equals_a_plus_succ_b (a b : xnat) : succ(a + b) = a + succ(b) := by unfold add theorem succ_is_succ_zero_add (a : xnat) : succ a = succ zero + a := begin induction a with k Hk, { unfold add }, { rw Hk, rw succ_a_plus_b_equals_a_plus_succ_b, rw Hk } end

#### Tony Wang (Mar 15 2019 at 12:18):

Nvm I found it: `rw ←add`

seems to work!

#### Calle Sönne (Mar 15 2019 at 12:19):

I have the following code:

definition digit (b : ℕ) (r : α) (n : ℕ) := floor(r * b ^ (n+1)) - floor(r * b ^ n)*b lemma digit_mul_base (b : ℕ) (r : α) (n : ℕ) : digit b r (n+1) = digit b (r*b) (n) := begin rwa [digit, digit, mul_assoc], conv begin congr, skip, rw [←nat.cast_pow, ←nat.cast_mul, ←pow_succ b (n+1)], end, end

This gives me an error with following tactic state:

rewrite tactic failed, did not find instance of the pattern in the target expression b * b ^ (n + 1) state: α : Type u_1, _inst_1 : linear_ordered_ring α, _inst_2 : floor_ring α, b : ℕ, r : α, n : ℕ ⊢ ⌊r * ↑(b * b ^ (n + 1))⌋ - ⌊r * ↑b * ↑b ^ n⌋ * ↑b = ?m_1

I cant seem to find the error, any help would be appreciated

#### Tony Wang (Mar 15 2019 at 12:27):

If I unfold a definition with more than one part, is it possible to specify which part I want to unfold?

#### Mario Carneiro (Mar 15 2019 at 12:30):

you can use `conv`

to focus on a subterm

#### Kevin Buzzard (Mar 15 2019 at 19:14):

[changed thread title]. @Calle Sönne

One `b * b ^ (n + 1)`

is

@has_mul.mul.{0} nat (@semigroup.to_has_mul.{0} nat (@monoid.to_semigroup.{0} nat nat.monoid)) b (@has_pow.pow.{0 0} nat nat (@monoid.has_pow.{0} nat nat.monoid) b (@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one)))

and the other is

(@has_mul.mul.{0} nat nat.has_mul b (@has_pow.pow.{0 0} nat nat nat.has_pow b (@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one)))))))

and these are apparently not defeq.

#### Kevin Buzzard (Mar 15 2019 at 19:17):

`example : @monoid.has_pow.{0} nat nat.monoid = nat.has_pow := rfl -- fails`

There's the problem. You have two different powers.

#### Kevin Buzzard (Mar 15 2019 at 19:24):

lemma test (a b : ℕ) : @has_pow.pow ℕ ℕ (@monoid.has_pow.{0} nat nat.monoid) a b = a ^ b := begin induction b with c Hc, refl, unfold has_pow.pow monoid.pow nat.pow at *, rw Hc, apply mul_comm, -- *boggle* end lemma digit_mul_base (b : ℕ) (r : α) (n : ℕ) : digit b r (n+1) = digit b (r*b) (n) := begin rwa [digit, digit, mul_assoc], conv begin congr, skip, rw [←nat.cast_pow, ←nat.cast_mul], rw ←test, -- no visible effect ;-) rw ←pow_succ b (n+1), -- works now ;-) end,

#### Kevin Buzzard (Mar 15 2019 at 19:24):

So there's a crappy fix, but actually someone with some sense should hopefully come along at some point and tell us what we should be doing. @Chris Hughes ?

#### Chris Hughes (Mar 15 2019 at 19:25):

There's a lemma `nat.pow_eq_pow`

I think.

#### Kevin Buzzard (Mar 15 2019 at 19:26):

Thanks. @Calle Sönne rewrite that instead of `test`

.

#### Chris Hughes (Mar 15 2019 at 19:26):

It's also a crappy fix

#### Kevin Buzzard (Mar 15 2019 at 19:26):

yes but at least we're going in the right direction. Why did it happen? Something to do with the casts no doubt.

#### Kevin Buzzard (Mar 15 2019 at 19:26):

We can add this one to Rob Lewis' list of cast issues ;-)

#### Chris Hughes (Mar 15 2019 at 19:32):

The better solution is actually to use `nat.pow_succ`

on closer inspection.

#### Calle Sönne (Mar 16 2019 at 10:01):

thanks, that worked

#### Kevin Buzzard (Mar 16 2019 at 10:02):

Aah bingo

#### Kevin Buzzard (Mar 16 2019 at 10:03):

Nat has its own suite of pow lemmas because nat.pow is in core so we can't redefine it to be monoid.pow

Last updated: May 11 2021 at 12:15 UTC