I was trying to prove that for a function defined like
Definition f (n:nat) : nat := n + 1.
There can be no
f n is
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
congruence (see edit)
Last updated: Oct 03 2023 at 19:01 UTC