Commit dbcc7dcd authored by Guillaume Melquiond's avatar Guillaume Melquiond

Turn I.neg_correct into an equivalence.

parent 381eee17
......@@ -1290,6 +1290,27 @@ split ; rewrite F.neg_correct ;
apply Ropp_le_contravar ; assumption.
Qed.
Theorem neg_correct' :
forall xi x,
contains (convert (neg xi)) (Xneg x) ->
contains (convert xi) x.
Proof.
intros [|xl xu] [|x] ; try easy.
simpl.
rewrite 2!F.neg_correct.
destruct (F.toX xl) as [|xl'] ;
destruct (F.toX xu) as [|xu'] ; simpl.
easy.
intros [H _].
apply (conj I).
now apply Ropp_le_cancel.
intros [_ H].
refine (conj _ I).
now apply Ropp_le_cancel.
intros [H1 H2].
now split ; apply Ropp_le_cancel.
Qed.
Theorem abs_correct :
extension Xabs abs.
Proof.
......
......@@ -387,6 +387,11 @@ Parameter div_correct : forall prec, extension_2 Xdiv (div prec).
Parameter power_int_correct : forall prec n, extension (fun x => Xpower_int x n) (fun x => power_int prec x n).
Parameter nearbyint_correct : forall mode, extension (Xnearbyint mode) (nearbyint mode).
Parameter neg_correct' :
forall xi x,
contains (convert (neg xi)) (Xneg x) ->
contains (convert xi) x.
Parameter bounded : type -> bool.
Parameter lower_bounded : type -> bool.
Parameter upper_bounded : type -> bool.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment