Failing to prove that substituting "by hand" is equivalent to... well, substituting

Using Coq
1

Posted this on stack overflow, then decided that it is even more appropriate here.

After many failures I discovered a strange thing Coq does that I don’t understand.
Sorry for involved code, I was not able to isolate a simpler example.
I have a formula I call trident in three variables p, q, r.
I then simply write out an instance of this formula with a <-> b in place of p, a in place of q and b in place of r, and just try to prove a lemma stating that the result is equivalent to the substitution into trident as above. When trying to prove I am stuck with the first subgoal which reads

 a, b : Prop
  H : b
  ============================
  a \/ (a <-> b)

and this is obviously unprovable: if b is assumed to be true, then a \/ (a <-> b) becomes just a, and there is no reason for it to be true.

Here is the whole code:

From Coq Require Import Setoid.

Definition denseover (p q : Prop) := (p -> q) -> q.

Definition trident (p q r : Prop) :=
  (
       (denseover p (q \/ r)) 
    /\ (denseover q (r \/ p))
    /\ (denseover r (p \/ q))
  ) -> (p \/ q \/ r).

Lemma triexpand : forall a b : Prop,
     ((a <-> b) \/ a \/ b)
<-> ((a \/ (a -> b)) /\ (b \/ (b -> a))).

Proof.
tauto.
Qed.

Lemma substritwo : forall a b : Prop,
   (trident (a <-> b) a b)
<->
   (
    (
         (denseover (a <-> b) (a \/ b)) 
      /\ (denseover a (b \/ (a <-> b)))
      /\ (denseover b (a \/ (a <-> b)))
    ) -> ((a <-> b) \/ a \/ b)
   ).

Proof.
  unfold trident, denseover.
  split.
  rewrite triexpand.
  split.
  destruct H.
  destruct H0.
  destruct H.
  destruct H0.
  destruct H.
  destruct H0.
  intuition.

What am I doing wrong here?

2

Look at the goal before the last destruct:

a, b : Prop
H0 : (b -> a \/ (a <-> b)) -> a \/ (a <-> b)
=========================
a -> b \/ (a <-> b)

H0 has a function type X -> Y, destruct H0 expects you to prove X so that Y can then be decomposed, but of course if X is not provable you will be stuck.

Note that this theorem is purely propositional (just a bunch of atoms with /\, \/, ->), so it is easily solved by firstorder.

In general, a good approach for this kind of “unfolding lemma” is to use “congruence lemmas” about the connectives used in your definitions to reduce an equivalence between big expressions to equivalences on their subterms:

and_iff_cong : (A <-> B) -> (C <-> D) -> (A /\ C) <-> (B /\ D)
or_iff_cong : (A <-> B) -> (C <-> D) -> (A \/ C) <-> (B \/ D)
impl_iff_cong : (A <-> B) -> (C <-> D) -> (A -> C) <-> (B -> D)
3

Thank you! So my problem was careless use of destruct, right? Already that goal you reproduce seems to be unprovable, so probably the disaster happened at some of the previous destructs…

In the meanwhile I got an answer at stack exchange too, turns out that just a single rewriting with or_comm does it…