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.