Zulip Chat Archive

Stream: new members

Topic: rw failure


view this post on Zulip Kenny Lau (Sep 12 2018 at 19:01):

div and mod just don't interact in Lean

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

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:07):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:09):

right.

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

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

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:12):

my Lean doesn't have your QR PR

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:13):

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

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:16):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:16):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:17):

or something

view this post on Zulip Reid Barton (Sep 12 2018 at 19:19):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:20):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:20):

that well-known fact

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:21):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:22):

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

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

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:23):

We have Rob's linear arithmetic tactic

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:23):

And maybe Seul will come back at some point

view this post on Zulip Chris Hughes (Sep 12 2018 at 19:24):

I don't think that handles mod and integer division

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:17):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:17):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:17):

I'm wondering if it makes the proof any easier

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:18):

that's after applying the lemma

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

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

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

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

view this post on Zulip Xita Meyers (Sep 13 2018 at 11:31):

simpa using an9, works! Thanks!

view this post on Zulip Chris Hughes (Sep 13 2018 at 11:32):

(deleted)

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

view this post on Zulip JIANXIONG SUN (Oct 16 2018 at 23:35):

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

view this post on Zulip Andrew Ashworth (Oct 16 2018 at 23:36):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 23:47):

import algebra.group_power

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

view this post on Zulip Simon Hudon (Feb 15 2019 at 02:12):

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

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

view this post on Zulip Simon Hudon (Feb 15 2019 at 02:15):

Also: welcome to Zulip Paula!

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

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

view this post on Zulip Robert Spencer (Mar 15 2019 at 12:00):

(deleted)

view this post on Zulip Tony Wang (Mar 15 2019 at 12:11):

(deleted)

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

view this post on Zulip Tony Wang (Mar 15 2019 at 12:18):

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

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

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

view this post on Zulip Mario Carneiro (Mar 15 2019 at 12:30):

you can use conv to focus on a subterm

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

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

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

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

view this post on Zulip Chris Hughes (Mar 15 2019 at 19:25):

There's a lemma nat.pow_eq_pow I think.

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 19:26):

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

view this post on Zulip Chris Hughes (Mar 15 2019 at 19:26):

It's also a crappy fix

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 19:26):

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

view this post on Zulip Chris Hughes (Mar 15 2019 at 19:32):

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

view this post on Zulip Calle Sönne (Mar 16 2019 at 10:01):

thanks, that worked

view this post on Zulip Kevin Buzzard (Mar 16 2019 at 10:02):

Aah bingo

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