The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Mon, Jul 15, 2013 at 7:36 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:

>> How would you prove the following?
>>
>> Inductive Structure :=
>>    |  shapeA:  Structure' ->  Structure
>>    |  shapeB:                Structure
>> with Structure' :=
>>    |  shapeA': Structure  ->  Structure'
>>    |  shapeB':               Structure'.
>>
>> Goal forall x, (shapeA (shapeA' x))<>  x.
>>    intro.
>>    congruence. (* Error: congruence failed *)
>
> I wouldn't expect it to work without some induction (so clearly I shouldn't
> have written "complete" :]), but here's another approach that avoids new
> induction:
>
> Fixpoint size (x : Structure) :=
>   match x with
>     | shapeA x' => S (size' x')
>     | shapeB => O
>   end
> with size' (x : Structure') :=
>   match x with
>     | shapeA' x' => S (size x')
>     | shapeB' => O
>   end.
>
> Require Import Omega.
>
> Goal forall x, (shapeA (shapeA' x)) <> x.
>   intros ? H; apply (f_equal size) in H; simpl in *; omega.
> Qed.

Viktor came up with the exact same solution. I only now realize he
sent it privately, not to the group. :-)

Yes, there are a number of problems with my huge mutually inductive
structure that might benefit from a size function like that.

Though shouldn't there be a generally applicable tactic / lemma for
this? Something to prove any goal of the form:

forall x, ( constructor_1 arg_{1,1} ... ( constructor_n arg_{n,1} ...
x ... arg_{n,m_n} ) ... arg_{1,n_1} ) <> x

Even more useful would be an automatically generated well-founded
partial order between constructs of any inductive type.

--
www.mhelvens.net