# Unexpectedly accepted eapply hypothesis

Hello!

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 `assert`s 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.

``````

Hello!

Thanks for the explanation (and the proof!).

I’m not sure if my original question was answered, though. I’m curious why this
was accepted without issue:

``````eapply (Rplus_le_compat x (x * (1 - f)) 0 (y * f) _ H0yf).
``````

Whereas this:

``````eapply Rplus_le_compat.
``````

… 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?

Hi !

Let us consider your tactic call:

``````eapply (Rplus_le_compat x (x * (1 - f)) 0 (y * f) _ H0yf).
``````

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.