Zulip Chat Archive

Stream: new members

Topic: inductive type constructor parameterized by Pi to itself


Chris M (Jul 31 2020 at 11:28):

I was reading the reference manual on inductive types and didn't understand how rec deals with so called "recursive arguments". It states: "The ith minor premise is a function which takes [...] an argument of type Π (d : δ), C (bⱼ d) corresponding to each recursive argument (bⱼ : βᵢⱼ), where βᵢⱼ is of the form Π (d : δ), foo (the recursive values of the function being defined)"

I didn't understand this, so tried this out:

universes v u
constant X:Type
inductive ind4 : Type (u+1)
| const5 : Π b:(Π x:X, ind4), ind4

#check @ind4.rec

There are two things I don't understand about this:

  1. How is const5 and ind4 well-defined? It seems like in order to construct the type Π x:X, ind4 we first need to have constructed the type ind4. I can vaguely imagine that this doesn't lead to contradictions and hence is ok, e.g. by arguing that in defining const5 f, the function f must be a function that doesn't have const5 f itself in its image. Nevertheless it seems a bit suspect and I'm not sure how to justify this.
  2. Even more suspect seems to me the use of rec for this. It has the type ind4.rec : Π {C : ind4 → Sort u_1}, (Π (b : X → ind4), (Π (x : X), C (b x)) → C (ind4.const5 b)) → Π (n : ind4), C n. The part of this that seems suspect is (Π (b : X → ind4), (Π (x : X), C (b x)) → C (ind4.const5 b)), because it's not obvious to me that this induces a well-founded recursion: How do we know that b only outputs members of ind4 for which the recursion "has already been done"?

I might be misunderstanding something more fundamental.

Kevin Buzzard (Jul 31 2020 at 14:20):

Are you happy with the definition of the natural numbers?

Kevin Buzzard (Jul 31 2020 at 14:20):

Is your situation any different?

Kevin Buzzard (Jul 31 2020 at 14:22):

The inductive command makes ind4 and ind4.const5 and ind4.rec all appear at the same time

Chris M (Jul 31 2020 at 17:21):

After thinking about it more, it seems like we at least want the condition \forall x:X, \forall (b:\Pi x:X, ind4), (b x) \neq (const5 b), and I'm guessing that this is automatically satisfied.

Chris B (Jul 31 2020 at 18:34):

There's no way to actually create an element of your type (if b's domain type is inhabited) . Mario Carneiro showed this proof in another thread, but it applies here.

universe u
variable {A : Type}

inductive ind4 : Type (u+1)
| const5 : Π b:(Π x:A, ind4), ind4

def no_ind4 [inst1 : inhabited A] : ind4 -> false :=
λ h, ind4.rec_on h (λ h1 h2, false.elim $ h2 inst1.default)

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Basic.20building.20block.20tactics/near/189382869

Alistair Tucker (Jul 31 2020 at 19:14):

This is like a bastardised version of the type I suggested in your other thread:

inductive tree {α : Type} (β : α  Type)
| mk (a : α) (φ : β a  tree) : tree

The addition of dependent types makes it more useful. Say α is and β is fin. A leaf node can be constructed with a = 0 because fin 0 is empty. You can construct further nodes out of those, parametrised by a the number of children. In general you have to understand that the only terms of a type are those you can actually construct. This way of thinking may seem a little alien if you have taken more maths classes than CS classes.

Chris M (Aug 01 2020 at 17:52):

Chris B said:

There's no way to actually create an element of your type (if b's domain type is inhabited) . Mario Carneiro showed this proof in another thread, but it applies here.

universe u
variable {A : Type}

inductive ind4 : Type (u+1)
| const5 : Π b:(Π x:A, ind4), ind4

def no_ind4 [inst1 : inhabited A] : ind4 -> false :=
λ h, ind4.rec_on h (λ h1 h2, false.elim $ h2 inst1.default)

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Basic.20building.20block.20tactics/near/189382869

To be clear, this doesn't actually prove that it's impossible to construct an instance of ind4, does it? It just proves that if this would be possible, Lean's type theory would be inconsistent. Do we actually know that it's consistent?

Kevin Buzzard (Aug 01 2020 at 18:11):

Oh come on. What do you mean by "know"?

Kevin Buzzard (Aug 01 2020 at 18:12):

I know it's consistent in the sense that it's equiconsistent with the system that me and gazillions of other mathematicians are using every day. But by Gödel we can't prove this within the system, we can only prove it within a system strictly more likely to be inconsistent

Chris M (Aug 01 2020 at 18:12):

For the purpose of that comment, I meant "have a proof of". I'm not saying I doubt it, I'm just curious in the meta mathematics of this

Kevin Buzzard (Aug 01 2020 at 18:13):

A proof assuming what?

Kevin Buzzard (Aug 01 2020 at 18:14):

Certainly lean can't prove its own consistency, in common with every consistent system strong enough to construct the natural numbers, by godel

Chris M (Aug 01 2020 at 18:17):

I think Godel's theorem tells us that we can't prove the consistency of a set of axioms within a logic, not that we can't prove the consistency of a formal deductive system of that logic?

Jalex Stark (Aug 01 2020 at 18:18):

you might find it helpful to read some of mario's msc thesis
https://github.com/digama0/lean-type-theory

Jalex Stark (Aug 01 2020 at 18:20):

Chris M said:

I think Godel's theorem tells us that we can't prove the consistency of a set of axioms within a logic, not that we can't prove the consistency of a formal deductive system of that logic?

i have a hard time imagining a difference between the two sides of the "not that"

Jalex Stark (Aug 01 2020 at 18:21):

i think if you want to have a nuanced discussion about the evidence for the consistency of lean, you need to start from precise definitions

Anatole Dedecker (Aug 01 2020 at 18:36):

Chris M said:

To be clear, this doesn't actually prove that it's impossible to construct an instance of ind4, does it? It just proves that if this would be possible, Lean's type theory would be inconsistent. Do we actually know that it's consistent?

Then I guess you can say that we can never prove 0≠1, we can just prove that if it was possible to prove 0=1 Lean would be inconsistent. This is just the definition of negation, if you accept to extend it to any Type u

Chris M (Aug 01 2020 at 18:37):

Ah mario's thesis says that ZFC and CIC can prove each other's consistency. That's basically what I wanted to know. :)

Chris M (Aug 01 2020 at 18:39):

Anatole Dedecker said:

Chris M said:

To be clear, this doesn't actually prove that it's impossible to construct an instance of ind4, does it? It just proves that if this would be possible, Lean's type theory would be inconsistent. Do we actually know that it's consistent?

Then I guess you can say that we can never prove 0≠1, we can just prove that if it was possible to prove 0=1 Lean would be inconsistent. This is just the definition of negation, if you accept to extend it to any Type u

Right, I hadn't thought of it that way, thanks :)

Kevin Buzzard (Aug 01 2020 at 21:06):

@Chris M I think that actually Lean is equiconsistent with ZFC + infinitely many universes, but mathematicians use universes when push comes to shove...


Last updated: Dec 20 2023 at 11:08 UTC