Zulip Chat Archive

Stream: general

Topic: inductive type with no base case is a constant ?


Anatole Dedecker (Oct 10 2020 at 17:18):

Why are docs#false and docs#empty marked as constants in the docs (including the scary red box) although they are just innocent inductive types ?

Patrick Massot (Oct 10 2020 at 17:19):

Every inductive type adds constant to the environment.

Patrick Massot (Oct 10 2020 at 17:20):

Those constant aren't listed in the docs usually, but I guess in those two cases there is nothing else to list since there are no constructors.

Anatole Dedecker (Oct 10 2020 at 17:21):

Oh indeed that makes sense. Thanks !

Patrick Massot (Oct 10 2020 at 17:26):

You run

run_cmd
do env  tactic.get_env,
   decl  env.get `nat,
   tactic.trace decl.is_constant,
   tactic.skip

run_cmd
do env  tactic.get_env,
   decl  env.get `nat.rec,
   tactic.trace decl.is_constant,
   tactic.skip

and put your cursor on each run_cmd to see that both nat and nat.recare constants.

Patrick Massot (Oct 10 2020 at 17:28):

The calculus of inductive construction is a huge machine to create mathematical objects from nowhere. When defining nat you are postulating the existence of a type with its constructors and recursor, coming out of nowhere, so you get constants everywhere.

Patrick Massot (Oct 10 2020 at 17:30):

This is very different from set theoretical foundations where the rule of the game is that everything must be a set, constructed using a handfull of allowed formulas, and you need tricks to encode everything (see eg https://en.wikipedia.org/wiki/Natural_number#Constructions_based_on_set_theory)

Anatole Dedecker (Oct 10 2020 at 17:37):

Yep that makes total sense now, thanks again. On the topic of esoteric set theory constructions, I'm a big fan of this one https://en.wikipedia.org/wiki/Ordered_pair#Defining_the_ordered_pair_using_set_theory

Patrick Massot (Oct 10 2020 at 19:19):

Yes, it's the same issue. And note that functions in set theory are defined as sets of pairs (their graphs), so things like this pile up.


Last updated: Dec 20 2023 at 11:08 UTC