fix Coq workshop

paper/no.tex

@@ -65,7 +65,7 @@ Unfortunately, there is currently no support for solving goals that are
 expressed in the combined decidable logic fragments of EUF~\cite{Ackermann} (Equality Logic with
 Uninterpreted Functions) and LIA~\cite{presburger} (Linear Integer Arithmetic).
 %
-Yet, \icoq{congruence}\footnote{\url{https://coq.inria.fr/refman/proof-engine/tactics.html\#coq:tacn.congruence}}~\cite{Corbineau06} subsumes EUF and \icoq{lia}\footnote{\url{https://coq.inria.fr/refman/addendum/micromega.html\#coq:tacn.lia}}~\cite{BessonCP11,Besson06} solves LIA.
+Yet, \icoq{congruence}\footnote{\url{https://coq.inria.fr/distrib/V8.13.0/refman/proofs/automatic-tactics/logic.html\#coq:tacn.congruence}}~\cite{Corbineau06} subsumes EUF and \icoq{lia}\footnote{\url{https://coq.inria.fr/distrib/V8.13.0/refman/addendum/micromega.html\#coq:tacn.lia}}~\cite{BessonCP11,Besson06} solves LIA.
 Moreover, Nelson and Oppen~\cite{NelsonO79} propose a combination scheme which is complete for the combination EUF+LIA.
 
 In the following, we present our \icoq{smt}
@@ -93,10 +93,10 @@ Proof. intros. assert (x = y+1) by congruence. assert (x-y = 1) by lia. congruen
 \end{example}
 
 \section{Nelson-Oppen Algorithm}
-The first task of the \icoq{smt} tactic is to identify equalities that
-are worth being propagated. This is done by the so-called
-\emph{purification} phase. The second task consists in propagating
-equalities until the goal is solved. These two phases are implemented
+The first task of the \icoq{smt} tactic is the so-called
+\emph{purification} phase which identifies terms that are shared across
+theories. The second task consists in propagating equalities between
+\emph{pure} terms until the goal is solved. These two phases are implemented
 as an OCaml plugin.
 
 \paragraph{Purification}

test-suite/no_test_lia.v

@@ -74,3 +74,16 @@ Proof.
   intros.
   smt.
 Qed.
+
+(* Reviewer 1 Coq Workshop 2021 (worst-case) *)
+
+Goal forall f x0 x1 x2 x3 x4,
+    f (x0 + 0)%Z    = 0%Z ->
+    f (x1 + f x0)%Z = 0%Z ->
+    f (x2 + f x1)%Z = 0%Z ->
+    f (x3 + f x2)%Z = 0%Z ->
+    f (x4 + f x3)%Z = 0%Z ->
+    f x4 = 0%Z.
+Proof.
+Time intros; smt.
+Qed.