What are simpl, reflexivity in rocq?

Two proof tactics that relates to Proof by simplification, that is, they both try to unfold the terms then evaluate the expressions.