Julin S (Jun 20 2022 at 08:55): 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.
Julin S (Jun 20 2022 at 09:03):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.
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?
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
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):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?
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
0does 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
Oh, right. My bad.
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: Oct 03 2023 at 04:02 UTC