First proof over Reals in Coq

Question

I'm new to Coq. I've been working through Pierce's Logical Foundations. I'm stepping out-of-scope of the text into Real numbers and finding myself clueless. I thought I'd prove something easy so I wrote out some formulas for interest calculations. Now I'd like to prove my conversions are correctly written in my Theorem.

I have no idea how to proceed and am in need of hints and guides!!!

From Coq Require Import Reals.Reals. 

Definition simple_compound (A r n m : R) : R :=
  A * (Rpower (1 + r / m) (m * n)). 
Definition continuous_compound (A r n: R) : R :=
  A * (exp (r * n)).

Definition simple_to_continuous_interest (Rm n m: R) : R :=
  m * ln (1 + Rm). 

Definition continuous_to_simple_interest (Rc n m: R) : R :=
  m * (exp (Rc / m) - 1). 

(** Prove that given Rm n m, then Rc is m * ln (1 + Rm). *)

Theorem continuous_to_simple_works : forall (A Rc n m : R),
  continuous_compound A Rc n = simple_compound A (continuous_to_simple_interest Rc n m) n m. 
Proof.
  intros A Rc n m.
  unfold continuous_compound. unfold simple_compound. unfold continuous_to_simple_interest.
  simpl. (** ... and I'm stuck. I would know how to do this algebraically but am clueless in Coq. *)

Answer 1

First, I suggest to unfold Rpower.

Second, a useful lemma is f_equal; it states that, to prove f a = f b, it suffices to prove a = b. (There is also a tactic with the exact same name, which will behave similarly.)

Third, you need to perform some algebraic simplifications. To do so, you can use replace foo with bar; as the name implies, it replaces all the occurrences of foo in the goal with bar and it requires you to prove bar = foo. This latter equality can then be discharged with the field tactic, which checks that two expressions are equal by using the rewriting rules of addition, multiplication, division.

Fourth, you should end up with a goal containing a subterm ln (exp baz). Obviously, you want to replace it with baz. You can use the command Search (ln (exp _)) to find the name of the corresponding lemma. It happens to be named ln_exp, so rewrite ln_exp will do the trick.