fact: Fixpoint simplify_domain (d : domain) : domain := match d with | And ld => let l := foldr (fun d acc => let d' := simplify_domain d in match d' with | Always => acc | And l => cat l acc | Never => Never :: nil | _ => d' :: acc end) nil ld in match l with | nil => Always | d :: nil => d | _ => And l end | Forall e1 e2 d => let d' := simplify_domain d in match d' with | Always => Always | Never => Never | _ => Forall e1 e2 d' end | Forone e d => let d' := simplify_domain d in match d' with | Always => Always | Never => Never | _ => Forone e d' end | Locally n d => let d' := simplify_domain d in match d' with | Always => Always | Never => Never | _ => Locally n d' end | Locally2 m n d => let d' := simplify_domain d in match d' with | Always => Always | Never => Never | _ => Locally2 m n d' end | ForallWide n e1 e2 d => let d' := simplify_domain d in match d' with | Always => Always | Never => Never | _ => ForallWide n e1 e2 d' end | _ => d end.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct