meta.yml

fullname: Analysis library compatible with Mathematical Components
shortname: analysis
organization: math-comp
opam_name: coq-mathcomp-analysis
community: false
action: true
nix: false
coqdoc: false

synopsis: >-
  An analysis library for mathematical components
description: |-
  This repository contains an experimental library for real analysis for
  the Coq proof-assistant and using the Mathematical Components library.
chat:
- url: https://coq.zulipchat.com/login/#narrow/stream/237666-math-comp-analysis
  shield: zulip
authors:
- name: Reynald Affeldt
  initial: true
- name: Yves Bertot
  initial: false
- name: Cyril Cohen
  initial: true
- name: Marie Kerjean
  initial: false
- name: Assia Mahboubi
  initial: true
- name: Damien Rouhling
  initial: true
- name: Pierre Roux
  initial: false
- name: Kazuhiko Sakaguchi
  initial: false
- name: Zachary Stone
  initial: false
- name: Pierre-Yves Strub
  initial: true
- name: Laurent Théry
  initial: false

opam-file-maintainer: Reynald Affeldt <reynald.affeldt@aist.go.jp>

opam-file-version: dev

license:
  fullname: CeCILL-C
  identifier: CECILL-C
  file: LICENSE

supported_coq_versions:
  text: Coq 8.14 to 8.15 (or dev)
  opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }'

tested_coq_opam_versions:
- version: '1.13.0-coq-8.14'
  repo: 'mathcomp/mathcomp'
- version: '1.13.0-coq-8.15'
  repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.14'
  repo: 'mathcomp/mathcomp'
- version: '1.14.0-coq-8.15'
  repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.14'
  repo: 'mathcomp/mathcomp'
- version: '1.15.0-coq-8.15'
  repo: 'mathcomp/mathcomp'
- version: 'coq-8.14'
  repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.15'
  repo: 'mathcomp/mathcomp-dev'

dependencies:
- opam:
    name: coq-mathcomp-ssreflect
    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
  description: |-
    [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-fingroup
    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
  description: |-
    [MathComp fingroup 1.13 or later](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-algebra
    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
  description: |-
    [MathComp algebra 1.13 or later](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-solvable
    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
  description: |-
    [MathComp solvable 1.13 or later](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-field
    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
  description: |-
    [MathComp field 1.13 or later](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-finmap
    version: '{ (>= "1.5.1" & < "1.6~") | (= "dev") }'
  description: |-
    [MathComp finmap 1.5.1](https://github.com/math-comp/finmap)
- opam:
    name: coq-mathcomp-bigenough
    version: '{ (>= "1.0.0") }'
  description: |-
    [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough)
- opam:
    name: coq-hierarchy-builder
    version: '{ (>= "1.2.0") }'
  description: |-
    [Hierarchy Builder >= 1.2.0](https://github.com/math-comp/hierarchy-builder)
namespace: mathcomp.analysis

keywords:
- name: analysis
- name: topology
- name: real numbers

categories:
- name: Mathematics/Real Calculus and Topology

publications:
- pub_url: https://jfr.unibo.it/article/view/8124
  pub_title:  Formalization Techniques for Asymptotic Reasoning in Classical Analysis
  pub_doi: 10.6092/issn.1972-5787/8124 
- pub_url: https://hal.inria.fr/hal-02463336
  pub_title: Competing inheritance paths in dependent type theory---a case study in functional analysis
  pub_doi: 10.1007/978-3-030-51054-1_1
- pub_url: http://www-sop.inria.fr/members/Damien.Rouhling/data/phd/thesis.pdf
  pub_title: Formalisation Tools for Classical Analysis

documentation: |-
  ## Disclaimer
 
  This library is still at an experimental stage.  Contents may
  change, definitions and theorems may be renamed, and inference
  mechanisms may be replaced at any major version bump.  Use at your
  own risk.

  ## Documentation

  Each file is documented in its header.

  Changes are documented in [CHANGELOG.md](CHANGELOG.md) and
  [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md).
  
  Overview presentation: [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)

  See also "Related publication(s)" [above](https://github.com/math-comp/analysis#meta).

  Other work using MathComp-Analysis: [A Formal Classical Proof of Hahn-Banach in Coq](https://lipn.univ-paris13.fr/~kerjean/slides/slidesTYPES19.pdf) (2019)

  ## Mathematical structures

  MathComp-Analysis adds mathematical structures on top of MathComp's ones.
  The following inheritance diagram displays the resulting hiearchy
  (excluding `countalg` and `finalg` structures). MathComp-Analysis
  mathematical structures are on the right, below `pointedType`
  included.

  ![Inheritance diagram](./hierarchy.png "Inheritance diagram")

  ## Development information

  [Detailed requirements and installation procedure](INSTALL.md)

  [Developping with nix](NIX.md)

  [Contributing](CONTRIBUTING.md)

  ## Previous work reused at the time of the first releases

  This library was inspired by the [Coquelicot library](http://coquelicot.saclay.inria.fr/)
  by Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond.
  `topology.v` and `normedtype.v` contained a reimplementation of file
  `Hierarchy.v` from the library Coquelicot.

  The instantiation of the mathematical structures of the Mathematical Components library
  with the real numbers of the standard Coq library used a well-known file (`Rstruct.v`)
  from the [CoqApprox library](http://tamadi.gforge.inria.fr/CoqApprox/) (with
  modifications from various authors).

  Our proof of Zorn's Lemma in `classical_sets.v` (NB: new filename) is a reimplementation
  of the one by Daniel Schepler (https://github.com/coq-community/zorns-lemma); we also took
  inspiration from his work on topology (https://github.com/coq-community/topology) for parts
  of `topology.v`.

  [ORIGINAL_FILES.md](ORIGINAL_FILES.md) gives more details about the
  files in the first releases.

  ## Acknowledgments

  Many thanks to [various contributors](https://github.com/math-comp/analysis/graphs/contributors)