Stream: Coq users

Topic: variable relation?

sara lee (Sep 13 2022 at 03:37):

a < S b
b2 = S b
b <= S a

a b b2 are nat. What information i can extract among the variables from above? Or existing relation may be prove wrong?

Michael Soegtrop (Sep 13 2022 at 09:35):

You can show a <= b <= a+1 - the relation to b2 should be obvious.

sara lee (Sep 13 2022 at 18:41):

Sorry, I have (<=) relation between a and b . In this case below is possible

   a <= S b
    b < c
    c = S a

What could be possible relation between a & c or false

James Wood (Sep 13 2022 at 20:11):

Just chaining things together, you get a <= S b < S c = S (S a). From S b < S (S a) you can get b <= a, so S b is either a or S a, similar to what you had before.

Michael Soegtrop (Sep 14 2022 at 07:54):

@sara lee : if you are unsure about such facts, you can easily test them with:

Require Import Lia.
Goal forall a b c, a <= S b -> b < c -> c = S a -> a <= b+1 <= a+1.
intros; lia.

You can check if this are the tightest bounds by increasing the left / decreasing the right bound and see if lia can still solve them.
If you are in the middle of a proof you can do

assert( a <= b+1 <= a+1 ) by lia.

lia is a decision procedure for the domain it can handle (addition, multiplication with constants, relational operators in N and Z).

sara lee (Sep 14 2022 at 12:18):

Thanks to all of you. I have asserted above relation in hypothesis. At the end i need (a=S c). Now how to extract this?

Michael Soegtrop (Sep 14 2022 at 12:25):

a = S c is obviously wrong since you have c = S a.
If it would be true, you could do:

Require Import Lia.
Goal forall a b c, a <= S b -> b < c -> c = S a -> a = S c.
intros; lia.

Indeed you can do:

Require Import Lia.
Goal forall a b c, a <= S b -> b < c -> c = S a -> a = S c -> False.
intros; lia.

which proves that a = S c together with the other premises is incompatible.

sara lee (Sep 14 2022 at 15:38):

Addition of a <= b in above three will change the result in any way? May i get some contra statement? I m in need of contra from these 4 relations.

Michael Soegtrop (Sep 14 2022 at 17:20):

@sara lee : I think I explained now in quite some detail how to ask lia such questions rather than us. You should also be able to figure this out pencil and paper. It is not a good idea to try to prove things you don't understand on pencil and paper.

My last example on this: adding a <= b does not lead to a contradiction:

Require Import Lia.
Goal forall a b c, a <= S b -> b < c -> c = S a -> a <= b -> False.
intros; lia.

The above fails. If the 4 statements would be contradicting, lia could derive False from it.

sara lee (Sep 15 2022 at 17:08):

In some (true and false) proposition, lia command works (it reply). But some time gives message" cannot not find witness".
It means some information is required in decision making .e.g have single hypothesis H:= a<=b and want to prove S a <= b (which is incorrect).
To prove it wrong i have asserted (a <= S b due to H). Having correct relation and on its inverse basis could i prove it wrong ? Or what is the missing relation to do this?

abab9579 (Sep 15 2022 at 23:54):

Uh, what?
Well, to prove that the implication is wrong, you could indeed prove
(a <= b -> S a <= b) -> False.
What do you even mean by "correct relation and inverse basis"? Also why are you even looking for missing relation?

Pierre Castéran (Sep 16 2022 at 05:57):

I would prefer not to talk about goals with undeclared free variables (as presented in this stream and a few others).

What we can prove is:

Goal (forall a b, a <= b -> S a <= b) -> False.
  intro H; specialize (H 42 42); lia.
Qed.

But not:

Variables a b: nat.
Goal  (a <= b -> S a <= b) -> False.
  Fail lia.
Abort.

When asking questions, it's important to give all the necessary information about the context (preferably a syntactically correct script we could replay). Otherwise, we can't help.

zohaze (Sep 21 2022 at 00:49):

Goal (forall a b, a <= b -> S a <= b) -> False.
intros;lia.

With specialize case it works but intros ; lia without specialize case it does not work (does not find witness).Why lia is not helpful here? Why we are giving particular case here?

Pierre Castéran (Sep 21 2022 at 10:48):

The statement of ab would mean "it's never the case that both a <= band a<bhold ". It's clearly false.
Please mind quantifiers scope!

In https://coq.inria.fr/distrib/current/refman/addendum/micromega.html#coq:tacn.lia, there is a description of the kind of formulas liaand a few other similar tactics are supposed to solve. The considered goal (with an inner quantification) is not in the shown domain.

zohaze (Sep 22 2022 at 11:39):

Thanks. First i import Lia, then copy lemma ab. Still i am unable to run code because of error "cannot find witness".

Pierre Castéran (Sep 22 2022 at 14:14):

You try to prove a false statement. Take for example a=1 and b=3.

zohaze (Sep 23 2022 at 14:02):

Actually both are true. If have only relation( a <= b) , then could i prove S a <= b ? For this i am using command " rewrite Le.le_Sn_le." .But get different behaviour.

Last updated: Feb 01 2023 at 13:03 UTC