namespace http://mathhub.info/MitM/core/arithmetics ❚

import base http://mathhub.info/MitM/Foundation ❚

theory RationalNumbers : base:?Logic =
	include ?IntegerNumbers ❙
	
	rationalNumbers : type ❘ # ℚ ❙
	axiom_intsAreRats : int_lit <* ℚ ❙
	axiom_natsAreRats : nat_lit <* ℚ ❙
	axiom_natsAreRats2 : NAT <* ℚ ❙
	axiom_posAreRats : pos_lit <* ℚ ❙

	fraction : ℤ ⟶ ℕ+ ⟶ ℚ ❘ # 1/2 ❙
	// TODO: this is the constructor ❙
❚
	
theory RationalArithmetics : base:?Logic =
	include ?IntegerArithmetics ❙
	include ?RationalNumbers ❙
	
	/T Negation ❙
	uminus : ℚ ⟶ ℚ ❘ # - 1 prec 33 ❙
	axiom_ratUminusIsIntUminus : {x : ℤ} ⊦ arithmetics?RationalArithmetics?uminus x ≐ arithmetics?IntegerArithmetics?uminus x ❙ 

	/T Addition ❙
	addition : ℚ ⟶ ℚ ⟶ ℚ ❘ #  1 + 2 prec 13 ❙
	axiom_ratPlusIsIntPlus : {x : ℤ, y : ℤ} ⊦ arithmetics?RationalArithmetics?addition x y ≐ arithmetics?IntegerArithmetics?addition x y ❙ 
	axiom_plusUminus : {x : ℚ} ⊦ x + (-x) ≐ 0 ❘ role Simplify ❙
	
	/T Subtraction ❙
	subtraction : ℚ ⟶ ℚ ⟶ ℚ ❘ = [a,b] a + (-b) ❘ # 1 - 2 prec 13 ❙
	
	/T Multiplication ❙
	multiplication : ℚ ⟶ ℚ ⟶ ℚ ❘ #  1 ⋅ 2 prec 23 ❙
	axiom_ratTimesIsNatTimes : {x : ℤ, y : ℤ} ⊦ arithmetics?RationalArithmetics?multiplication x y ≐ arithmetics?IntegerArithmetics?multiplication x y ❙

	/T Division ❙
	non_zero_rationals = ⟨ x : ℚ | ⊦ x ≠ 0 ⟩ ❘ # ℚ*❙
	inverse : {x:ℚ, p:⊦ x ≠ 0} ℚ ❘ # inv 1 %I2 prec 33 ❙
	inverseTyped : ℚ* ⟶ ℚ* ❙
	axiom_inv : {r : ℚ, p: ⊦ r ≠ 0} ⊦ r ⋅ (inv r) ≐ 1 ❘ //  role Simplify ❘ # Axiom_inv_rat 1 2 ❙
	axiom_inv2 : {r : ℚ* } ⊦ r ⋅ (inverseTyped r) ≐ 1 ❘ # axiom_inv2 ❙
	div : {r:ℚ,s:ℚ, p:⊦ s ≠ 0} ℚ ❘ = [r,s,p] r ⋅ (inv s) ❘ # 1 / 2 %I3 prec 6 ❙
	
	/T Exponentiation ❙
	exponentiation : ℚ ⟶ ℚ ⟶ ℚ ❘ #  1 ^ 2 prec 33 ❙
	axiom_ratExpIsNatExp : {x : ℤ, y : ℤ} ⊦ arithmetics?RationalArithmetics?exponentiation x y ≐ arithmetics?IntegerArithmetics?exponentiation x y ❙
	
	/T Roots ❙
	root : {n : ℚ, m : ℕ, p : ⊦ ∃![x] x^m ≐ n}ℚ ❘ = [n,m,p] ι [x] x^m ≐ n  ❘ # 2 √ 1 %I3 prec 33 ❙
	squareRoot : {n : ℚ, p : ⊦ ∃![m] m^2 ≐ n}ℚ ❘ = [n,p] 2 √ n ❘ # √ 1 %I2 prec 33 ❙
	
	/T Orders ❙
	leq : ℚ ⟶ ℚ ⟶ bool ❘ # 1 ≤ 2 prec 103 ❙
	geq : ℚ ⟶ ℚ ⟶ bool ❘ = [n,m] m ≤ n ❘ # 1 ≥ 2 prec 103 ❙
	lessthan : ℚ ⟶ ℚ ⟶ bool ❘ = [n,m] n ≤ m ∧ n ≠ m ❘ # 1 < 2 prec 103 ❙
	morethan : ℚ ⟶ ℚ ⟶ bool ❘ = [n,m] n ≥ m ∧ n ≠ m ❘ # 1 > 2 prec 103 ❙
	max : ℚ ⟶ ℚ ⟶ ℚ ❘ # max 1 2 ❙
	min : ℚ ⟶ ℚ ⟶ ℚ ❘ # min 1 2 ❙
	axiom_ratLeqIsIntLeq : {x : ℤ, y : ℤ} ⊦ arithmetics?RationalArithmetics?leq x y ≐ arithmetics?IntegerArithmetics?leq x y ❙
	
	/T Others ❙
	absolute : ℚ ⟶ ℚ ❘ = [q] case q < 0 ⟹ -q . q ❘ # | 1 | prec 9 ❙
	
	/T Field axioms ❙
	axiom_associativePlus : {x: ℚ,y,z} ⊦ x + (y + z) ≐ (x + y) + z ❘ # associative_plus_rat 1 2 3❙
	axiom_associativeTimes : {x: ℚ,y,z} ⊦ x ⋅ (y ⋅ z) ≐ (x ⋅ y) ⋅ z ❘ # associative_times_rat 1 2 3 ❙
	axiom_leftUnitalPlus : {x : ℚ} ⊦ arithmetics?RationalArithmetics?addition 0 x ≐ x ❘ # leftunital_plus_rat 1 ❙
	axiom_rightUnitalPlus : {x : ℚ} ⊦ arithmetics?RationalArithmetics?addition x 0 ≐ x ❘ # rightunital_plus_rat 1❙
	axiom_leftUnitalTimes : {x : ℚ} ⊦ 1 ⋅ x ≐ x ❘ # leftunital_times_rat 1 ❙
	axiom_rightUnitalTimes : {x : ℚ} ⊦ x ⋅ 1 ≐ x ❘ # rightunital_times_rat 1 ❙
	axiom_distributive : {x : ℚ, y : ℚ, z : ℚ} ⊦ x ⋅ (y + z) ≐ (x ⋅ y) + (x ⋅ z) ❘ # distributive_rat 1 2 3 ❙
	axiom_commutativePlus : {x : ℚ,y} ⊦ x + y ≐ y + x ❘ # addition_commutative_rat 1 2 ❙
	axiom_commutativeTimes : {x : ℚ,y} ⊦ x ⋅ y ≐ y ⋅ x ❘ # times_commutative_rat 1 2 ❙
❚