Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to prove that inductive substructures are not equal?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to prove that inductive substructures are not equal?


Chronological Thread 
  • From: Michiel Helvensteijn <mhelvens AT gmail.com>
  • To: Cedric Auger <sedrikov AT gmail.com>
  • Cc: Adam Chlipala <adamc AT csail.mit.edu>, 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 20:35:18 +0200

On Mon, Jul 15, 2013 at 8:03 PM, Cedric Auger
<sedrikov AT gmail.com>
wrote:

> Fixpoint size_mod_2 x :=
> match x with
> | shapeA x' => size_mod_2' x'
> | shapeB => true
> end
> with size_mod_2' x :=
> match x with
> | shapeA' x' => negb (size_mod_2 x')
> | shapeB' => true
> end.
>
> Goal forall x, (shapeA (shapeA' x)) <> x.
> intros x H; apply (f_equal size_mod_3) in H; simpl in *; destruct
> (size_mod_2 x); discriminate.
> Qed.

Yep, works fine. But only for that exact case, of course. Nesting the
goal one deeper makes it fail. :-) So I'd still prefer the general
size function. It's easier to understand, too. But like you said, it's
funny to use. ;-)

--
www.mhelvens.net



Archive powered by MHonArc 2.6.18.

Top of Page