The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

It used to not be possible, but using the new primitives of the tactic
engine available
in trunk you can hack something like this. The robustness of this
trick is not guaranteed.
Note that this couldn't be used to treat the other case at the same
time (negative multiplicand).

Require Classes.Morphisms.
Import Classes.Morphisms.ProperNotations.

Definition such_that {A : Type} (P : A -> Prop) (R : relation A) :=
  fun x y => P x /\ R x y.

Instance : Morphisms.Proper (Rle ++> such_that (fun x => x > 0) eq ++>
Rle) Rmult.
Proof.
  repeat red ; intros. subst.
  red in H0.
Admitted.

Instance : Morphisms.Proper (such_that (fun x => x > 0) eq ++> Rle ++>
Rle) Rmult.
Proof.
  repeat red ; intros. subst.
  red in H0.
Admitted.

Class Cond (A : Prop) := holds : A.
Hint Extern 1 (Cond ?A) =>
  (* The goals coming from setoid_rewriting might contain this
spurious assumption *)
  try match goal with [ H : Morphisms.apply_subrelation |- _ ] => clear H end;
  red; shelve (* This postpones the subgoal *)
 : typeclass_instances.

(** The trick: postpone the Cond subgoal but still ask for the Proper
subgoal to be resolved *)
Lemma such_that_shelve A (P : A -> Prop) R x :
  Cond (P x) ->
  Morphisms.Proper R x ->
  Morphisms.Proper (such_that P R) x.
Proof. repeat red; intuition. Qed.

Hint Extern 4 (Morphisms.Proper (such_that _ _) _) =>
  class_apply such_that_shelve : typeclass_instances.
  (* This is needed as the such_that_shelve lemma could apply all the
time and loop *)

Goal forall (x1 x2 y1 y2 : R), x1 > 0 -> y1 > 0 ->
   x1 <= x2 -> y1 <= y2 ->
   x1 * y1 <= x2 * y2.
Proof.
  intros x1 x2 y1 y2 x1pos x2pos x1_le_x2 y1_le_y2. intros.
  rewrite x1_le_x2, y1_le_y2.
  reflexivity.
  apply Rlt_le_trans with x1; auto with real.
  apply Rlt_le_trans with y1; auto with real.
Qed.

-- Matthieu

2015-01-15 23:40 GMT+05:30 Daniel Selsam 
<dselsam AT stanford.edu>:
> Hi,
>
> With respect to the relation Rle (<=), I can rewrite inside Rplus (+) and 
> Rminus (-), since both positions of both binary operators have fixed 
> variance:
>
> <<
>
> Require Import Setoid Relation_Definitions Reals.
> Open Scope R.
>
> Add Parametric Relation : R Rle
> reflexivity proved by Rle_refl
> transitivity proved by Rle_trans
> as Rle_setoid_relation.
>
> Add Parametric Morphism : Rplus with
> signature Rle ++> Rle ++> Rle as Rplus_Rle_mor.
> intros ; apply Rplus_le_compat ; assumption.
> Qed.
>
> Add Parametric Morphism : Rminus with
> signature Rle ++> Rle --> Rle as Rminus_Rle_mor.
> intros ; unfold Rminus ;
> apply Rplus_le_compat;
> [assumption | apply Ropp_le_contravar ; assumption].
> Qed.
>
> Goal forall (x1 x2 y1 y2 : R),
>    x1 <= x2 -> y1 <= y2 ->
>    x1 - y2 <= x2 - y1.
> Proof.
>   intros x1 x2 y1 y2 x1_le_x2 y1_le_y2;
>   rewrite x1_le_x2; rewrite y1_le_y2;
>   reflexivity.
> Qed.
>
>>>
>
> Unfortunately, Rmult (*) does not have this property: the variance depends 
> on whether the other multiplicand is positive or negative. Is it possible 
> to define a conditional morphism, so that Coq performs the rewriting step 
> and simply adds the non-negativity of the multiplicand as a proof 
> obligation?
>
> Thanks very much,
>
> Daniel
>



-- 
-- Matthieu