proposition: Lemma simplify_R_correct: forall (e : Expr_R), interpret_R e = interpret_R (simplify_R e).
proof: Proof. intros e; induction e as [q|r|z|f a IHa|f a IHa b IHb|a IHa b]. - reflexivity. - reflexivity. - cbn; unfold Q2R; cbn; ltac1:(lra). - cbn. destruct (simplify_R a); rewrite IHa; try reflexivity. cbn. destruct f; cbn. + rewrite Qreals.Q2R_opp; reflexivity. + destruct (Z.eqb_spec (Qnum q) 0) as [Heq|Hneq]; cbn. * reflexivity. * rewrite Qreals.Q2R_inv. 1: reflexivity. unfold Qeq; cbn. ltac1:(lia). - cbn. destruct (simplify_R a) as [qa| | | | |]; rewrite IHa; destruct (simplify_R b) as [qb| | | | |]; rewrite IHb; try reflexivity. cbn. destruct f; cbn. + rewrite Qreals.Q2R_plus; reflexivity. + rewrite Qreals.Q2R_minus; reflexivity. + rewrite Qreals.Q2R_mult; reflexivity. + destruct (Z.eqb_spec (Qnum qb) 0) as [Heq|Hneq]; cbn. * reflexivity. * rewrite Qreals.Q2R_div. 1: reflexivity. unfold Qeq; cbn. ltac1:(lia). + rewrite Q2R_max; reflexivity. + rewrite Q2R_min; reflexivity. - cbn. destruct (simplify_R a); rewrite IHa; try reflexivity. destruct b; cbn; try reflexivity. apply Q2R_pow. Qed.
imports: Reals ZArith QArith Lra Lia Ltac2.Ltac2 Ltac2.Printf Ltac2.Bool