The Coq mailing list

["Jevgenijs Sallinens" <jevgenijs AT dva.lv>]

Wojciech Moczydlowsi wrote:

 

>Does anyone know about any developments in Coq's standard library which
>would stop "working" if impredicativity from Prop was removed in the same
>way the impredicativity of Set was removed in transition to version 8.0?
>That is, if the first Prod rule in the reference manual, instead of being
>generated by tuples (Type, Prop, Prop), (Set, Prop, Prop), (Prop, Prop, Prop),
>would be generated only by (Set, Prop, Prop) and (Prop, Prop, Prop).

 

Here attached archievs with part of my development that show  possibility to build all or most of theory for

natural numbers without impredicativity. Actually Prop is replaced by Set to demonstrate  this fact.

It seems also that only Type_0 is required in all places where Type is used.

See compile.txt to get the order of files and NatProps.v with final modules that provides operations with

natural numbers and their properties (including quite general versions for recursion and induction) .

Similar development is possible also for lists and probably for most of developments within intuitionistic logic.

It would be very interesting to get expert's opinion.

 

Kind regards,

Jevgenijs.

Attachment: Nat.zip
Description: application/compressed

Attachment: Nat.rar
Description: application/rar-compressed

Scanned by evaluation version of Dr.Web antivirus Daemon 
http://drweb.ru/unix/