Stream: Coq users

Topic: rewriting in the presence of universal quantifiers


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.
  rewrite (add_comm n).
  (* ... *)

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.

view this post on Zulip 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.

view this post on Zulip 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.
  rewrite (add_comm n).
  (* ... *)

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.

view this post on Zulip 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:

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?

view this post on Zulip 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 :)

view this post on Zulip Pierre Rousselin (Aug 23 2023 at 06:58):

Nicolas Rinaudo said:

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

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) :


Last updated: Jun 23 2024 at 04:03 UTC