Coq did something earlier that I didn’t quite understand or expect. This is extracted from a larger development. The following is a straightforward linear interpolation function over reals:
Require Import Coq.Lists.List.
Require Import Coq.Init.Nat.
Require Import Coq.Arith.Peano_dec.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Reals.Reals.
Require Import Coq.Reals.ROrderedType.
Require Import Psatz.
Open Scope R_scope.
Definition isNormalized (x : R) : Prop :=
0 <= x /\ x <= 1.
(** Linearly interpolate between _x_ and _y_ by the (normalized)
factor _f_. *)
Definition interpolate
(x : R)
(y : R)
(f : R)
: R :=
(x * (1 - f)) + (y * f).
Then, a proof:
(** If the interpolation factor is normalized, then _interpolate_
always returns a value in _[x, y]_. *)
Lemma interpolateRange : forall x y f,
0 <= x <= y
-> isNormalized f
-> x <= interpolate x y f <= y.
Proof.
intros x y f [H0x Hxy] Hnf.
inversion Hnf as [Hnf0 Hnf1].
clear Hnf.
assert (0 <= y) as H0y by lra.
unfold interpolate.
assert (y * f <= y) as Hyf. {
pose proof (Rmult_le_compat_l y f 1 H0y Hnf1) as Hp.
assert (y * 1 = y) as Htr by lra.
rewrite <- Htr at 2.
trivial.
}
assert (x * (1 - f) <= x) as Hxf. {
assert (x * 1 = x) as Htr by lra.
rewrite <- Htr at 2.
apply (Rmult_le_compat_l x (1 - f) 1 H0x).
lra.
}
assert (0 <= y * f) as H0yf
by apply (Rmult_le_pos _ _ H0y Hnf0).
constructor. {
rewrite <- Rplus_0_r at 1.
eapply (Rplus_le_compat x (x * (1 - f)) 0 (y * f) _ H0yf).
Abort.
The oddity occurred there with the application of the Rplus_le_compat lemma. If we look at the actual context and subgoals, something slightly odd happens:
Lemma interpolateRange : forall x y f,
0 <= x <= y
-> isNormalized f
-> x <= interpolate x y f <= y.
Proof.
intros x y f [H0x Hxy] Hnf.
inversion Hnf as [Hnf0 Hnf1].
clear Hnf.
assert (0 <= y) as H0y by lra.
unfold interpolate.
assert (y * f <= y) as Hyf. {
pose proof (Rmult_le_compat_l y f 1 H0y Hnf1) as Hp.
assert (y * 1 = y) as Htr by lra.
rewrite <- Htr at 2.
trivial.
}
assert (x * (1 - f) <= x) as Hxf. {
assert (x * 1 = x) as Htr by lra.
rewrite <- Htr at 2.
apply (Rmult_le_compat_l x (1 - f) 1 H0x).
lra.
}
assert (0 <= y * f) as H0yf
by apply (Rmult_le_pos _ _ H0y Hnf0).
constructor. {
rewrite <- Rplus_0_r at 1.
eapply Rplus_le_compat.
At this point, the context looks like this:
2 goals
x, y, f : R
H0x : 0 <= x
Hxy : x <= y
Hnf0 : 0 <= f
Hnf1 : f <= 1
H0y : 0 <= y
Hyf : y * f <= y
Hxf : x * (1 - f) <= x
H0yf : 0 <= y * f
______________________________________(1/2)
x <= x * (1 - f)
______________________________________(2/2)
0 <= y * f
Note that the goal is x <= x * (1 - f) but the context has x * (1 - f) <= x, but somehow this was accepted by eapply before?
Am I missing something obvious here? I’ve not completed the proof, so I’m not actually sure if the resulting proof term would type check.
Looks like the context you built with asserts was not strong enough to apply simply Rplus_le_compat.
Thus, eapply is not guilty. The real culprit may be your decomposition of x and y into sums of products. Here’s is another choice (note that I use eapply Rplus_le_compat too).
unfold interpolate; split.
- replace x with (x * (1 - f) + x * f) at 1 by lra.
+ eapply Rplus_le_compat; try lra.
* now apply Rmult_le_compat_r.
- replace y with (y * (1 - f) + y * f) at 2 by lra.
+ eapply Rplus_le_compat; try lra.
* apply Rmult_le_compat_r; lra.
Qed.
… Shows a context that could not possibly have allowed that first eapply to succeed.
eapply Rplus_le_compat.
apply Hxf.
In environment
x, y, f : R
H0x : 0 <= x
Hxy : x <= y
Hnf0 : 0 <= f
Hnf1 : f <= 1
H0y : 0 <= y
Hyf : y * f <= y
Hxf : x * (1 - f) <= x
H0yf : 0 <= y * f
Unable to unify "x * (1 - f) <= x" with "x <= x * (1 - f)".
How did the original fully-applied eapply (minus that one _ placeholder) unify those?
it checks whether H0yf is a proof of 0 <= y * f, OK
Then it generates a subgoal (for the _) : to prove x <= x * (1 - f).
Then no error is detetected by eapply. But It would be difficult to prove this inequality …
There seems to a a confusion between an error (immediately detected) and a dead-end ?
In your second version, eapply Rplus_le_compat does not fail. Its just that apply Hxf doesn’t solve the sub-goal generated by the eapply.
In my solution, I transformed the goal in such a way that eapply Rplus_le_compat, generates solvable sub-goals.
AH! I see. I didn’t realize that eapply shelved a subgoal.
For example, if I substitute the following based loosely on your proof (no prizes for aesthetics, I just wanted to see the individual steps):
Lemma interpolateRange : forall x y f,
0 <= x <= y
-> isNormalized f
-> x <= interpolate x y f <= y.
Proof.
intros x y f [H0x Hxy] Hnf.
inversion Hnf as [Hnf0 Hnf1].
clear Hnf.
assert (0 <= y) as H0y by lra.
unfold interpolate.
assert (y * f <= y) as Hyf. {
pose proof (Rmult_le_compat_l y f 1 H0y Hnf1) as Hp.
assert (y * 1 = y) as Htr by lra.
rewrite <- Htr at 2.
trivial.
}
assert (x * (1 - f) <= x) as Hxf. {
assert (x * 1 = x) as Htr by lra.
rewrite <- Htr at 2.
apply (Rmult_le_compat_l x (1 - f) 1 H0x).
lra.
}
assert (0 <= y * f) as H0yf
by apply (Rmult_le_pos _ _ H0y Hnf0).
constructor. {
rewrite <- Rplus_0_r at 1.
eapply (Rplus_le_compat x (x * (1 - f)) 0 (y * f) _ H0yf).
} {
replace y with (y * (1 - f) + y * f) at 2 by lra.
eapply Rplus_le_compat.
apply Rmult_le_compat_r.
lra.
exact Hxy.
apply Rmult_le_compat_r.
exact Hnf0.
apply Rle_refl.
}
Abort.
I get all the way there but find there’s a subgoal left over that I didn’t know about:
All the remaining goals are on the shelf:
x <= x * (1 - f)
Bit of a user interface issue, but that’s fine. I see that the eapply didn’t actually succeed, it’s just that it quietly created more work in the background.
Yes, but, you probably didn’t give the right application of eapply. You still generate a non-provable goal …
Unshelve.
(*
x, y, f : R
H0x : 0 <= x
Hxy : x <= y
Hnf0 : 0 <= f
Hnf1 : f <= 1
H0y : 0 <= y
Hyf : y * f <= y
Hxf : x * (1 - f) <= x
H0yf : 0 <= y * f
============================
x <= x * (1 - f)
*)
The tactic eapply Rplus_le_compat succeeded, but was mis-used. Its normal use is “if your goal has the form a + c <= b + d and your are able to prove a <= b and c <= d, that’s OK”. But you didn’t use it that way.
