`conv {to_rhs, ...}` behaves poorly with `nat.modeq`.

[kim-em]

Mario helped me write a proof:

lemma foo (n k : ℕ) : k ≡ ((k / 2^n) + (k % 2^n)) [MOD 2^n - 1] :=
-- See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/help.20finding.20a.20lemma/near/177698446
begin
  conv {to_rhs, rw [← nat.mod_add_div k (2^n), add_comm]},
  refine nat.modeq.modeq_add _ (by refl),
  conv {to_rhs, skip, rw ← one_mul (k/2^n)},
  refine nat.modeq.modeq_mul _ (by refl),
  symmetry,
  rw [nat.modeq.modeq_iff_dvd, int.coe_nat_sub],
  exact nat.pow_pos dec_trivial _
end

in which both instances of to_rhs are a bit strange. The first one actually looks at the left-hand-side, while the second one requires a skip before actually reaching the right-hand-side.

[digama0]

I think that to_lhs and to_rhs are a bit poorly conceived. They make sense only for binary operators, and modeq is a ternary operator (the first argument is the modulus), so it's not even clear how to use them correctly. I would prefer something like to_nth 2 to go into the 2nd argument of an application, where the generalization to n-ary operators is clear.

That said, this isn't really a mathlib problem, so I'll close this. You should move this issue to leanprover_community/lean, since that's where conv and to_rhs are implemented.

[kim-em]

Oops, sorry, I thought to_lhs and to_rhs were tacked on in mathlib. Thanks.

[khoek]

Presumably the idea in the implementation is that is_relation should fail when you pass it a ternary (n>2-ary) function?

[jcommelin]

We could still write to_nth in mathlib, couldn't we? So maybe it is partly a mathlib issue as well.

[bryangingechen]

moved per Mario's suggestion.

[digama0]

I am not 100% sure, but at least in this case, we want to_lhs to pick the penultimate argument, and to_rhs the last argument of an application. This applies even to traditional functions like has_add.add because the first two arguments are the type and typeclass.

As for to_nth, we still don't want to_nth 1 to pick the type argument, and in any case that's not going to happen since conv uses congruence lemmas and those only enter an application in its nondependent arguments. I should check how to_lhs is currently implemented, but one easy option is to apply the congruence lemma, resulting in n subgoals, and to_nth k should close all of them with refl except for the k-th. (We should probably also have a conv tactic that closes none of these subgoals and just produces a subgoal for each argument. Perhaps to_args?)

[jcommelin]

Isn't congr doing what you suggest for to_args?

[digama0]

Is there a congr conv tactic? The regular conv doesn't have quite the same behavior, because it only applies when the goal is f x y = f x' y', while here we want it to reduce f x y = ?m1 to x = ?m2 and y = ?m3.

[bryangingechen]

There's conv.interactive.apply_congr as of a few days ago.