proposition: Lemma compare_correct : forall xi yi, forall x, BND x xi -> match compare xi yi with | ARimply => BND x yi | ARcontradict => not (BND x yi) | ARunknown => True end.
proof: Proof. intros (xl,xu) (yl,yu) x ; unfold compare, subset, empty_inter, BND ; simpl. intros (Hx1,Hx2). generalize (Fle2_correct yl xl) (Fle2_correct xu yu) (Flt2_correct xu yl) (Flt2_correct yu xl). case Fle2. case Fle2. intros H1 H2 _ _. split. apply Rle_trans with (2 := Hx1). now apply H1. apply Rle_trans with (1 := Hx2). now apply H2. case Flt2. intros H1 _ H2 _. apply False_rec. apply (Rlt_irrefl yl). apply Rle_lt_trans with (1 := H1 eq_refl). apply Rle_lt_trans with (1 := Hx1). apply Rle_lt_trans with (1 := Hx2). now apply H2. case Flt2 ; try easy. intros _ _ _ H. intros (_,Hy). apply (Rlt_irrefl x). apply Rle_lt_trans with (1 := Hy). apply Rlt_le_trans with (2 := Hx1). now apply H. case Flt2. intros _ _ H _. intros (Hy,_). apply (Rlt_irrefl x). apply Rle_lt_trans with (1 := Hx2). apply Rlt_le_trans with (2 := Hy). now apply H. case Flt2 ; try easy. intros _ _ _ H. intros (_,Hy). apply (Rlt_irrefl x). apply Rle_lt_trans with (1 := Hy). apply Rlt_le_trans with (2 := Hx1). now apply H. Qed.
imports: Reals List Bool Gappa_common