proposition: Theorem meet_correct' : forall xi yi v, contains (convert (meet xi yi)) v -> contains (convert xi) v /\ contains (convert yi) v.
proof: Proof. intros xi yi v. unfold meet. generalize (is_empty_correct xi v). destruct is_empty. { intros H Hv. now elim H. } intros _. generalize (is_empty_correct yi v). destruct is_empty. { intros H Hv. now elim H. } intros _. revert xi yi v. intros [|xl xu] [|yl yu] v H ; try easy. destruct v as [|v]; revert H; simpl; [now case (_ && _)|]. assert (HRmin: forall p q, (v <= Rmin p q)%R -> (v <= p /\ v <= q)%R). intros p q H. unfold Rmin in H. destruct Rle_dec as [H'|H'] ; lra. assert (HRmax: forall p q, (Rmax p q <= v)%R -> (p <= v /\ q <= v)%R). intros p q H. unfold Rmax in H. destruct Rle_dec as [H'|H'] ; lra. 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 (F.valid_ub_correct yu) ; ( case (F.classify yu) ; intros Vyu 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 (F.valid_ub_correct xu) ; ( case (F.classify xu) ; intros Vxu 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 (F.valid_lb_correct yl) ; ( case (F.classify yl) ; intros Vyl 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 (F.valid_lb_correct xl) ; ( case (F.classify xl) ; intros Vxl 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] | F.classify ?m = _ => generalize (F.valid_ub_correct m) ; rewrite Hmin => -> end ; try match type of Hmax with | F.toX _ = Xreal _ => rewrite F'.valid_lb_real; [|now rewrite F.real_correct, Hmax] | F.classify ?m = _ => generalize (F.valid_lb_correct m) ; rewrite Hmax => -> end ; simpl ; do 2 try match goal with | |- context [ F.toX ?x ] => match goal with | H : F.toX x = _ |- _ => rewrite H end end ; intros [Hl Hu] ; try match type of Hl with | (Rmax ?x ?y <= _)%R => apply (HRmax x y) in Hl end ; try match type of Hu with | (_ <= Rmin ?x ?y)%R => apply (HRmin x y) in Hu end ; lra. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval