Stream: Coq users

Topic: One less than other

zohaze (Sep 08 2022 at 15:50):

Could we convert a = S b into a <= b by le_S command?

Emilio Jesús Gallego Arias (Sep 08 2022 at 15:55):

not likely, as if you replace a by S b in a <= b you get S b <= b

zohaze (Sep 08 2022 at 17:35):

What about this relation

S b > 0 ->
x = S a ->
a <= S b->
x <=b.

a b x are nat

zohaze (Sep 09 2022 at 14:59):

Is above relation between two variables correct?

Mukesh Tiwari (Sep 09 2022 at 15:57):

@zohaze I am assuming you are working with natural numbers. We can assume b = 0 (S b = 1 > 0 holds), assume a = 0 (x = 1), a <= S b (0 <= 1 holds) but your goal x <= b (1 <= 0) does not hold and therefore, it's not provable.

Mukesh Tiwari (Sep 09 2022 at 15:59):

Another way to think: you have assumed a <= S b and then you are trying to prove S a <= b (replace x by S a in the goal).

zohaze (Sep 09 2022 at 17:19):

Ok, thank you.

zohaze (Sep 10 2022 at 04:27):

@Emilio Jesús Gallego Arias . Its means we can prove whole relation is false because S b <= b is wrong.

zohaze (Sep 10 2022 at 04:55):

1) From ( a<=S b) could we prove (a<=b) ? (Reverse of le_S.)
2) From ( a<=S b) could we prove (S a<= b) ?

zohaze (Feb 20 2024 at 16:39):

I have non empty list(k::t) and two hypothesis. H1: k <= list_max (k::t) & H2: list_max (k::t) <=k.
From these H1 and H2 , is it possible list_max (k::t) =k?

Michael Soegtrop (Feb 20 2024 at 16:57):

The lia tactic should be able to do this (assuming the type of k is some well known integer data type). E.g. assert(list_max (k::t) =k) by lia. should work.

Michael Soegtrop (Feb 20 2024 at 17:43):

@zohaze : btw: you can ask all of your above questions to lia. As long as you stay in the domain of linear integer arithmetic (+, -, S, <, <=, > >=, =, multiplication with constants) you can expect lia to give the right answer (prove provable things, fail on unprovable things). Here are a few examples:

Require Import Lia.

Example AskLia1: forall a b,
  a = S b -> a <= b.
Proof.
  intros.
  Fail lia.
Abort.

(* the above is abviously wrong (a=4, b=3 is an example, but we can prove the opposite: *)

Example AskLia2: forall a b,
  a = S b -> ~ (a <= b).
Proof.
  intros.
  lia.
Qed.

Example AskLia3: forall a b x,
  S b > 0 ->
  x = S a ->
  a <= S b->
  x <=b.
Proof.
  intros.
  Fail lia.
Abort.

Example AskLia4: forall a b x,
  (* S b > 0 -> this is always true so useless - see below *)
  x = S a ->
  a <= S b->
  x <= S (S b).
Proof.
  intros.
  lia.
Qed.

Example AskLia5: forall b,
  S b > 0.
Proof.
  intros.
  lia.
Qed.

Last updated: Oct 13 2024 at 01:02 UTC