Using or_comm in Coq

Question

I want to prove the following theorem:

Theorem T14 : forall s t u,
  S u s t <-> S u t s.

Where S is defined like this:

Definition S u s t := forall v,
  ((ObS u v) <-> (ObS v s \/ ObS v t)).

The first tactics I used are:

Proof.
  intros s t u.
  unfold S.

And my goal is now:

1 subgoal
s, t, u : Entity
______________________________________(1/1)
(forall v : Entity, ObS u v <-> ObS v s \/ ObS v t) <->
(forall v : Entity, ObS u v <-> ObS v t \/ ObS v s)

It feels like the proof can be finished if I use the commutativity of the OR operator, and then apply the tauto tactic. However, I don't know how to rewrite the inner bit of only the right part of the equivalence. Is it possible?

Answer 1

This can be done using generalized rewriting.

1. Require Setoid.

2. Use setoid_rewrite because you are rewriting under a binder (forall v). (Without binders, rewrite would be sufficient).

It works out-of-the-box in this case, but when your project gets more sophisticated, with your own combinators/logical connectives, some work will be necessary to ensure that "rewriting" is sound. The reference manual describes the set up required by generalized rewriting.

(* 1 *)
Require Import Setoid.

Parameter T : Type.
Parameter ObS : T -> T -> Prop.

Definition S u s t := forall v,
  ((ObS u v) <-> (ObS v s \/ ObS v t)).

Theorem T14 : forall s t u,
  S u s t <-> S u t s.
Proof.
  intros s t u.
  unfold S.
  (* 2 *)
  setoid_rewrite (or_comm (ObS _ s)).
  reflexivity.
Qed.