(proof-new) Add proofs for sine lemmas in the transcendental solver (#5952)

This PR adds proofs for the lemmas related to the sine function in the transcendental solver.
It introduces several new proof rules with corresponding proof checkers and produces proofs in the sine solver.

6 files changed, 395 insertions, 14 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 4fce88a39..a5dde78ab 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -162,7 +162,21 @@ const char* toString(PfRule id)
     case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
     case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
     case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI";
+    case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS";
     case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT";
+    case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY";
+    case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO:
+      return "ARITH_TRANS_SINE_TANGENT_ZERO";
+    case PfRule::ARITH_TRANS_SINE_TANGENT_PI:
+      return "ARITH_TRANS_SINE_TANGENT_PI";
+    case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG:
+      return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG";
+    case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS:
+      return "ARITH_TRANS_SINE_APPROX_ABOVE_POS";
+    case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG:
+      return "ARITH_TRANS_SINE_APPROX_BELOW_NEG";
+    case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS:
+      return "ARITH_TRANS_SINE_APPROX_BELOW_POS";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";
     default: return "?";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 9b7a54a09..28ea24533 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -1112,6 +1112,13 @@ enum class PfRule : uint32_t
   // Conclusion: (and (>= real.pi l) (<= real.pi u))
   // Where l (u) is a valid lower (upper) bound on pi.
   ARITH_TRANS_PI,
+
+  //======== Sine is always between -1 and 1
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (and (<= (sin t) 1) (>= (sin t) (- 1)))
+  ARITH_TRANS_SINE_BOUNDS,
   //======== Sine arg shifted to -pi..pi
   // Children: none
   // Arguments: (x, y, s)
@@ -1125,6 +1132,84 @@ enum class PfRule : uint32_t
   // into -pi..pi and s is a new integer skolem that is the number of phases y
   // is shifted.
   ARITH_TRANS_SINE_SHIFT,
+  //======== Sine is symmetric with respect to negation of the argument
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (= (- (sin t) (sin (- t))) 0)
+  ARITH_TRANS_SINE_SYMMETRY,
+  //======== Sine is bounded by the tangent at zero
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (and
+  //   (=> (> t 0) (< (sin t) t))
+  //   (=> (< t 0) (> (sin t) t))
+  // )
+  ARITH_TRANS_SINE_TANGENT_ZERO,
+  //======== Sine is bounded by the tangents at -pi and pi
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (and
+  //   (=> (> t -pi) (> (sin t) (- -pi t)))
+  //   (=> (< t pi) (< (sin t) (- pi t)))
+  // )
+  ARITH_TRANS_SINE_TANGENT_PI,
+  //======== Sine is approximated from above for negative values
+  // Children: none
+  // Arguments: (d, t, lb, ub, l, u)
+  // ---------------------
+  // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (secant sin l u t))
+  // Where d is an even positive number, t an arithmetic term, lb (ub) a
+  // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
+  // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
+  // zero (also called the Maclaurin series) of the sine function. (secant sin l
+  // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
+  // t, calculated as follows:
+  //    (p(l) - p(u)) / (l - u) * (t - l) + p(l)
+  // The lemma states that if t is between l and u, then (sin t) is below the
+  // secant of p from l to u.
+  ARITH_TRANS_SINE_APPROX_ABOVE_NEG,
+  //======== Sine is approximated from above for positive values
+  // Children: none
+  // Arguments: (d, t, c, lb, ub)
+  // ---------------------
+  // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (upper sin c))
+  // Where d is an even positive number, t an arithmetic term, c an arithmetic
+  // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
+  // containing pi). Let p be the d'th taylor polynomial at zero (also called
+  // the Maclaurin series) of the sine function. (upper sin c) denotes the upper
+  // bound on sin(c) given by p and lb,ub are such that sin(t) is the maximum of
+  // the sine function on (lb,ub).
+  ARITH_TRANS_SINE_APPROX_ABOVE_POS,
+  //======== Sine is approximated from below for negative values
+  // Children: none
+  // Arguments: (d, t, c, lb, ub)
+  // ---------------------
+  // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (lower sin c))
+  // Where d is an even positive number, t an arithmetic term, c an arithmetic
+  // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
+  // containing pi). Let p be the d'th taylor polynomial at zero (also called
+  // the Maclaurin series) of the sine function. (lower sin c) denotes the lower
+  // bound on sin(c) given by p and lb,ub are such that sin(t) is the minimum of
+  // the sine function on (lb,ub).
+  ARITH_TRANS_SINE_APPROX_BELOW_NEG,
+  //======== Sine is approximated from below for positive values
+  // Children: none
+  // Arguments: (d, t, lb, ub, l, u)
+  // ---------------------
+  // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (secant sin l u t))
+  // Where d is an even positive number, t an arithmetic term, lb (ub) a
+  // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
+  // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
+  // zero (also called the Maclaurin series) of the sine function. (secant sin l
+  // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
+  // t, calculated as follows:
+  //    (p(l) - p(u)) / (l - u) * (t - l) + p(l)
+  // The lemma states that if t is between l and u, then (sin t) is above the
+  // secant of p from l to u.
+  ARITH_TRANS_SINE_APPROX_BELOW_POS,
 
   //================================================= Unknown rule
   UNKNOWN,
diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp
index b5fccac85..bec2bd9b8 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.cpp
+++ b/src/theory/arith/nl/transcendental/proof_checker.cpp
@@ -27,10 +27,47 @@ namespace arith {
 namespace nl {
 namespace transcendental {
 
+namespace {
+
+/**
+ * Helper method to construct (t >= lb) AND (t <= up)
+ */
+Node mkBounds(TNode t, TNode lb, TNode ub)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  return nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::GEQ, t, lb),
+                                     nm->mkNode(Kind::LEQ, t, ub)});
+}
+
+/**
+ * Helper method to construct a secant plane:
+ * ((evall - evalu) / (l - u)) * (t - l) + evall
+ */
+Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  return nm->mkNode(Kind::PLUS,
+                    nm->mkNode(Kind::MULT,
+                               nm->mkNode(Kind::DIVISION,
+                                          nm->mkNode(Kind::MINUS, evall, evalu),
+                                          nm->mkNode(Kind::MINUS, l, u)),
+                               nm->mkNode(Kind::MINUS, t, l)),
+                    evall);
+}
+
+}  // namespace
+
 void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc)
 {
   pc->registerChecker(PfRule::ARITH_TRANS_PI, this);
   pc->registerChecker(PfRule::ARITH_TRANS_SINE_SHIFT, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_SINE_SYMMETRY, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_SINE_TANGENT_ZERO, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_SINE_TANGENT_PI, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG, this);
 }
 
 Node TranscendentalProofRuleChecker::checkInternal(
@@ -53,7 +90,16 @@ Node TranscendentalProofRuleChecker::checkInternal(
     Assert(args.size() == 2);
     return nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::GEQ, pi, args[0]),
                                        nm->mkNode(Kind::LEQ, pi, args[1])});
-  } else if (id == PfRule::ARITH_TRANS_SINE_SHIFT)
+  }
+  else if (id == PfRule::ARITH_TRANS_SINE_BOUNDS)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    Assert(args[0].getType().isReal());
+    Node s = nm->mkNode(Kind::SINE, args[0]);
+    return nm->mkNode(AND, nm->mkNode(LEQ, s, one), nm->mkNode(GEQ, s, mone));
+  }
+  else if (id == PfRule::ARITH_TRANS_SINE_SHIFT)
   {
     Assert(children.empty());
     Assert(args.size() == 3);
@@ -77,6 +123,159 @@ Node TranscendentalProofRuleChecker::checkInternal(
                 nm->mkNode(Kind::MULT, nm->mkConst<Rational>(2), s, pi)))),
         nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))});
   }
+  else if (id == PfRule::ARITH_TRANS_SINE_SYMMETRY)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    Assert(args[0].getType().isReal());
+    Node s1 = nm->mkNode(Kind::SINE, args[0]);
+    Node s2 = nm->mkNode(
+        Kind::SINE, Rewriter::rewrite(nm->mkNode(Kind::MULT, mone, args[0])));
+    return nm->mkNode(PLUS, s1, s2).eqNode(zero);
+  }
+  else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_ZERO)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    Assert(args[0].getType().isReal());
+    Node s = nm->mkNode(Kind::SINE, args[0]);
+    return nm->mkNode(
+        AND,
+        nm->mkNode(
+            IMPLIES, nm->mkNode(GT, args[0], zero), nm->mkNode(LT, s, args[0])),
+        nm->mkNode(IMPLIES,
+                   nm->mkNode(LT, args[0], zero),
+                   nm->mkNode(GT, s, args[0])));
+  }
+  else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_PI)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    Assert(args[0].getType().isReal());
+    Node s = nm->mkNode(Kind::SINE, args[0]);
+    return nm->mkNode(
+        AND,
+        nm->mkNode(IMPLIES,
+                   nm->mkNode(GT, args[0], mpi),
+                   nm->mkNode(GT, s, nm->mkNode(MINUS, mpi, args[0]))),
+        nm->mkNode(IMPLIES,
+                   nm->mkNode(LT, args[0], pi),
+                   nm->mkNode(LT, s, nm->mkNode(MINUS, pi, args[0]))));
+  }
+  else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 6);
+    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+           && args[0].getConst<Rational>().isIntegral());
+    Assert(args[1].getType().isReal());
+    Assert(args[2].getType().isReal());
+    Assert(args[3].getType().isReal());
+    Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL);
+    Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL);
+    std::uint64_t d =
+        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+    Node t = args[1];
+    Node lb = args[2];
+    Node ub = args[3];
+    Node l = args[4];
+    Node u = args[5];
+    TaylorGenerator tg;
+    TaylorGenerator::ApproximationBounds bounds;
+    tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
+    Node evall = Rewriter::rewrite(
+        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), l));
+    Node evalu = Rewriter::rewrite(
+        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), u));
+    Node lem = nm->mkNode(
+        Kind::IMPLIES,
+        mkBounds(t, lb, ub),
+        nm->mkNode(
+            Kind::LEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
+    return Rewriter::rewrite(lem);
+  }
+  else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 5);
+    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+           && args[0].getConst<Rational>().isIntegral());
+    Assert(args[1].getType().isReal());
+    Assert(args[2].getType().isReal());
+    Assert(args[3].getType().isReal());
+    std::uint64_t d =
+        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+    Node t = args[1];
+    Node c = args[2];
+    Node lb = args[3];
+    Node ub = args[4];
+    TaylorGenerator tg;
+    TaylorGenerator::ApproximationBounds bounds;
+    tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
+    Node eval = Rewriter::rewrite(
+        bounds.d_upperPos.substitute(tg.getTaylorVariable(), c));
+    return Rewriter::rewrite(
+        nm->mkNode(Kind::IMPLIES,
+                   mkBounds(t, lb, ub),
+                   nm->mkNode(Kind::LEQ, nm->mkNode(Kind::SINE, t), eval)));
+  }
+  else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 6);
+    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+           && args[0].getConst<Rational>().isIntegral());
+    Assert(args[1].getType().isReal());
+    Assert(args[2].getType().isReal());
+    Assert(args[3].getType().isReal());
+    Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL);
+    Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL);
+    std::uint64_t d =
+        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+    Node t = args[1];
+    Node lb = args[2];
+    Node ub = args[3];
+    Node l = args[4];
+    Node u = args[5];
+    TaylorGenerator tg;
+    TaylorGenerator::ApproximationBounds bounds;
+    tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
+    Node evall =
+        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), l));
+    Node evalu =
+        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), u));
+    Node lem = nm->mkNode(
+        Kind::IMPLIES,
+        mkBounds(t, lb, ub),
+        nm->mkNode(
+            Kind::GEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
+    return Rewriter::rewrite(lem);
+  }
+  else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 5);
+    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+           && args[0].getConst<Rational>().isIntegral());
+    Assert(args[1].getType().isReal());
+    Assert(args[2].getType().isReal());
+    Assert(args[3].getType().isReal());
+    std::uint64_t d =
+        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+    Node t = args[1];
+    Node c = args[2];
+    Node lb = args[3];
+    Node ub = args[4];
+    TaylorGenerator tg;
+    TaylorGenerator::ApproximationBounds bounds;
+    tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
+    Node eval =
+        Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), c));
+    return Rewriter::rewrite(
+        nm->mkNode(Kind::IMPLIES,
+                   mkBounds(t, lb, ub),
+                   nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SINE, t), eval)));
+  }
   return Node::null();
 }
 
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 0cca238b0..f5dc49da8 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -114,14 +114,26 @@ void SineSolver::checkInitialRefine()
           Node lem = nm->mkNode(Kind::AND,
                                 nm->mkNode(Kind::LEQ, t, d_data->d_one),
                                 nm->mkNode(Kind::GEQ, t, d_data->d_neg_one));
-          d_data->d_im.addPendingLemma(lem,
-                                       InferenceId::ARITH_NL_T_INIT_REFINE);
+          CDProof* proof = nullptr;
+          if (d_data->isProofEnabled())
+          {
+            proof = d_data->getProof();
+            proof->addStep(lem, PfRule::ARITH_TRANS_SINE_BOUNDS, {}, {t[0]});
+          }
+          d_data->d_im.addPendingLemma(
+              lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
         }
         {
           // sine symmetry: sin(t) - sin(-t) = 0
           Node lem = nm->mkNode(Kind::PLUS, t, symn).eqNode(d_data->d_zero);
-          d_data->d_im.addPendingLemma(lem,
-                                       InferenceId::ARITH_NL_T_INIT_REFINE);
+          CDProof* proof = nullptr;
+          if (d_data->isProofEnabled())
+          {
+            proof = d_data->getProof();
+            proof->addStep(lem, PfRule::ARITH_TRANS_SINE_SYMMETRY, {}, {t[0]});
+          }
+          d_data->d_im.addPendingLemma(
+              lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
         }
         {
           // sine zero tangent:
@@ -135,8 +147,15 @@ void SineSolver::checkInitialRefine()
                          nm->mkNode(Kind::IMPLIES,
                                     nm->mkNode(Kind::LT, t[0], d_data->d_zero),
                                     nm->mkNode(Kind::GT, t, t[0])));
-          d_data->d_im.addPendingLemma(lem,
-                                       InferenceId::ARITH_NL_T_INIT_REFINE);
+          CDProof* proof = nullptr;
+          if (d_data->isProofEnabled())
+          {
+            proof = d_data->getProof();
+            proof->addStep(
+                lem, PfRule::ARITH_TRANS_SINE_TANGENT_ZERO, {}, {t[0]});
+          }
+          d_data->d_im.addPendingLemma(
+              lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
         }
         {
           // sine pi tangent:
@@ -156,8 +175,15 @@ void SineSolver::checkInitialRefine()
                   nm->mkNode(Kind::LT,
                              t,
                              nm->mkNode(Kind::MINUS, d_data->d_pi, t[0]))));
-          d_data->d_im.addPendingLemma(lem,
-                                       InferenceId::ARITH_NL_T_INIT_REFINE);
+          CDProof* proof = nullptr;
+          if (d_data->isProofEnabled())
+          {
+            proof = d_data->getProof();
+            proof->addStep(
+                lem, PfRule::ARITH_TRANS_SINE_TANGENT_PI, {}, {t[0]});
+          }
+          d_data->d_im.addPendingLemma(
+              lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
         }
         {
           Node lem =
@@ -322,7 +348,8 @@ void SineSolver::checkMonotonic()
   }
 }
 
-void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region)
+void SineSolver::doTangentLemma(
+    TNode e, TNode c, TNode poly_approx, int region, std::uint64_t d)
 {
   NodeManager* nm = NodeManager::currentNM();
 
@@ -338,7 +365,7 @@ void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region)
       nm->mkNode(
           Kind::AND,
           nm->mkNode(
-              Kind::GEQ, e[0], usec ? Node(c) : regionToLowerBound(region)),
+              Kind::GEQ, e[0], usec ? regionToLowerBound(region) : Node(c)),
           nm->mkNode(
               Kind::LEQ, e[0], usec ? Node(c) : regionToUpperBound(region))),
       nm->mkNode(convexity == Convexity::CONVEX ? Kind::GEQ : Kind::LEQ,
@@ -351,8 +378,63 @@ void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region)
   Trace("nl-ext-sine") << "*** Tangent plane lemma : " << lem << std::endl;
   Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
   // Figure 3 : line 9
+  CDProof* proof = nullptr;
+  if (d_data->isProofEnabled())
+  {
+    proof = d_data->getProof();
+    if (convexity == Convexity::CONVEX)
+    {
+      if (usec)
+      {
+        proof->addStep(lem,
+                       PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG,
+                       {},
+                       {nm->mkConst<Rational>(2 * d),
+                        e[0],
+                        c,
+                        regionToLowerBound(region),
+                        c});
+      }
+      else
+      {
+        proof->addStep(lem,
+                       PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG,
+                       {},
+                       {nm->mkConst<Rational>(2 * d),
+                        e[0],
+                        c,
+                        c,
+                        regionToUpperBound(region)});
+      }
+    }
+    else
+    {
+      if (usec)
+      {
+        proof->addStep(lem,
+                       PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS,
+                       {},
+                       {nm->mkConst<Rational>(2 * d),
+                        e[0],
+                        c,
+                        regionToLowerBound(region),
+                        c});
+      }
+      else
+      {
+        proof->addStep(lem,
+                       PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS,
+                       {},
+                       {nm->mkConst<Rational>(2 * d),
+                        e[0],
+                        c,
+                        c,
+                        regionToUpperBound(region)});
+      }
+    }
+  }
   d_data->d_im.addPendingLemma(
-      lem, InferenceId::ARITH_NL_T_TANGENT, nullptr, true);
+      lem, InferenceId::ARITH_NL_T_TANGENT, proof, true);
 }
 
 void SineSolver::doSecantLemmas(TNode e,
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index 5eace6104..da4b48fd6 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -87,7 +87,8 @@ class SineSolver
   void checkMonotonic();
 
   /** Sent tangent lemma around c for e */
-  void doTangentLemma(TNode e, TNode c, TNode poly_approx, int region);
+  void doTangentLemma(
+      TNode e, TNode c, TNode poly_approx, int region, std::uint64_t d);
 
   /** Sent secant lemmas around c for e */
   void doSecantLemmas(TNode e,
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index ee422ebb6..7b87adab1 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -391,7 +391,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
     }
     else if (k == Kind::SINE)
     {
-      d_sineSlv.doTangentLemma(tf, c, poly_approx_c, region);
+      d_sineSlv.doTangentLemma(tf, c, poly_approx_c, region, d);
     }
   }
   else if (is_secant)