Stream: maths

Topic: Missing maths tactic?

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]

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.

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

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 [←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.

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.

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?

Andrew Ashworth (Nov 23 2018 at 22:10):

Omega only handles presburger arithmetic, ie no multiplication.

Kevin Buzzard (Nov 23 2018 at 22:11):

Hmm. I suspect by Groebner_basis might do it.

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

Kevin Buzzard (Nov 23 2018 at 22:11):

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

Reid Barton (Nov 23 2018 at 22:13):

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

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]


Reid Barton (Nov 23 2018 at 22:15):

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

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

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),
end


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.

Kevin Buzzard (Nov 23 2018 at 22:16):

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

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


Kenny Lau (Nov 23 2018 at 22:32):

... can someone teach me how to write tactics

Yes

Patrick Massot (Nov 23 2018 at 22:33):

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

Andrew Ashworth (Nov 23 2018 at 22:37):

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

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

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

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.

Simon Hudon (Nov 23 2018 at 22:56):

How can you be sure that he heard you?

Patrick Massot (Nov 23 2018 at 22:57):

That's the magic of Zulip's notification

Patrick Massot (Nov 23 2018 at 22:57):

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

You sure are

Simon Hudon (Nov 23 2018 at 22:58):

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

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
ring at *,
assumption
end


Patrick Massot (Nov 23 2018 at 23:00):

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

Simon Hudon (Nov 23 2018 at 23:01):

Wouldn't a lemma work just as well?

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

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


Simon Hudon (Nov 23 2018 at 23:06):

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

Simon Hudon (Nov 23 2018 at 23:07):

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

Patrick Massot (Nov 23 2018 at 23:07):

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

Reid Barton (Nov 23 2018 at 23:08):

Maybe a two-argument congr_arg₂ would be nice?

Patrick Massot (Nov 23 2018 at 23:08):

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

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

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

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'


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

Patrick Massot (Nov 23 2018 at 23:17):

And now, I really go to sleep

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
ring at *,
assumption
end


Kenny Lau (Nov 24 2018 at 00:55):

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

Kenny Lau (Nov 24 2018 at 00:57):

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

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
ring at *,
assumption
end


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
ring at *,
assumption
end


fair enough

Scott Morrison (Nov 24 2018 at 01:23):

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

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

Johan Commelin (Nov 24 2018 at 06:29):

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

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

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

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

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.

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"...

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.

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.

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]


Johan Commelin (Nov 24 2018 at 17:15):

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

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