Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Regression of lia ? #11191

Closed
erikmd opened this issue Nov 26, 2019 · 1 comment · Fixed by #11362
Closed

Regression of lia ? #11191

erikmd opened this issue Nov 26, 2019 · 1 comment · Fixed by #11362
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.
Milestone
8.11.0

Comments

@erikmd
Copy link
Member

erikmd commented Nov 26, 2019 •
edited

Description of the problem

When recompiling (some dev branch of) coq-interval with coq master with @proux01, we noticed what appears to be a regression of lia.

Minimal working example:

Require Import ZArith Psatz.

Goal forall p, (0 < Z.pos (p ^ 2))%Z.
intros.
Fail lia. (* worked with 8.10 *)
Abort.

Goal forall p n, (0 < Z.pos (p ^ n))%Z.
intros.
Fail lia. (* worked with 8.10 *)
Abort.

Cc @fajb

As an aside, do you think coq-interval could be added to Coq's CI? Cc @silene

Coq Version

coq master, compiled a few days ago;
still reproducible with 0e9cd0f
@erikmd erikmd added part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic. kind: bug An error, flaw, fault or unintended behaviour. labels Nov 26, 2019
@fajb
Copy link
Contributor

fajb commented Nov 26, 2019

Thanks for the report.
zify is doing a better job and this has a bad side-effect:

  p, n : positive
  cstr : (0 < Z.pos n)%Z
  cstr0 : (0 < Z.pos p)%Z
  ============================
  (0 < Z.pos p ^ Z.pos n)%Z

The workaround is to add saturation rules for Zpower. I'll propose a PR for that.

fajb added a commit that referenced this issue Dec 4, 2019
@fajb
[micromega] support for boolean operators, efficiency and bug fixes
3d413c3 
- New feature: support for boolean operators
  The following operators are now handled
  andb, orb, eqb, implb, Z.{eqb, leb, ltb, geb, gtb}

- Optimisation
  * interval analysis for product of variables
  * aggressive pruning of hypotheses
  * on-the-fly introduction of positivity constraints

fixes #11191, fixes #9615
fajb added a commit that referenced this issue Dec 4, 2019
@fajb
[micromega] support for boolean operators, efficiency and bug fixes
1bc3e93 
- New feature: support for boolean operators
  The following operators are now handled
  andb, orb, eqb, implb, Z.{eqb, leb, ltb, geb, gtb}

- Optimisation
  * interval analysis for product of variables
  * aggressive pruning of hypotheses
  * on-the-fly introduction of positivity constraints

fixes #11191, fixes #9615
@fajb fajb mentioned this issue Dec 4, 2019
Closed
fajb added a commit to fajb/coq that referenced this issue Dec 5, 2019
@fajb
[micromega] support for boolean operators, efficiency and bug fixes
bd0364c 
- New feature: support for boolean operators
  The following operators are now handled
  andb, orb, eqb, implb, Z.{eqb, leb, ltb, geb, gtb}

- Optimisation
  * interval analysis for product of variables
  * aggressive pruning of hypotheses
  * on-the-fly introduction of positivity constraints

fixes coq#11191, fixes coq#9615
fajb added a commit to fajb/coq that referenced this issue Dec 5, 2019
@fajb
[micromega] support for boolean operators, efficiency and bug fixes
8347ba4 
- New feature: support for boolean operators
  The following operators are now handled
  andb, orb, eqb, implb, Z.{eqb, leb, ltb, geb, gtb}

- Optimisation
  * interval analysis for product of variables
  * aggressive pruning of hypotheses
  * on-the-fly introduction of positivity constraints

fixes coq#11191, fixes coq#9615
fajb added a commit to fajb/coq that referenced this issue Dec 6, 2019
@fajb
[micromega] efficiency and bug fixes
0e3f9b0 
- PR coq#9725 fixes completness bugs introduces some inefficiency.
  The current PR intends to fix the inefficiency
  while retaining completness. The fix removes a pre-processing
  step and instead relies on a more elaborate proof
  format introducing positivity constraints on the fly.

fixes coq#11063, fixes coq#11242

- Better interval analysis for product of variables.
  (fixes coq#11191 , first case)

- Generation of positivity constrains for Z.pow
  (fixes coq#11191 , second case)

- More aggressive pruning of (useless) hypotheses
fajb added a commit to fajb/coq that referenced this issue Jan 6, 2020
@fajb
[micromega] partial fix of bug coq#11191
d0719ab 
Add an instance to ZifyInst to instruct zify that
 0 < x -> 0 < y -> 0 < Z.pow x y
fajb added a commit to fajb/coq that referenced this issue Jan 6, 2020
@fajb
[micromega] bugfix coq#11191
bd0d3a8 
More aggressive interval analysis to bound non-linear monomials.
@fajb fajb mentioned this issue Jan 6, 2020
Merged
1 task
fajb added a commit to fajb/coq that referenced this issue Jan 6, 2020
@fajb
[micromega] fix of bug coq#11191
cb9c016 
- Add an instance to ZifyInst to instruct zify that
 0 < x -> 0 < y -> 0 < Z.pow x y

- More aggressive interval analysis to bound non-linear monomials.
fajb added a commit to fajb/coq that referenced this issue Jan 6, 2020
@fajb
[micromega] fix of bug coq#11191
97bec68 
- Add an instance to ZifyInst to instruct zify that
 0 < x -> 0 < y -> 0 < Z.pow x y

- More aggressive interval analysis to bound non-linear monomials.
@coqbot coqbot added this to the 8.11.0 milestone Jan 17, 2020
ppedrot pushed a commit to ppedrot/coq that referenced this issue Jan 19, 2020
@fajb @ppedrot
[micromega] fix of bug coq#11191
f5c7322 
- Add an instance to ZifyInst to instruct zify that
 0 < x -> 0 < y -> 0 < Z.pow x y

- More aggressive interval analysis to bound non-linear monomials.

(cherry picked from commit 97bec68)
fajb added a commit to fajb/coq that referenced this issue Jan 20, 2020
@fajb
[zify] quick fix of coq#11191
269651e 
Z.pow_pos is defined in the separate ZifyPow.v
@fajb fajb mentioned this issue Jan 20, 2020
Merged
2 tasks
fajb added a commit to fajb/coq that referenced this issue Jan 20, 2020
@fajb
[zify] quick fix of coq#11191
10fe534 
Z.pow_pos is defined in the separate ZifyPow.v
ppedrot added a commit that referenced this issue Jan 21, 2020
@ppedrot
Merge PR #11430: [zify] quick fix of #11191
b5fcfc8 
Reviewed-by: ppedrot
Zimmi48 added a commit to Zimmi48/coq that referenced this issue Jan 22, 2020
@Zimmi48
Add ZifyPow module, forgotten in coq#11191.
0e86a8d
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.
Projects
None yet
Milestone
8.11.0
Development

Successfully merging a pull request may close this issue.

Lia bugfix 11191 fajb/coq
3 participants
@fajb @erikmd @coqbot