proposition: Lemma compatible_correct : forall t l, compatible t = true -> evalCArithExpr1 t l = evalCArithExpr2 t l.
proof: Proof. unfold evalCArithExpr1. induction t as [| | | OP | | | | |]; simpl; intros. 6, 7: now rewrite IHt, Rrnd.nearbyint_IZR. 1, 2, 3, 6: easy. - apply andb_prop in H. destruct H as [H1 H2]. destruct OP; simpl; (rewrite IHt1, IHt2; [| easy | easy]); [easy | easy | easy | easy |]. now rewrite Rrnd.nearbyint_IZR. - destruct m; [.. | easy]; now rewrite IHt. - now rewrite IHt. 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