feature request: conv perm

Stream: general

[Johan Commelin]

How hard is it to write a tactic that works like this:

-- goal is ⇑v ↑(x.snd) * ⇑v (y.fst) * ((⇑v ((y.snd).val))⁻¹ * (⇑v ((x.snd).val))⁻¹) ≤⇑v (y.fst) * (⇑v ((y.snd).val))⁻¹
conv { to_lhs,
-- goal is ⇑v ↑(x.snd) * ⇑v (y.fst) * ((⇑v ((y.snd).val))⁻¹ * (⇑v ((x.snd).val))⁻¹)
  perm "(1 * 4) * (2 * 3)",
-- goal is (⇑v ↑(x.snd) * (⇑v ((x.snd).val))⁻¹)) * (⇑v (y.fst) * (⇑v ((y.snd).val))⁻¹)
},
-- goal is (⇑v ↑(x.snd) * (⇑v ((x.snd).val))⁻¹)) * (⇑v (y.fst) * (⇑v ((y.snd).val))⁻¹) ≤⇑v (y.fst) * (⇑v ((y.snd).val))⁻¹
apply mul_le_mul_left,
-- etc

[Johan Commelin]

Some sort of permutation tactic would be very helpful, I feel.

[Johan Commelin]

The problem with rw show what_I_have = what_I_want is that you run into type class issues with writing that down. In the rw show doesn't have all the typing context that the perm tactic would have.

[Mario Carneiro]

I think the given syntax is underdetermined, if you say there's only three things what if there are multiple ways to split it up into three parts? Also I think we can do without the quotes

[Johan Commelin]

I haven't thought hard about the syntax...

[Mario Carneiro]

what about something more like perm a * b * (c * d) => (a * d) * (b * c)?

[Mario Carneiro]

where the thing on the left is a pattern that binds the names on the right

[Johan Commelin]

It would be more verbose, but I why it's needed

[Mario Carneiro]

we could do it your way but I'm worried about lack of transparency. Indexes are generally bad at explaining what is being referred to

[Mario Carneiro]

Also there are more complicated examples like perm a * b + c * d => d * c + a * b where it's less obvious what the atoms of the permutation are

[Johan Commelin]

Yes, so yours is better!

[Johan Commelin]

How hard is it to actually write such a tactic?

[Mario Carneiro]

good question. Would it match subterms or just the whole target?

[Johan Commelin]

Hmmm, matching subterms is probably better in the long run, right?

[Johan Commelin]

It would also avoid the conv part.

[Mario Carneiro]

it will be easier to use but possibly also harder to control, like rw

[Johan Commelin]

I see. But maybe we can use _s to guide Lean to the right subterm?

[Mario Carneiro]

That goes into my plans for more elaborate conv patterns

[Mario Carneiro]

Stuff like conv x in (foo (x + _)) to focus on the first summand of the argument to foo

[Mario Carneiro]

assuming foo ... is a subterm of the goal

[Johan Commelin]

If conv becomes more powerful, that'd be great! And then there is no problem with perm matching on the whole goal.

[Johan Commelin]

Seperation of concerns, I guess?