Zulip Chat Archive

Stream: general

Topic: congr with associativity


Martin Dvořák (Oct 10 2022 at 17:47):

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 (Oct 10 2022 at 17:54):

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

Martin Dvořák (Oct 10 2022 at 17:57):

[I specified the question.]

Junyan Xu (Oct 10 2022 at 18:05):

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 (Oct 10 2022 at 18:15):

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 (Oct 11 2022 at 07:43):

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 (Oct 11 2022 at 08:50):

Which tactic doesn't exist?

Martin Dvořák (Oct 11 2022 at 09:23):

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 (Oct 11 2022 at 09:25):

[my workaround idea didn't work either]

Scott Morrison (Oct 11 2022 at 09:48):

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 (Oct 11 2022 at 10:16):

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 (Oct 11 2022 at 18:01):

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

Eric Wieser (Oct 11 2022 at 18:02):

This feels pretty underspecified to me

Scott Morrison (Oct 11 2022 at 23:52):

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

Eric Wieser (Oct 12 2022 at 02:57):

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

Scott Morrison (Oct 12 2022 at 03:00):

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 (Oct 12 2022 at 06:20):

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 (Oct 12 2022 at 13:32):

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

Scott Morrison (Oct 12 2022 at 21:25):

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

Eric Wieser (Oct 13 2022 at 08:08):

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 (Oct 13 2022 at 09:57):

How is ac_change that doesn't use commutativity?

Eric Wieser (Oct 13 2022 at 11:42):

I think ac_change only uses commutativity if it's available

Eric Wieser (Oct 13 2022 at 11:42):

But I could be wrong

Martin Dvořák (Oct 13 2022 at 12:22):

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 (Oct 13 2022 at 13:09):

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 (Oct 13 2022 at 13:12):

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

Alex J. Best (Oct 13 2022 at 14:22):

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 (Oct 13 2022 at 14:26):

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

Patrick Massot (Oct 13 2022 at 14:30):

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

Alex J. Best (Oct 13 2022 at 14:31):

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 (Oct 13 2022 at 22:19):

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 (Oct 17 2022 at 07:57):

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 (Oct 17 2022 at 08:03):

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

Martin Dvořák (Oct 17 2022 at 08:38):

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 (Oct 25 2022 at 15:07):

@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 (Oct 26 2022 at 08:58):

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 (Oct 26 2022 at 09:37):

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 (Oct 26 2022 at 10:44):

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 (Oct 26 2022 at 12:14):

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

Martin Dvořák (Oct 26 2022 at 12:23):

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

Damiano Testa (Oct 26 2022 at 16:08):

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 (Oct 26 2022 at 16:11):

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 (Oct 27 2022 at 05:55):

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

Damiano Testa (Oct 27 2022 at 06:00):

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

Martin Dvořák (Oct 27 2022 at 09:25):

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 (Oct 27 2022 at 10:06):

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 (Oct 27 2022 at 10:09):

Amazing!!! Thank you!!!

Martin Dvořák (Oct 27 2022 at 10:11):

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 (Oct 27 2022 at 10:13):

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 (Oct 27 2022 at 10:14):

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

Damiano Testa (Oct 27 2022 at 10:14):

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 (Oct 27 2022 at 10:14):

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 (Oct 27 2022 at 10:16):

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

Damiano Testa (Oct 27 2022 at 10:17):

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

Martin Dvořák (Oct 27 2022 at 10:17):

Don't worry about that.

Damiano Testa (Oct 27 2022 at 10:18):

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

Damiano Testa (Oct 27 2022 at 10:22):

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

Damiano Testa (Oct 27 2022 at 10:24):

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

Martin Dvořák (Oct 27 2022 at 10:34):

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

Damiano Testa (Oct 27 2022 at 10:38):

Oh, I think it was "Force Left Associative"

Damiano Testa (Oct 27 2022 at 10:38):

Feel free to suggest a different name!

Martin Dvořák (Oct 27 2022 at 10:38):

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

Damiano Testa (Oct 27 2022 at 10:40):

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 (Oct 27 2022 at 10:41):

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

Damiano Testa (Oct 27 2022 at 10:46):

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 (Oct 27 2022 at 10:48):

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 (Oct 27 2022 at 10:49):

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 (Oct 27 2022 at 10:54):

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

Martin Dvořák (Oct 27 2022 at 12:23):

Damiano Testa said:

Feel free to suggest a different name!

Would you mind if I simply call it associativity?

Damiano Testa (Oct 27 2022 at 13:05):

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:


Last updated: Dec 20 2023 at 11:08 UTC