LAProof.accuracy_proofs.common
From LAProof.accuracy_proofs Require Import preamble.
Definition rounded t r:=
(Generic_fmt.round Zaux.radix2 (SpecFloat.fexp (fprec t) (femax t))
(BinarySingleNaN.round_mode BinarySingleNaN.mode_NE) r).
Definition neg_zero {t: type} := Binary.B754_zero (fprec t) (femax t) true.
Definition pos_zero {t: type} := Binary.B754_zero (fprec t) (femax t) false.
Definition Beq_dec_t {t: type}
(x y : ftype t) : {x = y} + {x ≠ y}.
Defined.
Create HintDb commonDB discriminated.
Global Hint Resolve
bpow_gt_0 bpow_ge_0 pos_INR lt_0_INR pow_le: commonDB.
Delimit Scope R_scope with Re.
Open Scope R_scope.
Lemma rev_list_rev: @rev = @List.rev.
Lemma size_not_empty_nat {A} (l: seq A) : l ≠ [] → Nat.le 1 (size l).
Section WithType.
Context {NAN: FPCore.Nans} {t : type}.
Definition iszero {t} (x: ftype t) : bool :=
match x with Binary.B754_zero _ _ _ ⇒ true | _ ⇒ false end.
Lemma iszeroR_iszeroF: ∀ x: ftype t, Binary.is_finite x → FT2R x = R0 → iszero x.
Number of nonzeros
Definition nnzF: seq (ftype t) → nat :=
count (fun x ⇒ negb (iszero x)).
Definition nnzR: seq R → nat :=
count (fun x ⇒ negb (0 == x)).
Lemma nnzF_zero l: (nnzF l == 0%nat) = (size l == count iszero l).
Lemma nnzR_zero l: (nnzR l == 0%nat) = (size l == count (eq_op 0) l).
Lemma nnzF_lemma l: (nnzF l == 0%nat) = all iszero l.
Lemma nnzR_lemma l: (nnzR l == 0%nat) = (all (eq_op R0) l).
Lemma nnzF_is_zero_cons a l: nnzF (a::l) == 0%nat → nnzF l == 0%nat.
Lemma nnzR_is_zero_cons a l: nnzR (a::l) == 0%nat → nnzR l == 0%nat.
Lemma nnzR_cons l :
nnzR (0%Re :: l) == nnzR l.
Definition default_rel : R :=
/ 2 × Raux.bpow Zaux.radix2 (- fprec t + 1).
Definition default_abs : R :=
/ 2 × Raux.bpow Zaux.radix2 (3 - femax t - fprec t).
Lemma default_rel_sep_0 :
default_rel ≠ R0.
Hint Resolve default_rel_sep_0 : commonDB.
Lemma default_rel_gt_0 :
0 < default_rel.
Hint Resolve default_rel_gt_0 : commonDB.
Lemma default_rel_ge_0 :
0 ≤ default_rel.
Hint Resolve default_rel_ge_0 : commonDB.
Lemma default_rel_plus_1_ge_1:
1 ≤ 1 + default_rel.
Hint Resolve default_rel_plus_1_ge_1 : commonDB.
Lemma default_rel_plus_0_ge_1:
0 ≤ 1 + default_rel.
Hint Resolve default_rel_plus_0_ge_1 : commonDB.
Lemma default_rel_plus_1_gt_1:
1 < 1 + default_rel.
Hint Resolve default_rel_plus_1_gt_1 : commonDB.
Lemma default_rel_plus_1_gt_0 :
0 < 1 + default_rel.
Hint Resolve default_rel_plus_1_gt_0 : commonDB.
Lemma default_rel_plus_1_ge_1' n:
1 ≤ (1 + default_rel) ^ n.
Hint Resolve default_rel_plus_1_ge_1': commonDB.
Lemma default_abs_gt_0 :
0 < default_abs .
Hint Resolve default_abs_gt_0: commonDB.
Lemma default_abs_ge_0 :
0 ≤ default_abs .
Hint Resolve default_abs_ge_0: commonDB.
Lemma abs_le_rel :
default_abs ≤ default_rel.
End WithType.
Global Hint Resolve
default_rel_sep_0
default_rel_gt_0
default_rel_ge_0
default_rel_plus_1_ge_1
default_rel_plus_1_gt_0
default_rel_plus_1_ge_1'
default_abs_ge_0
default_abs_gt_0
default_rel_plus_1_ge_1
abs_le_rel
default_rel_plus_0_ge_1
: commonDB.
Section WithType.
Context {NAN: FPCore.Nans} {t: type}.
Notation D := (@default_rel t).
Notation E := (@default_abs t).
Definition g (n: nat) : R := ((1 + D) ^ n - 1).
Lemma g_pos n:
0 ≤ g n.
Hint Resolve g_pos : commonDB.
Lemma le_g_Sn n :
g n ≤ g (S n).
Hint Resolve le_g_Sn : commonDB.
Lemma d_le_g n:
D ≤ g (n + 1).
Hint Resolve d_le_g : commonDB.
Lemma d_le_g_1 n:
(1≤ n)%nat → D ≤ g n.
Hint Resolve d_le_g_1 : commonDB.
Lemma one_plus_d_mul_g a n:
(1 + D ) × g n × a + D × a = g (n + 1) × a.
Hint Resolve one_plus_d_mul_g : commonDB.
Definition g1 (n1: nat) (n2: nat) : R :=
INR n1 × E× (1 + g n2 ).
Lemma g1_pos n m : 0 ≤ g1 n m.
Hint Resolve g1_pos : commonDB.
Lemma one_plus_d_mul_g1 n:
(1 ≤ n )%nat →
g1 n (n - 1) × (1 + D ) = g1 n n.
Hint Resolve g1_pos : commonDB.
Lemma one_plus_d_mul_g1' n m:
g1 n m × (1 + D) = g1 n (S m).
Hint Resolve g1_pos : commonDB.
Hint Resolve fprec_lt_femax :commonDB.
Lemma e_le_g1 n:
(1 ≤ n )%nat →
E ≤ g1 n n.
Hint Resolve e_le_g1 : commonDB.
Lemma plus_d_e_g1_le' n m:
(1 ≤ n )%nat → (1 ≤ m)%nat →
g1 n m + (1 + D) × E ≤ g1 (S n) m.
Hint Resolve plus_d_e_g1_le' : commonDB.
Lemma mult_d_e_g1_le' n m:
(1 ≤ n )%nat → (1 ≤ m)%nat →
g1 n m × (1 + D) + E ≤ g1 (S n) (S m).
Hint Resolve mult_d_e_g1_le' : commonDB.
Lemma plus_d_e_g1_le n:
(1 ≤ n )%nat →
g1 n n + (1 + D) × E ≤ g1 (S n) n.
Hint Resolve plus_d_e_g1_le : commonDB.
Lemma plus_e_g1_le n:
g1 n n + E ≤ g1 (S n) n.
Hint Resolve plus_e_g1_le : commonDB.
Lemma g1n_le_g1Sn n:
(1 ≤ n )%nat →
g1 n (n - 1) ≤ g1 (S n) (S (n - 1)).
Hint Resolve g1n_le_g1Sn : commonDB.
Lemma g1n_le_g1Sn' n:
g1 n n ≤ g1 (S n) (S n).
Hint Resolve g1n_le_g1Sn' : commonDB.
Lemma Rplus_le_lt_compat a1 a2 b1 b2 :
a1 ≤ a2 → b1 < b2 → a1 + b1 < a2 + b2.
Lemma Rmult_le_lt_compat a1 a2 b1 b2 :
0 < a1 → 0 < b1 → a1 < a2 → b1 ≤ b2 → a1 × b1 < a2 × b2.
Lemma g1n_lt_g1Sn n:
(1 ≤ n )%nat →
g1 n (n - 1) < g1 (S n) (S (n - 1)).
Lemma round_FT2R a :
(Generic_fmt.round Zaux.radix2 (SpecFloat.fexp (fprec t) (femax t))
(BinarySingleNaN.round_mode BinarySingleNaN.mode_NE) (FT2R a)) = @FT2R t a.
End WithType.
Global Hint Resolve
g_pos
le_g_Sn
d_le_g
d_le_g_1
g1_pos
plus_d_e_g1_le'
one_plus_d_mul_g1
e_le_g1
mult_d_e_g1_le'
plus_d_e_g1_le
plus_e_g1_le
g1n_le_g1Sn
Rplus_le_lt_compat
Rmult_le_lt_compat
g1n_lt_g1Sn
: commonDB.
Ltac field_simplify_Rabs :=
match goal with
|- Rabs ?a ≤ _ ⇒
field_simplify a;
(repeat split;
try match goal with |-?z ≠ 0 ⇒
field_simplify z
end)
end.