congr with associativity

Stream: general

[Martin Dvořák]

I'd like to have a tactic like congr but with associativity. Let's say ∘ is an associative operation (not commutative).

⊢  a ∘ (b ∘ (c ∘ d)) = (a ∘ x) ∘ (y ∘ d)

I'd like to call the tactic, then b ∘ c = x ∘ y would be the new goal.

[Heather Macbeth]

Maybe @Damiano Testa's tactic move_add #13483 would be relevant for this kind of task?

[Martin Dvořák]

[I specified the question.]

[Junyan Xu]

I wish tactic#slice could be extended to associative operations instead of only working in category theory ... in fact it's a TODO in comments file#tactic/slice

[Alex J. Best]

tactic#assoc_rw isn't what you want but is useful

import algebra.group.basic
.
lemma m {M : Type*} [monoid M] (a b c d x y : M) :
  a * (b * (c * d)) = (a * x) * (y * d) :=
begin
  assoc_rw (show b * c = x * y, from _),
  assoc_rw (show a * x * y * d = _, from rfl),
  sorry
end

also tactic#ac_refl, tactic#ac_change

[Martin Dvořák]

Since my project contains 155 explicit invocations of list.append_assoc I think I should automate it. The above-mentioned tactic does not exist. What will you recommend me to start with if I want to write it myself? I don't have experience with metaprogramming.

[Alex J. Best]

Which tactic doesn't exist?

[Martin Dvořák]

Martin Dvořák said:

I'd like to have a tactic like congr but with associativity. Let's say ∘ is an associative operation (not commutative).

⊢  a ∘ (b ∘ (c ∘ d)) = (a ∘ x) ∘ (y ∘ d)

I'd like to call the tactic, then b ∘ c = x ∘ y would be the new goal.

this

[Martin Dvořák]

[my workaround idea didn't work either]

[Scott Morrison]

A primitive implementation might just be:

• use the simplifier to left associate
• run congr
• use the simplifier to right associate
• run congr
  You should think pretty carefully about the specification of your tactic first before implementing it. (Mostly because for simple tactics the implementation follows directly from the spec.)

[Martin Dvořák]

Not exactly congr — it would attempt to match even the non-matching parts (before trying the other direction that might actually help to simplify the goal).

Nevertheless, you are right that I should first carefully specify what I want from my tactic.

[Eric Wieser]

What should it do on (a * b) * c = (a * c) * (b * d)?

[Eric Wieser]

This feels pretty underspecified to me

[Scott Morrison]

Surely b * c = c * b * d? It's only assuming associativity, no commutatively, right?

[Eric Wieser]

Why wouldn't it produce two goals, b = c * b and c = d?

[Scott Morrison]

Oh, I see. I was imagining only "splitting" on * if at least one side matches. I doubt "find minimal runs of non-matching elements" has a unique answer.

[Martin Dvořák]

Scott Morrison said:

A primitive implementation might just be:

• use the simplifier to left associate
• run congr
• use the simplifier to right associate
• run congr
  You should think pretty carefully about the specification of your tactic first before implementing it. (Mostly because for simple tactics the implementation follows directly from the spec.)

Let's say I only want to do the longest matching prefix and the longest matching suffix. Would there a similarly easy solution?

[Eric Wieser]

@Scott Morrison, that sounds like a clearer spec, but I don't think your suggested implementation implements it.

[Scott Morrison]

No, I agree. You'd replace congr with repeated application of lemmas like
b = c -> a * b = a * c.

[Eric Wieser]

What about a * b * x * b * a = a * b * a? Do you match the prefix or the suffix? I feel like most of this ambiguity is avoided by just having the user use ac_change in the first place to put things in whatever state they actually desire before using congr...

[Martin Dvořák]

How is ac_change that doesn't use commutativity?

[Eric Wieser]

I think ac_change only uses commutativity if it's available

[Eric Wieser]

But I could be wrong

[Martin Dvořák]

Here, the operation ++ is only associative. It doesn't do what it is supposed to do.

example (a b c d x y : list ℕ) : a ++ (b ++ (c ++ d)) = (a ++ x) ++ (y ++ d) :=
begin
  ac_change a ++ (b ++ c) ++ d = a ++ (x ++ y) ++ d;
  sorry
end

[Martin Dvořák]

This works:

example (a b c d : ℕ) : a + (b + (c + d)) = (a + b) + (c + d) :=
begin
  ac_refl,
end

This doesn't work:

example (a b c d : list ℕ) : a ++ (b ++ (c ++ d)) = (a ++ b) ++ (c ++ d) :=
begin
  ac_refl,
end

[Martin Dvořák]

Is there a tactic like ac_refl but for operations that are associative and not commutative?

[Alex J. Best]

I'm not sure if one exists already but here is one:

import tactic
.
open tactic

meta def tactic.interactive.assoc_refl : tactic unit :=
do (lhs, rhs) ← target >>= match_eq,
   assoc_refl lhs.app_fn.app_fn

example (a b c d : list ℕ) : a ++ (b ++ c) ++ d = (a ++ b) ++ (c ++ d) :=
begin
  assoc_refl,
end

[Patrick Massot]

Why not simply using simp only [list.append_assoc]?

[Patrick Massot]

It may look like cheating but the example of tactic#group shows this idea can already go quite a long way.

[Alex J. Best]

I think thats also a reasonable solution in this case, but to answer the question: some ways in which a specialized tactic can be better are if you want flexibility of the operation without needing to know the name of the appropriate lemma, and that the proofs produced are way shorter and more reasonable looking. But for most applications using simp is probably way more convenient.

[Martin Dvořák]

Patrick Massot said:

Why not simply using simp only [list.append_assoc]?

I conclude that, in a similar manner how ac_change does convert_to r n; try ac_refl, I should implement la_change as convert_to r n; try simp only [list.append_assoc] ok?
It will not fully automate what I wanted to do (as with la_change I have to create the new form of the goal in my head and write it down), but it will get me to a form which congr can then simplify really usefully.
Any other suggestion?

[Martin Dvořák]

What does (n : parse (tk "using" *> small_nat)?) mean?
https://github.com/leanprover-community/mathlib/blob/0c171f291c5e590f368974dc3a293c7b50de44a4/src/tactic/congr.lean#L228

[Floris van Doorn]

That a tactic takes an optional argument using n and n will be parsed as a natural number.

[Martin Dvořák]

I am confused. Example

example (a b c d x y : list ℕ) : a ++ (b ++ (c ++ d)) = (a ++ x) ++ (y ++ d) :=
begin
  convert_to a ++ (b ++ c) ++ d = a ++ (x ++ y) ++ d,
  { simp only [list.append_assoc] },
  { simp only [list.append_assoc] },
  -- I am talking about the goal remaining here.
  sorry,
end

leads to the goal a ++ (b ++ c) ++ d = a ++ (x ++ y) ++ d as I intended. However

example (a b c d x y : list ℕ) : a ++ (b ++ (c ++ d)) = (a ++ x) ++ (y ++ d) :=
begin
  convert_to a ++ (b ++ c) ++ d = a ++ (x ++ y) ++ d;
  try { simp only [list.append_assoc] },
  -- I am talking about the goal remaining here.
  sorry,
end

leaves me with a ++ (b ++ (c ++ d)) = a ++ (x ++ (y ++ d)) which I didn't ask for. Why?

[Damiano Testa]

@Martin Dvořák are you still stumped by this?

Note that try {...} means "try this block and do it, unless you get an error". It does not mean "try this block and do it only if you close the goal". The latter could probably be implemented as

  try { { tactics } }

note the second layer of curly braces: this acts as focus. The block will be executed only if it closes the goal. You could also use

  try { tactics, done }

to achieve the same effect.

[Martin Dvořák]

Damiano Testa said:

Martin Dvořák are you still stumped by this?

I gave up on implementing a tactic. I continue to prove stuff "manually". Nevertheless, your reply is useful!

[Damiano Testa]

If you change your mind and want some help with the tactic, let me know: I'd be happy to help and I think that I did something similar already.

As has been commented before, the main obstacle that I view is figuring out which exact cases you want the tactic to solve:

• you may want to use the initial parentheses as a guide to match LHS with RHS,
• you may want to first remove all parentheses and then do the matching,
• you may want to have a heuristic that tries the longest actual match from the beginning, before splitting out side-goals,
• ...

All these are easy to implement, it is just a matter of deciding which would be the most useful.

[Martin Dvořák]

I think I want to ignore the parentheses, match the longest prefix, then match the longest suffix of the remaining equality, and produce a single goal for what remained.

In the example a * b * x * b * a = a * b * a by Eric Wieser, I want the tactic to output a goal that x * b is the neutral element.

[Eric Wieser]

This tactic isn't congr at all if you want it to manufacture a 1 term

[Martin Dvořák]

For me, it makes sense as a special case of the tactic I described. Would you specify it otherwise?

[Damiano Testa]

Ok, it was fairly close to code that I already had. Below is something that works with a couple of examples. Let me know if it also works on your use cases! Some of the functions are a little hacky, so they may misbehave.

import algebra.group.defs

namespace list
/--  Let `l r` be two lists.  `in_match l r` is the longest, left-most consecutive
sublist of `l r`.  For example:
```lean
#eval in_match [1, 2, 3, 4] [1, 2, 4]  -- [1, 2]
```
-/
def in_match {α : Type*} [decidable_eq α] : list α → list α → list α
| [] _ := []
| _ [] := []
| (a::as) (b::bs) := if a = b then (a :: in_match as bs) else []

/--  Let `l r` be two lists.  `split3 l r` is the ordered triple
`(initial, (mid_l, mid_r), final)`, where
`l = initial ++ mid_l ++ final, r = initial ++ mid_r ++ final`, with
* `initial` chosen greedily (via `in_match`);
* `final` chosen next and again greedily (via `in_match`, but starting from the end of the lists);
* `mid_l, mid_r` chosen to be what is left-over.
For example:
```lean
#eval split3 [0, 1, 2, 8, 6, 3, 7] [0, 1, 2, 4, 5, 6, 3, 7]
-- ([0, 1, 2], (([8], [4, 5]), [6, 3, 7]))

#eval split3 [0, 1, 2, 6, 3, 7] [0, 1, 2, 4, 5, 6, 3, 7]
-- ([0, 1, 2], (([], [4, 5]), [6, 3, 7]))
```
-/
def split3 {α : Type*} [decidable_eq α] (l r : list α) : list α × (list α × list α) × list α :=
let ini         := in_match l r in
let lx_tail     := l.drop ini.length in
let rx_tail     := r.drop ini.length in
let lx_tail_rev := lx_tail.reverse in
let rx_tail_rev := rx_tail.reverse in
let fin         := (in_match lx_tail_rev rx_tail_rev).reverse in
  (ini,
    ((lx_tail_rev.drop fin.length).reverse,
     (rx_tail_rev.drop fin.length).reverse),
    fin)

/--  `sum_up_with_default e op l` folds the operation `op` over the list `l`, using the given
element `e` as output in the case of an empty list. -/
meta def sum_up_with_default {α : Type*} (e : α) (op : α → α → α) : list α → α
| []      := e
| [a]     := a
| (a::as) := as.foldl (λ x y, op x y) a

end list

namespace tactic

namespace fla

/--  Similar to `sum_up_with_default e op l` except it does not take the default element `e`,
but fails in the case of an empty list. -/
meta def sum_up {α : Type*} (op : α → α → α) : list α → tactic α
| []      := fail "no initial match -- could use a unit here"
| (a::as) := pure $ (a::as).sum_up_with_default a op

/--  `assoc_unit oper typ` is a hacky way of extracting a unit for the (binary) operation `oper`
on the type `typ`. -/
meta def assoc_unit (oper typ : expr) : tactic expr := do
some las ← pure $ oper.get_app_args.last',
et ← infer_type las,
match oper.get_app_fn.const_name with
  | `has_append.append := to_expr ``([] : %%typ) tt ff
  | `has_mul.mul       := to_expr ``(1 : %%typ) tt ff
  | `has_add.add       := to_expr ``(0 : %%typ) tt ff
  | _ := fail"the tactic does not support this operation"
  end

/--  `assoc_tac oper` is a hacky way of extracting a tactic for associating and eliminating
empty lists, multiplications by `1` or additions by `0` under the (binary) operation `oper`. -/
meta def assoc_tac (oper : expr) : tactic unit :=
match oper.get_app_fn.const_name with
  | `has_append.append := `[ simp only [list.append_assoc, list.nil_append], done ]
  | `has_mul.mul       := `[ simp only [mul_assoc, mul_one], done ]
  | `has_add.add       := `[ simp only [add_assoc, add_zero], done ]
  | _ := fail"the tactic does not support this operation"
  end

end fla

namespace interactive
open fla

/--  `fla` tries to extract side-goals for the "central part" of an equality between two
iterated applications of a binary associative operation. -/
meta def fla : tactic unit := do
`(%%lhs = %%rhs) ← target >>= instantiate_mvars <|> fail"goal is not an equality",
et ← infer_type lhs,
oper ← match lhs with
  | (expr.app (expr.app f _) _) := pure f
  | _ := fail "no operation found"
  end,
opl ← list_binary_operands oper lhs,
opr ← list_binary_operands oper rhs,
let (ini, (ldiff, rdiff), fin) := opl.split3 opr,
sini   ← sum_up (λ x y, oper.mk_app [x, y]) ini,
smidl  ← sum_up (λ x y, oper.mk_app [x, y]) ldiff,
smidr  ← sum_up (λ x y, oper.mk_app [x, y]) rdiff,
sfin   ← sum_up (λ x y, oper.mk_app [x, y]) fin,
nleft  ← sum_up (λ x y, oper.mk_app [x, y]) [sini, smidl, sfin],
nright ← sum_up (λ x y, oper.mk_app [x, y]) [sini, smidr, sfin],
l_eq ← mk_app `eq [lhs, nleft],
r_eq ← mk_app `eq [nright, rhs],
(_, pr_left)  ← solve_aux l_eq (assoc_tac oper),
(_, pr_right) ← solve_aux r_eq (assoc_tac oper),
refine ``(eq.trans %%pr_left (eq.trans _ %%pr_right)),
congr

/--  `fla_with_unit` is similar to `fla` except that it also tries to extract a unit for the
operation and uses it to handle cases where the expressions to match leave some empty sublist. -/
meta def fla_with_unit : tactic unit := do
`(%%lhs = %%rhs) ← target >>= instantiate_mvars,
et ← infer_type lhs,
oper ← match lhs with
  | (expr.app (expr.app f _) _) := pure f
  | _ := fail "no operation found"
  end,
un ← assoc_unit oper et,
opl ← list_binary_operands oper lhs,
opr ← list_binary_operands oper rhs,
let (ini, (ldiff, rdiff), fin) :=  opl.split3 opr,
let sini   :=  ini.sum_up_with_default un (λ x y, oper.mk_app [x, y]),
let smidl  :=  ldiff.sum_up_with_default un (λ x y, oper.mk_app [x, y]),
let smidr  :=  rdiff.sum_up_with_default un (λ x y, oper.mk_app [x, y]),
let sfin   :=  fin.sum_up_with_default un (λ x y, oper.mk_app [x, y]),
let nleft  :=  [sini, smidl, sfin].sum_up_with_default un (λ x y, oper.mk_app [x, y]),
let nright :=  [sini, smidr, sfin].sum_up_with_default un (λ x y, oper.mk_app [x, y]),
l_eq ← mk_app `eq [lhs, nleft],
r_eq ← mk_app `eq [nright, rhs],
(_, pr_left)  ← solve_aux l_eq (assoc_tac oper),
(_, pr_right) ← solve_aux r_eq (assoc_tac oper),
refine ``(eq.trans %%pr_left (eq.trans _ %%pr_right)),
congr

end interactive

end tactic

example (a b c d e f : list ℕ) (hp : e ++ f ++ e = f) :
  a ++ (b ++ c) ++ e ++ f ++ e ++ d = (a ++ b) ++ (c ++ f ++ d) :=
begin
  fla,
  assumption,
end

example {R : Type*} [semigroup R] (a b c d e f : R) (hp : e * f * e = f) :
  a * (b * c) * e * f * e * d = (a * b) * (c * f * d) :=
begin
  fla,
  assumption,
end

example {R : Type*} [add_semigroup R] (a b c d e f : R) (hp : e + f + e = f) :
  a + (b + c) + e + f + e + d = (a + b) + (c + f + d) :=
begin
  fla,
  assumption,
end

example {α : Type*} (a b c d e f : list α) (hp : e = []) :
  a ++ (b ++ c) ++ e ++ f ++ d = (a ++ b) ++ (c ++ f ++ d) :=
begin
  fla_with_unit,
  assumption,
end

example {R : Type*} [monoid R] (a b c d e f : R) (hp : e = 1) :
  a * (b * c) * e * f * d = (a * b) * (c * f * d) :=
begin
  fla_with_unit,
  assumption,
end

example {R : Type*} [add_monoid R] (a b c d e f : R) (hp : e = 0) :
  a + (b + c) + e + f + d = (a + b) + (c + f + d) :=
begin
  fla_with_unit,
  assumption,
end

[Damiano Testa]

I produced two tactics:

• fla applies associativity with your specifications, but fails if one of the 3 parts in which the expressions get split is empty;
• fla_with_unit works like fla, except that it tries to make a guess as to what the unit of the operation should be and hopes for the best!

[Martin Dvořák]

Wow! Thanks a lot!!! Imma test it today.

[Damiano Testa]

Great! If the tactic fails on some goals, please post the failure here and I will try to debug!

[Martin Dvořák]

It works great in many situations! However, it fails here.

example {B C : R} : a ++ [B] ++ [C] ++ d = a ++ [B, C] ++ d :=
begin
  fla,
end

[Damiano Testa]

What happens with this case is that the penultimate congr' already solves the goal. If you replace the last line of fla with

try $ tactic.congr' (some 1)

(i.e. simply adding try $ at the beginning) fixes this issue.

[Martin Dvořák]

Amazing!!! Thank you!!!

[Martin Dvořák]

It was confusing because when I wrote

example {B C : R} : a ++ [B] ++ [C] ++ d ++ e = a ++ [B, C] ++ d ++ f :=
begin
  fla,
end

it didn't match [B] ++ [C] with [B, C]. Hence I didn't expect fla to close the goal too early in the previous example.

[Damiano Testa]

Oh, that is probably because the 3-way split of the expressions is different: in the latter example, the expression have no common "tail", so everything is "beginning" or "middle". The earlier example that you posted has a common "tail". I think that this allows congr (that uses more defeqs and subsingleton) to be smarter and therefore close the goal too early!

[Martin Dvořák]

Is it possible to add fla to the list of tactics that hint tries inside my project?

[Damiano Testa]

Note that I think that currently [B] ++ [C] and [B, C] are not considered a match by the first part of the tactic, but likely they are unified by congr.

[Damiano Testa]

Martin Dvořák said:

Is it possible to add fla to the list of tactics that hint tries inside my project?

I think yes, though I need to look up what command is the right one to get it on hints radar.

[Damiano Testa]

Maybe it is a simple as adding @[hint_tactic] before meta def fla?

[Damiano Testa]

this works, but suggests the full name tactic.interactive.fla. I'll see if you can get fla only.

[Martin Dvořák]

Don't worry about that.

[Damiano Testa]

Yes, instead of the attribute at the beginning, simply put add_hint_tactic "fla" after the definition.

[Damiano Testa]

(I updated the tactic above with the try and the hint.)

[Damiano Testa]

Debugging and feature requests are fun: feel free to come up with more complicated examples and post them here!

[Martin Dvořák]

BTW why is fla the name? Is it short for something?

[Damiano Testa]

Oh, I think it was "Force Left Associative"

[Damiano Testa]

Feel free to suggest a different name!

[Martin Dvořák]

I will add it to my project. How do you want credits to be written?

[Damiano Testa]

I do not particularly mind: if it is its own separate file, you could add a "copyright" header like the one for mathlib.

In any case, most of the code here is stolen from similar code somewhere else already!

[Martin Dvořák]

Do you have any idea who else should get copyright, apart from you?

[Damiano Testa]

Not really, since I got a lot of this code from what I had been doing with move_add and that in turn was through the help of Arthur Paulino, Eric Wieser, Rob Lewis and whoever wrote the tactics that I browsed.

I have a feeling that in this community (and certainly for myself) there is not such a big emphasis on personal copyright, as much as "contributing to the whole".

[Martin Dvořák]

I'm not adding it to mathlib but to my own project. Therefore, I don't know how much "contributing to the whole" is a valid concept here. So I want to give you a proper copyright.

[Damiano Testa]

Ok, so let's ping @Arthur Paulino , @Eric Wieser and @Rob Lewis and see if any of them wants to have some specific recognition for the code above. I am certainly mostly indebted to the three of them for whatever knowledge of tactic-writing that I have.

[Arthur Paulino]

I don't mind copyrights. No need to mention me :+1:

[Martin Dvořák]

Damiano Testa said:

Feel free to suggest a different name!

Would you mind if I simply call it associativity?

[Damiano Testa]

No, I do not mind what the name ends up being. associativity might be a little long, but since you might be the only user of this tactic, it is entirely up to you! :smile: