Natural Number Game

Stream: lean4

[Kreijstal]

image.png
there's a natural number game here https://adam.math.hhu.de/#/g/hhu-adam/NNG4/world/AdvAddition/level/6
surely the tactic tauto solves the problem, but I feel like it is cheating, how are you supposed to solve this level?

[Luigi Massacci]

You might use apply False.elim (which I’m not sure was shown in NNG though) and zero_ne_succ if you want all the intermediate steps I guess

[Leo Shine]

Why's it cheating? The panel on the left suggests using it

[David Méndez]

contradiction solved it for me, but I'm also not convinced that that was the way in which we are supposed to solve this level.

[Kevin Buzzard]

Thank you for this discussion. There are often many ways that you can solve a level and I don't think I have a "right" or a "wrong" way in my mind when I'm writing worlds, I just have a route through to a solution which uses only tactics which I have introduced so far. I will take a closer look at this thread and see if I can tidy things up, but please bear in mind that right now game development is very active (I have advanced multiplication world ready to go, I am moving where tauto is introduced and encouraging people to use it more) and things are still likely to be shifting around.

[Kreijstal]

image.png
like this, lol

[Kreijstal]

image.png
yay

[James Sully]

Hiya, I'm working through the natural number game, I'm up to less than equal world level 5:
theorem le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by

The hint says

It's "intuitively obvious" that there are no numbers less than zero, but to prove it you will need a result which you showed in advanced addition world.

The theorems from that world are:

n ≠ succ n
a + n = b + n → a = b
n + a = n + b → a = b
x + y = y → x = 0
x + y = x → y = 0
a + b = 0 → a = 0
a + b = 0 → b = 0

I'm a bit stuck on this, can I get another hint? It feels like it's probably referring to the last two but I'm not sure how to start.

[Mario Carneiro]

from the link above it seems like level 6 is a + b = 0 -> a = 0 which looks like the right lemma to use here

[Mario Carneiro]

how is less-equal defined?

[James Sully]

a <= b if exists c such that b = a + c

[James Sully]

so it introduced me to use in earlier exercises

[Mario Carneiro]

okay, so you should use that definition to get a + b = 0 from the assumption

[Mario Carneiro]

do you know how to unpack an existence assumption? use is for constructing one

[James Sully]

I'm assuming I use cases?

[James Sully]

I'm pretty fuzzy on what it means though

[Mario Carneiro]

the basic idea is that if you are trying to prove goal P and you have an assumption h that says there exists an x such that Q x holds, then cases h will give you such an x and the fact that Q x holds, and your goal is still to prove P

[James Sully]

the lean server on the website keeps crashing unfortunately

[James Sully]

got it, thanks!

cases hx with a
symm at h
apply eq_zero_of_add_right_eq_zero at h
exact h

[James Sully]

where hx was x <= 0

[James Sully]

I guess I don't need the with, I had thought that was a required part of the syntax

[Mac Malone]

@Mario Carneiro I was thinking of suggesting using induction on n. Is that unadvised?

[Mario Carneiro]

The way this game is structured you generally only have to do one induction per level

[Mario Carneiro]

and you don't need to write your own inductive hypotheses

[Mario Carneiro]

in this case the lemma to prove by induction is a + b = 0 -> a = 0 by induction on b, and this was done already in a previous level (which is the reason for the hint)

[Mac Malone]

@Mario Carneiro What is the motivation behind avoiding induction? Typing induction x in the level autogenerates the case split for you, so there isn't much overhead there.

[Mario Carneiro]

induction is the "creative" step when it comes to these kind of problems

[Mario Carneiro]

so it is helpful to control when it is done when teaching

[Mac Malone]

What is a "creative" step?

[Mario Carneiro]

It's well known in ATPs that the hardest step when reasoning about inductive types like Nat is coming up with the right inductive hypothesis or loop invariant, everything else is just "follow your nose"

[Mario Carneiro]

In this case, you might be tempted to prove a <= 0 -> a = 0 by induction on a, but this is the wrong move and you will get stuck

[Mac Malone]

@Mario Carneiro I did that and it worked. (I passed the level via induction on exactly that).

[Mario Carneiro]

if you have the right other lemmas you can still do it

[Mario Carneiro]

it's true after all

[Mario Carneiro]

so you can never really get stuck when applying induction with the wrong IH, but the induction might not do you any good

[Mac Malone]

That's certainly fair and true. In this case, though, induction does help.

[Mac Malone]

But I presume your point is that the goal is to avoid cases were it could hurt. However, isn't that true of other theorems as well (i.e., le_trans and the like can be applied ad nauseum to little effect as well if you don't have a plan).

[Mario Carneiro]

not exactly, there is a precise sense in which those are easier from an ATP perspective (and to some extent when hand proving too): you can enumerate all the consequences of what you know until you don't get any new things, and this can handle le_trans reasoning

[Mac Malone]

@Mario Carneiro I assume this applies when the strategy is strictly to apply one of the possible theorems to the current goal. Because you could continue building infinite have s by le_trans/le_succ from 0 upwards in the Nats (in a manner similar to inducitng up them). (iirc, one of these is forward reasoning and one is backwards reasoning?)

[Mario Carneiro]

I think the trick that makes saturation work is the subformula property: (under some conditions) if there is a proof then there is a proof which only uses subterms of what you already have

[Mario Carneiro]

so you know that just building up big terms doesn't help

[James Sully]

Ok, now I'm stuck on one that definitely does involve induction:
https://adam.math.hhu.de/#/g/hhu-adam/NNG4/world/LessOrEqual/level/8

Here's what I have so far:

theorem le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by

induction y with d hd
-- base
right
exact zero_le x

-- inductive
cases hd with x_le_d d_le_x
-- x_le_d case
left
apply le_trans x d (succ d) x_le_d (le_succ_self d)

Now my goal is:

Current Goal
Objects:
xd: ℕ
Assumptions:
d_le_x: d ≤ x
Goal:
x ≤ succ d ∨ succ d ≤ x

but the goal doesn't seem to me to follow from the assumption? It's difficult for me to keep track of what's going on haha

[James Sully]

presumably it must and I'm mistaken. But i'm not sure where to go next

[Ruben Van de Velde]

Maybe you should have started with induction y with d hd generalizing x

[James Sully]

hmm, that may be a better approach, but I haven't been introduced to generalizing yet and don't know what it is, and the hint says

Start with induction y with d hd.

So presumably it's not the intended solution

[Kevin Buzzard]

Generalizing won't help you here, I think. Do I not offer some hints with this level? It's one of the hardest ones. How do you get over the line with generalizing? Am I pushing people the wrong way?

[Kevin Buzzard]

My idea was: cases on d_le_x with a and then cases on a

[Ruben Van de Velde]

I didn't actually manage to finish it with generalizing either :)

[Thomas Murrills]

The key for me was realizing how to use numbers to make progress on ≤ goals, then working backwards. Without the usual things accessible, it took a bit to figure out which of the very few tools available were suitable! :P

[James Sully]

Kevin Buzzard said:

My idea was: cases on d_le_x with a and then cases on a

it seems very simple and obvious and mechanical when you put it like that haha. I guess I just lost faith

induction y with d hd
-- base
right
exact zero_le x
-- inductive
cases hd with x_le_d d_le_x
-- x_le_d case
left
apply le_trans x d (succ d) x_le_d (le_succ_self d)
cases d_le_x with a
cases a
rw [add_zero] at h
rw [h]
left
exact le_succ_self d

rw [add_succ, ← succ_add] at h
right
use a_1
exact h

[Thomas Murrills]

(Btw, @Kevin Buzzard, typo at the end: "remarks that with you've")

[James Sully]

thanks for the help!

[Mac Malone]

Mario Carneiro said:

In this case, you might be tempted to prove a <= 0 -> a = 0 by induction on a, but this is the wrong move and you will get stuck

As an FYI, here is how I solved LE world level 5 via induciton:

theorem le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by

induction x
rfl
rw [n_ih $ le_trans _ _ _ (le_succ_self n) hx] at hx
cases hx
rw [add_comm, add_succ, add_zero] at h
exact False.elim <| zero_ne_succ _ h

Noting this here in case @Kevin Buzzard desires to forbid such an inductive solution.

[Mac Malone]

(One worry is that my use of cases on the ≤ term may be an unintentional leakage of the underlying definition.)

[Ruben Van de Velde]

Level 4 explicitly teaches using cases like this

[Mario Carneiro]

I doubt Kevin actually wants to forbid proofs off the beaten track; finding a solution via an unexpected strategy is one of the joys of gaming

[James Sully]

I finished the game!

[James Sully]

that was fun

[learnreal]

For one of my goals

Objects:
abn_1: ℕ
Assumptions:
n_ih: (a * b) ^ n_1 = a ^ n_1 * b ^ n_1
Goal:
(a * b) ^ n_1 * (a * b) = a ^ n_1 * (a * b ^ n_1 * b)

I am tring rw [mul_comm a b^n_1] but getting the following error:

tactic 'rewrite' failed, equality or iff proof expected
  ?m.39929
case succ
abn_1: ℕ
n_ih: (a * b) ^ n_1 = a ^ n_1 * b ^ n_1
⊢ (a * b) ^ n_1 * (a * b) = a ^ n_1 * (a * b ^ n_1 * b)

can someone please explain the error to me and how to apply mul_comm here?

[Riccardo Brasca]

rw [mul_comm a (b^n_1)] should work.

[Kevin Buzzard]

You're not the first person who has run into this and I don't know what to do about it :-/

[learnreal]

Explicitly add example in documenttion? May be it's there but I missed it!

[Alexander Bentkamp]

Maybe we could add a custom elaborator that would catch equalities raised to the power of something and then throw a sensible error message?

[Paul Söntgerath]

Hi,

I just came across Lean and wanted to start practising it by means of the Natural Number Game. However, I am stuck at:
World: Addition World, level 2/5, step case of the induction
image.png
I've tried numerous approaches, but cannot figure out how to reach the solution.

Does anyone have a hint/tip to get me in the right direction?

Thanks.

[Paul Söntgerath]

Managed to figure it out myself.

[Joscha Mennicken]

The game appears to be broken right now; a css and a js file are not transmitted correctly. The error is a content mismatch (partial content) error.

Looking at the server's response for https://adam.math.hhu.de/assets/index-c6c07006.js, it promises us Content-Length: 5909974 (around 6 MB) but the response is only about 100 kB long.

[Kevin Buzzard]

@Jon Eugster @Alexander Bentkamp could this be related to Dan Velleman's DM reporting the error "tmp/djvelleman_stg4_1168333537/game.zip: write error (disk full?). Continue? (y/n/^C)"?

[Jon Eugster]

might be, Ill have a look today

[Jon Eugster]

I can't reproduce this today. @Joscha Mennicken if you still experience problems could you open an issue here on the repo or DM me more details, please :)

[Kevin Buzzard]

The website was not working yesterday, for sure.

[Jon Eugster]

I see, the server is 97% full. So probably one of the scripts just freed up some space again this morning :light_bulb:

[Tainnor]

Hi, I'm somehow stuck on Advanced Addition World level 5. I tried:

cases b with d
rw [add_zero]
intro h
exact h
rw [add_succ]
intro h

And now I'm trying to do apply (succ_ne_zero (a+d)) - but I just get unknown identifier 'succ_ne_zero' - is that a bug?

[Ruben Van de Velde]

Yeah, that's odd. As far as I can tell this should work

[Ruben Van de Velde]

To unblock you, it seems to be possible to do symm at h and use zero_ne_succ instead

[Kevin Buzzard]

There's definitely a point in the game when you only have one of these, not the other.

[Tainnor]

Yeah but on the right panel, I see both

[Ruben Van de Velde]

^ that is what made me think it should be available

[Mauricio Collares]

It looks like this to me: AdvAdditionLvl5.png. Does it depend on what other levels you've finished?

[Tainnor]

it's possible since I did algorithm world first

[Damiano Testa]

Indeed: on my computer (Linux) using Chrome, when I use none as rules, I have all names in black, but using the other settings for the rules, there are some shaded lemmas.

[Tainnor]

it works with symm though - thanks @Ruben Van de Velde

[Jon Eugster]

Tactics stay available if you unlocked them in a different world. That's a decision that has been made to allow leave worlds that introduce high level tactics. E.g. the old NNG3 introduced simp somewhere out there, and it would completely optional to use in the rest of the game.

succ_ne_zero seems indeed not to be available yet. I understand why the error message is there, but it would be better if it said "not unlocked" instead of "unknown identifier". I'll add this as an issue to be improved:+1:

[Kevin Buzzard]

If the user chooses to do Algorithm World (which includes succ_ne_zero in level 6) before Advanced Addition World (which the map certainly allows them to do), should they be allowed to access succ_ne_zero in Advanced Addition World?

[Alexander Bentkamp]

Yes, I think typically users should be allowed everything they have learned. Maybe you can import succ ne zero in advanced addition world?

[Kevin Buzzard]

But would that make algorithm world a prerequisite for advanced addition world?

[Jon Eugster]

Kevin Buzzard said:

But would that make algorithm world a prerequisite for advanced addition world?

No, only if you use anything in your sample proofs. That's the only thing which determines the drawn dependencies between worlds. I think that part is not fully flechted out. For tactics it's clear: you are expected to import all tactics in all levels (i.e. in some preliminaries/metadata file, so that the only restriction to using tactics is the game disallowing some.

For theorems that does not work. If lemmas depend on each other, they simply cannot be available yet because they cannot be imported in the lean file. For your situation, importing adv. multiplication world works but in general I think there are always situations where the game would allow a theorem, but it's not imported in the underlying lean file :thinking: so that might need to be fixed.

[Kevin Buzzard]

I'll try this later today -- thanks!

[Tainnor]

I've had it happen multiple times that the game just replies with "oops!" - that makes it a bit hard to understand what one has done wrong

[Kevin Buzzard]

ha ha, that's @Adam Topaz 's fault :-) His preliminary version of apply ... at had that in, and it wasn't in actual mathlib at that time so I went with his version. Now apply ... at is in mathlib so we should bump mathlib and fix this. Thanks!

[Adam Topaz]

Oops!

[Kevin Buzzard]

It means "you used apply ... at in an invalid way" btw :-)

[Tainnor]

thanks for the explanation! I'm currently unsure, what I'm doing wrong here (inequality world, level 10):

cases x with x' hx'
left
rfl
cases x' with x'' hx''
right
rw [one_eq_succ_zero]
rfl
rw [one_eq_succ_zero] at hx
apply succ_le_succ at hx
apply le_antisymm at hx
apply zero_le at hx

that last line is an "oops" :)

[Adam Topaz]

just before apply zero_le at hx, the type of hx is 0 ≤ succ x'' → succ x'' = 0. What do you expect apply zero_le at hx to do in this case?

[Tainnor]

zero_le would prove 0 <= succ x'', no? So I would have thought that just gives me succ x'' = 0

[Adam Topaz]

ok, indeed apply .. at .. is not set up to handle such use cases. Do you know about the specialize tactic? Is that available in the NNG (I honestly don't know!)?

[Tainnor]

ah I don't think it's available

[Tainnor]

I guess I'll have to find another way then

[Adam Topaz]

For those who are familiar with coq's apply .. at .. tactic: is that something that one is able to do in coq?

[Kevin Buzzard]

OK: apply ... at is now oops-free on main; but I have not managed to fix the succ_ne_zero issue @Alexander Bentkamp . Do you expect the following error if I'm playing on "regular" rules?

succ_ne_zero.png

I imported all of algorithm world into level 1 of advanced addition world, compiled locally, cleared my save, I then speedran the game up to doing all of algorithm world and then started on advanced addition world and it wouldn't let me use succ_ne_zero even though I'd unlocked it.

[Alexander Bentkamp]

I didn't expect it when I wrote to you earlier today, but after speaking to @Jon Eugster , yes, that is the current behavior. Certainly not ideal. We have discussed a better solution today and I beliebe Jon will implement it.

[Kevin Buzzard]

Well, on the plus side the latest new world -- advanced multiplication world -- is now live! Much bigger than the original NNG3 advanced multiplication world, it also contains some of the basic things you'll need for the forthcoming divisibility world :-)

[Tainnor]

In level 6 of Advanced Multiplication World, it says "you can type ≠ with e" - is that a mistake? Or am I misunderstanding the instruction?

[Tainnor]

I guess it should say "with \ne"? Thinking of it, I'm wondering if somehow that "\n" got parsed as a newline somewhere :D

[Kevin Buzzard]

lol yes I'm sure you're right :-) Thanks!

[Kevin Buzzard]

Thanks for being a beta tester for Advanced Multiplication World!

[Kevin Buzzard]

I fixed the problem locally, pushed, didn't wait for it to compile, attempted to update the server, and now I think I've broken the game completely, but if it's any consolation, it's working fine for me with \ne so if you're in London then feel free to pop into my office.

[Kevin Buzzard]

OK, should be fixed on the server now! Thanks!

[Tainnor]

Kevin Buzzard said:

Thanks for being a beta tester for Advanced Multiplication World!

Thanks for making this project available. :)

[Kevin Buzzard]

I just wrote the Lean code -- there's a whole bunch of other people that did the "making it available" part :-) (Patrick Massot, Mohammad Pedramfar, Jon Eugster, Alex Bentkamp)

[Tainnor]

Thanks to all of you

[Tainnor]

Maybe one day I'll become a Lean wizard and can contribute something back :)

[Tainnor]

world 9 of Advanced Multiplication World doesn't appear to work. It tells me to use induction b with d hd generalizing c but when I try that it replies with You have not unlocked the tactic 'generalizing' yet!

[Kevin Buzzard]

@Jon Eugster @Alexander Bentkamp any idea what to do about this? Note that main has moved on from the commit which I deployed, which was almost certainly 2cbb347, and indeed when I compile this commit I get (a ton of deprecation warnings, now fixed on main +) the warning

./././Game.lean:113:0: warning: No world introducing generalizing, but required by AdvMultiplication

But generalizing isn't a tactic :-( (and it's not complaining that at isn't introduced, even though apply ... at ... is a thing...). Note that the "model answer" for that level in the repo starts with induction b with d hd generalizing c. To verify the bug report above I suspect I'd have to play through a load more of the game and right now I don't have time (I'm packing to leave for Italy tomorrow). @Tainnor I suspect that one fix might be to go back to the overworld and select "none" for rules -- this seems to work for me on the online version of the game.

Slightly off-topic remark: after removing all the deprecated commands and compiling I now get the even worse

stdout:
./././Game.lean:113:0: warning: No world introducing induction, but required by LessOrEqual
./././Game.lean:113:0: warning: No world introducing induction, but required by AdvMultiplication
./././Game.lean:113:0: warning: No world introducing generalizing, but required by AdvMultiplication
./././Game.lean:113:0: warning: No world introducing induction, but required by Multiplication
./././Game.lean:113:0: warning: No world introducing induction, but required by AdvAddition
./././Game.lean:113:0: warning: No world introducing induction, but required by Addition
./././Game.lean:113:0: warning: No world introducing induction, but required by Power

so goodness knows what I've screwed up here...

[Alexander Bentkamp]

We have a list of keywords that dont count as tactics. Apparently generalizing is not on it yet?

[Alexander Bentkamp]

["with", "fun", "at", "only", "by", "to"]

[Tainnor]

Setting "none" for the rules works. :thumbs_up:

[Kevin Buzzard]

You can switch it off after you've done the level :-) Perhaps the proof will stop working if you revisit the level, but to be honest I slightly reorganised one or two earlier levels when I added advanced multiplication world so your history is probably a bit broken anyway :-/ Thanks for beta testing the game! I played through it all but I was on "none" so I missed this issue.

[Tainnor]

neat - I'm done with this world now too

[Kevin Buzzard]

OK I'll try and get divisibility world up and running :-)

[Tainnor]

no rush, playing through Set Theory Game right now

[Kevin Buzzard]

#mil is another good thing to do next btw

[Tainnor]

yeah, I also started looking at that

[Tainnor]

my hope is that I'll learn enough so I can prove some theorems in my complex analysis text

[Jon Eugster]

Alexander Bentkamp said:

We have a list of keywords that dont count as tactics. Apparently generalizing is not on it yet?

I think it is fixed on the dev branch already and will be fixed for nng once the game updates to the next lean release.

[Michael]

I have a concern about Algorithm World level 5. It purports to show that succ_inj is a theorem and not an axiom.

But I don't see how the pred function can be defined at all without first postulating succ_inj. Suppose there were a natural number, 0', which was not equal to 7 but the successor of which was 8. In that case, the definition of pred would tell us that pred (succ 7) = 7, and it would also tell us that pred (succ 0') = 0'. But since succ 7 = 8 and succ 0' = 8, but 0' ≠ 7, this is a contradiction.

The Peano axiom that assures us that this contradiction cannot arise is succ_inj.

Am I missing something?

[Michael]

I guess the induction axiom could also provide this assurance?

[Mario Carneiro]

@Michael Lean does not use Peano Arithmetic as its foundation. It uses the Calculus of Inductive Constructions, which when specialized to

inductive Nat where
| zero : Nat
| succ : Nat -> Nat

gives something surprisingly close to the peano axioms, but not quite. Specifically, we get five things:

1. Nat : Type
2. zero : Nat
3. succ : Nat -> Nat
4. Nat.rec : {motive : Nat → Sort u} → motive zero → ((n : Nat) → motive n → motive (succ n)) → (t : Nat) → motive t

5. computation rules:

   • Nat.rec z s zero = z
   • Nat.rec z s (succ n) = s n (Nat.rec z s n)

If you squint, you might recognize Nat.rec as a variation on the peano induction axiom. But there is a twist, which is that motive can produce values in an arbitrary Sort u. If it is a Prop then this is induction, but if it is a Type then this is actually definition by recursion, which in PA is a derived principle; here it is primitive.

So the short answer to your question is that pred comes directly out of the ability to define functions by recursion on Nat, and with a very clever choice of recursive definition you can use this to prove succ_inj and succ_ne_zero.

[Kevin Buzzard]

This question comes up a lot, especially from people who have been indoctrinated by Peano's version of the axioms. As Mario says, the point is that the principle of recursion says that you are allowed to define a function by saying what it does on 0 and on succ n, so you're allowed to define pred, and you're just discovering the real power of this principle -- it has nontrivial consequences.

[Michael]

It's not obvious to me that this is coming from "the principle of recursion", but to be fair I don't see a statement of that to compare to.

There seems to be an implicit statement, I guess in the Calculus of Inductive Constructions, that when we define the inductive type Nat, the construction rule succ must produce a value that didn't otherwise exist. (If the only natural number were zero, that would violate the axiom that zero is not the successor of any number, but it would not appear to conflict with the definition

inductive Nat where
| zero : Nat
| succ : Nat -> Nat

; it would just imply that the successor of zero was also zero.)

Suppose I want to define a subset of the natural numbers this way:

$$5 \in S \\ n \in S \to n + 2 \in S \\ n \in S \to n + 3 \in S$$

I take it that if I were to make this an inductive type:

inductive my_subset where
| five : my_subset
| two_plus : my_subset -> my_subset
| three_plus : my_subset -> my_subset

there would be an implicit assumption that two_plus (two_plus (two_plus five)) is a different object than three_plus (three_plus five)?

I see a minor emphasis in https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html on the assumption that, when a type is defined inductively, the listed constructors are the only way to produce an object of the type, but I don't see a mention of the assumption that an object produced by a given series of constructors is necessarily distinct from an object produced by a different series of constructors.

[Mauricio Collares]

That's because you can prove this fact using the recursor, as explained in https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/ (that's the very clever choice of recursive definition Mario mentioned)

[Michael]

But this is not actually a fact. 2 + 2 + 2 + 5 is in fact equal to 3 + 3 + 5. The inductively defined set is still valid even though it's possible for most elements to be constructed in more than one way.

[Mauricio Collares]

But the only connection between b (b (b a)) and 2 + 2 + 2 + 5 are the names you picked for the constructors. You'd have to take quotients to assign arithmetic meaning to equality for your inductive type.

[Michael]

But until a meaning is assigned, we can't say that the objects are or aren't different. That includes not being able to say that they are different.

[Mauricio Collares]

Are you saying you want a system where equality depends on the names of the constructors you pick? I'm not sure other people would prefer that.

[Mauricio Collares]

You don't "assign meaning" to constructors for an inductive type (for the purposes of verifying equality), they're just constructors

[Michael]

I am saying that when you don't know whether two expressions are equal, it doesn't make sense to state that they aren't.

[Michael]

But looping back around, if part of the definition of the inductive keyword is that all related constructors are injective, it's not much of a theorem to show that an inductive constructor is injective.

[Michael]

As far as "you don't 'assign meaning' to constructors", I feel like it's pretty common to define sets in just this manner, by including certain elements explicitly and others by saying that the set is closed under certain operations. And an inductive type looks to me like it is meant to reflect that concept?

[Mauricio Collares]

Mario listed the axioms related to the inductive keyword, and injectivity is not one of the axioms since it follows from Nat.rec using the "no confusion" trick. If you don't like Kevin's blog post, there's also the nice paper of McBride where the term originated (see section 7): https://personal.cis.strath.ac.uk/conor.mcbride/PolyTest.pdf

[Mauricio Collares]

(actually, I'm not sure the term originated there, but that's where I know it from)

[Mauricio Collares]

But, yes, if it didn't follow from the axioms, injectivity would probably be added as a separate axiom. I think I understand where you're coming from, because inductively defined subsets are very common in computer science and mathematics. But the inductive keyword is not quite that; it is defining a new type, not a subset with certain properties.

I guess in HoTT you'd be able to express the desired equivalences as part of the definition? I know nothing about HoTT.

[Tainnor]

I didn't actually know that injectivity of constructors could be proven, I had assumed that it would have been an axiom. I'm somewhat familiar with ML type languages like Haskell and Idris where data constructors are injective by nature

[Tainnor]

Mauricio Collares said:

That's because you can prove this fact using the recursor, as explained in https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/ (that's the very clever choice of recursive definition Mario mentioned)

Hmm, but that definition of mytype_equal' only makes sense if we assume constructors to be disjoint. If we could have AA being the same value as ZZ, then that definition wouldn't even work.

Maybe the difference here is between "sameness of expressions" (two expressions are the same if they have the same normal form) and "equality as a proposition" - i.e., "axiomatically", AA and ZZ are different expressions but there isn't an axiom that is saying AA \ne ZZ - that's a theorem that can be derived. But in general, I think, two expressions A and B can be different and (by axiom or proof) still satsify A = B.

[Tainnor]

At least that's what my little knowledge of dependent type theory tells me, but I could be wrong

[Mauricio Collares]

My naïve/intuitive interpretation of recursors is "whatever is required of the underlying theory to make pattern matching work as expected". The pattern match in mytype_equal' gets compiled down to a Type.rec application, and you can print it to see how it's done.

[Mauricio Collares]

This is Lean 3 to match the blog post, but it doesn't really matter:

inductive mytype
| AA : mytype
| ZZ : mytype

open mytype

definition mytype_equal' : mytype → mytype → Prop
| AA AA := true
| AA ZZ := false
| ZZ AA := false
| ZZ ZZ := true

#print mytype_equal'._main
-- def mytype_equal'._main : mytype → mytype → Prop :=
-- λ (ᾰ ᾰ_1 : mytype),
--  ᾰ.cases_on (ᾰ_1.cases_on (id_rhs Prop true) (id_rhs Prop false))
--    (ᾰ_1.cases_on (id_rhs Prop false) (id_rhs Prop true))

#print mytype.cases_on
-- @[reducible]
-- protected def mytype.cases_on : Π {motive : mytype → Sort l} (n : mytype), motive AA → motive ZZ → motive n :=
-- λ {motive : mytype → Sort l} (n : mytype) (e_1 : motive AA) (e_2 : motive ZZ), mytype.rec e_1 e_2 n

#print mytype.rec
-- protected eliminator mytype.rec : Π {motive : mytype → Sort l}, motive AA → motive ZZ → Π (n : mytype), motive n

[Tainnor]

Sure, but when the runtime evaluates a rec expression somewhere, it ultimately has to decide when expressions are the same and when they aren't

[Kevin Buzzard]

You should think of inductive types as being "the universal object satisfying the rules", not just "any object satisfying the rules". The reason two_plus two_plus two_plus five isn't equal to three_plus three_plus five is because the inductive type you've constructed isn't "any old set with a 5 and a 2+ and a 3+", it's "the most general set with a 5 and a 2+ and a 3+" (where these are now random functions from the set to itself). If you want relations on your inductive type, that's absolutely fine: just write down what they are, make an equivalence relation, and take a quotient.

[Kevin Buzzard]

@Michael

[Patrick Massot]

Michael said:

But looping back around, if part of the definition of the inductive keyword is that all related constructors are injective, it's not much of a theorem to show that an inductive constructor is injective.

You need to accept that when you are so close to foundations then intuition no longer plays any role. The fact that you feel that injectivity of constructors are part of the definition of inductive type has no consequence on reality. Mario showed you the actual axioms that are generated and they do not include any injectivity. And then you were shown a actual proof that injectivity follows.

[Kevin Buzzard]

Another way to think about it: if you have any set N with an element Z and a function S : N -> N then the rules of lean guarantee that there must be a map f from Lean's naturals to N sending 0 to Z and succ(a) to S(f(a)). If you had "loops" in lean's naturals then this so-called universal property wouldn't hold

[Tainnor]

Patrick Massot said:

Michael said:

But looping back around, if part of the definition of the inductive keyword is that all related constructors are injective, it's not much of a theorem to show that an inductive constructor is injective.

You need to accept that when you are so close to foundations then intuition no longer plays any role. The fact that you feel that injectivity of constructors are part of the definition of inductive type has no consequence on reality. Mario showed you the actual axioms that are generated and they do not include any injectivity. And then you were shown a actual proof that injectivity follows.

sure, but there's quite some heavy lifting that is being done by the fact that you can even define functions on inductive datatypes (which wouldn't work if the constructors weren't disjoint).

[Mario Carneiro]

In CIC, you can define functions on inductive datatypes, by fiat. It is a consequence of this fact that the inductive constructors are disjoint. In PA it's the other way around: the inductive constructors are disjoint by fiat, and the induction principle holds, and it is a consequence of this that you can define functions by recursion. Same end result, different paths to get there.

[Mario Carneiro]

It's fine to keep as your mental model that the constructors of an inductive type are disjoint - it's true after all. But it turns out that recursors generalize better to all the different kinds of inductive type that lean supports, and disjointness is provable anyway, so there is no need to have it as a separate axiom.

[Michael]

Mario showed you the actual axioms that are generated and they do not include any injectivity.

Well...

Axiom (4) states that, given a value of f(0); a function which, given the value of f(n ∈ ℕ), tells you the value of f(succ n); and a value t ∈ ℕ, you can compute the value of f(t) . And then the computation rules state that you can do this by building t up from zero via repeatedly taking successors.

the principle of recursion says that you are allowed to define a function by saying what it does on 0 and on succ n, so you're allowed to define pred

The principle of recursion doesn't say that; you're always allowed to define a function by cases. Here is one:

$$f(x \in \mathbb{R}) = \left\{ \begin{array}{ll} 5 & x \leq 7 \\ x - 2 & x \geq 7 \\ \end{array} \right.$$

What you really want, defining a function by cases, is for the cases to be disjoint. They aren't here, but the function is well-defined anyway because, for all values of x where multiple cases apply, all applicable cases produce the same result, 5.

If we assume that the function posited by axiom (4) is well-defined, that is sufficient to prove that succ is injective.

But in the other direction, if we assume that succ is injective, then the computation rules given in (5) are an existence proof of the function posited by Nat.rec, and the assumption that succ is injective will prove that this function is well-defined.

(Unless I've made a mistake?)

If I haven't, then succ_inj is not really a consequence of axiom (4), it is a restatement of it. This is more or less why I view it as being postulated. I think it is strange to say that a collection of axioms does not include a particular axiom, when it does include an axiom that is logically equivalent.

[Mario Carneiro]

There's another reason why we don't make disjointness of constructors axiomatic though, which is that I lied just now, it's not always true:

inductive MyType : Prop
| AA : MyType
| ZZ : MyType
open MyType

example : AA = ZZ := rfl

[Mario Carneiro]

The trick is that on this type, MyType.noConfusion cannot be defined so the proof of disjointness doesn't work

[Tainnor]

huh, what is happening there?

[Mario Carneiro]

Axiom (4) states that, given a value of f(0); a function which, given the value of f(n ∈ ℕ), tells you the value of f(succ n); and a value t ∈ ℕ, you can compute the value of f(t) . And then the computation rules state that you can do this by building t up from zero via repeatedly taking successors.

I would phrase it slightly differently: It states that given a value z and a function s, gives you some function f, and the computation rules tell you what this function f does when operating on 0 and succ n. (It's not immediately obvious that every value t is of the form succ ... succ 0, and on an arbitrary variable f t doesn't have any particular computation rules, but you do know that it is of the right type because f is a function.)

[Mario Carneiro]

@Tainnor The type is in Prop and has two constructors, which means it is a "small eliminating inductive"; when this happens the MyType.rec function looks like this instead:

recursor MyType.rec : ∀ {motive : MyType → Prop}, motive AA → motive ZZ → ∀ (t : MyType), motive t

where the key point is the Prop in the motive argument (contrast with Sort u in the Nat.rec example from before). This recursor is only good for proofs by induction, you can't use it to construct functions

[Michael]

It's not immediately obvious that every value t is of the form succ ... succ 0

On the assumption that the constructors declared for an inductive type form an exhaustive list, which is explicitly mentioned... somewhere, this does look obvious to me?

[Tainnor]

Mario Carneiro said:

Tainnor The type is in Prop and has two constructors, which means it is a "small eliminating inductive"; when this happens the MyType.rec function looks like this instead:

recursor MyType.rec : ∀ {motive : MyType → Prop}, motive AA → motive ZZ → ∀ (t : MyType), motive t

where the key point is the Prop in the motive argument (contrast with Sort u in the Nat.rec example from before). This recursor is only good for proofs by induction, you can't use it to construct functions

Ok, this is beyond my pay grade. I'll check back in 5 years when I've thoroughly studied type theory. :D
It still confuses me that AA = ZZ, though

[Mario Carneiro]

That's because of proof irrelevance: AA and ZZ are both "proofs" of the proposition MyType, which is basically another way to write True

[Tainnor]

ah! ok yes, makes sense

[Tainnor]

I think I'm comparing Lean to something like Pie from "The Little Typer", where I think distinctness of constructors is really baked in the evaluation rules for specific types. But it makes sense that that wouldn't generalize to proof terms

[Mario Carneiro]

Michael said:

It's not immediately obvious that every value t is of the form succ ... succ 0

On the assumption that the constructors declared for an inductive type form an exhaustive list, which is explicitly mentioned... somewhere, this does look obvious to me?

It is true, but the proof of this involves another induction, and it's not clear how to turn the computation rules into something you can do induction on. You can only use the computation rules to completion on concrete numerals like 37, if you just have variables like example (m n : Nat) : m + n = n + m you can't "just compute both sides" because they aren't concrete numbers

[Mario Carneiro]

But perhaps this point is not so important

[Mario Carneiro]

Michael said:

Mario showed you the actual axioms that are generated and they do not include any injectivity.

Well...

Axiom (4) states that, given a value of f(0); a function which, given the value of f(n ∈ ℕ), tells you the value of f(succ n); and a value t ∈ ℕ, you can compute the value of f(t) . And then the computation rules state that you can do this by building t up from zero via repeatedly taking successors.

the principle of recursion says that you are allowed to define a function by saying what it does on 0 and on succ n, so you're allowed to define pred

The principle of recursion doesn't say that; you're always allowed to define a function by cases.

No, that's the principle of definition by cases (?). The principle of recursion says exactly what you wrote in the first paragraph: given values z : A and s : Nat -> A -> A there exists a function f such that f 0 = z and f (succ n) = s n (f n). In CIC this function is given the name Nat.rec z s.

[Michael]

The principle of recursion says exactly what you wrote in the first paragraph: given values z : A and s : Nat -> A -> A there exists a function...

I think we have some crossed terminology here; I'm going for the idea that I'm allowed to describe the function whether or not it exists, and once described I can investigate whether it's valid. As I read you, the principle of recursion says that a function matching this description is axiomatically valid.

[Mario Carneiro]

I suppose you are saying that there is an alternative definition of pred along the lines of:

def pred (n : Nat) : Nat :=
  if n = 0 then 0 else n - 1

And then you observe that in order to use this to deduce that pred (succ n) = n we have to prove that succ n != 0. This is true, but this isn't the definition of pred being used here.

[Mario Carneiro]

I think it is strange to say that a collection of axioms does not include a particular axiom, when it does include an axiom that is logically equivalent.

It's true that in such a situation it becomes largely a matter of taste which is taken as the axiom and which is the theorem. (As a terminological matter, this is fairly clear-cut though, axioms are explicitly and only the ones you are assuming directly and not other things which are logically equivalent to them. Keep in mind that all axioms and theorems are logically equivalent to True, so it's not a very discerning measure.)

In this case I think that's not what we have though, injectivity of constructors is not equivalent to the principle of recursion, it is a strictly weaker corollary of it. (For technical reasons even injectivity of constructors + induction is not equivalent to recursion in CIC, it requires the axiom of choice and even then you miss some definitional equalities given by the recursor.)

[Michael]

Mario Carneiro said:

I suppose you are saying that there is an alternative definition of pred along the lines of:

def pred (n : Nat) : Nat :=
  if n = 0 then 0 else n - 1

And then you observe that in order to use this to deduce that pred (succ n) = n we have to prove that succ n != 0. This is true, but this isn't the definition of pred being used here.

I'm a little queasy about having that attributed to me just because n - 1 isn't real. I'm happy to work with

$$f(n \in \mathbb{N}) = \left\{ \begin{array}{ll} 256 & n = 0 \\ m & \exists m \in \mathbb{N} (n = S(m)) \\ \end{array} \right.$$

where all the cases use terminology that exists.

But I guess you're right about what I'm thinking; in order to show that this function is well defined everywhere, it's necessary to show that when n = 0, no m (other than 256, in this example, I guess) exists for which n = succ m, which is the same thing as saying that succ n ≠ 0 for all n.

[Michael]

(It would also be necessary to show that for any two naturals sharing the same successor, they are equal to each other! This is precisely succ_inj.)

[Mario Carneiro]

you can't literally write that because m is out of scope of the existential

[Michael]

Mario Carneiro said:

you can't literally write that because m is out of scope of the existential

I don't understand?

[Mario Carneiro]

Michael said:

$$f(n \in \mathbb{N}) = \left\{ \begin{array}{ll} 256 & n = 0 \\ m & \exists m \in \mathbb{N} (n = S(m)) \\ \end{array} \right.$$

The $m$ here being returned is not a variable in scope

[Mario Carneiro]

I know what you are trying to say, but not only do you have to prove that the choice is independent of m, you also have to prove that such an m exists, which is exactly what you needed the function pred for

[Mario Carneiro]

remember that $n\ne0\to\exists m(n=S(m))$ is also not an axiom provided by CIC

[Michael]

(how are you doing the inline math?)

[Mario Carneiro]

basically, this is a definition approach that would make sense if you were given succ_inj and succ_ne_zero as primitives, but in CIC the more natural definition looks like:

$$\begin{align*} f(0) ={}& 256 \\ f(n+1) ={}& n \end{align*}$$

[Mario Carneiro]

Michael said:

(how are you doing the inline math?)

$$n\ne 0$$ -> $n\ne 0$. Also you can use "view message source" on any post to find out how it was done

[Michael]

As a terminological matter, this is fairly clear-cut though, axioms are explicitly and only the ones you are assuming directly and not other things which are logically equivalent to them.

This is fair, but it leaves me with a bad taste in my mouth over the in-game commentary saying "we will show you how to prove what Peano had to assume".

Keep in mind that all axioms and theorems are logically equivalent to True, so it's not a very discerning measure.

This is unfair; that's a different and weaker sense of "logical equivalence".

[Mario Carneiro]

I will be the first one to say that PA is a much simpler axiomatic system than CIC

[Mario Carneiro]

but it is true that CIC has this one swiss army knife recursor thing that subsumes 3 PA axioms

[Mario Carneiro]

it's not really a competition as such; rather this is a game with slightly different base rules than you might be used to and there are new strats to go with it

[Mario Carneiro]

in this game, definition by cases is less natural and in fact is re-cast as definitions by recursion on the inductive type

inductive Decidable (p : Prop) where
  | isFalse (h : ¬p) : Decidable p
  | isTrue (h : p) : Decidable p

Because in the CIC game, everything is defined using recursion on inductives (+ basic lambda calculus)

[Attila Vajda]

Hello, where can we ask questions about the number game? I am stuck:
Goal:
succ a + 0 = succ (a + 0)
typing rw [add_zero] does nothing
Screenshot-2024-05-27-at-10.24.41.png

[Yaël Dillies]

The best place is #new members

[Attila Vajda]

Thanks