Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Are proofs of inductive properties finite?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Are proofs of inductive properties finite?


chronological Thread 
  • From: Benjamin Werner <benjamin.werner AT inria.fr>
  • To: Edsko de Vries <devriese AT cs.tcd.ie>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Are proofs of inductive properties finite?
  • Date: Tue, 15 May 2007 17:23:41 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:in-reply-to:references:mime-version:content-type:message-id:cc:from:subject:date:to:x-mailer:sender; b=WKyzQbMzEgFVf6WDGH1rANUT282GJUtNOhAKdw40IsZqmHqlKhtSbUZ8zKBzKuSyCZTDZo2l3JycBvqXAcjzhOGjgAnBbFrtM2E7I8FUxAzFu93jBY5Y6CzLhTy+0NuiOfml4LwnKVP7l23THwy97yk3pX6C43fgTFaahePOpMM=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
You need to formulate your induction hypothesis in a good way I'd say.

This script proves your simplified example

cut (forall x y z, Foo x y z -> z=2).
intros h h'; generalize (h _ _ _ h'); discriminate.
induction  1; trivial.
Qed.


So yes, proofs of inductive properties are finite (or to be
precise, well-founded) and this is reflected in the associated
induction principle (here Foo_ind). 

But to use it here, you need to re-quantify over the arguments
of Foo.

Hope this helps,

Benjamin



Le 15 mai 07 à 17:05, Edsko de Vries a écrit :


Inductive Foo : nat -> nat -> nat -> Prop :=

  | FooBase : Foo 0 1 2

  | FooExchange : forall (m n o:nat), Foo m n o -> Foo n m o.

Lemma not_Foo : ~ (Foo 1 2 3).



Archive powered by MhonArc 2.6.16.

Top of Page