The Coq mailing list

[Carl Patenaude-Poulin <carlpaten AT protonmail.com>]

Hi coq-club! I'm a Coq hobbyist looking for technical guidance. I hope this is

a good place for this, if not I would appreciate being pointed in the right

direction!

Today, I am working on showing that a function recursing structurally on

either of two inductive parameters will always terminate. Here is my

development:

```

Section disjunct_relation.

  Context {A B: Type}.

  Context {RA: relation A}.

  Context {RB: relation B}.

  Definition disjunct_relation :=

    fun x y => RA (fst x) (fst y) \/ RB (snd x) (snd y).

  Theorem disjunct_relation_acc {a b}:

    Acc RA a -> Acc RB b -> Acc disjunct_relation (a, b).

  Admitted.

End disjunct_relation.

```

I'm struggling to put together a proof of `disjunct_relation_acc`. Do you have

suggestions for learning material that could help me sharpen my intuition on

how to approach proofs that involve non-trivial induction? I've already worked

through the first volume of Software Foundations, and also both of Adam

Chlipala's books.

I'd also like to hear about how people here approach thornier proofs. Do you

hash them out with pen and paper first? What intermediate steps can help you

understand the problem better before attempting an implementation?

Thank you in advance for your patient attention -

Carl Patenaude-Poulin