defeq abuse

Stream: lean4

[Richard Copley]

The Y problem: what's going on with the two examples? below The code between "BEGIN" and "END" is the same in both cases, but rw [Nat.pred_succ] succeeds in the first case and fails in the second. I suppose the 2 is actually Nat.succ 1 in the first case but not the second case? But then what is it in the second case?

The X problem: what's a sensible way to rewrite Nat.pred 2 to 1?

import Mathlib.Data.Nat.Size
example {x : ℕ} (d : 2 ∣ x) : 2 * (x - x / 2) = 2 * (x / 2) :=
  by
    -- BEGIN
    -- ⊢ 2 * (x - x / 2) = 2 * (x / 2)
    rw [mul_comm 2, mul_comm 2]
    rw [Nat.mul_sub_right_distrib]
    rw [Nat.div_mul_cancel d, ← Nat.mul_pred_right]
    -- ⊢ x * Nat.pred 2 = x
    rw [Nat.pred_succ]
    -- END
    -- ⊢ x * 1 = x
    rw [Nat.mul_one]

import Mathlib.Data.Nat.Size
example {x : ℕ} (d : 2 ∣ x) : x - x / 2 = x / 2 :=
  by
    apply Nat.eq_of_mul_eq_mul_left (zero_lt_two' ℕ)
    -- BEGIN
    -- ⊢ 2 * (x - x / 2) = 2 * (x / 2)
    rw [mul_comm 2, mul_comm 2]
    rw [Nat.mul_sub_right_distrib]
    rw [Nat.div_mul_cancel d, ← Nat.mul_pred_right]
    -- ⊢ x * Nat.pred 2 = x
    rw [Nat.pred_succ]
    -- END
    -- failed, did not find instance of pattern Nat.pred (Nat.succ ?n)

[David Renshaw]

Can you please include the imports for your examples, so that it's a #mwe?

[Richard Copley]

I have edited the imports into the examples.
Inserting any of these before rw [Nat.pred_succ] makes the second case work.

    rw [(rfl : 2 = 2)] -- no visible effect
    rw [(rfl : 2 = nat_lit 2)] -- no visible effect
    rw [(rfl : 2 = Nat.succ 1)] -- no visible effect
    rw [(rfl : Nat.pred 2 = 1)] -- no visible effect

But I wouldn't call them sensible!

[David Renshaw]

yeah, that's weird

[David Renshaw]

if I do set_option pp.all true, then the first example is

x : Nat
d : @Dvd.dvd.{0} Nat Nat.instDvdNat (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) x
⊢ @Eq.{1} Nat
    (@HMul.hMul.{0, 0, 0} Nat Nat Nat (@instHMul.{0} Nat instMulNat) x
      (Nat.pred (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))))
    x

and the second example is

x : Nat
d : @Dvd.dvd.{0} Nat Nat.instDvdNat (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) x
⊢ @Eq.{1} Nat
    (@HMul.hMul.{0, 0, 0} Nat Nat Nat (@instHMul.{0} Nat instMulNat) x
      (Nat.pred
        (@OfNat.ofNat.{0} Nat 2
          (@instOfNat.{0} Nat 2
            (@AddMonoidWithOne.toNatCast.{0} Nat
              (@AddCommMonoidWithOne.toAddMonoidWithOne.{0} Nat
                (@NonAssocSemiring.toAddCommMonoidWithOne.{0} Nat (@Semiring.toNonAssocSemiring.{0} Nat Nat.semiring))))
            (@instAtLeastTwoHAddNatInstHAddInstAddNatOfNat (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))))))
    x

[David Renshaw]

So I guess maybe all those typeclass instances mean than somehow definitional equality / normalization is not getting as far in the second example.

[Yuyang Zhao]

This may be because of the new numeric literal mechanism of lean4. 1+1=2 for AddMonoidWithOne (docs4#one_add_one_eq_two) is no longer a defeq. (edit: not the defeq problem, it's still defeq for Nats. But IIRC 2 in lean3 is syntactically equivalent to 1+1, and in lean4 it's not)

[Yuyang Zhao]

rw [← one_add_one_eq_two] may helps (edit: seems it not helps, but you can change x * 1 = x directly)

[Yuyang Zhao]

rw [← one_add_one_eq_two, Nat.add_one, Nat.pred_succ] also works.

[Richard Copley]

erw also works. To summarize,

import Mathlib.Data.Nat.Cast.Basic

def two' :=
  (@OfNat.ofNat.{0} Nat 2
    (@instOfNat.{0} Nat 2
      (@AddMonoidWithOne.toNatCast.{0} Nat
        (@AddCommMonoidWithOne.toAddMonoidWithOne.{0} Nat
          (@NonAssocSemiring.toAddCommMonoidWithOne.{0} Nat
            (@Semiring.toNonAssocSemiring.{0} Nat Nat.semiring))))
      (@instAtLeastTwoHAddNatInstHAddInstAddNatOfNat
        (@OfNat.ofNat.{0} Nat 0
          (instOfNatNat 0)))))

example : two' = 2 := rfl

theorem pred_succ (n : ℕ) : Nat.pred (Nat.succ n) = n := rfl

example : Nat.pred two' = 1 := by
  unfold two'
  try { rw [pred_succ 1] }
  sorry

example : Nat.pred two' = 1 := by
  unfold two'
  rw [← one_add_one_eq_two, Nat.add_one, Nat.pred_succ]

example : Nat.pred two' = 1 := by
  unfold two'
  erw [pred_succ 1]

[Richard Copley]

(I think this is unfortunate)