proposition: Theorem split_piece_correct : forall prec midp f fi p, (forall u v, valid f u v (fi u v)) -> invariant f (snd p) -> invariant f (snd (split_piece prec midp fi p)).
proof: Proof. intros prec midp f fi [sp p] Hfi [H1 [qh [qt [H2 H3]]]]. unfold split_piece. set (le_piece := le_piece prec). generalize (ptree_pop_correct le_piece p). destruct ptree_pop as [[u' v' i] p1]. intros H4. set (m := IBp (midp u' v')). generalize (pheap_insert_correct le_piece p1 (Piece u' m (fi u' m))). generalize (pheap_insert le_piece p1 (Piece u' m (fi u' m))). intros p2 H5. generalize (ptree_insert_correct le_piece p2 (Piece m v' (fi m v'))). generalize (ptree_insert le_piece p2 (Piece m v' (fi m v'))). intros p3 H6. unfold invariant. split. - apply permut_sym in H6. apply all_permut with (2 := H6). split. apply Hfi. apply permut_sym in H5. apply all_permut with (2 := H5). split. apply Hfi. clear -H1 H4. apply permut_sym in H4. eapply all_permut in H4. 2: apply H1. apply H4. - assert (H7 := permut_trans _ _ _ H4 H2). destruct (permut_remove _ _ _ H7) as [s [t [H8 H9]]]. assert (exists sh st, sh :: st = s ++ Piece u' m (fi u' m) :: nil) as [sh [st Ha]]. clear. destruct s as [|sh st]. now exists (Piece u' m (fi u' m)), nil. now exists sh, (st ++ Piece u' m (fi u' m) :: nil). exists sh, (st ++ Piece m v' (fi m v') :: t). split. change (sh :: st ++ _) with ((sh :: st) ++ Piece m v' (fi m v') :: t). rewrite Ha. apply permut_trans with (1 := H6). eapply permut_trans. 2: apply permut_insert. apply permut_cons. rewrite <- app_assoc. simpl. apply permut_trans with (1 := H5). eapply permut_trans. 2: apply permut_insert. now apply permut_cons. revert H3 H8 Ha. clear. generalize IBu. revert qh qt sh st. induction s as [|[u v i'] s IH] ; simpl ; intros qh qt sh st x H1 [= -> ->] [= -> ->]. simpl. destruct t as [|th tt]. now destruct H1. now destruct H1. destruct s as [|sh st]. destruct H1 as [H1 H2]. simpl. apply (conj H1). destruct v as [| |x'] ; try easy. destruct t as [|th tt]. now destruct H2. now destruct H2. destruct H1 as [H1 H2]. simpl. apply (conj H1). destruct v as [| |x'] ; try easy. now apply IH with (1 := H2). Qed.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority