proposition: Lemma destructLet : forall Tl T1 T2 (P : evalExprTypeRounded T1 -> evalExprTypeRounded T2 -> Prop) (Q : evalExprTypeRounded T1 -> Prop) (x : ArithExpr Tl T1) (t : ArithExpr (T1 :: Tl) T2) (lM : evalExprTypeRounded_list Tl) md, let xM := evalRounded x lM md in wellBehaved x lM md -> (wellBehaved x lM md -> Q (evalRounded x lM md)) -> (forall xM', Q xM' -> wellBehaved t (xM', lM) md /\ P xM' (evalRounded t (xM', lM) md)) -> wellBehaved (Let x t) lM md /\ P xM (evalRounded (Let x t) lM md).
proof: Proof. intros Tl T1 T2 P Q x t lM md xM IWB IQ H. specialize (IQ IWB). simpl. now split; [split; [assumption |] | fold xM]; apply H. Qed.
imports: Coq(Reals List) Flocq(Core BinarySingleNaN Operations) Lang_expr Lang_simpl