fact: Fixpoint simplify_R (e : Expr_R) : Expr_R := match e with | ER_Q q => ER_Q q | ER_R r => ER_R r | ER_Z z => ER_Q (z#1) | ER_Unary f a => let a':=simplify_R a in match a' with | ER_Q aq => if unary_check_args_Q f aq then ER_Q ((unary_fun_Q f) aq) else ER_Unary f a' | _ => ER_Unary f a' end | ER_Binary f a b => let a':=simplify_R a in let b':=simplify_R b in match a', b' with | ER_Q aq, ER_Q bq => if binary_check_args_Q f aq bq then ER_Q ((binary_fun_Q f) aq bq) else ER_Binary f a' b' | _, _ => ER_Binary f a' b' end | ER_Pow a b => let a':=simplify_R a in match a', b with | ER_Q aq, EN_lit bn => ER_Q (Qpower aq (Z.of_nat bn)) | _, _ => ER_Pow a' b end end.
imports: Reals ZArith QArith Lra Lia Ltac2.Ltac2 Ltac2.Printf Ltac2.Bool