Missing maths tactic?

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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.

[Kevin Buzzard]

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]

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]

Omega only handles presburger arithmetic, ie no multiplication.

[Kevin Buzzard]

Hmm. I suspect by Groebner_basis might do it.

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Kenny Lau]

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]

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

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

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

[Patrick Massot]

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

... can someone teach me how to write tactics

[Patrick Massot]

Yes

[Patrick Massot]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Patrick Massot]

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]

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]

How can you be sure that he heard you?

[Patrick Massot]

That's the magic of Zulip's notification

[Patrick Massot]

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

[Simon Hudon]

You sure are

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Simon Hudon]

Wouldn't a lemma work just as well?

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Simon Hudon]

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

[Patrick Massot]

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

[Reid Barton]

Maybe a two-argument congr_arg₂ would be nice?

[Patrick Massot]

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

[Kenny Lau]

Maybe a two-argument congr_arg₂ would be nice?

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

And now, I really go to sleep

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Scott Morrison]

@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

[Kenny Lau]

fair enough

[Scott Morrison]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

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]

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

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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