The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sat, Nov 15, 2014 at 4:47 AM, Pierre-Marie Pédrot
<pierre-marie.pedrot AT inria.fr>
 wrote:
> Yep, I even proposed a generalized version of this some time ago, under
> the form of a [wlog] tactic. If you have some goals
>
> [ g1 : Γ1 ⊢ A1 ; ... ; gn : Γn ⊢ An ]
>
> then [wlog gi] results in the state
>
> [ g1 : (forall Γi : Ai), Γ1 ⊢ A1 ; ... ; gn : Γn ⊢ An ]
>
> with some occur check to prevent loops.
>
> This would allow to do a lot of proof by symmetry in a very simple way.
> This is very easy to implement, but at the penultimate Coq WG, nobody
> seemed really interested so I just forgot about it. But if people here
> on Coq-club are interested, I can write it out.

What I think of when I hear wlog is more like: to prove
[ g1 : Γ1, ..., gn : Γn ⊢ P ]
invoke "wlog Q [as H]" to transform into
[ g1 : Γ1, ..., gn : Γn, _ : (forall g1 : Γ1, ..., gn : Γn, Q) ⊢ P,
 g1 : Γ1, ..., gn : Γn, H : Q ⊢ P ].

Just to give a simple concrete example of what I'm thinking:

Require Import Arith.

Lemma le_or_le : forall m n:nat, m <= n \/ n <= m.
Proof.
intros; destruct (le_or_lt m n); auto with arith.
Qed.

Proposition min_le_max : forall m n:nat,
  min m n <= max m n.
Proof.
intros.

(* wlog (m <= n) as Hle. *)
cut (forall m n:nat, m <= n -> min m n <= max m n);
  [ intro | (clear m n; intros m n Hle) ].

+ destruct (le_or_le m n); [ | rewrite Min.min_comm, Max.max_comm ]; auto.
+ rewrite Min.min_l, Max.max_r; auto.
Qed.

I've periodically run into situations, often a proof by symmetry as
you mentioned, where such a tactic would have been useful and I had to
roll it myself.  So, I'd be interested in seeing an implementation of
something like that.
-- 
Daniel Schepler