coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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…).
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>
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: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 aHm.. Not complete enough, it seems. I oversimplified my original example.
complete decision procedure for equality with constructors.
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 *)
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.intros ? H; apply (f_equal size) in H; simpl in *; omega.
Goal forall x, (shapeA (shapeA' x)) <> x.
Qed.
--
.../Sedrikov\...
- [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.