proposition: Theorem relate'_correct : forall p q rm, interp_pos_atom p rm -> match relate' p q with | ARimply => interp_pos_atom q rm | ARcontradict => not (interp_pos_atom q rm) | ARunknown => True end.
proof: Proof. intros [px pi|px pu|px pl|px pi|px py pi|px pc|px pc|px|px py] [qx qi|qx qu|qx ql|qx qi|qx qy qi|qx qc|qx qc|qx|qx qy] rm Hp ; try exact I ; simpl. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (compare_correct pi qi _ Hp). now case compare. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (Fle2_correct (upper pi) qu). case Fle2. intros H'. apply Rle_trans with (1 := proj2 Hp). now apply H'. intros _. generalize (Flt2_correct qu (lower pi)). case Flt2 ; try easy. intros H' H''. apply Rlt_not_le with (1 := H' eq_refl). now apply Rle_trans with (1 := proj1 Hp). generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (Fle2_correct ql (lower pi)). case Fle2. intros H'. apply Rle_trans with (2 := proj1 Hp). now apply H'. intros _. generalize (Flt2_correct (upper pi) ql). case Flt2 ; try easy. intros H' H''. apply Rlt_not_le with (1 := H' eq_refl). now apply Rle_trans with (2 := proj2 Hp). generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (Flt2_correct pu (lower qi)). case Flt2 ; try easy. intros H' H''. apply (Rlt_not_le _ _ (H' eq_refl)). apply Rle_trans with (2 := Hp). apply H''. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (Fle2_correct pu qu). case Fle2 ; try easy. intros H'. apply Rle_trans with (1 := Hp). now apply H'. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (Flt2_correct pu ql). case Flt2 ; try easy. intros H'. apply Rlt_not_le. apply Rle_lt_trans with (1 := Hp). now apply H'. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (Flt2_correct (upper qi) pl). case Flt2 ; try easy. intros H' H''. apply (Rlt_not_le _ _ (H' eq_refl)). apply Rle_trans with (1 := Hp). apply H''. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (Flt2_correct qu pl). case Flt2 ; try easy. intros H'. apply Rlt_not_le. apply Rlt_le_trans with (2 := Hp). now apply H'. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (Fle2_correct ql pl). case Fle2 ; try easy. intros H'. apply Rle_trans with (2 := Hp). now apply H'. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. generalize (Fpos0_correct (lower qi)). case Fpos0 ; try easy. intros H'. specialize (H' eq_refl). generalize (compare_correct pi qi _ (proj2 Hp)). case compare ; try easy. try now split. intros H''. contradict H''. apply H''. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. clear H. generalize (index_eq_correct py qy). case index_eq ; try easy. intros H. rewrite H in Hp by easy. clear H. unfold interp_pos_atom in Hp. unfold subset. generalize (Fle2_correct (lower qi) (lower pi)). case Fle2 ; try easy. intros Hl. generalize (Fle2_correct (upper pi) (upper qi)). case Fle2 ; try easy. intros Hu. destruct Hp as (e,(He,Hp)). exists e. split. split. now apply Rle_trans with (1 := Hl eq_refl). now apply Rle_trans with (2 := Hu eq_refl). exact Hp. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. clear H. generalize (Zle_cases qc pc). case (Zle_bool qc pc) ; try easy. intros H. destruct Hp as ((m,e),(Hm,He)). exists (Float2 m e). split. exact Hm. now apply Z.le_trans with (1 := H). generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. clear H. generalize (Zle_cases (Zpos pc) (Zpos qc)). case Zle_bool ; try easy. intros H. destruct Hp as ((m,e),(Hm,He)). exists (Float2 m e). split. exact Hm. apply Z.lt_le_trans with (1 := He). apply le_IZR. change (IZR (Zpower radix2 (Zpos pc)) <= IZR (Zpower radix2 (Zpos qc)))%R. apply IZR_le. now apply Zpower_le. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. now rewrite <- H. generalize (index_eq_correct px qx). case index_eq ; try easy. intros H. rewrite H in Hp by easy. clear H. generalize (index_eq_correct py qy). case index_eq ; try easy. intros H. now rewrite <- H. Qed.
imports: Reals List Bool Gappa_common