Skip to Content.
Sympa Menu

coq-club - [Coq-Club] lia handling of equalities

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] lia handling of equalities


Chronological Thread 
    < Chronological >      < Thread >
  • From: Basile Clement <basile AT clement.pm>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] lia handling of equalities
  • Date: Tue, 20 Apr 2021 18:36:58 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=basile AT clement.pm; spf=Pass smtp.mailfrom=basile AT clement.pm; spf=None smtp.helo=postmaster AT tobiko.clement.pm
  • Ironport-hdrordr: A9a23:4KhS5akd+ovQkgxHP94CtIeZne/pDfPhimdD5ilNYBxZY6Wkvuqpm+kW0gKxtSYJVBgb6Le9EYSjYVeZz5565oENIayvNTOK1FeAAYl+4eLZrQHINDb58odmtJtIVqhlFZnNCkJnhtzx+wmyH78bsb+62YWpn/qb83B2UQpxYbph5As8MwCADyRNNXB7LL4YMLbZ2cZdvTqnfh0sH6CGL10IRfLKqdGOtL+OW3E7LiUq4gWPkj+kgYSSe3Kl9ywTSjZehYolmFKkryXD6ri+qPb+8xfA1gbohKh+otfnx9dZbfb86fQ9ECnmiQqjee1aKti/lQ0yydvfimoCoZ2W/04nPYBYy165RBDPnTLdnyPc+gtry1KK8y7pvVLT5ebwQCszC8RHwapSbxvH61cx+PFQuZg7p16xht58DBvGmyj5o/jkPisa7HackD4MneIfhHRUU88/RdZq3P0i1XIQNJ8BGS7ggbpXbdVGPYXm6OtLalTfVnjFvy1PwNuwN05DYiuucww4vNOU1DYTtnh81kMZyssekx47he0AYqgB3OLaMqNn0JFCJ/VmE55AOA==
  • Ironport-phdr: A9a23:Zv5m1x9zCLi7C/9uWf+8ngc9DhMPi/DPJgcQr6AfoPdwSMyLwZ3uMQTl6Ol3ixeRBMOHsqMC0bKL+Pu/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe5bL9oMhm6sQXcusYYjIZgN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gqFGrhyhuRJxzZLbb4+aO/dle6PRYckXSHBdUstLVSFMBJ63YYsVD+oGOOZVt5TwqEEVrRu/AQmjGv7kxyFMhnDo2K01zeIhER3b1wEnBN0Bqm/UrNTxNKgMSu260K3IwivGb/xI3zf99JLEcggkofyVW797bMXex1U1GQzfklWQtZLqPymT1ukVvGaW7OVtWOauhmM7pQx8piajy9sxhoTUhY8YxV/J+CF3zos2KtC1Rk92bN6qHZVety+UOZd7T98sTW9otis3zrsLsoO4cigS0JkqxwTTZvidf4WK5h/vTvudLDd2iX59Zr6wnQq+/VWlx+LiSsW7ylNHoypFn9XRs30ByQLf5tSCR/Z/8EqtxDOC2x7N5exHL0A5kKnWJIM8zbEtk5cfrEfOEy34mEjwkaSYbF8r+vKy5OTierjmpoGTN4tzigzmLqQundewAeU7MggJRWSU5eC826Pm/ULnRrVKkuc6krHcsJzCJMQboLC2AxNN34sj8RqyCy2q3dYckHUdMV5IeByKg5DsO17UIfD4Cfm/g06rkDdu3/3JJafuAo7MLnjHjrjsZqpy60pCxwo2099f4Y5UBqsZIPL2QkPxrsDXDgclMwyoxObqEMly1oQHWW6WHqCZNL7SvkST6+I0I+iMYZcVtyznJ/gk4f7ul345lkUHcamnx5tEIEy/S/9hOgCSZWfmqtYHC2YD+AQkH8Lwj1jXezdIZnK/F4k46zQ2Dp7uWY3KXYGpjZSK2Cq+E5tKIHhDXAPfWUz0fpmJDq9fIBmZJdVsx2RsfYjkcJco0FSVjCG/y7djKYL85ioStJHkktNx6ujekw107TkmV6y14yS2V2hx21gwaXoz1aF7r1Z6zz+r2qx1hvFeCZpL4qEQOi8KcKXExuk/MOjcHxrbd7+hQ1KrR9igHXcpS4Bpq+I=
Dear Coq-Club,

It seems like `lia` fails on some goals containing equalities, but
succeeds after a simple application of the `subst` tactic. See
attached .v file for such an example.

I was surprised by this, because I assumed that exploiting
substitutions (i.e. equalities where one side is a variable) would be
generally beneficial due to reducing the number of variables to handle.

Is this expected from the `lia` tactic?

Regards,
- Basile
Require Import ZArith Psatz.
Open Scope Z_scope.

Goal
  forall n n0 n1 n2 n3 n4 n5 n6 n7 : Z,
    0 <= n0
    -> n0 < n - 2
      -> 0 <= n1
        -> n1 < n0 + 2 - 1
          -> 0 <= n2
            -> n2 < n - (n1 + 1)
              -> n1 + 1 = n4
                -> n0 + 2 = n3
                  -> n1 + 1 - 1 = n7
                    -> n1 + 1 = n6
                      -> n0 + 2 = n5
                        -> (0 < n2
                           /\ ((- n4 + n1 + 2 = 0 /\ n3 - n0 - 2 = 0)
                              /\ n7 - n1 - 1 = 0
                                /\ - n6 + n1 + 2 = 0 /\ n5 - n0 - 2 = 0)
                             /\ (0 < - n2 + 2
                                \/ - n4 + n1 + 3 <> 0 \/ n3 - n0 - 2 <> 0)
                               /\ ((0 < - n4 + n1 + 3 \/ 0 < n4 - n1 - n2 - 1)
                                  \/ n3 - n0 - 2 <> 0)
                           \/ (0 < n4 - n1 - 1 /\ 0 < - n4 + n1 + n2 + 2)
                             /\ n3 - n0 - 2 = 0
                               /\ n7 - n1 - 1 = 0
                                 /\ - n6 + n4 = 0 /\ n5 - n0 - 2 = 0
                             \/ (0 < n6 - n1 - 1 /\ 0 < - n6 + n1 + n2 + 2)
                               /\ ((n6 - n4 = 0 /\ n3 - n0 - 2 = 0)
                                  /\ n7 - n1 - 1 = 0 /\ n5 - n0 - 2 = 0)
                                 /\ (0 < n6 - n1 - n2
                                    \/ n6 - n4 + 1 <> 0 \/ n3 - n0 - 2 <> 0)
                                   /\ ((0 < n6 - n4 + 1 \/ 0 < n4 - n1 - n2 - 1)
                                      \/ n3 - n0 - 2 <> 0)
                               \/ 0 < n2
                                 /\ ((- n4 + n1 + n2 + 1 = 0 /\ n3 - n0 - 2 = 0)
                                    /\ n7 - n1 - 1 = 0
                                      /\ - n6 + n1 + n2 + 1 = 0
                                        /\ n5 - n0 - 2 = 0)
                                   /\ ((0 < - n4 + n1 + n2 + 2
                                       \/ 0 < n4 - n1 - n2 - 1)
                                      \/ n3 - n0 - 2 <> 0)
                                 \/ (0 < n4 - n1 - 1 /\ 0 < - n4 + n1 + n2 + 2)
                                   /\ n3 - n0 - 2 = 0
                                     /\ n7 - n1 - 1 = 0
                                       /\ - n6 + n4 = 0 /\ n5 - n0 - 2 = 0
                                   \/ (0 < n4 - n1 - 1 /\ 0 < - n4 + n1 + n2 + 2)
                                     /\ n3 - n0 - 2 = 0
                                       /\ n7 - n1 - 1 = 0
                                         /\ - n6 + n4 = 0 /\ n5 - n0 - 2 = 0)
                          \/ (0 < - n2 + 1 \/ - n4 + n1 + 2 <> 0 \/ n3 - n0 - 2 <> 0)
                            /\ ((0 < - n4 + n1 + 2 \/ 0 < n4 - n1 - n2 - 1)
                               \/ n3 - n0 - 2 <> 0).
Proof. 
  intros. 
  (* Time lia. *)
  (* Finished failing transaction in 18.923 secs (18.529u,0.13s) (failure)

     Stack overflow.
  *)
  subst.
  Time lia. 
  (* Finished transaction in 0.007 secs (0.007u,0.s) (successful) *)
Qed.

Archive powered by MHonArc 2.6.19+.

Top of Page