move_oper HAnd.hAnd?

Stream: new members

[Markus Schmaus]

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]

Does putting round brackets around the name work?

[Damiano Testa]

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

[Damiano Testa]

Actually, this line

https://github.com/leanprover-community/mathlib4/blob/master/test/MoveAdd.lean#L64

Suggests that it should "just work"...

[Alex J. Best]

Your goal is parsing as

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]

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]

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]

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]

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]

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]

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

[Markus Schmaus]

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]

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]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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