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 (n1) 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.)
Your theorem f_inj
should assume a > 0
and b > 0
.
Okay. :+1:
Like this?
Theorem f_inj : forall a b:nat, (a > 0) > (b > 0) >
(f a = f b) > (a = b).
Proof.
intros.
Goal became:
1 subgoal
a, b : nat
H : a > 0
H0 : b > 0
H1 : f a = f b
========================= (1 / 1)
a = b
if (Nat.eqb 1 0) then 1
you probably meant Nat.eqb n 1
?
Oops.. Yeah that was a mistake. Correcting.
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
.
I thought we would need a way to somehow use H1: f a = f b
. But couldn't figure out how.
Case analysis as with destruct a
?
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 subgoa became:
b : nat
H : 0 > 0
H0 : b > 0
H1 : f 0 = f b
========================= (1 / 1)
0 = b
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
.
Right, and now if you look at your context you will see that it includes an impossibility.
So you can solve the goal with any number of tactics; probably lia
will work.
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?
You did the part of my algorithm I described as "get rid of the 0
case".
Does that make sense? Is there anything in particular I could explain so that you feel like you proceeded less blindly?
Sorry! I'm still new to this.
How do we get rid of the zero case?
Actually, taking a step back. Have you proved this on paper?
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.
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?
(Although it clearly can't)
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.
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.
But then we would loose the
f(1) = 0
1 is odd thus we compute (1  1)/2 = 0
1 is odd thus we compute (1  1)/2 = 0
Oh, right. My bad.
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.
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