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?
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
Isn’t neq_succ_diag_l proven using induction? (uhm, not directly in the stdlib)
IIUC, the proof must rely on induction, since n = S’ n would be solvable for coinductive nats
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.
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