Zulip Chat Archive

Stream: general

Topic: creating a new inductive type


view this post on Zulip Kevin Buzzard (Mar 16 2018 at 22:51):

What happens to the underlying system when a new inductive type X is created in Lean? A new axiom seems to appear, namely the eliminator for the type -- X.rec. Is that right? A new axiom appears? Is that the only new axiom that appears, and all of the other stuff I see when I type #print prefix X is always deducible from X.rec? I see that occasionally other stuff is used, like and or eq.rec or propext. Is it possible to list exactly which functions are used when creating these new facts? I am trying to get to the bottom of the difference between equality and definitional equality and I think one main difference is these random axioms that seem to appear every time to create a new type.

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 22:53):

For example I think a+(b+c)=(a+b)+c for nats isn't a defeq, it's a theorem, and the reason seems to be that the proof uses induction on c, which uses nat.rec, which seems to be a way of proving that things are equal other than by definitional equality.

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 22:53):

Have I got all this sort-of straight?

view this post on Zulip Simon Hudon (Mar 16 2018 at 22:57):

Something seems to be missing

view this post on Zulip Simon Hudon (Mar 16 2018 at 22:58):

I think a + succ b = succ (a + b) is a definitional equality despite relying on rec

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:17):

Why does this rely on rec?

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:17):

Isn't it just the definition of addition?

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:18):

oh

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:19):

#print nat.add._main was rather more complex than I had expected

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:20):

This is funny because the definition of nat.add in core.lean seems to be the standard one

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:20):

Oh it somehow relies on everything either being zero or a succ

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:23):

Somehow this is OK. We are defining nat.add using what might be called the equation compiler, and internally Lean has to make sense of this definition. Hmm. Maybe what is going on is that I don't understand the definition of defeq that Lean uses in practice.

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:25):

The definition of nat.add_main looks like a mess to me, but nat.add.equations._eqn_2 is the assertion that a+succ b = succ(a+b). The proof isn't rfl though.

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:25):

If you use nat.rec f (succ n) it looks to me like Lean treats it as definitionally equal to f n

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:26):

Is this just some weirdness with nat though, because it's such a primitive object?

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:27):

The proof isn't rfl though.

I don't think that equations get labelled as rfl

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:29):

you'd think rec wouldn't be part of defeq but it's common in type theory settings to include delta reduction as part of it

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:29):

I just rolled my own nat and nat.add and the same happens, it's not something specific to nat

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:31):

Maybe this is iota reduction

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:31):

Why did you guys choose such weird names for all these reductions?

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:33):

most people regard alonzo church as a mathematician :)

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:34):

OK so I am going to say that the reason a + succ b = succ (a+b) is a defeq despite relying on nat.rec is that the entire definition of add relies on nat.rec, and nonetheless they're defeq because of iota reduction. I knew what none of this stuff meant a few months ago though so if this isn't right then I hope someone lets me know.

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:34):

Funny ... and they regard Turing as a sort of computer scientist. They pretty much did the same things

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:35):

you'd think rec wouldn't be part of defeq but it's common in type theory settings to include delta reduction as part of it

Isn't delta reduction about definitions? If rec is a constant, it doesn't have a definition ... what am I missing?

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:36):

According to Wikipedia Church was a mathematician and logician, so maybe he was being a logician at that point

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:37):

Haha! Your honor is safe then!

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:37):

I am only going on the Lean reference manual, but delta reduction seems to say that if I define something without using matching then I can just substitute and I'm still defeq.

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:37):

Do mathematicians regard logicians in a similar way in which they regard philosophers?

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:38):

Using matching is implicitly using what seems to be called iota reduction

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:38):

That's what I'm going with as well

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:38):

No, philosophers aren't doing maths at all. Logicians are doing stuff which some people would say was maths but most maths departments don't have any

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:38):

you'd think rec wouldn't be part of defeq but it's common in type theory settings to include delta reduction as part of it

Isn't delta reduction about definitions? If rec is a constant, it doesn't have a definition ... what am I missing?

i'd have to check. i make no guarantees on whatever i remember about the lambda calculus

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:39):

Let me compress the path for you: https://leanprover.github.io/reference/expressions.html#computation

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:39):

I was suggesting that you can't use delta reduction to prove a + succ b = succ (a + b) because the definition of + depends on how the inductive type inputs were born

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:40):

so I am not sure + is a "defined constant".

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:40):

However + does sound a lot like a function defined by recursion on an inductive type

view this post on Zulip Reid Barton (Mar 16 2018 at 23:41):

+ is a defined constant, its definition is going to be something like nat.rec [...] or possibly lam a b, nat.rec [...]

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:41):

and a + succ b does sound a lot like the function "a +" being applied to an element given by an explicit constructor

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:41):

Oh!

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:42):

Right, this also makes sense.

view this post on Zulip Reid Barton (Mar 16 2018 at 23:42):

Then maybe (a) beta reduction(s) will apply to cancel the lambdas with the arguments, and then finally iota reduction will apply to nat.rec.

view this post on Zulip Reid Barton (Mar 16 2018 at 23:43):

(At least, this is my understanding without actually checking the definitions.)

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:43):

What is the point of iota-reduction then?

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:43):

That would be my thought as well. So the remaining question is: is iota reduction part of the def_eq definition?

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:43):

ι-reduction : When a function defined by recursion on an inductive type is applied to an element given by an explicit constructor, the result ι-reduces to the specified function value

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:44):

from the reference manual

view this post on Zulip Reid Barton (Mar 16 2018 at 23:44):

I think it's the rule that, after expanding the definition of + and then substituting the arguments, allows one to replace nat.rec [...] (succ [...]) by something simpler.

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:44):

Oh so it only explicitly applies to the recursor?

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:44):

That sounds relevant doesn't it? I think here, "recursion" and "pattern matching" are synonymous

view this post on Zulip Reid Barton (Mar 16 2018 at 23:44):

And I think that has been paraphrased into a higher-level form in the lean documentation

view this post on Zulip Reid Barton (Mar 16 2018 at 23:45):

i.e. what Simon said.

view this post on Zulip Reid Barton (Mar 16 2018 at 23:45):

(But I've never encountered the phrase "iota reduction" outside the context of lean, so I am guessing a bit.)

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:45):

At the end of the day it all adds up to the same thing -- a + succ b = succ (a + b) is defeq despite relying on nat.rec

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:47):

Google led me to some pages about CIC:

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:47):

" A specific conversion rule is associated to the inductive objects in the environment. We shall give later on (section 4.5.4) the precise rules but it just says that a destructor applied to an object built from a constructor behaves as expected. This reduction is called iota-reduction and is more precisely studied in [103, 117]."

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:47):

This seems to say more explicitly that iota reduction is exactly how you prove that blah.rec is defeq to something else

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:49):

On the other hand, the manual doesn't seem to give a definition of "what Lean uses for defeq" other than observing that (a) it's not the actual definition of defeq (proof: Lean's defeq isn't transitive) and (b) I think they're saying it's decidable (and actual defeq isn't).

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:50):

So some of these reductions are from lambda calculus and iota reduction has just been tagged on afterwards as something coming from CIC it seems to me.

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:50):

yes, lean and coq are CIC + extras

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:50):

and we don't know what Lean is doing.

view this post on Zulip Reid Barton (Mar 16 2018 at 23:50):

Yes--specifically blah.rec applied to a constructor.
This will also go by names like "the elimination rule for the constructor"

view this post on Zulip Simon Hudon (Mar 16 2018 at 23:52):

Yes--specifically blah.rec applied to a constructor.
This will also go by names like "the elimination rule for the constructor"

I don't get what you're responding to

view this post on Zulip Reid Barton (Mar 16 2018 at 23:53):

To

iota reduction is exactly how you prove that blah.rec is defeq to something else

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:53):

the extras that are added to CIC make defeq not transitive

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:55):

and it has something something to do with how you can go from an inductively defined proposition to a Type

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:55):

but we don't want to do without because classical reasoning is so convenient

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:55):

so little bits are stuck on here and there and we sort of politely ignore it

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:56):

is my terrible understanding of the base theory

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:57):

if you go completely constructive you get HoTT and you may then hop on voevodsky's bandwagon

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 23:59):

the extras that are added to CIC make defeq not transitive

My reading of section 3.7 of the manual is that "true defeq" is transitive by definition, and "Lean defeq" is not.

view this post on Zulip Andrew Ashworth (Mar 16 2018 at 23:59):

yup, that's my understanding as well

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:04):

So implicit in the reference manual is a description of two terms which have different weak head normal forms but which can be proved equal using rfl.

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:05):

def R (x y : unit) := false
def accrec := @acc.rec unit R (λ_, unit) (λ _ a ih, ()) ()
example (h) : accrec h = accrec (acc.intro _ (λ y, acc.inv h)) := rfl
example (h) : accrec h = accrec (acc.intro _ (λ y, acc.inv h)) :=
begin
conv begin
to_rhs,
whnf,
end,
conv begin
to_lhs,
whnf,
end,
admit,
end

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:05):

rfl works, but if you reduce both terms to weak head normal form then you see they are different.

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:11):

So I am at a loss as to what Lean's definition of defeq is, but I understand it a lot better after this chat.

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:11):

Looking back at the proof of associativity of nat.add it's interesting to actually try and point at exactly what stops the argument being rfl.

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:12):

You prove it by induction on c; the zero case is rfl

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:13):

and the inductive step is a bunch of rfls up to a+(b+c)=(a+b)+c -> nat.succ (a+(b+c))=nat.succ((a+b)+c)

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:13):

but the inductive hypothesis isn't rfl, it's an assumption because we're using nat.rec

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:14):

and in particular we can't deduce associativity from this iota-reduction thing because even though c is either zero or a succ, in the succ case we need more than a case split, we need induction.

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:15):

It seems to me that it's this one point which stops associativity being defeq

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:19):

On the other hand you can chase this back to congr_arg and hence to eq.subst and eq.rec

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:21):

Somehow this is not relevant.

view this post on Zulip Reid Barton (Mar 17 2018 at 00:26):

More simply, you might consider the relationship between (p.1, p.2) and p

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:56):

Also the coq page I was looking at seems to be saying that iota reduction says that a definition by cases can be reduced to its value for a given constructor when applied to a term constructed using this constructor.

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 00:57):

This seems to be weaker than what it says in the Lean reference manual, which seems to imply that general definitions by recursion (like the definition of nat.add) can be iota-reduced.

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 01:16):

So looking at what the manual says about inductive types, it seems that the answer to my original question is that what is added is the type, the constructors, and the recursor, and then everything else is worked out from this. And it also seems to say that iota reduction is fine for eliminating X.rec.

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 01:17):

For example I think (a,b).1=a is rfl

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 01:18):

but is @Reid Barton suggesting that p=(p.1,p.2) is not? It doesn't seem to be.

view this post on Zulip Reid Barton (Mar 17 2018 at 01:18):

Yes and yes (the latter is not definitionally equal)

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 01:18):

Do you know Lean's definition of definitionally equal?

view this post on Zulip Reid Barton (Mar 17 2018 at 01:19):

Not really, no.

view this post on Zulip Reid Barton (Mar 17 2018 at 01:41):

I just have some bits of type theory knowledge cobbled together from various sources.

view this post on Zulip Mario Carneiro (Mar 17 2018 at 03:06):

Aah, you really should see this paper I'm working on

view this post on Zulip Mario Carneiro (Mar 17 2018 at 03:07):

I basically lay all of this out in precise (too precise, probably) detail


Last updated: May 10 2021 at 00:31 UTC