Stream: Coq users

Topic: Proof of function being injective


view this post on Zulip 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.)

view this post on Zulip Olivier Laurent (Jun 20 2022 at 09:01):

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

view this post on Zulip Julin S (Jun 20 2022 at 09:03):

Okay. :+1:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ana de Almeida Borges (Jun 20 2022 at 09:12):

if (Nat.eqb 1 0) then 1

you probably meant Nat.eqb n 1?

view this post on Zulip Julin S (Jun 20 2022 at 09:13):

Oops.. Yeah that was a mistake. Correcting.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julin S (Jun 20 2022 at 09:15):

Case analysis as with destruct a?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip Julin S (Jun 20 2022 at 09:48):

Sorry! I'm still new to this.

How do we get rid of the zero case?

view this post on Zulip Ana de Almeida Borges (Jun 20 2022 at 09:48):

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

view this post on Zulip 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.

view this post on Zulip Julin S (Jun 20 2022 at 09:53):

No, I hadn't.

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?

view this post on Zulip Julin S (Jun 20 2022 at 09:53):

(Although it clearly can't)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Julin S (Jun 20 2022 at 10:06):

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

Oh, right. My bad.

view this post on Zulip 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.

view this post on Zulip 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: Mar 28 2024 at 22:01 UTC