When performing proofs about mathematical formulas, it is often enough to perform small computation on the shape of the statement rather than complex reasoning on the meaning of all its components. These computations can be programmed directly in Coq, as long as we define a language to describe the shapes…
There are several types of numbers, and these can be arranged in two categories. The inductive types: nat, positive, Z, … the axiomatized types: R is the prominent one The difference comes in how to compute with these numbers. If a type is inductive then we know how to describe…
This example was sent to me by Matej Kosik, in preparation for a Coq Implementors Workshop. (* ————————————————————————– *) (* *) (* Initial ritual dance *) (* *) (* ————————————————————————– *) DECLARE PLUGIN “demo” (* Use this macro before any of the other Ocaml macros. Each plugin has a unique…
In an article with David Pichardie that dates back to 2001, we consider determinants to compute the oriented surface of triangles, of the following form In some place, we need a formula that is called Cramer’s formula, which can be summarized as follows: In more recent work, I wish to…
In a talk at Isaac Newton Institute during the Big Proofs seminar, Joe Korneli referred to a problem that he attributes to T. Gowers What is the 500th decimal of ? He describes how mathematics are discovered, what kind of trials and discussions may happen. It is not the point…
I happen to serve on a regular basis as a reviewer for submissions dealing with formalized mathematics. These submissions often consist of regular papers, accompanied with the source code of a library of formal proofs. This source code is meant to be machine-checked with a certain proof assistant. Inspecting a…
Cyril Cohen published an extension to the Mathematical Components library to handle finite subsets of types. In the course of experimenting with this extension, I need to generalize a lemma that already exists for finite subsets of finite types to finite sets. The lemma is stated in the Mathematical Components…
Today, I wish to show how to prove the computation of a well-known integral. I am using Coquelicot 2.1.1. The integral is as follows and m is positive. There is a lemma named is_RInt_derive with the following statement: forall (f df : R -> R) (a b : R), (forall…
I am using the Coquelicot library to describe a variety of proofs around real numbers. For one of my experiments, I need to work with improper integrals, in particular, integrals where one of the bounds is at infinity. To state a theorem of dominated convergence, I need to express that…
