8000 `firstorder lia` is slow and fails with "reversible in 1st order mode" · Issue #12687 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

firstorder lia is slow and fails with "reversible in 1st order mode" #12687

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
Open
samuelgruetter opened this issue Jul 13, 2020 · 1 comment
Open

firstorder lia is slow and fails with "reversible in 1st order mode" #12687

samuelgruetter opened this issue Jul 13, 2020 · 1 comment
Labels
kind: performance Improvements to performance and efficiency. part: firstorder Issues and PRs about the firstorder tactic.

Comments

@samuelgruetter
Copy link
Contributor 
Require Import Coq.ZArith.ZArith.
Require Import Coq.Strings.String.
Require Import Coq.micromega.Lia.

Open Scope Z_scope.

Axiom src2imp: Type.
Definition fake{T: Type}: T. Admitted.

Module map.
  Definition injective: src2imp -> Prop := fake.
  Definition get: src2imp -> string -> option Z := fake.
End map.

Axiom dom_bound: src2imp -> Z -> Prop.

Goal forall (x : string) (r2 : src2imp) (av2 : Z) (r : src2imp) (z : Z),
  map.injective r2 ->
  (forall (x0 : string) (w : Z), map.get r x0 = Some w -> map.get r2 x0 = Some w) ->
  z <= av2 ->
  dom_bound r2 av2 ->
  (forall (x0 : string) (y : Z), map.get r2 x0 = Some y -> z <= y < av2 \/ map.get r x0 = Some y) ->
  forall (r1 : src2imp) (av1 z0 : Z),
  map.injective r1 ->
  dom_bound r1 av1 ->
  map.injective r ->
  (forall (x0 : string) (w : Z), map.get r1 x0 = Some w -> map.get r x0 = Some w) ->
  av1 <= z ->
  dom_bound r z ->
  (forall (x0 : string) (y : Z), map.get r x0 = Some y -> av1 <= y < z \/ map.get r1 x0 = Some y) ->
  map.get r x = Some z0 ->
  map.injective r ->
  (forall (x0 : string) (w : Z), map.get r1 x0 = Some w -> map.get r x0 = Some w) ->
  av1 <= z ->
  dom_bound r z ->
  (forall (x0 : string) (y : Z), map.get r x0 = Some y -> av1 <= y < z \/ map.get r1 x0 = Some y) ->
  map.get r x = Some z0 ->
  forall (x0 : string) (y : Z), map.get r2 x0 = Some y -> av1 <= y < av2 \/ map.get r1 x0 = Some y.
Proof.
  (* firstorder lia. Takes ~25s and fails with "Error: Tactic failure: reversible in 1st order mode." *)
  intros.
  specialize H3 with (1 := H18).
  destruct H3 as [D | D].
  + left. lia.
  + specialize H16 with (1 := D).
    destruct H16 as [D' | D'].
    * left. lia.
    * right. assumption.
Qed.

As far as I understand, the above goal is part of the fragment that firstorder lia should be able to solve.
However, it runs for about 25 seconds and then fails with Error: Tactic failure: reversible in 1st order mode.

Desired behavior: It should solve the goal in, say, less than 1s.

Coq version: 8.11.0

/cc @PierreCorbineau
@ppedrot ppedrot added the kind: performance Improvements to performance and efficiency. label Jul 13, 2020
This was referenced Jul 21, 2020
Open
Open
@mrhaandi
Copy link
Contributor
mrhaandi commented Aug 4, 2021

(* firstorder lia. Takes ~25s and fails with "Error: Tactic failure: reversible in 1st order mode." *)

For reference, the goal can be solved in about a minute (Coq 8.13.2) by

Set Firstorder Depth 4.
firstorder lia.

@Alizter Alizter added the part: firstorder Issues and PRs about the firstorder tactic. label Aug 4, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: performance Improvements to performance and efficiency. part: firstorder Issues and PRs about the firstorder tactic.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@ppedrot @samuelgruetter @Alizter @mrhaandi
0