## 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

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

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

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
but is expected to have type


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!

(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


(deleted)

(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,
{
},
{
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):

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


and the other is

     (@has_mul.mul.{0} nat nat.has_mul b
(@has_pow.pow.{0 0} nat nat nat.has_pow b


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

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