Library Numeric
Common interface for numerics domains.
A part of Bicolano project by David Pichardie,
adapted to fit into CoJaq project.
Require Export ZArith BinPosDef BinNums.
Require Import Common List.
Import List.ListNotations.
Open Local Scope Z_scope.
Require Import Common List.
Import List.ListNotations.
Open Local Scope Z_scope.
Parameter t : Set.
Parameter toZ : t → Z.
Parameter power : Z.
Parameter power_positive: power > 0.
Definition half_base := 2^power.
Definition base := 2×half_base.
Definition range (z:Z) : Prop := -half_base ≤ z < half_base.
Parameter range_prop : ∀ x:t, range (toZ x).
Definition smod (x:Z) : Z :=
let z := x mod base in
match Zcompare z half_base with
| Lt ⇒ z
| _ ⇒ z - base
end.
Parameter add : t → t → t.
Parameter add_prop : ∀ i1 i2,
toZ (add i1 i2)= smod (toZ i1 + toZ i2).
Parameter sub : t → t → t.
Parameter sub_prop : ∀ i1 i2,
toZ (sub i1 i2)= smod (toZ i1 - toZ i2).
Parameter mul : t → t → t.
Parameter mul_prop : ∀ i1 i2,
toZ (mul i1 i2)= smod (toZ i1 × toZ i2).
Parameter div : t → t → t.
Parameter div_prop : ∀ i1 i2,
toZ (div i1 i2)= smod (toZ i1 / toZ i2).
Parameter rem : t → t → t.
Parameter rem_prop : ∀ i1 i2,
toZ (rem i1 i2)= smod (toZ i1 mod toZ i2).
Parameter shr : t → t → t.
Parameter shr_prop : ∀ i1 i2,
toZ (shr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter shl : t → t → t.
Parameter shl_prop : ∀ i1 i2,
toZ (shr i1 i2) = smod (toZ i1 × 2^(toZ i2 mod 32)).
Parameter ushr : t → t → t.
Parameter ushr_prop1 : ∀ i1 i2,
toZ i1 < 0 →
toZ (ushr i1 i2) = smod ((toZ i1 + base) / 2^(toZ i2 mod 32)).
Parameter ushr_prop2 : ∀ i1 i2,
toZ i1 ≥ 0 →
toZ (ushr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter and : t → t → t.
Parameter or : t → t → t.
Parameter xor : t → t → t.
Parameter neg : t → t.
Parameter neg_prop : ∀ i,
toZ (neg i) = smod (- toZ i).
Parameter const : Z → t.
Parameter const_prop : ∀ z,
range z → toZ (const z) = z.
Parameter toZ : t → Z.
Parameter power : Z.
Parameter power_positive: power > 0.
Definition half_base := 2^power.
Definition base := 2×half_base.
Definition range (z:Z) : Prop := -half_base ≤ z < half_base.
Parameter range_prop : ∀ x:t, range (toZ x).
Definition smod (x:Z) : Z :=
let z := x mod base in
match Zcompare z half_base with
| Lt ⇒ z
| _ ⇒ z - base
end.
Parameter add : t → t → t.
Parameter add_prop : ∀ i1 i2,
toZ (add i1 i2)= smod (toZ i1 + toZ i2).
Parameter sub : t → t → t.
Parameter sub_prop : ∀ i1 i2,
toZ (sub i1 i2)= smod (toZ i1 - toZ i2).
Parameter mul : t → t → t.
Parameter mul_prop : ∀ i1 i2,
toZ (mul i1 i2)= smod (toZ i1 × toZ i2).
Parameter div : t → t → t.
Parameter div_prop : ∀ i1 i2,
toZ (div i1 i2)= smod (toZ i1 / toZ i2).
Parameter rem : t → t → t.
Parameter rem_prop : ∀ i1 i2,
toZ (rem i1 i2)= smod (toZ i1 mod toZ i2).
Parameter shr : t → t → t.
Parameter shr_prop : ∀ i1 i2,
toZ (shr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter shl : t → t → t.
Parameter shl_prop : ∀ i1 i2,
toZ (shr i1 i2) = smod (toZ i1 × 2^(toZ i2 mod 32)).
Parameter ushr : t → t → t.
Parameter ushr_prop1 : ∀ i1 i2,
toZ i1 < 0 →
toZ (ushr i1 i2) = smod ((toZ i1 + base) / 2^(toZ i2 mod 32)).
Parameter ushr_prop2 : ∀ i1 i2,
toZ i1 ≥ 0 →
toZ (ushr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter and : t → t → t.
Parameter or : t → t → t.
Parameter xor : t → t → t.
Parameter neg : t → t.
Parameter neg_prop : ∀ i,
toZ (neg i) = smod (- toZ i).
Parameter const : Z → t.
Parameter const_prop : ∀ z,
range z → toZ (const z) = z.
Parameter zero : t.
Axiom PzeroToZ: toZ zero = 0.
Parameter one : t.
Axiom PoneToZ: toZ one = 1.
Parameter minus_one : t.
Axiom PminusOneToZ: toZ minus_one = -1.
Parameter isNotZero : t → Prop.
Axiom PisNotZero: ∀ arg, isNotZero arg ↔ toZ arg ≠ 0.
Axiom PoneIsNotZero: isNotZero one.
Axiom PzeroToZ: toZ zero = 0.
Parameter one : t.
Axiom PoneToZ: toZ one = 1.
Parameter minus_one : t.
Axiom PminusOneToZ: toZ minus_one = -1.
Parameter isNotZero : t → Prop.
Axiom PisNotZero: ∀ arg, isNotZero arg ↔ toZ arg ≠ 0.
Axiom PoneIsNotZero: isNotZero one.
Parameter compare: t → t → comparison.
Parameter is_eq : t → t → bool.
Parameter is_ne : t → t → bool.
Parameter is_le : t → t → bool.
Parameter is_lt : t → t → bool.
Parameter is_ge : t → t → bool.
Parameter is_gt : t → t → bool.
Axiom Pcompare_toZ: ∀ arg1 arg2,
compare arg1 arg2 = Z.compare (toZ arg1) (toZ arg2).
Parameter is_eq : t → t → bool.
Parameter is_ne : t → t → bool.
Parameter is_le : t → t → bool.
Parameter is_lt : t → t → bool.
Parameter is_ge : t → t → bool.
Parameter is_gt : t → t → bool.
Axiom Pcompare_toZ: ∀ arg1 arg2,
compare arg1 arg2 = Z.compare (toZ arg1) (toZ arg2).
The operation to truncate a number in the current representation
to the representation given by p-bit number where p is its second argument
Creates an actual module implementing NUMERIC for a given power.
In fact, the implementation is incomplete (some Parameters and Axioms left).
Module Make (S:NUMSIZE) : NUMERIC with Definition power := S.power.
Parameter t : Set.
Parameter toZ : t → Z.
Definition power := S.power.
Definition half_base := 2^power.
Definition base := 2×half_base.
Definition range (z:Z) : Prop := -half_base ≤ z < half_base.
Parameter range_prop : ∀ x:t, range (toZ x).
Lemma power_positive : power > 0.
Proof.
apply S.power_positive.
Qed.
Definition smod (x:Z) : Z :=
let z := x mod base in
match Zcompare z half_base with
| Lt ⇒ z
| _ ⇒ z - base
end.
Parameter add : t → t → t.
Parameter add_prop : ∀ i1 i2,
toZ (add i1 i2)= smod (toZ i1 + toZ i2).
Parameter sub : t → t → t.
Parameter sub_prop : ∀ i1 i2,
toZ (sub i1 i2)= smod (toZ i1 - toZ i2).
Parameter mul : t → t → t.
Parameter mul_prop : ∀ i1 i2,
toZ (mul i1 i2)= smod (toZ i1 × toZ i2).
Parameter div : t → t → t.
Parameter div_prop : ∀ i1 i2,
toZ (div i1 i2)= smod (toZ i1 / toZ i2).
Parameter rem : t → t → t.
Parameter rem_prop : ∀ i1 i2,
toZ (rem i1 i2)= smod (toZ i1 mod toZ i2).
Parameter shr : t → t → t.
Parameter shr_prop : ∀ i1 i2,
toZ (shr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter shl : t → t → t.
Parameter shl_prop : ∀ i1 i2,
toZ (shr i1 i2) = smod (toZ i1 × 2^(toZ i2 mod 32)).
Parameter ushr : t → t → t.
Parameter ushr_prop1 : ∀ i1 i2,
toZ i1 < 0 →
toZ (ushr i1 i2) = smod ((toZ i1 + base) / 2^(toZ i2 mod 32)).
Parameter ushr_prop2 : ∀ i1 i2,
toZ i1 ≥ 0 →
toZ (ushr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter and : t → t → t.
Parameter or : t → t → t.
Parameter xor : t → t → t.
Parameter neg : t → t.
Parameter neg_prop : ∀ i,
toZ (neg i) = smod (- toZ i).
Parameter const : Z → t.
Parameter const_prop : ∀ z,
range z → toZ (const z) = z.
Lemma half_base_ge_2: 2 ≤ half_base.
Proof.
unfold half_base.
change (2^1 ≤ 2^power).
apply Z.pow_le_mono.
omega.
assert (H := power_positive).
omega.
Qed.
Axiom PToZDistinct: ∀ i1 i2,
toZ i1 = toZ i2 → i1 = i2.
Axiom PNumericEqDec: eqDecS t.
Definition zero : t := const 0.
Lemma PzeroToZ: toZ zero = 0.
Proof.
apply const_prop.
unfold range.
assert (H := half_base_ge_2).
omega.
Qed.
Definition one : t := const 1.
Lemma PoneToZ: toZ one = 1.
Proof.
apply const_prop.
unfold range.
assert (H := half_base_ge_2).
omega.
Qed.
Definition minus_one : t := const (-1).
Lemma PminusOneToZ: toZ minus_one = -1.
Proof.
apply const_prop.
unfold range.
assert (H := half_base_ge_2).
omega.
Qed.
Definition isNotZero (arg: t): Prop := toZ arg ≠ 0.
Lemma PisNotZero: ∀ arg, isNotZero arg ↔ toZ arg ≠ 0.
Proof.
intuition.
Qed.
Lemma PoneIsNotZero: isNotZero one.
Proof.
apply PisNotZero.
rewrite PoneToZ.
discriminate.
Qed.
Definition compare arg1 arg2 :=
Z.compare (toZ arg1) (toZ arg2).
Definition is_eq arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ false
| Eq ⇒ true
| Gt ⇒ false
end.
Definition is_ne arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ true
| Eq ⇒ false
| Gt ⇒ true
end.
Definition is_le arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ true
| Eq ⇒ true
| Gt ⇒ false
end.
Definition is_lt arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ true
| Eq ⇒ false
| Gt ⇒ false
end.
Definition is_ge arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ false
| Eq ⇒ true
| Gt ⇒ true
end.
Definition is_gt arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ false
| Eq ⇒ false
| Gt ⇒ true
end.
Lemma Pcompare_toZ: ∀ arg1 arg2,
compare arg1 arg2 = Z.compare (toZ arg1) (toZ arg2).
Proof.
auto.
Qed.
Parameter t : Set.
Parameter toZ : t → Z.
Definition power := S.power.
Definition half_base := 2^power.
Definition base := 2×half_base.
Definition range (z:Z) : Prop := -half_base ≤ z < half_base.
Parameter range_prop : ∀ x:t, range (toZ x).
Lemma power_positive : power > 0.
Proof.
apply S.power_positive.
Qed.
Definition smod (x:Z) : Z :=
let z := x mod base in
match Zcompare z half_base with
| Lt ⇒ z
| _ ⇒ z - base
end.
Parameter add : t → t → t.
Parameter add_prop : ∀ i1 i2,
toZ (add i1 i2)= smod (toZ i1 + toZ i2).
Parameter sub : t → t → t.
Parameter sub_prop : ∀ i1 i2,
toZ (sub i1 i2)= smod (toZ i1 - toZ i2).
Parameter mul : t → t → t.
Parameter mul_prop : ∀ i1 i2,
toZ (mul i1 i2)= smod (toZ i1 × toZ i2).
Parameter div : t → t → t.
Parameter div_prop : ∀ i1 i2,
toZ (div i1 i2)= smod (toZ i1 / toZ i2).
Parameter rem : t → t → t.
Parameter rem_prop : ∀ i1 i2,
toZ (rem i1 i2)= smod (toZ i1 mod toZ i2).
Parameter shr : t → t → t.
Parameter shr_prop : ∀ i1 i2,
toZ (shr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter shl : t → t → t.
Parameter shl_prop : ∀ i1 i2,
toZ (shr i1 i2) = smod (toZ i1 × 2^(toZ i2 mod 32)).
Parameter ushr : t → t → t.
Parameter ushr_prop1 : ∀ i1 i2,
toZ i1 < 0 →
toZ (ushr i1 i2) = smod ((toZ i1 + base) / 2^(toZ i2 mod 32)).
Parameter ushr_prop2 : ∀ i1 i2,
toZ i1 ≥ 0 →
toZ (ushr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
Parameter and : t → t → t.
Parameter or : t → t → t.
Parameter xor : t → t → t.
Parameter neg : t → t.
Parameter neg_prop : ∀ i,
toZ (neg i) = smod (- toZ i).
Parameter const : Z → t.
Parameter const_prop : ∀ z,
range z → toZ (const z) = z.
Lemma half_base_ge_2: 2 ≤ half_base.
Proof.
unfold half_base.
change (2^1 ≤ 2^power).
apply Z.pow_le_mono.
omega.
assert (H := power_positive).
omega.
Qed.
Axiom PToZDistinct: ∀ i1 i2,
toZ i1 = toZ i2 → i1 = i2.
Axiom PNumericEqDec: eqDecS t.
Definition zero : t := const 0.
Lemma PzeroToZ: toZ zero = 0.
Proof.
apply const_prop.
unfold range.
assert (H := half_base_ge_2).
omega.
Qed.
Definition one : t := const 1.
Lemma PoneToZ: toZ one = 1.
Proof.
apply const_prop.
unfold range.
assert (H := half_base_ge_2).
omega.
Qed.
Definition minus_one : t := const (-1).
Lemma PminusOneToZ: toZ minus_one = -1.
Proof.
apply const_prop.
unfold range.
assert (H := half_base_ge_2).
omega.
Qed.
Definition isNotZero (arg: t): Prop := toZ arg ≠ 0.
Lemma PisNotZero: ∀ arg, isNotZero arg ↔ toZ arg ≠ 0.
Proof.
intuition.
Qed.
Lemma PoneIsNotZero: isNotZero one.
Proof.
apply PisNotZero.
rewrite PoneToZ.
discriminate.
Qed.
Definition compare arg1 arg2 :=
Z.compare (toZ arg1) (toZ arg2).
Definition is_eq arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ false
| Eq ⇒ true
| Gt ⇒ false
end.
Definition is_ne arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ true
| Eq ⇒ false
| Gt ⇒ true
end.
Definition is_le arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ true
| Eq ⇒ true
| Gt ⇒ false
end.
Definition is_lt arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ true
| Eq ⇒ false
| Gt ⇒ false
end.
Definition is_ge arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ false
| Eq ⇒ true
| Gt ⇒ true
end.
Definition is_gt arg1 arg2 :=
match compare arg1 arg2 with
| Lt ⇒ false
| Eq ⇒ false
| Gt ⇒ true
end.
Lemma Pcompare_toZ: ∀ arg1 arg2,
compare arg1 arg2 = Z.compare (toZ arg1) (toZ arg2).
Proof.
auto.
Qed.
Transforms the given positive x into its list of least significant bits
according to the representation in p bits
Fixpoint digits_of_pos (x:positive) (p:positive) : list bool :=
let addfalse li := false :: li in
match x with
| xO y ⇒ false :: digits_of_pos y (Pos.pred p)
| xI y ⇒ true :: digits_of_pos y (Pos.pred p)
| xH ⇒ match p with
| xH ⇒ true :: nil
| _ ⇒ true :: Pos.iter (Pos.pred p) addfalse nil
end
end.
Lemma testdop45 : (digits_of_pos 4 5) = [false; false; true; false; false].
Proof.
simpl.
trivial.
Qed.
Transforms the given integer x into its list of least significant bits
according to the representation in p bits
Fixpoint digits_of_Z (x:Z) (p:positive) : list bool :=
let addfalse li := false :: li in
match x with
| Z0 ⇒ Pos.iter p addfalse nil
| Zpos x1 ⇒ digits_of_pos x1 p
| Zneg x1 ⇒ digits_of_pos ((Pos.pow 2 p) - x1)%positive p
end.
Fixpoint pos_of_digits (d:list bool) : positive :=
match d with
| nil ⇒ xH
| true :: nil ⇒ xH
| false :: nil ⇒ xH
| true :: tl ⇒ xI (pos_of_digits tl)
| false :: tl ⇒ xO (pos_of_digits tl)
end.
Fixpoint clear_false (d:list bool) : list bool :=
match d with
| nil ⇒ nil
| true :: tl ⇒ d
| false :: tl ⇒ clear_false tl
end.
let addfalse li := false :: li in
match x with
| Z0 ⇒ Pos.iter p addfalse nil
| Zpos x1 ⇒ digits_of_pos x1 p
| Zneg x1 ⇒ digits_of_pos ((Pos.pow 2 p) - x1)%positive p
end.
Fixpoint pos_of_digits (d:list bool) : positive :=
match d with
| nil ⇒ xH
| true :: nil ⇒ xH
| false :: nil ⇒ xH
| true :: tl ⇒ xI (pos_of_digits tl)
| false :: tl ⇒ xO (pos_of_digits tl)
end.
Fixpoint clear_false (d:list bool) : list bool :=
match d with
| nil ⇒ nil
| true :: tl ⇒ d
| false :: tl ⇒ clear_false tl
end.
TODO we assume d is in two's complement
Fixpoint Z_of_digits (d:list bool) : Z :=
let rl := rev d in
let cf := clear_false rl in
match rl with
| nil ⇒ Z0
| true :: tl ⇒ Zneg (2^(P_of_succ_nat ((length rl) -1)) - (pos_of_digits d))
| false :: tl ⇒ match cf with
| nil ⇒ Z0
| x ⇒ Zpos (pos_of_digits (rev cf))
end
end.
Definition truncateZ (x:Z) (p:positive) : Z :=
Z_of_digits (firstn (nat_of_P p) (digits_of_Z x (Pos.of_nat (Z.to_nat power)))).
Definition truncate (x:t) (p:positive) : t := const (truncateZ (toZ x) p).
Lemma testm75 : power = 5 → (truncateZ (-7) 5) = (-7).
Proof.
intros.
unfold truncateZ.
rewrite H.
trivial.
Qed.
Lemma testm74 : power = 5 → (truncateZ (-7) 4) = (-7).
Proof.
intros.
unfold truncateZ.
rewrite H.
trivial.
Qed.
Lemma testm73 : power = 5 → (truncateZ (-7) 3) = 1.
Proof.
intros.
unfold truncateZ.
rewrite H.
trivial.
Qed.
Lemma testm45 : power = 5 → (truncateZ 4 5) = 4.
Proof.
intros.
unfold truncateZ.
rewrite H.
simpl.
trivial.
Qed.
Lemma testm44 : power = 5 → (truncateZ 4 4) = 4.
Proof.
intros.
unfold truncateZ.
rewrite H.
simpl.
trivial.
Qed.
Lemma testm43 : power = 5 → (truncateZ 4 3) = -4.
Proof.
intros.
unfold truncateZ.
rewrite H.
compute.
trivial.
Qed.
Lemma testm42 : power = 5 → (truncateZ 4 2) = 0.
Proof.
intros.
unfold truncateZ.
rewrite H.
trivial.
Qed.
End Make.
let rl := rev d in
let cf := clear_false rl in
match rl with
| nil ⇒ Z0
| true :: tl ⇒ Zneg (2^(P_of_succ_nat ((length rl) -1)) - (pos_of_digits d))
| false :: tl ⇒ match cf with
| nil ⇒ Z0
| x ⇒ Zpos (pos_of_digits (rev cf))
end
end.
Definition truncateZ (x:Z) (p:positive) : Z :=
Z_of_digits (firstn (nat_of_P p) (digits_of_Z x (Pos.of_nat (Z.to_nat power)))).
Definition truncate (x:t) (p:positive) : t := const (truncateZ (toZ x) p).
Lemma testm75 : power = 5 → (truncateZ (-7) 5) = (-7).
Proof.
intros.
unfold truncateZ.
rewrite H.
trivial.
Qed.
Lemma testm74 : power = 5 → (truncateZ (-7) 4) = (-7).
Proof.
intros.
unfold truncateZ.
rewrite H.
trivial.
Qed.
Lemma testm73 : power = 5 → (truncateZ (-7) 3) = 1.
Proof.
intros.
unfold truncateZ.
rewrite H.
trivial.
Qed.
Lemma testm45 : power = 5 → (truncateZ 4 5) = 4.
Proof.
intros.
unfold truncateZ.
rewrite H.
simpl.
trivial.
Qed.
Lemma testm44 : power = 5 → (truncateZ 4 4) = 4.
Proof.
intros.
unfold truncateZ.
rewrite H.
simpl.
trivial.
Qed.
Lemma testm43 : power = 5 → (truncateZ 4 3) = -4.
Proof.
intros.
unfold truncateZ.
rewrite H.
compute.
trivial.
Qed.
Lemma testm42 : power = 5 → (truncateZ 4 2) = 0.
Proof.
intros.
unfold truncateZ.
rewrite H.
trivial.
Qed.
End Make.
Module NumericProperties (_Numeric: NUMERIC).
Import _Numeric.
Lemma Pcompare_const: ∀ z1 z2,
range z1 → range z2 →
Z.compare z1 z2 = compare (const z1) (const z2).
Proof.
intros z1 z2 Hr1 Hr2.
rewrite Pcompare_toZ.
rewrite const_prop.
rewrite const_prop.
reflexivity.
assumption.
assumption.
Qed.
Axiom example_is_eq_t: is_eq zero zero = true.
Axiom example_is_eq_f: is_eq one zero = false.
Axiom example_is_ne_t: is_ne one zero = true.
Axiom example_is_ne_f: is_ne zero zero = false.
Axiom example_is_le_t: is_le minus_one zero = true.
Axiom example_is_le_f: is_le one zero = false.
Axiom example_is_lt_t: is_lt minus_one zero = true.
Axiom example_is_lt_f: is_lt one zero = false.
Axiom example_is_ge_t: is_ge one zero = true.
Axiom example_is_ge_f: is_ge minus_one zero = false.
Axiom example_is_gt_t: is_gt one zero = true.
Axiom example_is_gt_f: is_gt minus_one zero = false.
Axiom is_eq_t_toZ_prop: ∀ arg1 arg2,
is_eq arg1 arg2 = true →
toZ arg1 = toZ arg2.
Axiom is_eq_f_toZ_prop: ∀ arg1 arg2,
is_eq arg1 arg2 = false →
¬ toZ arg1 = toZ arg2.
Axiom is_ne_t_toZ_prop: ∀ arg1 arg2,
is_ne arg1 arg2 = true →
toZ arg1 ≠ toZ arg2.
Axiom is_ne_f_toZ_prop: ∀ arg1 arg2,
is_ne arg1 arg2 = false →
¬ toZ arg1 ≠ toZ arg2.
Axiom is_le_t_toZ_prop: ∀ arg1 arg2,
is_le arg1 arg2 = true →
toZ arg1 ≤ toZ arg2.
Axiom is_le_f_toZ_prop: ∀ arg1 arg2,
is_le arg1 arg2 = false →
¬ toZ arg1 ≤ toZ arg2.
Axiom is_lt_t_toZ_prop: ∀ arg1 arg2,
is_lt arg1 arg2 = true →
toZ arg1 < toZ arg2.
Axiom is_lt_f_toZ_prop: ∀ arg1 arg2,
is_lt arg1 arg2 = false →
¬ toZ arg1 < toZ arg2.
Axiom is_ge_t_toZ_prop: ∀ arg1 arg2,
is_ge arg1 arg2 = true →
toZ arg1 ≥ toZ arg2.
Axiom is_ge_f_toZ_prop: ∀ arg1 arg2,
is_ge arg1 arg2 = false →
¬ toZ arg1 ≥ toZ arg2.
Axiom is_gt_t_toZ_prop: ∀ arg1 arg2,
is_gt arg1 arg2 = true →
toZ arg1 > toZ arg2.
Axiom is_gt_f_toZ_prop: ∀ arg1 arg2,
is_gt arg1 arg2 = false →
¬ toZ arg1 > toZ arg2.
End NumericProperties.