coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Michiel Helvensteijn <mhelvens AT gmail.com>
- To: Adam Chlipala <adamc AT csail.mit.edu>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How to prove that inductive substructures are not equal?
- Date: Mon, 15 Jul 2013 19:55:13 +0200
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
- [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Adam Chlipala, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Adam Chlipala, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Cedric Auger, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Cedric Auger, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Adam Chlipala, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Adam Chlipala, 07/15/2013
Archive powered by MHonArc 2.6.18.