# \#coq-equations

**URL:** https://discourse.rocq-prover.org/tag/coq-equations/1.md

[Latest](https://discourse.rocq-prover.org/latest.md) · [Categories](https://discourse.rocq-prover.org/categories.md) · [Tags](https://discourse.rocq-prover.org/tags.md)

---

## [How do I write a summation on Coq?](https://discourse.rocq-prover.org/t/how-do-i-write-a-summation-on-coq/1869)

<div class="topic-metadata">

**Author:** [@icarosadero](https://discourse.rocq-prover.org/u/icarosadero)\
**Replies:** 2\
**Last updated:** [January 9, 2023, 11:38am UTC](https://discourse.rocq-prover.org/t/how-do-i-write-a-summation-on-coq/1869 "2023-01-09T11:38:05Z")

</div>

I have just started getting acquainted with Coq and I would like to write this sum on it: \\sum\_{p=1}^{n} \\frac{\\mathrm{d}^p}{\\mathrm{d}x^p} f(x) This is what I have tried: Require Import Coquelicot.Coquelicot. Requir…

---

## [Can the Equations plugin generate a graph that does not reference the original function?](https://discourse.rocq-prover.org/t/can-the-equations-plugin-generate-a-graph-that-does-not-reference-the-original-function/1445)

<div class="topic-metadata">

**Author:** [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Replies:** 1\
**Last updated:** [September 22, 2021, 3:07pm UTC](https://discourse.rocq-prover.org/t/can-the-equations-plugin-generate-a-graph-that-does-not-reference-the-original-function/1445 "2021-09-22T15:07:50Z")

</div>

I’m experimenting with the equations plugin, and I’m surprised by the graphs that it generates. Here is an example: From Equations Require Import Equations. Inductive Arith := | Const (n: nat) | Plus (a1 a2: Arith). …

---

## [Why Coq cannot compute the equality of two Real number (like R1,1,2,3) directly?](https://discourse.rocq-prover.org/t/why-coq-cannot-compute-the-equality-of-two-real-number-like-r1-1-2-3-directly/1304)

<div class="topic-metadata">

**Author:** [@zhengpushi](https://discourse.rocq-prover.org/u/zhengpushi)\
**Replies:** 2\
**Last updated:** [May 17, 2021, 9:15am UTC](https://discourse.rocq-prover.org/t/why-coq-cannot-compute-the-equality-of-two-real-number-like-r1-1-2-3-directly/1304 "2021-05-17T09:15:12Z")

</div>

Hi everyone: I am designing some functions about R type in the Coq standard library Coq.Reals. I’m so sad that I can’t find/write a function to calculate equality of two Real numbers. code detail (under Coq 8.13): F…

---

## [Equations 1.2.4 release](https://discourse.rocq-prover.org/t/equations-1-2-4-release/1236)

<div class="topic-metadata">

**Author:** [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Replies:** 0\
**Last updated:** [March 17, 2021, 11:03am UTC](https://discourse.rocq-prover.org/t/equations-1-2-4-release/1236 "2021-03-17T11:03:54Z")

</div>

I am happy to announce availability of equations 1.2.4, a bugfix release that improves the compatibility of equations with ssreflect’s tactics and has more robust automated proofs of the elimination principle associated …

---

## [Equations 1.2.2 for Coq 8.11 and Coq 8.12](https://discourse.rocq-prover.org/t/equations-1-2-2-for-coq-8-11-and-coq-8-12/895)

<div class="topic-metadata">

**Author:** [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Replies:** 0\
**Last updated:** [June 20, 2020, 12:45pm UTC](https://discourse.rocq-prover.org/t/equations-1-2-2-for-coq-8-11-and-coq-8-12/895 "2020-06-20T12:45:07Z")

</div>

It is my pleasure to announce the release of Equations 1.2.2 for Coq 8.11 and Coq 8.12. Equations 1.2.2 is a bugfix release of the 1.2 version solving a number of issues detailed in the release notes, notably on the depe…

---

## [Equations, Elimination into Type](https://discourse.rocq-prover.org/t/equations-elimination-into-type/176)

<div class="topic-metadata">

**Author:** [@gert-smolka](https://discourse.rocq-prover.org/u/gert-smolka)\
**Replies:** 2\
**Last updated:** [March 19, 2019, 7:32pm UTC](https://discourse.rocq-prover.org/t/equations-elimination-into-type/176 "2019-03-19T19:32:26Z")

</div>

As is, elimination with funelim is restricted to Prop. It seems to me that elimination into Type should be fine (since the underlying Acc allows elimination into Type).

---

## [Equations, funelim and new variables](https://discourse.rocq-prover.org/t/equations-funelim-and-new-variables/172)

<div class="topic-metadata">

**Author:** [@gert-smolka](https://discourse.rocq-prover.org/u/gert-smolka)\
**Replies:** 3\
**Last updated:** [March 19, 2019, 7:31pm UTC](https://discourse.rocq-prover.org/t/equations-funelim-and-new-variables/172 "2019-03-19T19:31:03Z")

</div>

I’m very happy with the funelim tactic except for the new variable names it introduces. I would like to control the names chosen (as with the induction tactic). Currently I use for instance funelim (dnf C D); re…

---

## [Equations 1.2beta2](https://discourse.rocq-prover.org/t/equations-1-2beta2/232)

<div class="topic-metadata">

**Author:** [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Replies:** 0\
**Last updated:** [March 19, 2019, 7:28pm UTC](https://discourse.rocq-prover.org/t/equations-1-2beta2/232 "2019-03-19T19:28:24Z")

</div>

Equations 1.2beta2 is out on opam and sources are available on github! It fixes a few issues that were mentionned here :wink: Enjoy! http://mattam82.github.io/Coq-Equations/equations/2019/03/19/1.2beta2.html

---

## [Trouble in implementing dependently typed lookup in Coq using Equations](https://discourse.rocq-prover.org/t/trouble-in-implementing-dependently-typed-lookup-in-coq-using-equations/198)

<div class="topic-metadata">

**Author:** [@rodrigogribeiro](https://discourse.rocq-prover.org/u/rodrigogribeiro)\
**Replies:** 2\
**Last updated:** [March 7, 2019, 4:21pm UTC](https://discourse.rocq-prover.org/t/trouble-in-implementing-dependently-typed-lookup-in-coq-using-equations/198 "2019-03-07T16:21:50Z")

</div>

I’m trying to use Equations package to define a function over vectors in Coq. The minimum code that shows the problem that I will describe is available at the following gist: My idea is to code a function that does a …

---

## [Equations and FE](https://discourse.rocq-prover.org/t/equations-and-fe/127)

<div class="topic-metadata">

**Author:** [@gert-smolka](https://discourse.rocq-prover.org/u/gert-smolka)\
**Replies:** 4\
**Last updated:** [February 26, 2019, 8:46pm UTC](https://discourse.rocq-prover.org/t/equations-and-fe/127 "2019-02-26T20:46:06Z")

</div>

The Equations package uses FE (functional extensionality) to prove the unfolding equation needed for the realization of well-founded recursion. It seems that this generous use of the axiom functional\_extensionality\_dep …