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: Adam Chlipala <adamc AT csail.mit.edu>
  • To: Michiel Helvensteijn <mhelvens AT gmail.com>
  • 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 13:36:53 -0400

On 07/15/2013 01:16 PM, Michiel Helvensteijn wrote:
On Mon, Jul 15, 2013 at 3:19 PM, Adam
Chlipala<adamc AT csail.mit.edu>
wrote:

Generally this work is easy to push off onto [congruence], which is a
complete decision procedure for equality with constructors.
Hm.. Not complete enough, it seems. I oversimplified my original example.
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.




Archive powered by MHonArc 2.6.18.

Top of Page