proposition: Corollary extractCProp_correct {Tl T} : forall (t : ArithExpr Tl T), ArrayFree t -> forall (lM : evalExprTypeRounded_list Tl) md, md <> mode_NA -> let lR := M2R_list lM in let '(bt, p) := extractCProp t md in let l' := BTreeToList bt in (forall k, compatible_atom (nth k l' (InInt32 (CInt 0))) = true) /\ (CPropToProp (merge l' p) (toList lR) -> wellBehaved t lM md).
proof: Proof. intros t IAF lM md Hmd lR. unfold extractCProp. set (l := toList lR). set (vars := (map add_compatibility (list_var (length Tl)))). generalize (decomposeToCProp_correct t IAF lM vars l md Hmd). set (q := decomposeToCProp _ _ _). destruct_tuple_obj q. unfold vars. unfold l at 1. intros H. specialize (H (well_formed_list_var lR)). rewrite merge_decomp in H. rewrite merge_decomp. rewrite simplifyCProp_correct. split; apply H. Qed.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr