reason why `rw` tactic is inappropriate vs `rel`

Stream: new members

[rzeta0]

Consider the following very simple, perhaps trivial, proof:

-- Prove a < c if we know a < b and b ≤ c, where a,b,c ∈ ℕ.
example {a b c : ℕ} (h1: a < b) (h2: b ≤ c) : a < c :=
  calc
    a < b := by rel [h1]
    _ ≤ c := by rel [h2]

We use the rel tactic to reason about hypotheses that are inequalities.

Question: What is the real reason we can't use the rw tactic and must use rel ?

Is it because rw is a very simple tactic that only does syntactic replacement - that is, only performs a substitution if an exact pattern is matched - and does not perform additional checks such as ensuring monotonicity of the functions involved in a potential substitution?

[Robert Maxton]

No, as a general rule faulty tactics cannot break Lean's proof system/cannot be used to prove false; the kernel runs its own checks and a buggy tactic will fail if it can't prove the result sound. (There are of course much weaker guarantees on whether or not a tactic has in fact proven the thing you thought it was proving, of course, but that's a separate problem)

[Kyle Miller]

rw only handles rewriting using equalities and iffs. There's a notion of generalized rewriting for more general relations, but it's not as well-defined of a problem. It's not just about checking monotonicity, it would have to synthesize proofs of monotonicity and create "congruence arguments". This is what the gcongr tactic does (what mathlib calls the book's rel) given a particular goal to prove — having a LHS and RHS is useful for being able to solve for what the correct congruences should be.

By the way, you definitely don't need tactics here. This is just transitivity of the hyptheses:

example {a b c : ℕ} (h1: a < b) (h2: b ≤ c) : a < c :=
  calc
    a < b := h1
    _ ≤ c := h2

[Kyle Miller]

rw is simple, but it's able to do things that rel cannot, and vice versa.