Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?


chronological Thread 
  • From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
  • To: Daniel Schepler <dschepler AT gmail.com>
  • Cc: coq-club AT inria.fr, Lauri Alanko <la AT iki.fi>
  • Subject: Re: [Coq-Club] Can I use this nonempty inductive type in a fixpoint (without declaring variable that will lead to an axiom) ?
  • Date: Thu, 19 May 2011 20:18:21 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=EIcOQp+50FYCBle2g186uQr3ILejzKEAyza3l4KAvUIUzDo928n9j2ktar7p5Az9L1 b7V2DHx6Xnu+C3+2BR498TtQXZKMAjCO110xa4ZENcBBil0L5u9fqxVvookwXElN+Q6i DEEwJTrMfCo7Qk/uy5NitUA25z4XRsAxZrL9g=
As far as I understand, the fact that (T -> False) (or any equivalent
coq statement) means that the set of closed term having type T is
empty is a meta property and cannot be expressed in coq itself. It is
usually proved "on paper" from the fact that the set of closed terms
of type False is itself empty. This latter property is generally
proved as a corollary of the definition of inductive types and their
recursors and from the subject reduction and strong normalization
properties of CCI.

Strictly speaking I would say that the emptyness of the set of closed
term of type False *is exactly* the property of consistency of CIC. I
would therefore agree with Lauri on his nitpicking :)

Hope this helps,
Pierre

Archive powered by MhonArc 2.6.16.

Top of Page