Zulip Chat Archive

Stream: maths

Topic: Missing maths tactic?


view this post on Zulip Kevin Buzzard (Nov 23 2018 at 21:39):

example (a b c d : ℤ) (H : a - b = c * d) : b - a = c * (-d) := by simp [H] -- fails.

Is this one of those instances when someone familiar with Coq says "oh, it would work if you had <insert name of tactic which I don't know what it does, but it turns out it does this>"? I'm teaching equivalence relations shortly, and this stuff comes up with congruences; I want to give Lean a big push if possible but I want to make it look slick, ideally.

I remark that example (a b c d : ℤ) (H : a - b = c * d) : b - a = c * (-d) := by simp [H.symm] works! But I am stuck with having it this way round because it's how has_dvd.dvd unfolds on int :-( [I'm trying to prove congruence mod c is symmetric in a completely transparent way]

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 22:05):

heh:

example (a b c : ) : a - c = a - b + (b - c) := by simp -- fails
import tactic.ring

example (a b c : ) : a - c = a - b + (b - c) := by ring -- works (of course)

but the surprise is

import tactic.ring

example (a b c : ) : a - c = a - b + (b - c) := by simp -- works!

For this one I knew the tactic, but then I realised I didn't need it.

view this post on Zulip Patrick Massot (Nov 23 2018 at 22:07):

I think last year we had an extended discussion about how to define this equivalence relation in order to get an easy proof

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 22:07):

But I really want a one-liner for this if possible:

example (m a b c j k : ) (Hj : a - b = m * j) (Hk : b - c = m * k) :
a - c = m * (j + k) :=
begin
  rw [mul_add],
  rw [Hj,Hk],
  -- ⊢ a - c = a - b + (b - c)
  simp, -- works if tactic.ring imported
end

I want to do ring [Hj,Hk] or something, but I'm well aware that life isn't so easy.

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

I think last year we had an extended discussion about how to define this equivalence relation in order to get an easy proof

Yes, the trick is to define congruence mod m (it was mod 37 last time) in a different way -- the order matters. But unfortunately in my lectures I defined congruence mod m to mean m | (a - b) so now I'm stuck with it and it unfolds to something which is not in the optimal order.

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

Is this one of those things which is done by omega or cooper or something -- these tactics that I have no idea what they are?

view this post on Zulip Andrew Ashworth (Nov 23 2018 at 22:10):

Omega only handles presburger arithmetic, ie no multiplication.

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 22:11):

Hmm. I suspect by Groebner_basis might do it.

view this post on Zulip Andrew Ashworth (Nov 23 2018 at 22:11):

Cooper might do it, but I don't have lean in front of me to try it

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 22:11):

I have Lean in front of me -- how do I get cooper working?

view this post on Zulip Reid Barton (Nov 23 2018 at 22:13):

Maybe you can add https://github.com/skbaek/qe as a dependency now

view this post on Zulip Kenny Lau (Nov 23 2018 at 22:15):

example (m a b c j k : ) (Hj : a - b = m * j) (Hk : b - c = m * k) :
  a - c = m * (j + k) :=
by rw [mul_add,  Hj,  Hk, sub_add, sub_sub_self]

view this post on Zulip Reid Barton (Nov 23 2018 at 22:15):

(but I don't know how to actually use it)

view this post on Zulip Andrew Ashworth (Nov 23 2018 at 22:15):

I think the examples in https://github.com/skbaek/qe/blob/master/src/examples.lean are self explanatory

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 22:16):

definition cong_mod_37 (a b : ) :=  k : , 37 * k = a - b

example (a : ) : cong_mod_37 a a :=
begin
  use 0,
  simp,
end

example (a b : ) (H : cong_mod_37 a b) : cong_mod_37 b a :=
begin
  cases H with k Hk,
  use -k,
  simp [Hk],
end

example (a b c : ) (H1 : cong_mod_37 a b) (H2 : cong_mod_37 b c) : cong_mod_37 a c :=
begin
  cases H1 with j Hj,
  cases H2 with k Hk,
  use (j+k),
  simp [mul_add,Hj,Hk],
end

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 22:16):

@Kenny Lau I know how to do it, but the problem is that your proof is a great example of how to put first year undergraduates off Lean.

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 22:16):

Compare with my 37 proofs, where everything is just simp.

view this post on Zulip Patrick Massot (Nov 23 2018 at 22:30):

@Kevin Buzzard about example (m a b c j k : ℤ) (Hj : a - b = m * j) (Hk : b - c = m * k) : a - c = m * (j + k). For students I think a two-liner is good enough. The proof you would tell them is: "add equations Hj and Hk, then compute". Having a tactic add_eq Hk Hj is clearly within reach (actually we should both know how to do that by now). It would replace the first line in:

example (m a b c j k : ) (Hj : a - b = m * j) (Hk : b - c = m * k) :
a - c = m * (j + k) :=
begin
  have : (a - b) + (b - c) = (m * j) + (m * k) := congr (congr_arg int.add Hj) Hk,
  ring at *,
  assumption
end

view this post on Zulip Kenny Lau (Nov 23 2018 at 22:32):

... can someone teach me how to write tactics

view this post on Zulip Patrick Massot (Nov 23 2018 at 22:33):

Yes

view this post on Zulip Patrick Massot (Nov 23 2018 at 22:33):

Johannes, Mario, Simon, Rob, Scott...

view this post on Zulip Andrew Ashworth (Nov 23 2018 at 22:37):

The textbook everyone recommends is Handbook of Practical Logic and Automated Reasoning

view this post on Zulip Andrew Ashworth (Nov 23 2018 at 22:40):

Term rewriting and all that is good too, so is Modern Computer Algebra, depending on what you want your tactics to do

view this post on Zulip Patrick Massot (Nov 23 2018 at 22:53):

Andrew, our problem stops us before needing anything from these books. It's about Lean meta programming (especially parsing arguments in our case).

view this post on Zulip Patrick Massot (Nov 23 2018 at 22:55):

Our only immediate hope is @Simon Hudon will pity us, and we'll wake up with a add_eq tactic PR'ed to mathlib.

view this post on Zulip Simon Hudon (Nov 23 2018 at 22:56):

How can you be sure that he heard you?

view this post on Zulip Patrick Massot (Nov 23 2018 at 22:57):

That's the magic of Zulip's notification

view this post on Zulip Patrick Massot (Nov 23 2018 at 22:57):

And it's midnight here, so I'm allowed to dream

view this post on Zulip Simon Hudon (Nov 23 2018 at 22:57):

You sure are

view this post on Zulip Simon Hudon (Nov 23 2018 at 22:58):

What's the gist of this add_eq that you're looking for?

view this post on Zulip Patrick Massot (Nov 23 2018 at 22:59):

It replaces

example (m a b c j k : ) (Hj : a - b = m * j) (Hk : b - c = m * k) :
a - c = m * (j + k) :=
begin
  have : (a - b) + (b - c) = (m * j) + (m * k) := congr (congr_arg int.add Hj) Hk,
  ring at *,
  assumption
end

by

example (m a b c j k : ) (Hj : a - b = m * j) (Hk : b - c = m * k) :
a - c = m * (j + k) :=
begin
  add_eq Hj Hk,
  ring at *,
  assumption
end

view this post on Zulip Patrick Massot (Nov 23 2018 at 23:00):

It's similar in spirit to the mul_left tactic that we never finished writing

view this post on Zulip Simon Hudon (Nov 23 2018 at 23:01):

Wouldn't a lemma work just as well?

view this post on Zulip Patrick Massot (Nov 23 2018 at 23:05):

I don't understand how you can miss such opportunities to save the world with a new tactic

view this post on Zulip Patrick Massot (Nov 23 2018 at 23:05):

lemma add_eq {α : Type*} [has_add α] {b c d e : α} (H : b = c) (H' : d = e) :
  b + d = c + e := congr (congr_arg has_add.add H) H'

example (m a b c j k : ) (Hj : a - b = m * j) (Hk : b - c = m * k) :
a - c = m * (j + k) :=
begin
  have := add_eq Hj Hk,
  ring at *,
  assumption,
end

view this post on Zulip Simon Hudon (Nov 23 2018 at 23:06):

My favorite tactics are those I don't have to write :P

view this post on Zulip Simon Hudon (Nov 23 2018 at 23:07):

(btw, you type faster than I do, I was about to write that!)

view this post on Zulip Patrick Massot (Nov 23 2018 at 23:07):

I wonder whether this lemma is already in mathlib, the hypothesis has_add α is really weak

view this post on Zulip Reid Barton (Nov 23 2018 at 23:08):

Maybe a two-argument congr_arg₂ would be nice?

view this post on Zulip Patrick Massot (Nov 23 2018 at 23:08):

Yes, I also thought about that when writing the first version of the proof

view this post on Zulip Kenny Lau (Nov 23 2018 at 23:12):

Maybe a two-argument congr_arg₂ would be nice?

https://github.com/leanprover/mathlib/pull/118#discussion_r183841541

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

But for students I would still prefer to have the add_eq lemma and its friends that the abstract version

view this post on Zulip Patrick Massot (Nov 23 2018 at 23:15):

Same story as ever: an impressive proof from Kenny

theorem congr_arg₂ {α β γ : Type*} (f : α  β  γ) {x₁ x₂ : α} {y₁ y₂ : β}
  (Hx : x₁ = x₂) (Hy : y₁ = y₂) : f x₁ y₁ = f x₂ y₂ :=
eq.drec (eq.drec rfl Hy) Hx

lemma add_eq {α : Type*} [has_add α] {b c d e : α} (H : b = c) (H' : d = e) :
  b + d = c + e := congr_arg₂ has_add.add H H'

and then Mario wins:

lemma add_eq {α : Type*} [has_add α] {b c d e : α} (H : b = c) (H' : d = e) :
  b + d = c + e := by congr'

view this post on Zulip Patrick Massot (Nov 23 2018 at 23:17):

I still think all versions deserve to be in mathlib: congr_arg₂ and add_eq with its one-word proof

view this post on Zulip Patrick Massot (Nov 23 2018 at 23:17):

And now, I really go to sleep

view this post on Zulip Kenny Lau (Nov 24 2018 at 00:55):

man these 10 lines took me 1.5 hours to write:

import tactic.ring

namespace tactic.interactive
open lean.parser tactic interactive
meta def add_eq (h1 : parse ident) (h2 : parse ident)
  (h : parse (optional (tk "with" *> ident))) : tactic unit :=
do
e1  get_local h1, e2  get_local h2,
e  to_expr ```(_root_.congr (congr_arg has_add.add %%e1) %%e2),
tactic.note (h.get_or_else `this) none e
>> skip
end tactic.interactive

example (m a b c j k : ) (Hj : a - b = m * j) (Hk : b - c = m * k) :
  a - c = m * (j + k) :=
begin
  add_eq Hj Hk,
  ring at *,
  assumption
end

view this post on Zulip Kenny Lau (Nov 24 2018 at 00:55):

@Kevin Buzzard I wrote my first tactic just by browsing through core / mathlib

view this post on Zulip Kenny Lau (Nov 24 2018 at 00:57):

@Mario Carneiro are you going to replace my 5-line tactic with 1 line now?

view this post on Zulip Kenny Lau (Nov 24 2018 at 01:04):

golfed:

import tactic.ring

namespace tactic.interactive
open lean.parser tactic interactive
meta def add_eq (h1 : parse ident) (h2 : parse ident)
  (h : parse (optional (tk "with" *> ident))) : tactic unit :=
do e1  get_local h1, e2  get_local h2,
   «have» h none ```(_root_.congr (congr_arg has_add.add %%e1) %%e2)
end tactic.interactive

example (m a b c j k : ) (Hj : a - b = m * j) (Hk : b - c = m * k) :
  a - c = m * (j + k) :=
begin
  add_eq Hj Hk,
  ring at *,
  assumption
end

view this post on Zulip Scott Morrison (Nov 24 2018 at 01:20):

@Kenny Lau, why not reuse the lemma, and save yourself constructing the expression by hand:

import tactic.ring

lemma add_eq {α : Type*} [has_add α] {b c d e : α} (H : b = c) (H' : d = e) :
  b + d = c + e := by congr'

namespace tactic.interactive
open lean.parser tactic interactive
meta def add_eq (h1 : parse ident) (h2 : parse ident)
  (h : parse (optional (tk "with" *> ident))) : tactic unit :=
do e1 ← get_local h1,
   e2 ← get_local h2,
   «have» h none ```(add_eq %%e1 %%e2)
end tactic.interactive

example (m a b c j k : ℤ) (Hj : a - b = m * j) (Hk : b - c = m * k) :
  a - c = m * (j + k) :=
begin
  add_eq Hj Hk,
  ring at *,
  assumption
end

view this post on Zulip Kenny Lau (Nov 24 2018 at 01:21):

fair enough

view this post on Zulip Scott Morrison (Nov 24 2018 at 01:23):

Quotations are your friend, both for constructing expr instances and pattern matching on them.

view this post on Zulip Johan Commelin (Nov 24 2018 at 06:28):

Doesn't this mean that we should provide instance {A : Type*} [has_add A] : has_add (eq A)? And then prove that it is associative and commutative in the appropriate cases...

view this post on Zulip Johan Commelin (Nov 24 2018 at 06:29):

@Mario Carneiro Is it possible to do ring at * using [foo,bar]?

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 07:45):

This sounds unlikely as it sounds like you're asking Lean to figure out if an element of a ring is in the ideal generated by the inputs, which is surely well beyond the ring tactic

view this post on Zulip Mario Carneiro (Nov 24 2018 at 08:41):

Right. As you have identified this needs groebner bases, which could be a future generalization of ring but is a completely different algorithm

view this post on Zulip Mario Carneiro (Nov 24 2018 at 08:43):

@Kenny Lau , be careful golfing tactic code. Because we don't have the same assurances on correctness of meta code, it's much more like conventional programming, and it is important to be clear rather than compact, for maintainability

view this post on Zulip Rob Lewis (Nov 24 2018 at 10:01):

FYI, a student of ours who just started his BS thesis project is interested in Grobner basis algorithms. I'm not sure exactly which direction his project will go. Hopefully we'll get the core of an algorithm for this kind of thing, and then either he or we will turn it into a tactic.

view this post on Zulip Johan Commelin (Nov 24 2018 at 15:06):

Wouldn't it be faster (both development, and user experience) to piggyback on some other CAS? You already have the Mathematica interface. I guess a pari or sage interface would also be helpful. And we would get grobner basis tactics "for free"...

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 15:26):

Oh! It's just like the matrix inverse isn't it! You ask magma or whatever for a proof that the element is in the ideal, it supplies an explicit linear combination claiming to prove this but which hasn't been formally verified, and then you formally verify it in Lean with the ring tactic.

view this post on Zulip Rob Lewis (Nov 24 2018 at 15:28):

Sure, but there are upsides to implementing the algorithm natively too. Our student will learn how it works, of course. And it would be portable, so the tactic would be usable in mathlib without external dependencies. There's also theoretical interest in implementing the algorithm in non-meta Lean and proving it correct, even if it can't be efficiently executed in the kernel. And any tactic built on this should be modular enough to use an external oracle too.

view this post on Zulip Johan Commelin (Nov 24 2018 at 17:14):

By the way, I think my question about ring using [foo,bar] was misunderstood. I didn't want it to find relations on its own. I wanted to be able to type something like

ring using [add_eq H1 H2]

view this post on Zulip Johan Commelin (Nov 24 2018 at 17:15):

And using notation, that might be improved to ring using [H1 + H2]

view this post on Zulip Mario Carneiro (Nov 25 2018 at 00:07):

that seems more reasonable. You give some linear combination of hypotheses, like a * h1 + x^2 * h2, and it checks that goal - (a*h1 + x^2 * h2) is an equality of ring expressions


Last updated: May 11 2021 at 16:22 UTC