Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page