proposition: Lemma join_correct : forall xi yi v, contains (convert xi) v \/ contains (convert yi) v -> contains (convert (join xi yi)) v.
proof: Proof. intros xi yi v H. unfold join. generalize (is_empty_correct xi v). intros Ex. destruct is_empty. { destruct H as [H|H]. now elim Ex. exact H. } clear Ex. generalize (is_empty_correct yi v). intros Ey. destruct is_empty. { destruct H as [H|H]. exact H. now elim Ey. } clear Ey. revert H. assert (H1v0 : forall v, ~(1 <= v <= 0)%R). { intros v' Hf. apply (Rlt_irrefl 0), (Rlt_le_trans _ 1); [apply Rlt_0_1|]. elim Hf; apply Rle_trans. } revert xi yi v. simpl. intros [|xl xu] [|yl yu] [|v]; simpl; try rewrite Hxl, Hxu; try rewrite Hyl, Hyu; simpl; try tauto; [|]. { now case (_ && _); case (_ && _); intros [H|H]. } generalize (F.max_correct xu yu). generalize (F.min_correct xl yl). generalize (F.real_correct yu) ; generalize (F.classify_correct yu) ; generalize (F.valid_ub_correct yu) ; case (F.classify yu) => -> -> ; [xreal_tac yu; [easy|intros _]|xreal_tac yu; [intros _|easy]..] ; ( generalize (F.real_correct xu) ; generalize (F.classify_correct xu) ; generalize (F.valid_ub_correct xu) ; case (F.classify xu) => -> -> ; [xreal_tac xu; [easy|intros _]|xreal_tac xu; [intros _|easy]..] ) ; ( generalize (F.real_correct yl) ; generalize (F.classify_correct yl) ; generalize (F.valid_lb_correct yl) ; case (F.classify yl) => -> -> ; [xreal_tac yl; [easy|intros _]|xreal_tac yl; [intros _|easy]..] ) ; ( generalize (F.real_correct xl) ; generalize (F.classify_correct xl) ; generalize (F.valid_lb_correct xl) ; case (F.classify xl) => -> -> ; [xreal_tac xl; [easy|intros _]|xreal_tac xl; [intros _|easy]..] ) ; simpl ; intros Hmin Hmax ; rewrite ?Hmin, ?Hmax ; try ( intro H; exfalso; lra ) ; try match type of Hmin with | F.classify _ = _ => generalize (F.valid_lb_correct (F.min xl yl)) ; rewrite Hmin => -> | F.toX _ = Xreal _ => rewrite F'.valid_lb_real; [|now rewrite F.real_correct, Hmin] end ; try match type of Hmax with | F.classify _ = _ => generalize (F.valid_ub_correct (F.max xu yu)) ; rewrite Hmax => -> | F.toX _ = Xreal _ => rewrite F'.valid_ub_real; [|now rewrite F.real_correct, Hmax] end ; simpl ; try match goal with | |- context [ F.valid_lb ?x ] => match goal with | H : F.toX x = Xreal _ |- _ => rewrite F'.valid_lb_real; [|now rewrite F.real_correct, H] end end ; try match goal with | |- context [ F.valid_ub ?x ] => match goal with | H : F.toX x = Xreal _ |- _ => rewrite F'.valid_ub_real; [|now rewrite F.real_correct, H] end end ; simpl ; try match goal with | |- context [ F.toX (F.min _ _) ] => match type of Hmin with | F.classify _ = _ => generalize (F.classify_correct (F.min xl yl)) ; rewrite Hmin, F.real_correct ; case (F.toX (F.min xl yl)); try easy; intros _ end end ; try match goal with | |- context [ F.toX (F.max _ _) ] => match type of Hmax with | F.classify _ = _ => generalize (F.classify_correct (F.max xu yu)) ; rewrite Hmax, F.real_correct ; case (F.toX (F.max xu yu)); try easy; intros _ end end ; do 2 try match goal with | |- context [ F.toX ?x ] => match goal with | H : F.toX x = _ |- _ => rewrite H end end ; intro H ; split ; try exact I ; destruct H ; try ( exfalso ; lra ) ; try match goal with | |- context [ Rmin ?x ?y ] => generalize (Rmin_l x y) ; generalize (Rmin_r x y) ; lra end ; try match goal with | |- context [ Rmax ?x ?y ] => generalize (Rmax_l x y) ; generalize (Rmax_r x y) ; lra end ; easy. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval