is `rewrite` more 'fundamental' than `simp only`?

Stream: lean4

[Paige Thomas]

How do these differ? Does simp only call rewrite? I notice that sometimes I have to use rewrite instead of simp only when simp only runs into an infinite recursion. Is there a tactic more 'fundamental' than rewrite?

[Henrik Böving]

rewrite applies a singular rewrite using the equality it was given simp only performs all possible rewrites with the equalities it was given until it reaches a fixpoint.

[Paige Thomas]

I think I see. So simp only does call rewrite one or more times?

[Robin Arnez]

I don't think that their implementations share much code (simp uses its own rewriting logic)

[Robin Arnez]

To answer your implicit question: You can use the +singlePass option on simp to prevent loops:

example (a b : Bool) : a = b := by
  simp +singlePass [Bool.eq_iff_iff]
  show a = true ↔ b = true
  sorry

[Paige Thomas]

I was more just wondering how these tactics worked, but thank you.

[Paige Thomas]

Is there a detailed description somewhere about how rewrite works?

[Paige Thomas]

I mean not what it does, but how it works in the type theory.

[Robin Arnez]

Well its proof output is Eq.mpr (congrArg (fun x => ...) h) ?_ where the ... is just the original expression with all occurrences of the left-hand side substituted

[Paige Thomas]

And h is the equality being applied?

[Paige Thomas]

Thank you.

[Jovan Gerbscheid]

Paige Thomas said:

I was more just wondering how these tactics worked

A few months ago @Mirek Olšák (with some help from me) wrote a tutorial about metaprogramming in Lean. The first file is a general introduction to tactic programming, and the second and third file are about how rw and simp work respecively. So if you want to learn about this in more detail, feel free to read this tutorial. See also #metaprogramming / tactics > Introduction to tactic programming

[Paige Thomas]

Awesome! Thank you!