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: Cedric Auger <sedrikov AT gmail.com>
  • To: Adam Chlipala <adamc AT csail.mit.edu>
  • Cc: Michiel Helvensteijn <mhelvens AT gmail.com>, 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:03:19 +0200

Without using omega, but with same idea, it can also be funny to use:

Require Import Bool. (* not sure it is necessary… *)

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.

and then:

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.

I didn't tried it, but it should work, and will probably be faster and lighter for Coq (although "discriminate" is not very optimal…).



2013/7/15 Adam Chlipala <adamc AT csail.mit.edu>
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.




--
.../Sedrikov\...



Archive powered by MHonArc 2.6.18.

Top of Page