## Stream: new members

### Topic: move_oper HAnd.hAnd?

#### Markus Schmaus (Nov 23 2023 at 15:41):

I just discovered docs#MoveAdd, and the documentation claims that move_oper supports and. However I can't make it work:

import Mathlib

example (a b c : Prop) : a ∧ b ∧ c = c ∧ b ∧ a := by
move_oper HAnd.hAnd [a, b, c]
rfl


BesidesHAnd.hAnd I also tried And.and, And.intro, and, and maybe one or two more, but nothing works. Is it possible to make this tactic work?

#### Damiano Testa (Nov 23 2023 at 15:42):

Does putting round brackets around the name work?

#### Damiano Testa (Nov 23 2023 at 15:43):

I'm on mobile, so I won't be able to help until tomorrow, but it should work.

#### Damiano Testa (Nov 23 2023 at 15:44):

Actually, this line

Suggests that it should "just work"...

#### Alex J. Best (Nov 23 2023 at 15:45):

example (a b c : Prop) : a ∧ (b ∧ c = c ∧ b ∧ a) := by


this is one of the reasons why its good to use iff for props

example (a b c : Prop) : a ∧ b ∧ c ↔ c ∧ b ∧ a := by


#### Alex J. Best (Nov 23 2023 at 15:46):

Turning off notation we can see that the and symbol actually means And not HAnd.hand, and indeed

import Mathlib

set_option pp.notation false -- toggle this to see
example (a b c : Prop) : a ∧ b ∧ c ↔ c ∧ b ∧ a := by
move_oper And [a, b, c]
rfl


works

#### Damiano Testa (Nov 23 2023 at 15:58):

I'm glad that this works, since it might be the first "real world" use of move_oper that isn't about addition or multiplication!

#### Damiano Testa (Nov 23 2023 at 16:11):

Also, once I'm back at a computer, I'll update the docs to specify exactly what to type to get move_oper working: right now, it mentions HAdd.hAdd twice, uses and instead of And and I'm not sure if the min/max are correct either.

#### Markus Schmaus (Nov 23 2023 at 16:35):

One curious note: move_oper And arranges the terms left-associative, which makes sense for +, while the standard for ∧ is right-associative. I will look into move_oper And and see how helpful it is with the kind of proofs, I'm currently encountering.

#### Damiano Testa (Nov 23 2023 at 18:39):

move_oper was really written thinking of moving additions. Since immediately there were questions about multiplication, I decided to do it operation-agnostic. Once I had it agnostic, I thought of adding support for more operations that are associative and commutative. Thus, and was really an after-thought. An early version supported inf and sup, but since it required a new import, I removed it.

#### Damiano Testa (Nov 23 2023 at 18:39):

Anyway, making and associate differently is probably a tiny change.

#### Markus Schmaus (Nov 23 2023 at 22:09):

What I'm really interested in is moving ∃ and statements of the form a' = a, such that docs#exists_eq_left can be used, move_oper And is a start. Now that I know it works, I will have a look at the code and see if I can figure out how it works and if I can adapt it.

#### Damiano Testa (Nov 23 2023 at 22:21):

I don't remember how much move_oper enters into binders. My recollection is "not much", especially since I do not think that you can name explicitly the bound variables: they may only be accessible via metavariables and relations among them.

#### Damiano Testa (Nov 23 2023 at 22:22):

If you have a specific example where move_oper might work, but does not, please post it and I will see what can be done about it.

#### Damiano Testa (Nov 24 2023 at 06:26):

#8606 corrects the doc-strings and adds tests to show how to use move_oper for operations other than + and *.

#### Damiano Testa (Nov 24 2023 at 06:28):

I'll take a look at associating and/or differently, though this is a change that affects the actual internals.

#### Damiano Testa (Nov 24 2023 at 07:54):

#8607 adds support for left-associative operations. In the PR, it is only turned on for And/Or.

Last updated: Dec 20 2023 at 11:08 UTC