proposition: Lemma decomposeToCProp_correct {Tl T} : forall (t : ArithExpr Tl T), ArrayFree t -> forall (lM : evalExprTypeRounded_list Tl) vars l md, md <> mode_NA -> let lR := M2R_list lM in well_formed lR vars l -> let '(t', b, bt, p) := decomposeToCProp t vars md in let l' := BTreeToList bt in ( ((b = true -> compatible t' = true) /\ (evalCArithExpr2 t' l = evalReal t lR md)) /\ forall k, compatible_atom (nth k l' (InInt32 (CInt 0))) = true) /\ (CPropToProp (merge l' p) l -> wellBehaved t lM md).
proof: Proof. assert (Haux : forall l', (forall k, compatible_atom (nth k l' (InInt32 (CInt 0))) = true) <-> map (fun p => compatible_atom p) l' = repeat true (length l')). { induction l'; [now split; [| intros _ [|]] |]. destruct IHl' as [IHl'_0 IHl'_1]. simpl. split; intros H. - rewrite (H O). now rewrite IHl'_0; [| intros k; specialize (H (S k))]. - inversion H as [[H0 H1]]. clear H. intros [| k]; [easy |]. rewrite H0 in H1. rewrite H0. now apply IHl'_1. } induction t as [| | Tl n | Tl T OP | Tl OP | | | | | | | | Tl T | | | |]; intros IAF lM vars l md Hmd lR Iwf. 16, 17: now apply IHt. 15: easy. { repeat split. now intros [|]. } all: simpl. - now destruct Prim2B; (split; [| easy]); [simpl; rewrite Rmult_1_r | | | unfold B2R, F2R; destruct s; simpl]; (split; [| destruct k]). - set (d := nth n vars (CInt 0, false)). destruct_tuple_obj d. unfold d. clear d. split; [| easy]. split; [| now intros [|]]. clear IAF. revert n vars l Iwf. induction Tl as [| T Tl]; [now intros [|] [|] | intros [|] [| tb vars] l Hl; destruct_tuple_obj tb; simpl]; [easy | now destruct Hl | easy |]. destruct lM as (xM, lM). apply (IHTl lM _ _ l). now simpl in Hl. - destruct IAF as [IAF1 IAF2]. specialize (IHt1 IAF1 lM vars l md Hmd Iwf). specialize (IHt2 IAF2 lM vars l md Hmd Iwf). revert IHt1 IHt2. fold lR. set (q1 := decomposeToCProp t1 vars md). destruct_tuple_obj q1. set (pq1 := snd q1). set (lq1 := snd (fst q1)). set (bq1 := snd (fst (fst q1))). set (tq1 := fst (fst (fst q1))). set (q2 := decomposeToCProp t2 vars md). destruct_tuple_obj q2. set (pq2 := snd q2). set (lq2 := snd (fst q2)). set (bq2 := snd (fst (fst q2))). set (tq2 := fst (fst (fst q2))). unfold evalCArithExpr1. intros [[[IHt1_1 IHt1_2] IHt1_3] IHt1_4] [[[IHt2_1 IHt2_2] IHt2_3] IHt2_4]. rewrite merge_decomp in IHt1_4, IHt2_4. rewrite Haux in IHt1_3, IHt2_3. destruct T; rewrite Haux. + split. { destruct bq1, bq2; (split; [split | unfold BTreeToList; simpl BTreeToList_aux]); [intros _ | | | easy | | | easy | | | easy | |]. { apply andb_true_intro. now split; [apply IHt1_1 | apply IHt2_1]. } 1, 3, 5, 7: now destruct OP; rewrite <-IHt1_2, <-IHt2_2. all: rewrite (BTreeToList_aux_concat lq1); rewrite (BTreeToList_aux_concat lq2). 2, 4: rewrite 2app_length, 2repeat_app, 2map_app; rewrite IHt1_3, IHt2_3; easy. 2: destruct OP; simpl; [| | | rewrite IHt2_1 by easy]; rewrite 2app_length, 2repeat_app, 2map_app; rewrite IHt1_3, IHt2_3; easy. destruct OP; simpl; rewrite IHt1_1, IHt2_1 by easy; simpl; rewrite 2app_length, 2repeat_app, 2map_app; rewrite IHt1_3, IHt2_3; easy. } rewrite merge_decomp. unfold BTreeToList. simpl. rewrite 3BTreeToList_aux_concat. rewrite 3merge_app. intros [[HOP [Hm1 [Hm2 Hm3]]] [HP [HP1 [HP2 HP3]]]]. fold (BTreeToList lq2) in Hm2. split; [now apply IHt1_4; split | split; [now apply IHt2_4; split |]]. destruct OP; [.. | split]; (destruct bq1, bq2; simpl in HOP; [destruct HOP as [H HOP] | | |]). all: simpl in *. 17-20: now apply neq_IZR; fold (M2R (evalRounded t2 lM md)); rewrite <-evalReal_evalRounded; fold lR; rewrite <-IHt2_2; destruct Hm1. 1-4: rewrite plus_IZR; fold (M2R (evalRounded t1 lM md)); fold (M2R (evalRounded t2 lM md)); rewrite <-2evalReal_evalRounded; fold lR; now rewrite <-IHt1_2, <-IHt2_2. 1-4: rewrite minus_IZR; fold (M2R (evalRounded t1 lM md)); fold (M2R (evalRounded t2 lM md)); rewrite <-2evalReal_evalRounded; fold lR; now rewrite <-IHt1_2, <-IHt2_2. 1-4: rewrite mult_IZR; fold (M2R (evalRounded t1 lM md)); fold (M2R (evalRounded t2 lM md)); rewrite <-2evalReal_evalRounded; fold lR; now rewrite <-IHt1_2, <-IHt2_2. 1-4: rewrite <-Ztrunc_div_; change Ztrunc with (round_mode mode_ZR); rewrite <-Rrnd.nearbyint_IZR; fold (M2R (evalRounded t1 lM md)); fold (M2R (evalRounded t2 lM md)); rewrite <-2evalReal_evalRounded; fold lR; now rewrite <-IHt1_2, <-IHt2_2. + split. { destruct bq1, bq2; (split; [split | unfold BTreeToList; simpl BTreeToList_aux]); [intros _ | | | easy | | | easy | | | easy | |]. { destruct md; [.. | easy]; apply andb_true_intro; now split; [apply IHt1_1 | apply IHt2_1]. } 1, 3, 5, 7: now destruct OP; rewrite <-IHt1_2, <-IHt2_2. all: rewrite (BTreeToList_aux_concat lq1); rewrite (BTreeToList_aux_concat lq2). 2, 4: rewrite 2app_length, 2repeat_app, 2map_app; rewrite IHt1_3, IHt2_3; easy. 2: destruct OP; simpl; [| | | rewrite IHt2_1 by easy]; rewrite 2app_length, 2repeat_app, 2map_app; rewrite IHt1_3, IHt2_3; easy. destruct OP; simpl; rewrite IHt1_1, IHt2_1 by easy; simpl; rewrite 2app_length, 2repeat_app, 2map_app; rewrite IHt1_3, IHt2_3; destruct md; easy. } rewrite merge_decomp. unfold BTreeToList. simpl. rewrite 3BTreeToList_aux_concat. rewrite 3merge_app. intros [[HOP [Hm1 [Hm2 Hm3]]] [HP [HP1 [HP2 HP3]]]]. fold (BTreeToList lq2) in Hm2. split; [now apply IHt1_4; split | split; [now apply IHt2_4; split |]]. destruct OP; [.. | split]; (destruct bq1, bq2; simpl in HOP; [destruct HOP as [H HOP] | | |]). all: simpl in *. 17-20: now fold (M2R (evalRounded t2 lM md)); rewrite <-evalReal_evalRounded; fold lR; rewrite <-IHt2_2; destruct Hm1. 1-4: fold (M2R (evalRounded t1 lM md)); fold (M2R (evalRounded t2 lM md)); rewrite <-2evalReal_evalRounded; fold lR; now rewrite <-IHt1_2, <-IHt2_2. 1-4: fold (M2R (evalRounded t1 lM md)); fold (M2R (evalRounded t2 lM md)); rewrite <-2evalReal_evalRounded; fold lR; now rewrite <-IHt1_2, <-IHt2_2. 1-4: fold (M2R (evalRounded t1 lM md)); fold (M2R (evalRounded t2 lM md)); rewrite <-2evalReal_evalRounded; fold lR; now rewrite <-IHt1_2, <-IHt2_2. 1-4: fold (M2R (evalRounded t1 lM md)); fold (M2R (evalRounded t2 lM md)); rewrite <-2evalReal_evalRounded; fold lR; now rewrite <-IHt1_2, <-IHt2_2. - destruct IAF as [IAF1 IAF2]. specialize (IHt1 IAF1 lM vars l md Hmd Iwf). specialize (IHt2 IAF2 lM vars l md Hmd Iwf). revert IHt1 IHt2. fold lR. set (q1 := decomposeToCProp t1 vars md). destruct_tuple_obj q1. set (pq1 := snd q1). set (lq1 := snd (fst q1)). set (bq1 := snd (fst (fst q1))). set (tq1 := fst (fst (fst q1))). set (q2 := decomposeToCProp t2 vars md). destruct_tuple_obj q2. set (pq2 := snd q2). set (lq2 := snd (fst q2)). set (bq2 := snd (fst (fst q2))). set (tq2 := fst (fst (fst q2))). unfold evalCArithExpr1. intros [[[IHt1_1 IHt1_2] IHt1_3] IHt1_4] [[[IHt2_1 IHt2_2] IHt2_3] IHt2_4]. rewrite merge_decomp in IHt1_4, IHt2_4. rewrite Haux in IHt1_3, IHt2_3. rewrite Haux. split. { destruct bq1, bq2; (split; [split | unfold BTreeToList; simpl BTreeToList_aux]); [intros _ | | | easy | | | easy | | | easy | |]. { destruct md; [.. | easy]; apply andb_true_intro; now split; [apply IHt1_1 | apply IHt2_1]. } 1, 3, 5, 7: now destruct OP; rewrite <-IHt1_2, <-IHt2_2. all: rewrite (BTreeToList_aux_concat lq1); rewrite (BTreeToList_aux_concat lq2). 2, 4: rewrite 2app_length, 2repeat_app, 2map_app; rewrite IHt1_3, IHt2_3; easy. 2: destruct OP; simpl; rewrite 2app_length, 2repeat_app, 2map_app; rewrite IHt1_3, IHt2_3; easy. destruct OP; simpl; rewrite IHt1_1, IHt2_1 by easy; simpl; rewrite 2app_length, 2repeat_app, 2map_app; rewrite IHt1_3, IHt2_3; destruct md; easy. } rewrite merge_decomp. unfold BTreeToList. simpl. rewrite 3BTreeToList_aux_concat. rewrite 3merge_app. intros [[HOP [Hm1 Hm2]] [[HP HP3] [HP1 HP2]]]. fold (BTreeToList lq2) in Hm2. destruct OP; [| | | split]. 5: { fold (M2R (evalRounded t2 lM md)). rewrite <-evalReal_evalRounded. fold lR. rewrite <-IHt2_2. destruct bq1, bq2; simpl in HOP; [destruct HOP as [[_ H] HOP] | | |]; now simpl in HP. } 1-4: split; [now apply IHt1_4; split | split; [now apply IHt2_4; split | split]]. 1-8: fold (M2R (evalRounded t1 lM md)). 1-8: fold (M2R (evalRounded t2 lM md)). 1-8: rewrite <-2evalReal_evalRounded. 1-8: fold lR. 1-8: rewrite <-IHt1_2, <-IHt2_2. 1, 3, 5, 7: destruct bq1, bq2; simpl in *; now destruct HOP. 1-4: now simpl in HP3. - destruct IAF as [IAF1 [IAF2 IAF3]]. specialize (IHt1 IAF1 lM vars l md Hmd Iwf). specialize (IHt2 IAF2 lM vars l md Hmd Iwf). specialize (IHt3 IAF3 lM vars l md Hmd Iwf). revert IHt1 IHt2 IHt3. set (q1 := decomposeToCProp t1 vars md). destruct_tuple_obj q1. set (pq1 := snd q1). set (lq1 := snd (fst q1)). set (bq1 := snd (fst (fst q1))). set (tq1 := fst (fst (fst q1))). set (q2 := decomposeToCProp t2 vars md). destruct_tuple_obj q2. set (pq2 := snd q2). set (lq2 := snd (fst q2)). set (bq2 := snd (fst (fst q2))). set (tq2 := fst (fst (fst q2))). set (q3 := decomposeToCProp t3 vars md). destruct_tuple_obj q3. set (pq3 := snd q3). set (lq3 := snd (fst q3)). set (bq3 := snd (fst (fst q3))). set (tq3 := fst (fst (fst q3))). unfold evalCArithExpr1. intros [[[IHt1_1 IHt1_2] IHt1_3] IHt1_4] [[[IHt2_1 IHt2_2] IHt2_3] IHt2_4] [[[IHt3_1 IHt3_2] IHt3_3] IHt3_4]. rewrite merge_decomp in IHt1_4, IHt2_4, IHt3_4. rewrite Haux in IHt1_3, IHt2_3, IHt3_3. rewrite Haux. split. { destruct bq1, bq2, bq3; (split; [split | unfold BTreeToList; simpl BTreeToList_aux]); [intros _ | | | easy | | | easy | | | easy | | | easy | | | easy | | | easy | | | easy | |]. { destruct md; [.. | easy]; apply andb_true_intro; (split; [| now apply IHt3_1]); apply andb_true_intro; now split; [apply IHt1_1 | apply IHt2_1]. } 2: simpl; rewrite IHt1_1, IHt2_1, IHt3_1 by easy; simpl. 2, 4, 6, 8, 10, 12, 14, 16: rewrite (BTreeToList_aux_concat lq1); rewrite (BTreeToList_aux_concat lq2); rewrite (BTreeToList_aux_concat lq3); rewrite 3app_length, 3repeat_app, 3map_app; rewrite IHt1_3, IHt2_3, IHt3_3; destruct md; easy. all: now unfold lR; rewrite <-IHt1_2, <-IHt2_2, <-IHt3_2. } rewrite merge_decomp. unfold BTreeToList. simpl. rewrite 3BTreeToList_aux_concat. rewrite 3merge_app. intros [[HOP [Hm1 [Hm2 Hm3]]] [HP [[HP1 HP2] HP3]]]. fold (BTreeToList lq3) in Hm3. split; [now apply IHt1_4; split | split; [now apply IHt2_4; split | split; [now apply IHt3_4; split |]]]. destruct bq1, bq2, bq3; simpl in HOP; [destruct HOP as [_ HOP] | | | | | | |]. 1-8: simpl in HP. 1-8: fold (M2R (evalRounded t1 lM md)). 1-8: fold (M2R (evalRounded t2 lM md)). 1-8: fold (M2R (evalRounded t3 lM md)). 1-8: rewrite <-3evalReal_evalRounded. 1-8: now rewrite <-IHt1_2, <-IHt2_2, <-IHt3_2. - destruct IAF as [IAF1 [IAF2 IAF3]]. specialize (IHt1 IAF1 lM vars l md Hmd Iwf). specialize (IHt2 IAF2 lM vars l md Hmd Iwf). specialize (IHt3 IAF3 lM vars l md Hmd Iwf). revert IHt1 IHt2 IHt3. set (q1 := decomposeToCProp t1 vars md). destruct_tuple_obj q1. set (pq1 := snd q1). set (lq1 := snd (fst q1)). set (bq1 := snd (fst (fst q1))). set (tq1 := fst (fst (fst q1))). set (q2 := decomposeToCProp t2 vars md). destruct_tuple_obj q2. set (pq2 := snd q2). set (lq2 := snd (fst q2)). set (bq2 := snd (fst (fst q2))). set (tq2 := fst (fst (fst q2))). set (q3 := decomposeToCProp t3 vars md). destruct_tuple_obj q3. set (pq3 := snd q3). set (lq3 := snd (fst q3)). set (bq3 := snd (fst (fst q3))). set (tq3 := fst (fst (fst q3))). unfold evalCArithExpr1. intros [[[IHt1_1 IHt1_2] IHt1_3] IHt1_4] [[[IHt2_1 IHt2_2] IHt2_3] IHt2_4] [[[IHt3_1 IHt3_2] IHt3_3] IHt3_4]. rewrite merge_decomp in IHt1_4, IHt2_4, IHt3_4. rewrite Haux in IHt1_3, IHt2_3, IHt3_3. rewrite Haux. split. { destruct bq1, bq2, bq3; (split; [split | unfold BTreeToList; simpl BTreeToList_aux]); [intros _ | | | easy | | | easy | | | easy | | | easy | | | easy | | | easy | | | easy | |]. { destruct md; [.. | easy]; apply andb_true_intro; (split; [| now apply IHt3_1]); apply andb_true_intro; now split; [apply IHt1_1 | apply IHt2_1]. } 2: simpl; rewrite IHt1_1, IHt2_1, IHt3_1 by easy; simpl. 2, 4, 6, 8, 10, 12, 14, 16: rewrite (BTreeToList_aux_concat lq1); rewrite (BTreeToList_aux_concat lq2); rewrite (BTreeToList_aux_concat lq3); rewrite 3app_length, 3repeat_app, 3map_app; rewrite IHt1_3, IHt2_3, IHt3_3; destruct md; easy. all: now unfold lR; rewrite <-IHt1_2, <-IHt2_2, <-IHt3_2. } rewrite merge_decomp. unfold BTreeToList. simpl. rewrite 3BTreeToList_aux_concat. rewrite 3merge_app. intros [[HOP [Hm1 [Hm2 Hm3]]] [[HP [[HP1 HP2] HP3]] HP4]]. fold (BTreeToList lq3) in Hm3. split; [now apply IHt1_4; split | split; [now apply IHt2_4; split | split; [now apply IHt3_4; split |]]]. fold (M2R (evalRounded t1 lM md)). fold (M2R (evalRounded t2 lM md)). fold (M2R (evalRounded t3 lM md)). rewrite <-3evalReal_evalRounded. unfold Rrnd.fma. rewrite <-IHt1_2, <-IHt2_2, <-IHt3_2. split; [| easy]. now destruct bq1, bq2, bq3; simpl in HOP; [destruct HOP as [_ HOP] | | | | | | |]. - specialize (IHt IAF lM vars l md Hmd Iwf). revert IHt. set (q := decomposeToCProp t vars md). destruct_tuple_obj q. set (pq := snd q). set (lq := snd (fst q)). set (bq := snd (fst (fst q))). set (tq := fst (fst (fst q))). intros [[[IHt_1 IHt_2] IHt_3] IHt_4]. rewrite Haux in IHt_3. rewrite Haux. split; [| assumption]. now destruct bq; simpl; (split; [split | assumption]); [assumption | | easy |]; rewrite IHt_2. - specialize (IHt IAF lM vars l md Hmd Iwf). simpl in IHt. revert IHt. set (q := decomposeToCProp t vars md). destruct_tuple_obj q. set (pq := snd q). set (lq := snd (fst q)). set (bq := snd (fst (fst q))). set (tq := fst (fst (fst q))). intros [[[IHt_1 IHt_2] IHt_3] IHt_4]. rewrite Haux in IHt_3. rewrite Haux. destruct bq; simpl; (split; [split; [split; [assumption | now rewrite IHt_2] |] |]); [rewrite IHt_1 by easy; now apply f_equal | | assumption | unfold BTreeToList]; rewrite merge_decomp; cbn; rewrite IHt_2, evalReal_evalRounded; simpl; [intros [H0 [[_ H1] [H2 H3]]] | intros [H0 [[H2 H3] H1]]]; (split; [| easy]); apply IHt_4; rewrite merge_decomp; split; assumption. - specialize (IHt IAF lM vars l md Hmd Iwf). simpl in IHt. revert IHt. set (q := decomposeToCProp t vars md). destruct_tuple_obj q. set (pq := snd q). set (lq := snd (fst q)). set (bq := snd (fst (fst q))). set (tq := fst (fst (fst q))). intros [[[IHt_1 IHt_2] IHt_3] IHt_4]. rewrite Haux in IHt_3. rewrite Haux. destruct bq; simpl; (split; [split; [split; [assumption | now rewrite IHt_2] |] |]); [rewrite IHt_1 by easy; now apply f_equal | | assumption | unfold BTreeToList]; rewrite merge_decomp; cbn; rewrite IHt_2, evalReal_evalRounded; simpl; [intros [H0 [[_ H1] [H2 H3]]] | intros [H0 [[H2 H3] H1]]]; (split; [| easy]); apply IHt_4; rewrite merge_decomp; split; assumption. - specialize (IHt IAF lM vars l md Hmd Iwf). simpl in IHt. revert IHt. set (q := decomposeToCProp t vars md). destruct_tuple_obj q. set (pq := snd q). set (lq := snd (fst q)). set (bq := snd (fst (fst q))). set (tq := fst (fst (fst q))). intros [[[IHt_1 IHt_2] IHt_3] IHt_4]. rewrite Haux in IHt_3. rewrite Haux. destruct bq; simpl; (split; [split; [split; [assumption | now rewrite IHt_2] |] |]); [rewrite IHt_1 by easy; now apply f_equal | | assumption | unfold BTreeToList]; rewrite merge_decomp; cbn; unfold Rrnd.trunc; rewrite IHt_2, round_FIX_IZR, evalReal_evalRounded; simpl; [intros [H0 [[_ H1] [H2 H3]]] | intros [H0 [[H2 H3] H1]]]; rewrite <-opp_IZR in H2; apply le_IZR in H2, H3; (split; [| easy]); apply IHt_4; rewrite merge_decomp; split; assumption. - specialize (IHt IAF lM vars l md Hmd Iwf). simpl in IHt. revert IHt. set (q := decomposeToCProp t vars md). destruct_tuple_obj q. set (pq := snd q). set (lq := snd (fst q)). set (bq := snd (fst (fst q))). set (tq := fst (fst (fst q))). intros [[[IHt_1 IHt_2] IHt_3] IHt_4]. rewrite Haux in IHt_3. rewrite Haux. split; [split; [easy |] |]. + destruct bq; simpl; unfold BTreeToList in IHt_3; [now rewrite IHt_1, IHt_3 |]. now unfold BTreeToList. + intros H. destruct bq; rewrite merge_decomp in H; simpl in H; destruct H as [H1 [H3 H4]]; rewrite merge_decomp in H1; destruct H1 as [H1 H2]; simpl in H1, H2; destruct H2; (split; [now apply IHt_4; unfold BTreeToList; rewrite merge_decomp |]); fold (M2R (evalRounded t lM md)); rewrite <-evalReal_evalRounded; now rewrite <-IHt_2. - specialize (IHt IAF lM vars l md Hmd Iwf). simpl in IHt. revert IHt. set (q := decomposeToCProp t vars md). destruct_tuple_obj q. set (pq := snd q). set (lq := snd (fst q)). set (bq := snd (fst (fst q))). set (tq := fst (fst (fst q))). intros [[[IHt_1 IHt_2] IHt_3] IHt_4]. rewrite Haux in IHt_3. destruct T; rewrite Haux. + split; [split; [split; [easy | now simpl; unfold lR; rewrite IHt_2] |] |]. * destruct bq; simpl; unfold BTreeToList in IHt_3; [now rewrite IHt_1, IHt_3 |]. now unfold BTreeToList. * intros H. destruct bq; rewrite merge_decomp in H; simpl in H; destruct H as [H1 [H3 H4]]; rewrite merge_decomp in H1; destruct H1 as [H1 H2]; simpl in H1, H2; destruct H2; (split; [now apply IHt_4; unfold BTreeToList; rewrite merge_decomp |]); fold (M2R (evalRounded t lM md)); rewrite <-evalReal_evalRounded; rewrite <-IHt_2; lra. + split; [split; [split; [now destruct md | now simpl; unfold lR; rewrite IHt_2] |] |]. * destruct bq; simpl; unfold BTreeToList in IHt_3; [now rewrite IHt_1, IHt_3 |]. now unfold BTreeToList. * intros H. destruct bq; rewrite merge_decomp in H; simpl in H; destruct H as [H1 [H3 H4]]; rewrite merge_decomp in H1; destruct H1 as [H1 H2]; simpl in H1, H2; destruct H2; (split; [now apply IHt_4; unfold BTreeToList; rewrite merge_decomp |]); fold (M2R (evalRounded t lM md)); rewrite <-evalReal_evalRounded; rewrite <-IHt_2; lra. - set (xM := evalRounded t1 lM md). set (xR := evalReal t1 lR md). destruct IAF as [IAF1 IAF2]. specialize (IHt1 IAF1 lM vars l md Hmd Iwf). revert IHt1. set (q1 := decomposeToCProp t1 vars md). destruct_tuple_obj q1. set (pq1 := snd q1). set (lq1 := snd (fst q1)). set (bq1 := snd (fst (fst q1))). set (tq1 := fst (fst (fst q1))). unfold evalCArithExpr1. intros [[[IHt1_1 IHt1_2] IHt1_3] IHt1_4]. specialize (IHt2 IAF2 (xM, lM) ((tq1, bq1) :: vars) l md Hmd). simpl in IHt2. assert (H : (bq1 = true -> compatible tq1 = true) /\ evalCArithExpr2 tq1 l = xR /\ well_formed lR vars l). { now repeat split. } unfold xR, lR in H. rewrite evalReal_evalRounded in H. fold xM in H. specialize (IHt2 H). revert IHt2. set (q2 := decomposeToCProp t2 ((tq1, bq1) :: vars) md). destruct_tuple_obj q2. set (pq2 := snd q2). set (lq2 := snd (fst q2)). set (bq2 := snd (fst (fst q2))). set (tq2 := fst (fst (fst q2))). intros [[[IHt2_1 IHt2_2] IHt2_3] IHt2_4]. rewrite merge_decomp in IHt1_4, IHt2_4. rewrite Haux in IHt1_3, IHt2_3. rewrite Haux. split. { split; [split; [easy |]; rewrite IHt2_2; unfold xM, xR, lR; now rewrite evalReal_evalRounded |]. unfold BTreeToList. simpl. rewrite (BTreeToList_aux_concat lq1). rewrite (BTreeToList_aux_concat lq2). rewrite 2app_length, 2repeat_app, 2map_app. now rewrite IHt1_3, IHt2_3. } rewrite merge_decomp. unfold BTreeToList. simpl. rewrite 2BTreeToList_aux_concat. rewrite 2merge_app. intros [[Hm1 [Hm2 _]] [HP1 HP2]]. split; [now apply IHt1_4 | now apply IHt2_4]. 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