creating a new inductive type

Stream: general

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

Have I got all this sort-of straight?

[Simon Hudon]

Something seems to be missing

[Simon Hudon]

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

[Kevin Buzzard]

Why does this rely on rec?

[Kevin Buzzard]

Isn't it just the definition of addition?

[Kevin Buzzard]

oh

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Simon Hudon]

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

[Kevin Buzzard]

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

[Simon Hudon]

The proof isn't rfl though.

I don't think that equations get labelled as rfl

[Andrew Ashworth]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Maybe this is iota reduction

[Kevin Buzzard]

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

[Andrew Ashworth]

most people regard alonzo church as a mathematician :)

[Kevin Buzzard]

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.

[Simon Hudon]

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

[Simon Hudon]

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?

[Kevin Buzzard]

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

[Simon Hudon]

Haha! Your honor is safe then!

[Kevin Buzzard]

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.

[Simon Hudon]

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

[Kevin Buzzard]

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

[Simon Hudon]

That's what I'm going with as well

[Kevin Buzzard]

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

[Andrew Ashworth]

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

[Simon Hudon]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh!

[Kevin Buzzard]

Right, this also makes sense.

[Reid Barton]

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.

[Reid Barton]

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

[Kevin Buzzard]

What is the point of iota-reduction then?

[Simon Hudon]

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

[Kevin Buzzard]

ι-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

[Kevin Buzzard]

from the reference manual

[Reid Barton]

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.

[Kevin Buzzard]

Oh so it only explicitly applies to the recursor?

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

i.e. what Simon said.

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Google led me to some pages about CIC:

[Kevin Buzzard]

" 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]."

[Kevin Buzzard]

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

[Kevin Buzzard]

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).

[Kevin Buzzard]

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.

[Andrew Ashworth]

yes, lean and coq are CIC + extras

[Kevin Buzzard]

and we don't know what Lean is doing.

[Reid Barton]

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

[Simon Hudon]

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

[Reid Barton]

To

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

[Andrew Ashworth]

the extras that are added to CIC make defeq not transitive

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

is my terrible understanding of the base theory

[Andrew Ashworth]

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

[Kevin Buzzard]

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.

[Andrew Ashworth]

yup, that's my understanding as well

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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)

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Somehow this is not relevant.

[Reid Barton]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

Yes and yes (the latter is not definitionally equal)

[Kevin Buzzard]

Do you know Lean's definition of definitionally equal?

[Reid Barton]

Not really, no.

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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