Stream: Coq users

Topic: ✔ Searching for tactic


view this post on Zulip Lessness (Oct 15 2022 at 18:04):

How can one prove that set of linear inequalities in real numbers has no solution, using Coq? Is there some tactic that can do that?

view this post on Zulip Karl Palmskog (Oct 15 2022 at 18:06):

this may be the closest: https://github.com/validsdp/validsdp

view this post on Zulip Lessness (Oct 15 2022 at 18:31):

It seems that lra tactic can do that too, if one is careful.

Require Import Reals Psatz.
Open Scope R.

Theorem T01 x1 x2 mu1 mu2 mu3:
  3 * x1 + 2 * x2 <= 18 + mu1 ->
  -3 * x1 + x2 <= 6 + mu2 ->
  4 * x1 - 3 * x2 <= 12 + mu3 ->
  18 + mu1 < 0 ->
  x1 >= 0 ->
  x2 >= 0 ->
  False.
Proof.
  lra.
Qed.

Theorem T02 x1 x2 mu1 mu2 mu3:
  3 * x1 + 2 * x2 <= 18 + mu1 ->
  -3 * x1 + x2 <= 6 + mu2 ->
  4 * x1 - 3 * x2 <= 12 + mu3 ->
  18 + mu1 >= 0 ->
  6 + mu2 >= 0 ->
  12 + mu3 < 0 ->
  9 + mu1 / 2 < -4 - mu3 / 3 ->
  x1 >= 0 ->
  x2 >= 0 ->
  False.
Proof.
  lra.
Qed.

view this post on Zulip Notification Bot (Oct 16 2022 at 11:40):

Lessness has marked this topic as resolved.


Last updated: Feb 05 2023 at 23:30 UTC