proposition: Lemma simplify_domain_correct : forall d l, interp_domain l (simplify_domain d) -> interp_domain l d.
proof: Proof. intros d. induction d using domain_ind' => l ; try easy ; simpl. set (f := fun (d : domain) (acc : seq domain) => match simplify_domain d with | Never => Never :: nil | Always => acc | And l0 => l0 ++ acc | _ => simplify_domain d :: acc end). intros H'. have: (foldr (fun d acc => interp_domain l d /\ acc) True (foldr f nil ld)). by move: (foldr f nil ld) H' => [|h [|s]]. clear H'. revert H. induction ld as [|t] => H. easy. simpl in H |- *. destruct H as (Ha,Hb). revert Ha. rewrite /f -/f. case (simplify_domain t) ; simpl. now intros _ (H,_). exact (fun H1 H2 => conj (H1 l I) (IHld Hb H2)). intros df e H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros n k f' le H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros m n k f' le H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros n e H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros m n e H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros e0 e1 e2 H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros n e0 e1 e2 H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros n e0 e1 H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros ls H1 H2. rewrite foldr_cat in H2. refine ((fun H => conj (H1 l (proj1 H)) (IHld Hb (proj2 H))) _). revert H2. generalize (foldr f nil ld). clear. induction ls. done. simpl. split. split. apply H2. eapply (fun s H => proj1 (IHls s H)). apply H2. now apply IHls. intros e1 e2 d H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros e d H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros n d H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros m n d H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). intros n e1 e2 d H1 (H2,H3). exact (conj (H1 l H2) (IHld Hb H3)). revert IHd. assert (HH: forall d', (forall l, interp_domain l d' -> interp_domain l d) -> interp_domain l (Forall e1 e2 d') -> interp_domain l (Forall e1 e2 d)). simpl. intros d' H1 H2 t Ht. apply H1. now apply H2. destruct (simplify_domain d) ; try (apply HH ; fail). easy. simpl. intros H _ t Ht. now apply H. revert IHd. assert (HH: forall d', (forall l, interp_domain l d' -> interp_domain l d) -> interp_domain l (Forone e d') -> interp_domain l (Forone e d)). simpl. intros d' H1 H2. apply H1. now apply H2. destruct (simplify_domain d) ; apply HH. revert IHd. assert (HH: forall d', (forall l, interp_domain l d' -> interp_domain l d) -> interp_domain l (Locally n d') -> interp_domain l (Locally n d)). simpl. intros d' H1 (eps,H2). exists eps => t Ht. apply H1. now apply H2. destruct (simplify_domain d) ; try (apply HH ; fail). easy. simpl. intros H _. exists (mkposreal _ Rlt_0_1) => t Ht. now apply H. revert IHd. assert (HH: forall d', (forall l, interp_domain l d' -> interp_domain l d) -> interp_domain l (Locally2 m n d') -> interp_domain l (Locally2 m n d)). simpl. intros d' H1 (eps,H2). exists eps => u v Hu Hv. apply H1. now apply H2. destruct (simplify_domain d) ; try (apply HH ; fail). easy. simpl. intros H _. exists (mkposreal _ Rlt_0_1) => u v Hu Hv. now apply H. revert IHd. assert (HH: forall d', (forall l, interp_domain l d' -> interp_domain l d) -> interp_domain l (ForallWide n e1 e2 d') -> interp_domain l (ForallWide n e1 e2 d)). simpl. intros d' H1 (e,H2). exists e => t u Ht Hu. apply H1. now apply H2. destruct (simplify_domain d) ; try (apply HH ; fail). easy. simpl. intros H _. exists (mkposreal _ Rlt_0_1) => u v Hu Hv. now apply H. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct