I am learning Coq and I need to use, for the first time, the ring tactic. I have tried using it after Require Ring. or Require ArithRing. to simplify the right side of an equation that I have as a goal, but Coq takes it a reference that does not exist. I copy my piece of code here (I have tried several times with ring and ring_simplify):
Lemma sum_n_p : forall n, 2 * sum_n n + n = n * n.
(* sum_n n is inductively defined as the sum of all numbers between 1 and n *)
Proof.
intros n.
induction n as [ |m IHm].
+simpl.
reflexivity.
+assert (SnSn : S m * S m = m * m + 2 * m + 1).
ring_simplify in [S m * S m = m * m + 2 * m + 1]. (*or just ring. , neither works*)
rewrite SnSn.
rewrite <- IHm.
simpl.
ring.
Qed.
To call those tactics, you need to import those modules, not just require them:
Require Import ArithRing Ring.
I tried running your proof after adding those lines, but Coq got stuck in a different error. You might still need to adjust your script before it gets accepted by Coq.