Commit c74e88d4 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added a function for recovering bracket location.

parent 72dcf8b0
......@@ -9,10 +9,29 @@ Inductive location := loc_Exact | loc_Inexact : comparison -> location.
Variable x : R.
Definition inbetween_loc :=
match Rcompare x d with
| Gt => loc_Inexact (Rcompare x ((d + u) / 2))
| _ => loc_Exact
end.
Inductive inbetween : location -> Prop :=
| inbetween_Exact : x = d -> inbetween loc_Exact
| inbetween_Inexact l : (d < x < u)%R -> Rcompare x ((d + u) / 2)%R = l -> inbetween (loc_Inexact l).
Theorem inbetween_spec :
(d <= x < u)%R -> inbetween inbetween_loc.
Proof.
intros Hx.
unfold inbetween_loc.
destruct (Rcompare_spec x d) as [H|H|H].
now elim Rle_not_lt with (1 := proj1 Hx).
now constructor.
constructor.
now split.
easy.
Qed.
Section Fcalc_bracket_any.
Variable l : location.
......
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