arXiv subjects

Assia Mahboubi

Publications and source records attributed to Assia Mahboubi.

11 recordsLinked to original sources

arXiv2024

Geometric theories for real number algebra without sign test or dependent choice axiom

In this memoir, we seek to construct a constructive theory that is as complete as possible to describe the algebraic properties of the real number field in constructive mathematics without a dependent choice axiom. To this purpose, we use a dynamical version of geometric theories. We obtain a nice description of the algebraic properties of the real number field, but also a first outline for a constructive theory of certain o-minimal structures. The memoir we present here is an unfinished development of the article by the authors https://inria.hal.science/hal-01426164. Compared to that paper, however, we have modified the definition of continuous semialgebraic functions, in the same spirit in which Bishop defines a continuous real function as a uniformly continuous function on any bounded interval. Despite its unfinished nature and the many questions that we do not currently know how to answer, we hope that this paper will arouse interest for its original approach to the subject. This paper is an English translation of a French version on arXiv:2406.15218

math.LO↗

arXiv2024

Th\'eories g\'eom\'etriques pour l'alg\`ebre des nombres r\'eels sans test de signe ni axiome de choix d\'ependant

In this memoir, we seek to construct a dynamical theory as complete as possible to describe the algebraic properties of the field of real numbers in constructive mathematics without axiom of dependent choice. We propose a theory which turns out to be very close to the theory of real closed local rings in classical mathematics. The theory of real closed rings is presented here in constructive form as a natural purely equational theory, which uses virtual root functions introduced in previous work. This work is also a first step through an essential goal for the future, which is to obtain a constructive version of o-minimal structures.

math.LO↗

arXiv2024

Machine-Checked Categorical Diagrammatic Reasoning

This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature.

cs.LO↗

arXiv2023

A First Order Theory of Diagram Chasing

This paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chases can be captured by a simple many-sorted first-order theory, and we study the models and decidability of this theory. The longer-term motivation of this work is the design of a computer-aided instrument for writing reliable proofs in homological algebra, based on interactive theorem provers.

cs.LO↗

arXiv2023

Trocq: Proof Transfer for Free, With or Without Univalence

Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of theorems, when such obvious replacements are typically left implicit on paper. This article presents Trocq, a new proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Coq proof assistant, in the CoqElpi meta-language. We use this plugin on a gallery of representative examples of proof transfer issues in interactive theorem proving, and illustrate how Trocq covers the spectrum of several existing tools, used in program verification as well as in formalized mathematics in the broad sense.

cs.LO↗

arXiv2022

Valuative lattices and spectra

The first part of the present article consists in a survey about the dynamical constructive method designed using dynamical theories and dynamical algebraic structures. Dynamical methods uncovers a hidden computational content for numerous abstract objects of classical mathematics, which seem a priori inaccessible constructively, e.g., the algebraic closure of a (discrete) field. When a proof in classical mathematics uses these abstract objects and results in a concrete outcome, dynamical methods generally make possible to discover an algorithm for this concrete outcome. The second part of the article applies this dynamical method to the theory of divisibility. We compare two notions of valuative spectra present in the literature and we introduce a third notion, which is implicit in an article devoted to the dynamical theory of algebraically closed discrete valued fields. The two first notions are respectively due to Huber \& Knebusch and to Coquand. We prove that the corresponding valuative lattices are essentially the same. We establish formal Valuativestellens\"atze corresponding to these theories, and we compare the various resulting notions of valuative dimensions.

math.AG↗

arXiv2022

Compositional pre-processing for automated reasoning in dependent type theory

In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of pre-processing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines.

cs.LO↗

arXiv2019

A Formal Proof of the Irrationality of $\zeta(3)$

This paper presents a complete formal verification of a proof that the evaluation of the Riemann zeta function at 3 is irrational, using the Coq proof assistant. This result was first presented by Ap\'ery in 1978, and the proof we have formalized essentially follows the path of his original presentation. The crux of this proof is to establish that some sequences satisfy a common recurrence. We formally prove this result by an a posteriori verification of calculations performed by computer algebra algorithms in a Maple session. The rest of the proof combines arithmetical ingredients and asymptotic analysis, which we conduct by extending the Mathematical Components libraries.

cs.LO↗

arXiv2014

Axiomatic constraint systems for proof search modulo theories

Goal-directed proof search in first-order logic uses meta-variables to delay the choice of witnesses; substitutions for such variables are produced when closing proof-tree branches, using first-order unification or a theory-specific background reasoner. This paper investigates a generalisation of such mechanisms whereby theory-specific constraints are produced instead of substitutions. In order to design modular proof-search procedures over such mechanisms, we provide a sequent calculus with meta-variables, which manipulates such constraints abstractly. Proving soundness and completeness of the calculus leads to an axiomatisation that identifies the conditions under which abstract constraints can be generated and propagated in the same way unifiers usually are. We then extract from our abstract framework a component interface and a specification for concrete implementations of background reasoners.

cs.LO↗

arXiv2012

Two simulations about DPLL(T)

In this paper we relate different formulations of the DPLL(T) procedure. The first formulation is based on a system of rewrite rules, which we denote DPLL(T). The second formulation is an inference system of, which we denote LKDPLL(T). The third formulation is the application of a standard proof-search mechanism in a sequent calculus LKp(T) introduced here. We formalise an encoding from DPLL(T) to LKDPLL(T) that was, to our knowledge, never explicitly given and, in the case where DPLL(T) is extended with backjumping and Lemma learning, never even implicitly given. We also formalise an encoding from LKDPLL(T) to LKp(T), building on Ivan Gazeau's previous work: we extend his work in that we handle the "-modulo-Theory" aspect of SAT-modulo-theory, by extending the sequent calculus to allow calls to a theory solver (seen as a blackbox). We also extend his work in that we handle advanced features of DPLL such as backjumping and Lemma learning, etc. Finally, we re fine the approach by starting to formalise quantitative aspects of the simulations: the complexity is preserved (number of steps to build complete proofs). Other aspects remain to be formalised (non-determinism of the search / width of search space).

cs.LO↗

arXiv2012

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic properties. The theory of real algebraic numbers and more generally of semi-algebraic varieties is at the core of a number of effective methods in real analysis, including decision procedures for non linear arithmetic or optimization methods for real valued functions. After defining an abstract structure of discrete real closed field and the elementary theory of real roots of polynomials, we describe the formalization of an algebraic proof of quantifier elimination based on pseudo-remainder sequences following the standard computer algebra literature on the topic. This formalization covers a large part of the theory which underlies the efficient algorithms implemented in practice in computer algebra. The success of this work paves the way for formal certification of these efficient methods.

cs.LO↗