## Stream: Coq users

### Topic: Proof of function being injective

#### Julin S (Jun 20 2022 at 08:55):

I wanted to prove that a function like:

``````f:ℕ₁ → ℤ

f(1)    = 0
f(2k)   = k
f(2k+1) = -k
``````

was injective.

How would we go about it?

(Since `nat` includes `0` as well..)

I started with:

``````Require Import ZArith.

Definition f (n:nat) : Z :=
if (Nat.eqb n 1) then 0
else if (Nat.even n) then (Z.of_nat (Nat.div n 2))
else -(Z.of_nat (Nat.div (n-1) 2)).

Theorem f_inj : forall a b:nat,
(f a = f b) -> (a = b).
Proof.
intros.
``````

The goal at this point was:

``````1 subgoal

a, b : nat
H : f a = f b

========================= (1 / 1)

a = b
``````

(Haven't worked much with `ZArith` before.)

#### Olivier Laurent (Jun 20 2022 at 09:01):

Your theorem `f_inj` should assume `a > 0` and `b > 0`.

Okay. :+1:

#### Julin S (Jun 20 2022 at 09:04):

Like this?

``````Theorem f_inj : forall a b:nat, (a > 0) -> (b > 0) ->
(f a = f b) -> (a = b).
Proof.
intros.
``````

#### Julin S (Jun 20 2022 at 09:05):

Goal became:

``````1 subgoal

a, b : nat
H : a > 0
H0 : b > 0
H1 : f a = f b

========================= (1 / 1)

a = b
``````

#### Ana de Almeida Borges (Jun 20 2022 at 09:12):

`if (Nat.eqb 1 0) then 1`

you probably meant `Nat.eqb n 1`?

#### Julin S (Jun 20 2022 at 09:13):

Oops.. Yeah that was a mistake. Correcting.

#### Ana de Almeida Borges (Jun 20 2022 at 09:14):

I haven't tried to prove it, but I would say the next step is to do a case analysis on `a` and `b`, exactly along the lines of your definition of `f`.

#### Julin S (Jun 20 2022 at 09:15):

I thought we would need a way to somehow use `H1: f a = f b`. But couldn't figure out how.

#### Julin S (Jun 20 2022 at 09:15):

Case analysis as with `destruct a`?

#### Julin S (Jun 20 2022 at 09:16):

Did:

``````Theorem f_inj : forall a b:nat, (a > 0) -> (b > 0) ->
(f a = f b) -> (a = b).
Proof.
intros.
destruct a.
-
``````

And the next sub-goa became:

``````b : nat
H : 0 > 0
H0 : b > 0
H1 : f 0 = f b

========================= (1 / 1)

0 = b
``````

#### Ana de Almeida Borges (Jun 20 2022 at 09:18):

That is one way of doing a case analysis, yes. Here it won't be too helpful because you actually want to distinguish between even and odd numbers. What I would do is unfold `f` in `H1` and then do a case analysis on `Nat.even a` and later `Nat.even b` (`destruct (Nat.even a)`). Actually, I would probably get rid of the `0` and `1` cases first with `destruct a` and `destruct b`.

#### Ana de Almeida Borges (Jun 20 2022 at 09:18):

Right, and now if you look at your context you will see that it includes an impossibility.

#### Ana de Almeida Borges (Jun 20 2022 at 09:18):

So you can solve the goal with any number of tactics; probably `lia` will work.

#### Julin S (Jun 20 2022 at 09:45):

I sort of blindly tried:

``````Theorem f_inj : forall a b:nat, (a > 0) -> (b > 0) ->
(f a = f b) -> (a = b).
Proof.
intros.
destruct a.
- lia.
- destruct b.
* lia.
* auto.
``````

when the goal became:

``````1 subgoal

a, b : nat
H : S a > 0
H0 : S b > 0
H1 : f (S a) = f (S b)

========================= (1 / 1)

S a = S b
``````

Is it a good way?

#### Ana de Almeida Borges (Jun 20 2022 at 09:47):

You did the part of my algorithm I described as "get rid of the `0` case".

#### Ana de Almeida Borges (Jun 20 2022 at 09:47):

Does that make sense? Is there anything in particular I could explain so that you feel like you proceeded less blindly?

#### Julin S (Jun 20 2022 at 09:48):

Sorry! I'm still new to this.

How do we get rid of the zero case?

#### Ana de Almeida Borges (Jun 20 2022 at 09:48):

Actually, taking a step back. Have you proved this on paper?

#### Olivier Laurent (Jun 20 2022 at 09:51):

If the value for `0` does not matter, you should probably simplify the definition of `f`:

``````Definition f n : Z :=
if Nat.even n then Z.of_nat (Nat.div n 2)
else -(Z.of_nat (Nat.div (n - 1) 2)).
``````

Then focus on the definition of `f`: if you want to compute something about `f a` and `f b` you should first know the value of `Nat.even a` and `Nat.even b`, thus the following possible start of a proof:

``````Theorem f_inj a b : 0 < a -> 0 < b -> f a = f b -> a = b.
Proof.
intros Ha Hb Hf; unfold f in Hf.
case_eq (Nat.even a); case_eq (Nat.even b);
intros Heqb Heqa; rewrite Heqb, Heqa in Hf.
``````

then you should mostly be back to "paper situation" where you need to deal with arithmetic properties.

#### Julin S (Jun 20 2022 at 09:53):

Could it be like this?

We got:

``````f(a) = f(b)  ->   a=b
``````

Fixing value of `a`, first, got three cases.

a = 1 means

``````f(1) = f(b)  ->  1 = b
``````

But how do we prove that that other 2 cases (where a!=1) can't produce 1 as well?

#### Julin S (Jun 20 2022 at 09:53):

(Although it clearly can't)

#### Julin S (Jun 20 2022 at 09:59):

if the value for `0` does not matter

But then we would loose the `f(1) = 0` part, right? Though we won't need the `f(0)` part.

#### Ana de Almeida Borges (Jun 20 2022 at 10:03):

But how do we prove that that other 2 cases (where a!=1) can't produce 1 as well?

This depends on how you do the case analysis in Coq. The first `destruct a` gives you the cases `a = 0` and `a = S a'`. The former is the zero case I mentioned above. You assumed `a > 0`, so it can be easily discharged with `lia` (since it is not the case that `0 > 0`). In the `a = S a'` case, if you do `destruct a'` you get two cases again: `a' = 0` and `a' = S a''`. In terms of `a` this becomes `a = S a' = S 0 = 1` and `a = S a' = S (S a'')`. The former is the `1` case. And from the moment you are in the latter case, you are assuming that your `a` is a double successor, so it clearly can't be either `0` or `1`.

But you could also not destruct `a` at all and destruct `Nat.eqb n 1` instead. If you do with with `case_eq`, as in `case_eq (Nat.eqb n 1)`, you will get an assumption that `n` equals `1` in the first case and an assumption that `n` does not equal `1` in the second one.

#### Olivier Laurent (Jun 20 2022 at 10:03):

But then we would loose the `f(1) = 0`

1 is odd thus we compute -(1 - 1)/2 = 0

#### Julin S (Jun 20 2022 at 10:06):

``````1 is odd thus we compute -(1 - 1)/2 = 0
``````

#### Julin S (Jun 20 2022 at 10:42):

Something like:

``````  intros.
destruct a.
- lia.   (* case: a = 0 *)
- destruct a.
* lia.    (* case: a = S a' = S 0 = 1 *)
*         (* case: a = S a' = S (S a'') *)
``````

right?

And regarding the way with `case_eq`,

``````  intros.
case_eq (Nat.eqb a 1).
- intros.
``````

gave

``````a, b : nat
H : a > 0
H0 : b > 0
H1 : f a = f b
H2 : (a =? 1) = true

========================= (1 / 1)

a = b
``````

Just to know, is there a way to use the `(a =? 1) = true` to get a = 1 as a hypothesis?

as goal.

#### Ana de Almeida Borges (Jun 20 2022 at 11:31):

Just to know, is there a way to use the (a =? 1) = true to get a = 1 as a hypothesis?

`Search (_ =? _) (_ = _).` suggests `Nat.eqb_eq`.

Last updated: Feb 01 2023 at 12:30 UTC