## Stream: new members

### Topic: Tutorial Exercise

#### Lukas (May 09 2019 at 08:30):

I am working on the Blog article on constructing the natural numbers https://xenaproject.wordpress.com/2017/10/31/building-the-non-negative-integers-from-scratch/

Now I am stuck in one proof:

theorem one_add_eq_succ (n : xnat) : one + n = succ n :=
begin
rewrite one,
induction n with t Ht,
{
},
{
sorry,
}
end


I think this scan be solved via succ.inj, but I do not know how to apply this here.

#### Mario Carneiro (May 09 2019 at 08:31):

injection is the tactic version of apply succ.inj

#### Mario Carneiro (May 09 2019 at 08:31):

or cases in some cases

#### Lukas (May 09 2019 at 08:39):

apply succ.inj turns ⊢ succ (succ zero + t) = succ (succ t) goal into ⊢ succ (succ (succ zero + t)) = succ (succ (succ t)) so it does the inverse of what I want to do.

How can I apply the injection tactic here?

#### Mario Carneiro (May 09 2019 at 08:42):

oh, you want congr then

#### Mario Carneiro (May 09 2019 at 08:43):

if you have h : succ a = succ b in the context, injection h will turn it into a = b

#### Mario Carneiro (May 09 2019 at 08:43):

but if succ a = succ b is the goal, then you don't need injectivity, that's just functions respecting equality which is congr

#### Kevin Buzzard (May 09 2019 at 08:53):

After rewrite add you can use the inductive hypothesis Ht -- just rewrite Ht.

#### Kevin Buzzard (May 09 2019 at 08:58):

PS any feedback welcome. Over the summer I fully intend to expand that stuff into a more coherent and far-reaching tutorial for mathematicians, covering the naturals, the complexes, and various other ideas I have lying around.

#### Lukas (May 09 2019 at 08:59):

That should have been obvious...

#### Lukas (May 09 2019 at 09:01):

The Tutorial for the natural numbers is great, but as there are no solutions to the exercise I have to ask many questions.

#### Johan Commelin (May 09 2019 at 09:02):

That's how all of us have learnt Lean

#### Johan Commelin (May 09 2019 at 09:02):

Except for some magic wizards, who read the source code

#### Kevin Buzzard (May 09 2019 at 09:04):

@Lukas I wrote that tutorial and I had no solutions to the exercises either ;-) Some students at Imperial College sent me solutions and I did dump them somewhere on the internet...perhaps in the Xena project github repository (a.k.a. pile of random Lean files which I and some students wrote when we were all complete beginners 18 months ago).

#### Lukas (May 10 2019 at 11:17):

I just came across another problem. I defined the predicate for even like this:

definition even: xnat → Prop
| zero := true
| (succ m) := ¬ (even m)


but I can not figure out a way to test this #check even one does only show the Type prop but not the value. #reduce even zero leads as expected to true, but #reduce even one leads true → false which is false, but this becomes quickly unreadable as #reduce even two is (true → false) → false.

#### Kevin Buzzard (May 10 2019 at 11:30):

I think I would be tempted to define beven here, a function from xnat to bool, which is defined in Lean as {ff,tt}, and use bnot instead of not. Then you can define even to mean beven n = tt

#### Kevin Buzzard (May 10 2019 at 11:31):

PS you might have more luck with #eval than #reduce?

#### Lukas (May 10 2019 at 11:45):

The definition as function from xnat to Prop is taken from the blog article. With bool, bnot the definition works. Now my implementation look like this:

definition beven: xnat → bool
| zero := tt
| (succ m) :=  bnot (beven m)

definition even (m: xnat): Prop := beven m = tt


#reduce zero no gives me tt = tt and #reduce one gives tt = ff.

I am not yet clear if this is what I should expect. And why is the version returning a Prop better than to bool version?

#### Kevin Buzzard (May 10 2019 at 11:46):

I guess the author of the blog article was quite incompetent at that time.

#### Kevin Buzzard (May 10 2019 at 11:47):

To a mathematician, Prop and bool are difficult to tell apart. In Lean the key difference between them is that they sit in different places in the hierarchy. bool is a type, and Prop is a universe.

#### Kevin Buzzard (May 10 2019 at 11:47):

So in type theory, Prop is somehow a lot bigger than bool.

#### Kevin Buzzard (May 10 2019 at 11:48):

In type theory, there are universes, and then types in those universe, and then terms in those types. I say "in" because that's how I think of it, I guess type theorist would say "t has type T and T has type u" or something

#### Kevin Buzzard (May 10 2019 at 11:48):

Because they're quite different in the type theory world, they behave quite differently.

#### Kevin Buzzard (May 10 2019 at 11:49):

Both both definitions "work" and "give the right answer". I guess the big question is what you want to do with the definitions.

#### Kevin Buzzard (May 10 2019 at 11:49):

Let's stick with the Prop version for now, if the prestigious blog writer thinks that this is a good idea.

</sarcasm>

#### Kevin Buzzard (May 10 2019 at 11:50):

You can still try and prove that 2 is even

#### Kevin Buzzard (May 10 2019 at 11:50):

You've got to prove not not true

#### Kevin Buzzard (May 10 2019 at 11:50):

and that should be OK, because P implies not not P

#### Kevin Buzzard (May 10 2019 at 11:51):

and I can prove true, because that just means constructing a term of type true and I can look at the definition of true to find out what that term is called. Just write #check true and then right click on true and peek at the definition.

#### Kevin Buzzard (May 10 2019 at 11:51):

eew that is a rubbish name

#### Kevin Buzzard (May 10 2019 at 11:51):

that is a really confusing name

#### Kevin Buzzard (May 10 2019 at 11:52):

I think there's a tactic which proves true, called trivial or something

(deleted)

#### Kevin Buzzard (May 11 2019 at 16:53):

@Lukas your interest made me go back to that blog post and think about how I would have done it nowadays. I didn't think about even/odd but I did think about inequalities. Those 4 inequalities at the bottom were terrifically difficult. I didn't really know what I was doing at the time. I just tried various versions of le and lt, and I think that actually this is the best:

def le (a b : xnat) : Prop := ∃ c, a + c = b


Using this definition of le, it is not too hard to prove le versions of all the inequalities. And conversely, this one was by far the hardest to use:

inductive le : xnat → xnat → Prop
| refl (a : xnat) : le a a
| succ (a b : xnat) : le a b → le a (succ b)


Even proving a <= b implies succ a <= succ b was horrible with this; in the end I proved that this inductive le was the same as the easier-to-use le.

#### Kevin Buzzard (May 11 2019 at 17:13):

Another thing I noticed was that manipulating xnat is far more tedious than manipulating nat, because you constantly want stuff which is true but which I didn't prove -- stuff like succ a = succ b -> a = b, or a + b = a -> b = 0; the proofs are all easy, but they are not there.

#### Kevin Buzzard (May 11 2019 at 17:14):

I distinctly remember in 2017 firmly believing that every question about le on nat should almost by definition be completely trivial, because how can there even be any content?

#### Chris Hughes (May 11 2019 at 21:23):

@Kevin Buzzard maybe you weren't so stupid https://github.com/leanprover/lean4/blob/master/library/init/data/nat/basic.lean#L47

#### Patrick Massot (May 11 2019 at 21:24):

I think this version is good for computation

not for proofs

#### Kevin Buzzard (May 11 2019 at 21:24):

One thing I learnt today was that my cool inductive predicate idea seems to be the worst of them all

#### Chris Hughes (May 11 2019 at 21:52):

My attempt at the proof using the inductive definition. Pretty short, but it took me a while to work it out. I also used pred

open nat
namespace xnat
inductive le (a : ℕ) : ℕ → Prop
| refl : le a
| succ : ∀ b, le b → le (succ b)

infix  ≤' : 50 := le

lemma le_succ (a : ℕ) : a ≤' succ a :=
le.succ _ (le.refl _)

lemma le_of_succ_le {a b : ℕ} (ha : succ a ≤' b) : a ≤' b :=
le.rec_on ha (le_succ _) (λ _ _, le.succ _)

lemma succ_le_succ {a b : ℕ} (h : succ a ≤' succ b) : a ≤' b :=
show a ≤' pred (succ b),
from le.rec_on h (le.refl _) (λ _ h _, le_of_succ_le h)

lemma le_trans {a b c : ℕ} (hab : a ≤' b) (hbc : b ≤' c) : a ≤' c :=
le.rec_on hbc hab (λ _ _, le.succ _)


Nice!

#### Chris Hughes (May 11 2019 at 21:55):

This does illustrate a difficulty with inductive predicates. They're hard to use when not applied directly to local constants.

#### Chris Hughes (May 11 2019 at 21:57):

When you induct you want the fact that succ b has something to do with b, but the computed motives rarely give you that.

#### Chris Hughes (May 11 2019 at 22:04):

If I was recursing on equality, it would be completely obvious to do something like the method I chose. Interesting how my intuition for the equality recursor is so much better than other predicates, yet they're not that different.

#### Chris Hughes (May 11 2019 at 22:05):

This has changed the way I think about induction.

#### Kevin Buzzard (May 11 2019 at 22:09):

It was my job as your M1F teacher to teach you induction, I'm glad you now understand it better than me ;-)

#### Kevin Buzzard (May 11 2019 at 22:10):

After my M1F induction lecture last year, someone came up to me at the end of the lecture and complained that they thought they understood induction when they came into the lecture but now they realised they were completely confused about it ;-)

#### Chris Hughes (May 11 2019 at 22:11):

It's so obvious now I think about it. If i had succ a = succ b, it's obviously completely useless to try and recurse on that until I have a succ b in my goal. same applies here.

#### Kevin Buzzard (May 11 2019 at 22:11):

What confused them was that I told them that proofs were finite in length by definition but if you think about the proof of P(100) which you get by induction, it looks like "P(0) is true, therefore P(1) is true, therefore P(2) is true...therefore P(100) is true", so maybe "forall n, P(n)" has infinite length and can't be a proof?

#### Chris Hughes (May 11 2019 at 22:13):

I guess it does without the axiom of infinity.

#### Chris Hughes (May 11 2019 at 22:15):

If you don't say induction is an axiom and instead give that as the explanation, then it is an infinite length proof.

#### Kevin Buzzard (May 11 2019 at 22:15):

This was in my introduction to proof lectures -- I guess you can feel like induction is obvious, and then you start thinking about it that way and then you realise that actually there's more to it than meets the eye.

#### Chris Hughes (May 11 2019 at 22:17):

There's a lot to it. Have you ever tried to prove eq_of_heq in term mode from axioms? It's really hard.

#### Kevin Buzzard (May 11 2019 at 22:18):

I have never tried doing anything with heq, mostly because I remember you going through a period several months ago where you were continually moaning about it!

#### matt rice (May 12 2019 at 07:41):

@Kevin Buzzard
That definition you gave

def le (a b : xnat) : Prop := ∃ c, a + c = b


Is the exact one used in Logic and Proof, chapter 17/18 i believe

#### Kevin Buzzard (May 12 2019 at 08:00):

I think that the inductive predicate is used in Lean 3 and the definition by cases is used in Lean 4

#### Neil Strickland (May 20 2019 at 13:21):

So it seems that Lean 4 defines the order and decidable equality on Nat via maps to Bool, but reverts to using the same kind of framework as Lean 3 for Int, list Nat and so on. Does anyone know why that is?

#### François G. Dorais (May 21 2019 at 21:10):

@Neil Strickland My best guess is that derived Bool equality hasn't been built into inductive types yet. It's pretty ubiquitous, so I'm pretty sure it will be built in eventually.

Last updated: May 10 2021 at 19:16 UTC