coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Edsko de Vries <devriese AT cs.tcd.ie>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Are proofs of inductive properties finite?
- Date: Thu, 17 May 2007 11:34:42 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
Thanks for all the replies! Sometimes I get slightly confused about the
difference between inversion (which does not give you the induction
hypothesis) and induction (which does give you the induction hypothesis,
but is a pain to use if the arguments to the inductive properties aren't
variables). The general suggestion of using induction to prove that
something must hold, and then use inversion to show that it doesn't is
indeed very useful.
Thanks!
Edsko
- [Coq-Club] Are proofs of inductive properties finite?, Edsko de Vries
- Re: [Coq-Club] Are proofs of inductive properties finite?,
Edsko de Vries
- Re: [Coq-Club] Are proofs of inductive properties finite?, Benjamin Werner
- Re: [Coq-Club] Are proofs of inductive properties finite?, jean-francois . monin
- Re: [Coq-Club] Are proofs of inductive properties finite?,
Eduardo Gimenez
- Re: [Coq-Club] Are proofs of inductive properties finite?, Randy Pollack
- Re: [Coq-Club] Are proofs of inductive properties finite?, Pierre Courtieu
- Re: [Coq-Club] Are proofs of inductive properties finite?, Gyesik Lee
- <Possible follow-ups>
- [Coq-Club] Are proofs of inductive properties finite?, Edsko de Vries
- Re: [Coq-Club] Are proofs of inductive properties finite?,
Edsko de Vries
Archive powered by MhonArc 2.6.16.