Library Wlog

Set Implicit Arguments.
Unset Strict Implicit.

Lemma wlog1_lemma Ta (a: Ta) m P :
  (forall (WLOG: forall a, m a -> P a), P a) ->
  (forall a, m a -> P a) -> P a.
Proof. eauto. Qed.
Implicit Arguments wlog1_lemma [Ta].

Lemma wlog2_lemma Ta (a: Ta) Tb (b: Tb) m P :
  (forall (WLOG: forall a b, m a b -> P a b), P a b) ->
  (forall a b, m a b -> P a b) -> P a b.
Proof. eauto. Qed.
Implicit Arguments wlog2_lemma [Ta Tb].

Tactic Notation "wlog" hyp(x1) "/" constr(m) :=
  match eval pattern x1 in m with
    ?f _ => apply (wlog1_lemma x1 f); [intro|clear x1; intros x1]
  end.

Tactic Notation "wlogC" hyp(x1) "/" constr(m) :=
  match goal with
    |- ?P =>
      let WLOG := fresh "WLOG" in
      let EQ := fresh "EQ" in
      match eval pattern x1 in m with
        ?f _ =>
           apply (wlog1_lemma x1 f); [intro WLOG;
           set (EQ := P); case_eq m; subst EQ; [exact (WLOG x1)|]
          |clear x1; intros x1]
      end
  end.

Tactic Notation "wlog" hyp(x1) hyp(x2) "/" constr(m) :=
  match goal with
    |- ?P =>
      match eval pattern x1, x2 in m with
        ?f _ _ => apply (wlog2_lemma x1 x2 f); [intro|clear x1 x2; intros x1 x2]
      end
  end.

Tactic Notation "wlogC" hyp(x1) hyp(x2) "/" constr(m) :=
  match goal with
    |- ?P =>
      let WLOG := fresh "WLOG" in
      let EQ := fresh "EQ" in
      match eval pattern x1, x2 in m with
        ?f _ _ => apply (wlog2_lemma x1 x2 f);
          [intro WLOG;
           set (EQ := P); case_eq m; subst EQ;
           [exact (WLOG x1 x2)|
            intro EQ; try rewrite EQ; intros; generalize (WLOG x2 x1)]
          |clear x1 x2; intros x1 x2]
      end
  end.