Tutorial Exercise

Stream: new members

[Lukas]

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,
  {
    rewrite add_zero,
  },
  {
    rewrite add,
    sorry,
  }
end

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

[Mario Carneiro]

injection is the tactic version of apply succ.inj

[Mario Carneiro]

or cases in some cases

[Lukas]

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]

oh, you want congr then

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

That should have been obvious...

[Lukas]

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]

That's how all of us have learnt Lean

[Johan Commelin]

Except for some magic wizards, who read the source code

[Kevin Buzzard]

@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]

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]

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]

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

[Lukas]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

</sarcasm>

[Kevin Buzzard]

You can still try and prove that 2 is even

[Kevin Buzzard]

You've got to prove not not true

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

eew that is a rubbish name

[Kevin Buzzard]

that is a really confusing name

[Kevin Buzzard]

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

[Maxim Gerspach]

(deleted)

[Kevin Buzzard]

@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]

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]

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]

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

[Patrick Massot]

I think this version is good for computation

[Patrick Massot]

not for proofs

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

Nice!

[Chris Hughes]

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

[Chris Hughes]

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]

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]

This has changed the way I think about induction.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

I guess it does without the axiom of infinity.

[Chris Hughes]

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]

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]

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]

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]

@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]

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

[Neil Strickland]

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]

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