## 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.
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: Oct 03 2023 at 19:01 UTC