Problem with tactic rw

Stream: new members

[Yicheng Qian]

I'm new to lean and I found the behaviour of tactic rw hard to comprehend.
First problem:

example (h₁ : x ∣ y) (h₂ : x ∣ z) : x ∣ (y + k * z) :=
  let ⟨k₁, d₁⟩ := h₁
  let ⟨k₂, d₂⟩ := h₂
  ⟨k₁ + k * k₂,
    calc
      (k₁ + k * k₂) * x = k₁ * x + k * k₂ * x   := by rw [Nat.add_mul]
              _         = k₁ * x + k * (k₂ * x) := by rw [Nat.mul_assoc]
              _         = y + k * z             := by rw [d₁, d₂]⟩

The above code works, however after a slight modification, it no longer works:

example (h₁ : x ∣ y) (h₂ : x ∣ z) : x ∣ (y + k * z) :=
  let ⟨k₁, d₁⟩ := h₁
  let ⟨k₂, d₂⟩ := h₂
  ⟨k₁ + k * k₂,
    calc
      (k₁ + k * k₂) * x = k₁ * x + k * k₂ * x   := by rw [Nat.add_mul]
              _         = y + k * z             := by rw [→Nat.mul_assoc, →d₁, →d₂] ⟩

Second problem: I was experimenting with the rw tactic and found this. It might seem made-up

example (H : x = 3) : 2 + x = 5 := by
  rw [← H]
/-  rw fails -/

I thought that it wouldn't fail because 5 is Nat.succ (Nat.succ 3).

[Martin Dvořák]

Do rw [H] instead of rw [← H] to replace x by 3.

[Martin Dvořák]

I noticed it is written in Lean 4, which I have no experience with. Better wait for someone else's reply.

[Kevin Buzzard]

I thought that it wouldn't fail because 5 is Nat.succ (Nat.succ 3) : it is definitionally that, but not syntactically that, and rw works up to syntactic equality.

[Ruizhe Wan]

while I use the tactic ring_nf to solve equation involving ε/37 in R, but will it still works if I change R to a field of characteristic 37 (which is certainly a ring)?

[Mario Carneiro]

#mwe?

[Mario Carneiro]

ring_nf doesn't know anything about division. It will just treat your epsilon/37 opaquely

[Mario Carneiro]

there is nothing illegal about writing the term epsilon/37 itself in a ring of characteristic 37, it's just defined to be some nonsense, probably zero

[Mario Carneiro]

in particular, it is a proper element of the ring and so ring theorems still apply to it

[Mario Carneiro]

however the theorem is unlikely to be useful in that case since it's a true theorem about a garbage value

[Mario Carneiro]

the theorem that would fail is something like (ε/37) * 37 = ε, this will require that 37 is invertible, so in particular the characteristic cannot be 37

[Ruizhe Wan]

well that's true, undefined term would not appear in a theorem anyway~

[Mark Andrew Gerads]

Supposing you make a Prop claiming 37 is not 0, then field_simp can simplify something like (ε/37) * 37 = ε.
https://leanprover-community.github.io/mathlib_docs/tactic/field_simp.html