zohaze (Sep 02 2022 at 17:06): zohaze (Sep 02 2022 at 17:06):(a <= k) ->
((S a) <= k) ->
(a <= S k) .
If first two relations hold then we can prove third one? Secondly,below statement is contra statement?
(1 <= k)
(0 <= S k)
zohaze said:
(a <= k) -> ((S a) <= k) -> (a <= S k) .If first two relations hold then we can prove third one?
You only need the first relation to prove the third.
zohaze (Sep 03 2022 at 01:30):What about second part of question?
abab9579 (Sep 03 2022 at 01:31):Seems like k = 1 satisfies both 1 <= k and 0 <= S k..
zohaze (Sep 03 2022 at 01:37):From above three relation , can i say a > 0 or a <> 0?
abab9579 (Sep 03 2022 at 01:39):Well, a = 0 and k = 1 satisfies all three.. could I ask why you are asking these questions?
zohaze (Sep 03 2022 at 01:43):In hypothesis i have a=0 and want to check H is true or false. May be it is contra statement. I am looking for some contra statement in all above.
abab9579 (Sep 03 2022 at 01:44):Contradiction you are seeking here does not exist. I feel like this is XY problem, could you show the whole of what you are doing?
zohaze (Sep 03 2022 at 01:51):I have sub goal statement = False. There is no other hypothesis above 3 and a=0. Want to complete it.
abab9579 (Sep 03 2022 at 01:52):That still does not sound like the whole thing. Why are you doing that, what do you ultimately want to prove?
zohaze (Sep 03 2022 at 01:55):Just to prove above combination is not possible.
abab9579 (Sep 03 2022 at 01:56):I mean, there must be a reason you are proving this somewhat arbitrary proposition. (Which I believe is not true, after all)
zohaze (Sep 03 2022 at 02:00):between_le: forall (P : nat -> Prop) (k l : nat), between P k l -> k <= l
exists_le_S: forall (Q : nat -> Prop) (k l : nat), exists_between Q k l -> S k <= l
By using above , could i prove below one
H: a <= k
Goal: S a <=k
No, and the counterexample is any case where a = k (say, both are 0).
Paolo Giarrusso (Sep 03 2022 at 14:27):If you get to this goal from a valid theorem, then you have chosen the wrong proof strategy.
Paolo Giarrusso (Sep 03 2022 at 14:31):So, @abab9579 is 100% right. We cannot help you solve your task with the questions you're asking.
zohaze (Sep 03 2022 at 16:42):If above is not true then we can prove it False? Secondly, what maximum information we can extract from below (especially S a=0 or S a=1)
H: a <= k
H1: S a <= k
H2: a <= S k
For the first question: whether the implication (a <= k -> S a <= k) is true or false depends on aand k. But you didn't give any information about these variables. As several of us already mentionned, we cannot help to solve sub-goals which are too partially presented; the best being a script we can replay without having to guess and re-type the missing information.
The following three lemmas clearly show that this implication is sometimes false, sometimes true.
Require Import Arith Lia.
Lemma L : ~ forall a k, (a <= k -> S a <= k).
Proof. intro H . specialize (H 0 0). lia. Qed.
Lemma L': exists a k, ~ (a <= k -> S a <= k).
Proof. exists 0, 0; lia. Qed.
Lemma L'' : exists a k, (a <= k -> S a <= k).
Proof. exists 0, 42; lia. Qed.
For the second question, the conjunction of your three propositions is clearly equivalent to a < k.
Goal forall a k, (a <= k /\ S a <= k /\ a <= S k) <-> a < k.
Proof. lia. Qed.
Thank you. a & k are natural numbers. Therefore they can be zero or non zero. Should i consider both cases separately?
James Wood (Sep 05 2022 at 08:29):If what you're trying to prove is not true, no proof strategy will help.
zohaze (Sep 06 2022 at 03:31):Ok, thanks to all of you.
zohaze (Sep 06 2022 at 07:09):H1: S a <= k
H2: a <= S k
H3: S k >0
From above could i write (S a=k) or (a=k) or what other information may extract?
James Wood (Sep 06 2022 at 08:15):H3 is redundant: You could prove it for any k because a successor is always greater than 0. H1 implies H2: From S a <= k we get S a <= S k and S a <= S (S k) by applying le_S twice. Then, le_S_n gives us a <= S k. So, in summary, all you know is that S a <= k.
Last updated: Sep 30 2023 at 05:01 UTC