Rewrite issue

Stream: lean4

[François G. Dorais]

I haven't had the chance to investigate this issue but there must be a bug somewhere...

In this snippet, the rewrite succeeds but does not change the goal at all.

example (m n : Nat) : Nat.ble (n+1) (n+0) = false := by rw [Nat.add_zero]; admit

In this snppet, the rewrite succeeds and does change the goal to Nat.ble (n+1) n as I would expect.

example (m n : Nat) : Nat.ble (n+1) (n+0) = false := by rw [Nat.add_zero n]; admit

[Mario Carneiro]

One possibility is that it is deciding to rewrite with Nat.add_zero (n+0), and n+0+0 matches with n+0 in the goal (which is why the rewrite succeeds)

[François G. Dorais]

I'm thinking it's something like that but why would it do that?

[Leonardo de Moura]

@François G. Dorais The unifier in Lean 4 uses the "offset" module: https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Offset.lean
This module handles offset constraints such as ?x + 100 =?= a + 300 (solution: ?x := a + 200), and the different ways natural numbers can be represented in Lean.
This module is always active. So, the constraint ?x + 0 =?= n is solved as ?x := n. Note that Lean 3 also has a more primitive version of the "offset" module.

example (m n : nat) : not ((n+1) < (n+0)) :=
begin
  rw [nat.add_zero],
  -- m n : ℕ ⊢ ¬n + 1 < n + 0
  sorry
end

I have considered disabling Offset.lean when the reducibility setting is low, but it would negatively impact use-cases we care about. For example, a simp theorem of the form f (x + 2) = .. currently "fires" in goals containing f (a + 5). The feature is also important for programs manipulating types such as bit-vectors and vectors.

I acknowledge that the behavior in your example is counterintuitive, but I expect very few users will have to apply rw [Nat.add_zero] in the future. For educational material, I can see the value of using rw [Nat.add_zero]. We could add a flag for disabling the Offset.lean module, but I am not sure it would be easy to explain why the option is being used in the material. For educational material, one could avoid this issue by defining their own natural number type and add.

[Mario Carneiro]

@Leonardo de Moura In this case the constraint is ?x + 0 =?= n + 0, right? The two ways of solving this that I see are: (1) use the usual "congruence" heuristic when it applies in preference to the offset module, or (2) have the offset module take into account coefficients on both sides when cancelling, so that this goal reduces to ?x =?= n