$6$ Functions

Show that the function f on the natural numbers N given by f$($n$)=5$n $+2$

in injective, but not surjective. The Coq definition of this function can be expressed as a relation,

Definition f :$=$ by$\_$formula $($fun x : nat $=>5*$ x $+1).$

Prove that f is injective and not surjective,

Lemma prob$6$ : injective f $/\backslash$ ~surjective f$.$

You will likely find it necessary to use Nat.add cancel r$,$ Nat.mul cancel l$,$ and discriminate in the first proof. You might use discriminate in the second step.

Use the template:

From Coq Require Import Bool.Bool.

From Coq Require Import Classes.RelationClasses.

Variable $($choice : forall $\{$A P$\}($prf : exists a : A$,$ P a$),$ A$).$

Hypothesis $($choice$\_$ok : forall $\{$A P$\}($prf : exists a : A$,$ P a$),$ P $($choice prf$)).$

Record Func $($dom cod : Type$)$ : Type :$=$

mkFunc $\{$

rel : dom $->$ cod $->$ Prop

; total : forall x : dom, exists y : cod, rel x y

; functional : forall x : dom, forall y z : cod, rel x y $->$ rel x z $->$ y $=$ z

$\}.$

Definition app : forall $\{$dom cod$\},$ Func dom cod $->$ dom $->$ cod.

Proof.

intros dom cod f x$.$

exact $($choice $($f$.($total dom cod$)$ x$)).$

Defined.

Lemma app$\_$iff$\_$rel : forall $\{$dom cod$\}($f : Func dom cod$)($x : dom$)($y : cod$),$

app f x $=$ y $<->($f$.($rel dom cod$)$ x y$).$

Proof.

intros dom cod f x y$.$

set $($s :$=$ total dom cod f x$).$

unfold app.

fold s$.$

split.

$-$ intros app.

rewrite $<-$ app.

exact $($choice$\_$ok s$).$

$-$ intros rel.

apply $($f$.($functional dom cod$))$ with $($x :$=$ x$).$

$+$ exact $($choice$\_$ok s$).$

$+$ exact rel.

Qed.

Definition by$\_$formula : forall $\{$dom cod : Type$\},($dom $->$ cod$)->$ Func dom cod.

Proof.

intros dom cod f$.$

refine $($mkFunc dom cod $($fun x y $=>$ f x $=$ y$)\_\_).$

$-$ intros x$.$

exists $($f x$).$

reflexivity.

$-$ intros x y z eq$1$ eq$2.$

rewrite $<-$ eq$1.$

rewrite $<-$ eq$2.$

reflexivity.

Defined.

Lemma by$\_$formula$\_$ok : forall $\{$dom cod : Type$\}($formula : dom $->$ cod$)($x : dom$),$

app $($by$\_$formula formula$)$ x $=$ formula x$.$

Proof.

intros dom cod formula x$.$

unfold by$\_$formula.

unfold app.

simpl.

set $($ok :$=$ choice$\_$ok

$($ex$\_$intro $($fun y : cod $=>$ formula x $=$ y$)($formula x$)$ eq$\_$refl$)).$

symmetry.

exact ok$.$

Qed.

Definition surjective $\{$dom cod$\}($f : Func dom cod$)$ :$=$ forall y : cod,

exists x : dom, app f x $=$ y$.$

Definition injective $\{$dom cod$\}($f : Func dom cod$)$ :$=$ forall x xp : dom,

app f x $=$ app f xp $->$ x $=$ xp$.$

Definition f :$=$ by$\_$formula $($fun x : nat $=>5*$ x $+1).$

Lemma prob$6$ : injective f $/\backslash$ ~surjective f$.$

Proof.

Qed.