Stream: Coq users

Topic: rewriting in the presence of universal quantifiers

Nicolas Rinaudo (Aug 23 2023 at 06:15):

I'm a little confused by the rules for rewriting when our goal contains a universal quantifier.

For a concrete example, see the following theorem:

``````Theorem plus_n_Sm :
forall n m : nat, S (n + m) = n + (S m).
``````

This lends itself to a trivial proof by induction, whose first half is:

``````Proof.
induction n as [| n' IHn'].
- reflexivity.
``````

I am however a little confused by something going on in the inductive case. Instinctively, I wanted to write:

``````  - simpl. rewrite IHn'. reflexivity.
``````

The `simpl` calls takes me to:

``````  n' : nat
IHn' : forall m : nat, S (n' + m) = n' + S m
============================
forall m : nat, S (S (n' + m)) = S (n' + S m)
``````

I would have assumed that, since both the goal and `IHn'` are quantified universally, I'd be able to rewrite the nested `S (n' + m)` in my goal and be done, but that fails. I first need to explicitly introduce `m`.

I'm perfectly fine with having to do this, but I would like to understand why. Clearly, my intuition is incorrect. What am I missing?

Rodolphe Lepigre (Aug 23 2023 at 06:36):

The problem is that you need to rewrite under a universal quantifier, which `rewrite` cannot do. You can instead use `setoid_rewrite` to do what you want:

``````From Coq Require Import PeanoNat.
Import Nat.

Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m).
Proof.
induction n as [|n' IHn'].
- reflexivity.
- simpl. setoid_rewrite IHn' at 1. reflexivity.
Qed.
``````

Note that the `at 1` specifies to rewrite at a particular occurrence, otherwise the rewrite happens in the right-hand-side of the conclusion.

Nicolas Rinaudo (Aug 23 2023 at 06:41):

Mmm... I was under the impression that you could. Just to clarify: I'm convinced you're correct, just, this means something I thought I had understood, well, I had not.

Here's what I mean:

``````Theorem more_occurences (n m p : nat) : p + (n + m) = (n + m) + p.
Proof.
(* ... *)
``````

My naive understanding of that `add_comm n` was that it "partially applied" `add_comm` and simplified it to `forall m, n + m = m + n.`. This has a universal quantifier, and Coq is perfectly happy to rewrite using it.

Pierre Rousselin (Aug 23 2023 at 06:45):

Grr, you beat me to it :smile:
As a side remark, while having the most general induction hypothesis is a good habit, you don't lose anything if you `intros m` after `induction`.

I would probably write it this way:

``````Theorem plus_n_Sm :
forall n m : nat, S (n + m) = n + (S m).
Proof.
induction n as [| n' IHn']; intros m. (* intros m on all subgoals *)
- reflexivity. (* ok by computation (definition of add) *)
- simpl; rewrite (IHn' m). (* specifying m make it match only LHS *)
reflexivity.
Qed.
``````

Or if you like one-liners: (`now` is like `(...); easy` and `easy` combines several concluding tactics such as `assumption`, `reflexivity`, `trivial`, ...):

``````Theorem plus_n_Sm' :
forall n m : nat, S (n + m) = n + (S m).
Proof.
now induction n as [| n' IHn']; intros m; [| simpl; rewrite (IHn' m)].
Qed.
``````

Pierre Rousselin (Aug 23 2023 at 06:47):

Nicolas Rinaudo said:

Mmm... I was under the impression that you could. Just to clarify: I'm convinced you're correct, just, this means something I thought I had understood, well, I had not.

Here's what I mean:

``````Theorem more_occurences (n m p : nat) : p + (n + m) = (n + m) + p.
Proof.
(* ... *)
``````

My naive understanding of that `add_comm n` was that it "partially applied" `add_comm` and simplified it to `forall m, n + m = m + n.`. This has a universal quantifier, and Coq is perfectly happy to rewrite using it.

The universal quantifier in this case is on the rewriting rule, not the goal (or in the hypothesis if need be) you want to rewrite in.

Nicolas Rinaudo (Aug 23 2023 at 06:50):

Pierre Rousselin said:

The universal quantifier in this case is on the rewriting rule, not the goal (or in the hypothesis if need be) you want to rewrite in.

Ah! So in `rewrite RULE in TARGET`, universal quantifiers are:

• fine in `RULE`
• not fine in `TARGET`

I realise this is not very formal and I will eventually learn the proper vocabulary for this, but for the moment, this is not too incorrect a way of thinking about it?

Nicolas Rinaudo (Aug 23 2023 at 06:51):

Pierre Rousselin said:

As a side remark, while having the most general induction hypothesis is a good habit, you don't lose anything if you `intros m` after `induction`.

I was not aware you could use `intros` right after `induction`! Thank you so much.

Ah, this is to do with `;`, isn't it? I'm technically not supposed to know about this yet, and will not pretend I understand how it works :)

Pierre Rousselin (Aug 23 2023 at 06:58):

Nicolas Rinaudo said:

Ah! So in `rewrite RULE in TARGET`, universal quantifiers are:

• fine in `RULE`
• not fine in `TARGET`

I realise this is not very formal and I will eventually learn the proper vocabulary for this, but for the moment, this is not too incorrect a way of thinking about it?

Actually (this is linked to your other post, there are two separate components here (please, Coq experts, correct me if I'm wrong) :

• the first one is Coq's unification algorithm. If you use for instance `rewrite add_comm`, `add_comm` has the form `forall n m, n + m = m + n`, so first Coq has to "fill the holes" because you did not provide the arguments to `add_comm` explicitely. This unification part happens before the `rewrite part`.
• next is the behavior of `rewrite`: once the holes are filled (once and for all), perform all rewritings possible on the goal (or less if you specify the occurrences explicitly with `at`)

Last updated: Jun 23 2024 at 04:03 UTC