How can I generalise Coq proofs of an iff?

user_5947247 0
Viewed 179

A common kind of proof I have to make is something like

Lemma my_lemma : forall y, (forall x x', Q x x' y) -> (forall x x', P x y <-> P x' y).
Proof.
  intros y Q_y.
  split.
  + <some proof using Q>
  + <the same proof using Q, but x and x' are swapped>

where Q is itself some kind of iff-shaped predicate.

My problem is that the proofs of P x y -> P x' y and P x' y -> P x y are often basically identical, with the only difference between that the roles of x and x' are swapped between them. Can I ask Coq to transform the goal into

forall x x', P x y -> P x' y

which then generalises to the iff case, so that I don't need to repeat myself in the proof?

I had a look through the standard library, the tactic index, and some SO questions, but nothing told me how to do this.

coq
2 Answers

Here is a custom tactic for it:

Ltac sufficient_if :=
  match goal with
  | [ |- forall (x : ?t) (x' : ?t'), ?T <-> ?U ] =>    (* If the goal looks like an equivalence (T <-> U) (hoping that T and U are sufficiently similar)... *)
    assert (HHH : forall (x : t) (x' : t'), T -> U);   (* Change the goal to (T -> U) *)
      [ | split; apply HHH ]                           (* And prove the two directions of the old goal  *)
  end.

Parameter Q : nat -> nat -> nat -> Prop.
Parameter P : nat -> nat -> Prop.
Lemma my_lemma : forall y, (forall x x', Q x x' y) -> (forall x x', P x y <-> P x' y).
Proof.
  intros y Q_y.
  sufficient_if.
user_68637490

In mathematics, one often can make "assumptions" "without loss of generality" (WLOG) to simplify proofs of this kind. In your example, you could say "assume without loss of generality that P x y holds. To prove P x y <-> P x' y it is sufficient to prove P x' y."

If you are using ssreflect, you have the wlog tactic.

You essentially cut in another goal which can easily solve your goal. You can also do it with standard tactics like assert or enough (which is like assert but the proof obligations are in the other order).

An example to show what I mean: below I just want to show the implication in one direction, because it can easily solve the implication in the other direction (with firstorder).

Context (T:Type) (P:T->T->Prop).

Goal forall x y, P x y <-> P y x.

  enough (forall x y, P x y -> P y x) by firstorder.

Now I just have to show the goal in one direction, because it implies the real goal's both directions.

For more about WLOG see for instance 1

user_3042840
Related