The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

If you take a closer look at A. Chipala answer, he used the "induction" tactic.
You didn’t. congruence is not enough smart to reason by induction.

The bad thing is that Coq does not have a nice way to deal with mutual induction.
There are many ways to do it, but none of them are really friendly.

You can try to start with:

Lemma foo : ∀ x, (shapeA (shapeA' x)) ≠ x
with bar : ∀ y, (shapeA' (shapeA y)) ≠ y.
Proof. (* foo *)
  intros [y|].
  * (* shapeA (shapeA' (shapeA y)) ≠ shapeA y *)
    generalize (bar y); clear foo bar.
    <do your proof here>
  * (* shapeA (shapeA' shapeB) ≠ shapeB *)
    clear foo bar.
    <do your proof here>
Proof. (* bar *)
  intros [x|].

  * (* shapeA' (shapeA (shapeA' y)) ≠ shapeA' y *)
    generalize (bar y); clear foo bar.
    <do your proof here>
  * (* shapeA' (shapeA shapeB') ≠ shapeB' *)
    clear foo bar.
    <do your proof here>
Qed.


I did not tried it, for the <do your proof here>, the congruence tactic A. Chipala told of can be useful.
Note that if you do the proof this way, the "clear foo bar." might not be necessary, but I highly advise it.

You can also take a look at "Induction Scheme" in the manual. I never use it personally, but I do not think either it is bad taste to use it.

--
.../Sedrikov\...