From 6631700c7191c49e1db46eae0259a383e9c16213 Mon Sep 17 00:00:00 2001 From: Florent Schaffhauser Date: Mon, 20 Apr 2026 12:08:10 +0200 Subject: [PATCH] Fix indications about rewrite tactic in vanilla Rocq vs. ssreflect, add corresponding solution to the vanilla Rocq version --- tuto1_nat.v | 5 +++-- tuto1_nat_solution.v | 11 +++++++++++ tuto1_ssrnat.v | 5 ++--- 3 files changed, 16 insertions(+), 5 deletions(-) diff --git a/tuto1_nat.v b/tuto1_nat.v index 7ce4e05..b407c8d 100644 --- a/tuto1_nat.v +++ b/tuto1_nat.v @@ -76,8 +76,9 @@ Qed. Goal forall n m : nat, n = 2 * m -> m = 6 -> (n - 5) * m = 42. Proof. intros n m nE mE. -(* [rewrite] actually accepts any number of arguments, which are all equalities - that get rewritten one after the other. Try [rewrite nE mE.]. +(* [rewrite] actually accepts any number of arguments, separated by commas, + which are all equalities that get rewritten one after the other. + Try [rewrite nE, mE.]. *) diff --git a/tuto1_nat_solution.v b/tuto1_nat_solution.v index e315a07..fb66dda 100644 --- a/tuto1_nat_solution.v +++ b/tuto1_nat_solution.v @@ -64,6 +64,17 @@ Goal forall n m : nat, n = 3 * m -> n + 1 = 3 * m + 1. reflexivity. Qed. +Goal forall n m : nat, n = 2 * m -> m = 6 -> (n - 5) * m = 42. +Proof. + intros n m nE mE. +(* [rewrite] actually accepts any number of arguments, separated by commas, + which are all equalities that get rewritten one after the other. + Try [rewrite nE, mE.]. +*) + rewrite nE, mE. + reflexivity. +Qed. + (** Addition *) (* Natural numbers are defined by two rules: diff --git a/tuto1_ssrnat.v b/tuto1_ssrnat.v index c1f3f78..b784573 100644 --- a/tuto1_ssrnat.v +++ b/tuto1_ssrnat.v @@ -80,9 +80,8 @@ Qed. Goal forall n m : nat, n = 2 * m -> m = 6 -> (n - 5) * m = 42. Proof. move=> n m nE mE. -(* [rewrite] actually accepts any number of arguments, separated by commas, - which are all equalities that get rewritten one after the other. - Try [rewrite nE mE.]. +(* [rewrite] actually accepts any number of arguments, which are all equalities + that get rewritten one after the other. Try [rewrite nE mE.]. *)