Library structures

Require Import algebra.

Natural Numbers

Inductive NatStruct : Type := mk_NatStruct :
forall R : Type,
forall o : R,
forall p : R -> R -> R, forall m : R -> R -> R,
forall l : R -> R -> Prop,
commutative R p ->
associative R p ->
commutative R m ->
associative R m ->
identity_l R o m ->
distributes R p m ->
irreflexive R l ->
transitive R l ->
trichotomy R l ->
less_plus_2 R p l ->
less_mult_2 R m l ->
eq_plus_injective R p ->
plus_irreflexive R p ->
inductionaxiom R o p ->
NatStruct.

Inductive NatStruct' : Type := mk_NatStruct' :
forall R : Type,
forall o : R,
forall p : R -> R -> R, forall m : R -> R -> R,
forall le : R -> R -> Prop,
commutative R p ->
associative R p ->
commutative R m ->
associative R m ->
identity_l R o m ->
distributes R p m ->
linear R le ->
transitive R le ->
antisymmetric R le ->
less_plus_2 R p le ->
less_mult_2 R m le ->
NaturalNumbers_minimal R o p m ->
NatStruct'.

Integers

Inductive IntegerStruct : Type :=
mk_IntegerStruct :
forall R : Type,
forall z o : R,
forall p : R -> R -> R, forall m : R -> R -> R,
forall n : R -> R,
forall le : R -> R -> Prop,
commutative R p ->
associative R p ->
identity_l R z p ->
inverse_l R z p n ->
commutative R m ->
associative R m ->
identity_l R o m ->
distributes R p m ->
linear R le ->
transitive R le ->
antisymmetric R le ->
less_plus_2 R p le ->
less_mult_2 R m le ->
Integer_minimal R z o p n ->
IntegerStruct.

Positive Rational Numbers

Inductive PositiveRationalStruct : Type :=
mk_PositiveRationalStruct :
forall R : Type,
forall o : R,
forall p : R -> R -> R, forall m : R -> R -> R,
forall r : R -> R,
forall l : R -> R -> Prop,
commutative R p ->
associative R p ->
commutative R m ->
associative R m ->
identity_l R o m ->
inverse_l R o m r ->
distributes R p m ->
trichotomy R l ->
transitive R l ->
irreflexive R l ->
less_plus_2 R p l ->
less_mult_2 R m l ->
dense R l ->
noendp_l R l ->
noendp_r R l ->
PositiveRational_minimal R o p m r ->
PositiveRationalStruct.

Inductive PositiveRationalStruct' : Type :=
mk_PositiveRationalStruct' :
forall R : Type,
forall o : R,
forall p : R -> R -> R, forall m : R -> R -> R,
forall r : R -> R,
forall le : R -> R -> Prop,
commutative R p ->
associative R p ->
commutative R m ->
associative R m ->
identity_l R o m ->
inverse_l R o m r ->
distributes R p m ->
linear R le ->
transitive R le ->
antisymmetric R le ->
less_plus_2 R p le ->
less_mult_2 R m le ->
PositiveRational_minimal R o p m r ->
PositiveRationalStruct'.

Rational Numbers

Inductive RationalStruct : Type :=
mk_RationalStruct :
forall R : Type,
forall z o : R,
forall p : R -> R -> R, forall m : R -> R -> R,
forall n : R -> R,
forall r : R -> R,
forall le : R -> R -> Prop,
commutative R p ->
associative R p ->
identity_l R z p ->
inverse_l R z p n ->
commutative R m ->
associative R m ->
identity_l R o m ->
inverse_exception_l R z o m r ->
distributes R p m ->
linear R le ->
transitive R le ->
antisymmetric R le ->
less_plus_2 R p le ->
less_mult R z m le ->
Rational_minimal R z o p m n r ->
RationalStruct.

Real Numbers

Harrison's Axioms for the Reals

Axioms from Section 2.1 of John Harrison's _Theorem Proving with the Real Numbers_

Inductive RealStructJH : Type :=
mk_RealStructJH :
forall R : Type,
forall z o : R,
forall p : R -> R -> R, forall m : R -> R -> R,
forall n : R -> R,
forall r : R -> R,
forall l : R -> R -> Prop,
zero_not_one R z o ->
commutative R p ->
associative R p ->
identity_l R z p ->
inverse_l R z p n ->
commutative R m ->
associative R m ->
identity_l R o m ->
inverse_exception_l R z o m r ->
distributes R p m ->
trichotomy R l ->
transitive R l ->
irreflexive R l ->
less_plus_1 R p l ->
less_mult_pos R o m l ->
HAsupremum R l ->
RealStructJH.

Dieudonne's Axioms for the Reals - Page 16 Fondements de l'analyse moderne

Inductive RealStructJD : Type :=
mk_RealStructJD :
forall R : Type,
forall z o : R,
forall p : R -> R -> R, forall m : R -> R -> R,
forall le : R -> R -> Prop,
commutative R p ->
associative R p ->
identity_l R z p ->
exist_inv_l R z p ->
commutative R m ->
associative R m ->
zero_not_one R z o ->
identity_l R o m ->
exist_inv_l_ex R z o m ->
distributes R p m ->
transitive R le ->
antisymmetric R le ->
linear R le ->
less_plus_1 R p le ->
less_mult_pos R o m le ->
JDarchimedean R z p le ->
JDnestedIntervals R le ->
RealStructJD.

Axiom System A'

Section 61 of Alfred Tarski's _Introduction to Logic and to the Methodology of Deductive Sciences_ 1994 Edited by Jan Tarski.

Inductive RealStructTA' : Type :=
mk_RealStructTA' :
forall R : Type,
forall o : R,
forall p : R -> R -> R,
forall l : R -> R -> Prop,
trichotomy R l ->
asymmetric R l ->
dense R l ->
TAcompleteness R l ->
ac_twist R p ->
exist_solns_1 R p ->
less_plus R p l ->

one_less_two R o p l ->
RealStructTA'.

Axiom System A''

Section 63 of Alfred Tarski's _Introduction to Logic and to the Methodology of Deductive Sciences_ 1994 Edited by Jan Tarski. This is said to be similar to Hilbert's 1900 axiomatization.

Inductive RealStructTA'' : Type :=
mk_RealStructTA'' :
forall R : Type,
forall z o : R,
forall p : R -> R -> R, forall m : R -> R -> R,
forall l : R -> R -> Prop,
trichotomy R l ->
asymmetric R l ->
transitive R l ->
TAcompleteness R l ->

commutative R p ->
associative R p ->
exist_solns_1 R p ->
less_plus_1 R p l ->

identity_r R z p ->

commutative R m ->
associative R m ->
exist_solns_2 R z m ->
less_mult R z m l ->
distributes R p m ->

identity_r R o m ->
zero_not_one R z o ->
RealStructTA''.