coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] lia: strange performance behavior

From: Armaël Guéneau <armael.gueneau AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] lia: strange performance behavior
Date: Mon, 12 Nov 2018 21:54:54 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=armael.gueneau AT ens-lyon.fr; spf=Pass smtp.mailfrom=armael.gueneau AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Ironport-phdr: 9a23:UOA2bx2n2NNeFjkAsmDT+DRfVm0co7zxezQtwd8Zse0TK/ad9pjvdHbS+e9qxAeQG9mDtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmlicJOSM6/m/ZhMN/g75Urh26qhxjwIPZep2ZOOZwc67fe94RWGpPXtxWVyxEGo6xc5EPD+8bMuFEq4nyv1oArQakAgmqGuzg0CJIjWLx0KIgyeQhFBvJ0xIkH94Uv3TUscv6NKEMXu+v0anF1ivMb/VN2Tvk7IjJchchofeWUbJ+a8rc0E8iHB7GgFWIsYHpIjyY2vgXv2WZ7edsT/+jhm8lpg1rvDSj2NkghpHKi48W0FzI6CF0zJsvKdGlSUN3f8SoHIZTuiyYMYZ9X9ksTHtyuCkgz70LoZ67czYOyJQg3xPfb+aIfJOT7R39TuqePzF4hGl8dLK7hxey9k6gxvfyVsmuyFpKryxFncfQtn0VyhDe5dSLRuF/80qjwzqDygHe5+NeLUwqi6bXNYYtwrsqmZoStUTDEDX2mELzjKKObEok4O2o5P75bbXivJOcOJJ0hR/4MqswgMO/HP81PRYIX2iA4Oi80L3i/Ur/QLlQgP02iLHVsIrGKsQDuq65HwhV354/5Ba4FjeqycgXnX0aLF1eYx+HlIjoO1TWIP/iF/u/glKskC1qx//cJLHhDI/NfTD/l+Lqeq844EpBwiIyy8pe7tRaEOIvOvX2D2brsdVbCigWLo2yzu/6QIF0zIYXVGbJDbKUNq7brHeF4PlqJ/iLYskbomCueLAe+/fygCphyhcmdq6z0M5PMSHqLrFdO0ycJEHUrJIEGGYOsBA5SbWx2lCESntXdnG0GawmtGhiVNCWSLzbT4Xou4SvmT+hF8QNNG1AERWIAHDuMYueCa9VNXCiZ/R5mzlBboCPDo8s0Rb35V3+wrBtI6zZ/DZdsYPk0p57/b+LmA==

Dear coq-club,

Consider the following proof script:

Require Import ZArith Psatz.
Open Scope Z_scope.

Goal forall a b c,
(((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\
((0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\
((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\
(0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\
((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\
((0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)) /\
((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\
(0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)
->
False.
Proof.
intros.
Time Fail Fail lia. (* Succeeds but takes 6s *)
(* trivially split on /\ by hand *)
repeat match goal with h: _ /\ _ |- _ => destruct h end.
Time lia. (* Takes 0.06s *)
Qed.

Does anyone have an explanation? Why is lia struggling so much on the
first goal, and why does manually splitting conjunctions makes it
suddenly much easier?

Cheers,
Armaël

[Coq-Club] lia: strange performance behavior, Armaël Guéneau, 11/12/2018
- Re: [Coq-Club] lia: strange performance behavior, Frédéric Besson, 11/13/2018