proposition: Theorem meet_correct : forall xi yi v, contains (convert xi) v -> contains (convert yi) v -> contains (convert (meet xi yi)) v.
proof: Proof. intros xi yi v Hx Hy. unfold meet. destruct is_empty. easy. destruct is_empty. easy. revert xi yi v Hx Hy. intros [|xl xu] [|yl yu] [|v] ; simpl ; trivial; [now case (_ && _)|]. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; exfalso; lra]. intros Vxu Vxl. case_eq (F.valid_lb yl); [|intros _ _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub yu); [|intros _ _ _ [H0 H1]; exfalso; lra]. intros Vyu Vyl. intros (Hxl, Hxu) (Hyl, Hyu). simpl. generalize (F.max_correct xl yl). generalize (F.min_correct xu yu). generalize (F.real_correct yu) ; generalize (F.is_nan_correct yu) ; generalize (F.classify_correct yu) ; generalize Vyu; rewrite F.valid_ub_correct ; case (F.classify yu); try easy; intros _ H H'; rewrite H, H'; clear H H' ; [xreal_tac yu; [easy|intros _]|xreal_tac yu; [intros _|easy]..] ; ( generalize (F.real_correct xu) ; generalize (F.is_nan_correct xu) ; generalize (F.classify_correct xu) ; generalize Vxu; rewrite F.valid_ub_correct ; case (F.classify xu); try easy; intros _ H H'; rewrite H, H'; clear H H' ; [xreal_tac xu; [easy|intros _]|xreal_tac xu; [intros _|easy]..] ) ; ( generalize (F.real_correct yl) ; generalize (F.is_nan_correct yl) ; generalize (F.classify_correct yl) ; generalize Vyl; rewrite F.valid_lb_correct ; case (F.classify yl); try easy; intros _ H H'; rewrite H, H'; clear H H' ; [xreal_tac yl; [easy|intros _]|xreal_tac yl; [intros _|easy]..] ) ; ( generalize (F.real_correct xl) ; generalize (F.is_nan_correct xl) ; generalize (F.classify_correct xl) ; generalize Vxl; rewrite F.valid_lb_correct ; case (F.classify xl); try easy; intros _ H H'; rewrite H, H'; clear H H' ; [xreal_tac xl; [easy|intros _]|xreal_tac xl; [intros _|easy]..] ) ; simpl ; intros Hmin Hmax ; rewrite ?Hmin, ?Hmax, ?Vxu, ?Vxl, ?Vyu, ?Vyl ; try match type of Hmin with | F.toX _ = Xreal _ => rewrite F'.valid_ub_real; [|now rewrite F.real_correct, Hmin] end ; try match type of Hmax with | F.toX _ = Xreal _ => rewrite F'.valid_lb_real; [|now rewrite F.real_correct, Hmax] end ; simpl ; do 2 try match goal with | |- context [ F.toX ?x ] => match goal with | H : F.toX x = _ |- _ => rewrite H end end ; split ; try exact I ; try match goal with | |- (?z <= Rmin ?x ?y)%R => generalize (Rmin_glb x y z) ; lra end ; try match goal with | |- (Rmax ?x ?y <= ?z)%R => generalize (Rmax_lub x y z) ; lra end ; easy. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval