`revert` does not respect the argument order

eric-wieser commented 7 months ago

[x] Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

The revert tactic ignores the order of its arguments

[Broader context that the issue occured in. If there was any prior discussion on the Lean Zulip, link it here as well.]

example (a b c : Nat) : a * b * c = 1 := by
  revert c a b
  sorry

Expected behavior: Goal is ∀ (c a b : Nat), a * b * c = 1 like it was in Lean 3

Actual behavior: Goal is ∀ (a b c : Nat), a * b * c = 1, ignoring the argument order

4.4.0-rc1

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

eric-wieser commented 7 months ago

It looks like this is trivially fixed by adding (preserveOrder := true) to:

Is the choice to not preserve order deliberate?

semorrison commented 7 months ago

I suspect this is just an oversight. Could you make the PR?

leanprover / lean4