rw failure

Stream: new members

[Kenny Lau]

div and mod just don't interact in Lean

[Etienne Laurin]

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]

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

[Kevin Buzzard]

right.

[Kevin Buzzard]

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

[Chris Hughes]

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]

my Lean doesn't have your QR PR

[Etienne Laurin]

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

[Kevin Buzzard]

How about a | (b / c) -> b % (a * c) < a modulo edge cases.

[Chris Hughes]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

or something

[Reid Barton]

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

[Kevin Buzzard]

b % (a * c) = b % c + c * ((b / c) % a)or something

[Kevin Buzzard]

that well-known fact

[Kevin Buzzard]

Is there some standard name like omega or sledgehammer or something, for a linear arithmetic solver?

[Kevin Buzzard]

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

[Chris Hughes]

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

[Patrick Massot]

We have Rob's linear arithmetic tactic

[Patrick Massot]

And maybe Seul will come back at some point

[Chris Hughes]

I don't think that handles mod and integer division

[Kevin Buzzard]

My attempt to write some div mod stuff is div_mod_stuff.lean in the cocalc repo

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I'm wondering if it makes the proof any easier

[Kevin Buzzard]

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

[Kevin Buzzard]

that's after applying the lemma

[Reid Barton]

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]

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

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]

Does simpa or simpa using an9 work? I think there's a simp lemma for rewriting pow on nat.

[Xita Meyers]

simpa using an9, works! Thanks!

[Chris Hughes]

(deleted)

[Tobias Grosser]

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

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

[Andrew Ashworth]

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

[Kenny Lau]

import algebra.group_power

[Paula Neeley]

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]

[a] is the same as a :: nil (it's a special notation)

[Simon Hudon]

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]

Also: welcome to Zulip Paula!

[Paula Neeley]

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]

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]

(deleted)

[Tony Wang]

(deleted)

[Tony Wang]

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]

Nvm I found it: rw ←add seems to work!

[Calle Sönne]

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]

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

[Mario Carneiro]

you can use conv to focus on a subterm

[Kevin Buzzard]

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

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

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

[Kevin Buzzard]

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]

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]

There's a lemma nat.pow_eq_pow I think.

[Kevin Buzzard]

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

[Chris Hughes]

It's also a crappy fix

[Kevin Buzzard]

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]

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

[Chris Hughes]

The better solution is actually to use nat.pow_succ on closer inspection.

[Calle Sönne]

thanks, that worked

[Kevin Buzzard]

Aah bingo

[Kevin Buzzard]

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