Search code examples
coq

How to prove a constant function that neither injective nor surjective in Coq?

So the definition is giving out as : Definition constant {X:Type} (c:X) := fun x y : X => y = c. and I need to generate proof for Theorem const_not_inj : forall c:nat, ~injective (constant c).

I started proof like this:

Theorem const_not_inj : forall c:nat, ~injective (constant c).
unfold injective.
unfold not.
intros.
induction c.

then I get stuck having no clue how to continue. Any thought woule be helpful :)

Solution

  • Following on Pierre's suggestion, you can just pass, for instance, 0 and 1 to the H hypothesis you got after the intros, thus getting a contradiction. A short proof in SSReflect would be:

    From mathcomp Require Import ssreflect ssrfun. 

Definition constant {X:Type} (c:X) := fun x y : X => y = c.

Theorem const_not_inj : forall c:nat, ~injective (constant c).
Proof. by move=> c /(_ 0 1 erefl). Qed.

    Note that erefl is a proof of the equality of identical terms.