I'm new to Coq. I've been working through Pierce's Logical Foundations. I'm stepping into new ground.
I'm trying use of the field tactic for the first time. I use it thrice in the below theorem. Twice it fails, yielding m <> 0%R where m is a term in context.
I'm sure I just fail to understand proper use. May someone enlighten me? (I tried reading this doc page but didn't gain much understanding!)
From Coq Require Import Reals.Reals.
Require Import Field.
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 (Rs n m: R) : R :=
m * ln (1 + Rs / m).
Definition continuous_to_simple_interest (Rc n m: R) : R :=
m * ((exp (Rc / m)) - 1).
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.
unfold Rpower. apply f_equal.
assert (H: (m * (exp (Rc / m) - 1) / m)%R = (exp (Rc / m) - 1)%R). {
field. admit.
}
rewrite -> H.
assert (H2: (1 + (exp (Rc / m) - 1))%R = (exp (Rc / m))%R). {
field.
}
rewrite -> H2.
assert (H3: (m * n * ln (exp (Rc / m)))%R = (ln (exp (Rc / m)) * m * n)%R). {
rewrite -> Rmult_comm. rewrite -> Rmult_assoc. reflexivity.
}
rewrite -> H3.
rewrite -> ln_exp.
assert (H4: (Rc / m * m)%R = Rc%R). {
field. admit.
}
rewrite -> H4.
reflexivity.
Admitted.
That is expected. Your first use of field is on a goal akin to (m * x) / m = x. There is absolutely no way of defining the division over real numbers so that this equality holds for all real numbers x when m is equal to 0. So, the field tactic is able to prove this equality only if you are able to prove m <> 0. Your third use of field is on an equality (x / m) * m = x, and again, it can only hold for any x if you know that m is nonzero.