Awesome
Actuary
This is an experimental package where the basic part of actuarial mathematics is formalized using the Coq Proof Assistant.
Requirements
- Coq 8.17.1 or later
- Mathematical Components 1.17.0 or 1.18.0
- Coquelicot 3.4.0 or later
Building and installation instructions
The easiest way to install the latest released version is via opam:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-actuary
To instead build and install manually, do:
git clone https://github.com/Yosuke-Ito-345/Actuary.git
cd Actuary
make # or make -j <number-of-cores-on-your-machine>
make install
Description of files in theories directory
all_Actuary.v
: This file imports all theory modules defined by files below:Basics
,Interest
,LifeTable
,Premium
,Reserve
.Basics.v
: Some basic facts of mathematics are collected for the main part of the package.Interest.v
: The theory of interest is formalized, including the present and future values of annuities.LifeTable.v
: The life table is defined axiomatically, and is examined mainly from probability theory.Premium.v
: Basic actuarial notations are introduced, including various facts on the present values of annuities, insurance and so on.Reserve.v
: The level premium reserve is defined, and some useful formulas are also proved formally.Examples.v
: Some applications of this package are shown.
Notice
- Classical logic is assumed.
- The axiom of choice is used.
- The following functions are set to be coercions:
INR : nat >-> R
IZR : Z >-> R
- The infix notation
^
is redefined asRpower
, and the original functionpow
is represented as.^
. - The future updates of this package may not be backward compatible.
- Any advice or comment is welcome.
Main changes from version 1.0 to version 2.0
- Inequalities
>
and>=
are replaced with<
and<=
(advice from Zulip Chat). - The force of mortality is formalized.
- Notations
δ
,ω
are changed to\δ
,\ω
, respectively. - Some basic lemmas are taken in the
auto
tactic byHint Resolve
. - Generalized the frequency of payments in
Premium.v
andReserve.v
. - The continuous payment case is newly formalized.