## Stream: Coq users

### Topic: extract info

#### 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)
``````

#### 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.

#### 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
``````

#### Paolo Giarrusso (Sep 03 2022 at 14:26):

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.

#### 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
``````

#### 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 `a`and `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.
``````

#### 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?

#### 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: Jun 25 2024 at 18:02 UTC