Stream: Coq users

Topic: extract info


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

view this post on Zulip John Wiegley (Sep 02 2022 at 18:43):

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.

view this post on Zulip zohaze (Sep 03 2022 at 01:30):

What about second part of question?

view this post on Zulip abab9579 (Sep 03 2022 at 01:31):

Seems like k = 1 satisfies both 1 <= k and 0 <= S k..

view this post on Zulip zohaze (Sep 03 2022 at 01:37):

From above three relation , can i say a > 0 or a <> 0?

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

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

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

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

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

view this post on Zulip zohaze (Sep 03 2022 at 01:55):

Just to prove above combination is not possible.

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

view this post on Zulip zohaze (Sep 03 2022 at 02:00):

Last, may extract and write (S a) =1

view this post on Zulip Paolo Giarrusso (Sep 03 2022 at 14:26):

No, and the counterexample is any case where a = k (say, both are 0).

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

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

view this post on Zulip zohaze (Sep 03 2022 at 16:42):

If above is not true then we can prove it false?

view this post on Zulip Pierre Castéran (Sep 03 2022 at 17:45):

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.

view this post on Zulip zohaze (Sep 04 2022 at 03:58):

Thank you. a & k are natural numbers. Therefore they can be zero or non zero. Should i consider both cases separately?

view this post on Zulip James Wood (Sep 05 2022 at 08:29):

If what you're trying to prove is not true, no proof strategy will help.

view this post on Zulip zohaze (Sep 06 2022 at 03:31):

Ok, thanks to all of you.

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

view this post on Zulip 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: Feb 06 2023 at 12:04 UTC