coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] lia handling of equalities

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] lia handling of equalities
Date: Tue, 20 Apr 2021 22:23:58 +0200
Ironport-hdrordr: A9a23:M6K5CK0OnUySrnvKlUgt7AqjBKUkLtp033Aq2lEZdDV5etGV/vrEoN01zhnx4Qx9ZFgFlcqbMKeNBVPQnKQe3aArMb2vXBbrtQKTRelfxLH/yD7tETCWzIFg/JpnGpITNOHN

>
> Is this expected from the `lia` tactic?

Yes it is a known issue

https://github.com/coq/coq/issues/13794

Sometimes lia is not capable to build the witness of the contraction :
it is too big. You are fortunate subst makes it find a short-cut.

Your problem could be solved in future version of Coq (I did not check
with master)

--
Laurent

[Coq-Club] lia handling of equalities, Basile Clement, 04/20/2021
- Re: [Coq-Club] lia handling of equalities, Frédéric Besson, 04/20/2021
  - Re: [Coq-Club] lia handling of equalities, Basile Clement, 04/21/2021
- Re: [Coq-Club] lia handling of equalities, Laurent Thery, 04/20/2021