# Zulip Chat Archive

## 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 [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 (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), simp [mul_add,Hj,Hk], 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

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

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

#### Simon Hudon (Nov 23 2018 at 22:57):

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

#### Kenny Lau (Nov 24 2018 at 01:21):

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