Stream: Coq users

Topic: Showing that a function has no fixpoint

Julin S (Jun 05 2022 at 08:10):

I was trying to prove that for a function defined like

Definition f (n:nat) : nat := n + 1.

There can be no n where f n is n itself.

So I started off (till getting stuck) by doing:

Theorem fnofix : forall n:nat,
    f n <> n.
Proof.
  intros.
  induction n.
  - discriminate.
  -

The goal at this point was:

1 subgoal

n : nat
IHn : f n <> n

========================= (1 / 1)

f (S n) <> S n

How can I set this right?

Was I proceding in a wrong direction?

Olivier Laurent (Jun 05 2022 at 08:35):

If you are only interested in this particular function then it is not really a matter of using induction, but more of using properties of addition and axioms of Peano.
You can find appropriate properties in the standard library with From Coq Require Import PeanoNat:

Nat.add_1_r : forall n : nat, n + 1 = S n
Nat.neq_succ_diag_l : forall n : nat, S n <> n

Paolo Giarrusso (Jun 05 2022 at 09:29):

Isn’t neq_succ_diag_l proven using induction? (uhm, not directly in the stdlib)

Paolo Giarrusso (Jun 05 2022 at 09:36):

IIUC, the proof must rely on induction, since n = S’ n would be solvable for coinductive nats

Paolo Giarrusso (Jun 05 2022 at 09:48):

Concretely, while reusing the stdlib proof is probably a good idea, here's a direct one:

From Coq Require Import PeanoNat.

Definition f (n:nat) : nat := n + 1.

Theorem fnofix : forall n:nat,
  f n <> n.
Proof.
  intros.
  unfold f; rewrite Nat.add_1_r.
  Fail discriminate. Fail congruence.
  induction n.
  - discriminate.
  -
    now intros [= H].
    Undo.
    (* Expanding. *)
    intros H. apply IHn.
    injection H. auto.
Qed.

Paolo Giarrusso (Jun 05 2022 at 09:51):

This strategy generalizes to proving C x <> x for your constructor C, and it is not implemented by discriminate or congruence (see edit)

Last updated: Apr 20 2024 at 05:01 UTC