induction, trying to come to grips with baby lean concepts

Stream: new members

[Lane Biocini]

hi all. I'm diving head first into Lean and would like to use it to assist in my math education. particularly, I want to get real handy with it for proofs and for programming applications. But I don't see the point in trying to pick up lean3 when lean4 is already in the milestone phase. So I'm diving into lean4. Unfortunately, it doesn't have a rational type yet, so I figured that some proficiency with lean will come if I attempt to construct them myself. I am using this paper as a model of how to construct canonical rationals with inductive types. It uses Coq, but the syntax is similar enough that I don't see why the model Bertot is using can't be adapted to Lean's syntax. In trying to do this ostensibly simple task, I'm seeing how bad the learning curve really is for my current level of knowledge. But I'm willing to chip away at it. I have some simple questions, that if I can't figure out I can hardly begin the work at all.

One of the inductive types defined for an initial type, Qplus (strictly positive rationals) contains as one of its inductive type defs Qplus.one, which represents unity in this system. The others are Qplus.num and Qplus.denom which are Qplus -> Qplus types. The idea is that you chain together expressions using recursion to define unique expressions ('words') in Qplus that represent canonical quotients interpretable as expressions of p/q. Okay, so far so good. In the paper, it specifies a few different ways of constructing such expressions. One involves a function c(x) : Qplus -> Qplus (this is how I interpret its type, at least), which maps expressions in Qplus to other expressions in Qplus. Okay. So for c(one) we get one. That's simple enough. But then this function is intended, for example, to be able to specify for x > 1 that we return num c (x-1). Fine. But as far as I can tell lean has no idea what it means to do arithmetic involving expressions with Qplus, nor how to judge inequalities, because of course that's my job. So as far as I can tell I can't use this method. I thought about the idea of trying to define Qplus.one as an expression of the ordered pair (1,1) Nat x Nat, and then translating expressions from Qplus so that I can tell lean how to handle cases where the arithmetic is identical to natural number arithmetic (I.e. Qplus.one + Qplus.one = 2, which is also (2,1) if we take Nat x Nat to be a valid representation of a quotient).

I get some strange errors when I try to define a function like Nat x Nat -> Qplus involving ConSort. So that tells me I'm just thinking about things the wrong way perhaps, and trying to take advantage of the defined natural number arithmetic might be the wrong approach. I guess my mental stumbling block here is that I'm used to recursive functions in traditional programming cases where the underlying number system and representation is already defined. So for example, in a factorial in C or the like, we can use the function call because at each call the function is returning elements of the total product which are each integers, while the argument eventually terminates when it returns 1 returning a completely defined product expression. This idea of recursion just isn't making any sense for me in lean, where its not easy to see just at what stage the definition of the expression is occurring. I have some sense that the uniqueness of the expression formed by these recursive types has to do with the unique signature of the compositions expressing them. I feel like I'm close to coming to grips with what I need to do, but I need some guidance on where to look or how to go about things.

[Yakov Pechersky]

Have you done the Natural Numbers Game? #NNG

[Yakov Pechersky]

That shows exactly how one might go about constructing a number system (in that case, naturals) from scratch, mathlib style

[Kevin Buzzard]

This is a very idiosyncratic way to define rationals; one natural way to define them is as a quotient but because quotients seem to get computer scientists all hot and bothered for some reason they come up with crazy ideas like this. The idiomatic and quick way to define the rationals in lean would just be as the localisation of the integers. But this isn't your question, and there's nothing stopping you formalising this idiosyncratic definition anyway.

However, you don't say anything about your background, and you don't post any code, and hence your questions are basically impossible to answer right now. If you want to know how to make progress, show us what you've done -- and you might want to start another thread in the #lean4 stream because right now most people here are using lean 3 until the maths library is ported (and when it is, we'll have the rationals so won't have to make them ;-) )

[Lane Biocini]

Yes, I've gotten fairly far in it which inspired me to take this on. But I feel like what I need to do in my project involves something fundamental which is already given to you when you begin the natural numbers game. I.e. "import mynat.definition -- imports the natural numbers {0,1,2,3,4,...}."

[Lane Biocini]

@Kevin Buzzard my background is that I'm an amateur programmer, familiar with the traditional imperative languages C, Python, Java, etc. and to a lesser extent languages like Julia, and a current math undergrad (at Calc III level (i.e. beginnings of vector calculus, lin alg, multi-variable calc and so on)). I am currently working through the HoTT book and excited to pick up type theory. The Natural Numbers game convinced me that Lean is my best target to learn how to work with all of this practically. I don't have any code to post for this example because this is how far I've gotten:

inductive Qplus : Type
| one : Qplus
| num : Qplus → Qplus
| denom : Qplus → Qplus

Even the most general direction as far as an approach would give me something to wrap my head around. I've done a lot of reading in the documentation in the Logic and Proof and Theorem Proving with Lean guides and I am catching hints of how I might need to think about it, but any guidance is well appreciated.

[Lane Biocini]

also @Kevin Buzzard as an aside, thank you very much for your work in making #NNG and your general work in this community. This journey I'm on was started basically after encountering the game, it singlehandedly put me into firm contact with one the most exciting subjects I've had the pleasure to investigate in a long, long time. I look forward to bootstrapping myself to contribute alongside everyone here.

[Kevin Buzzard]

For those who didn't click through, num and denom don't stand for numerator and denominator; num x is x + 1 and denom x is x/(1+x). The theory of continued fractions shows pretty easily that this gives a bijection to the positive rationals, however @Lane Biocini my feeling is that now defining addition and multiplication on this monstrosity is just the kind of thing which a computer scientist might get quite excited about but which is not something I'd like to sink time into without a good excuse, because I can define the positive naturals really easily by putting an equivalence relation on $\mathbb{N_{>0}}^2$ and then addition and multiplication are extremely easy to define assuming you've already defined them on $\mathbb{N}_{>0}$.

[Kevin Buzzard]

You've seen how much hard work it is defining them on the naturals, it looks ten times as hard to define them on this monstrosity representation of the positive rationals. Why not reuse the work? In a system like Lean where quotients are easy to manipulate there are many much easier ways to define a working copy of the rationals.

[Mario Carneiro]

Also, don't go thinking that this is a good representation of rationals. Natural numbers are represented in unary here

[Mario Carneiro]

The fact that a tree representation of the positive rationals is possible is useful for some applications (I think this is the Stern–Brocot tree) but Kevin is right that the arithmetic ops are horrible in this form

[Mario Carneiro]

hm, actually it's closer to the Calkin–Wilf tree but it's not exactly that either. There are apparently quite a few variations on that concept that work

[Lane Biocini]

well, regardless it has been a fun project to work on and I've made a lot of progress. I've learned a lot about Lean's syntax and inner workings in the process. Particularly I've been able to define inversion, constructions of Qplus instances from Nat x Nat, interpretation from Qplus instances to Nat x Nat, as well as quality of life code that defines coercions between Naturals and Qplus. arithmetic operations of addition and multiplication are also defined. So I can write something like (2/3 : Qplus) and I get the corresponding representation in a neat form

[Lane Biocini]

I've been having an issue with defining the order. Mainly, I expected that I would be able to use recursion to define a proposition that judges whether a given instance of Qplus is less than another.

def lt (w w' : Qword) : Prop :=
  match (w : Qword) with
  | Qplus.one =>
    match w' with
    | Qplus.one => False
    | Qplus.num x => True
    | Qplus.den x => False
  | Qplus.num y =>
    match w' with
    | Qplus.one => False
    | Qplus.num x => (lt y x)
    | Qplus.den x => True
  | Qplus.denom y =>
    match w' with
    | Qplus.one => True
    | Qplus.num x => True
    | Qplus.den x => (lt y x)

the compiler complains that the matching expression is supposed to be of type Sort ?m. This isn't an error I get on any other function that I define with a very similar recursive technique. Observe this function

def mk_mod (p q n : Nat) : Qplus :=
  match (n : Nat) with
  | Nat.zero => Qplus.one
  | Nat.succ x =>
    match (p - q : Nat) with
    | Nat.succ y => Qplus.num (mk_mod (Nat.succ y) q x)
    | Nat.zero => match (q - p : Nat) with
      | Nat.zero => Qplus.one
      | Nat.succ y => (Qplus.den (mk_mod p (Nat.succ y) x))

Or

def interpret (w : Qplus) : Nat × Nat :=
  match w with
  | Qplus.one => (1,1)
  | Qplus.num x => ((interpret x).2 + (interpret x).1, (interpret x).2)
  | Qplus.den x => ((interpret x).1, (interpret x).1 + (interpret x).2)

Both of these work just fine. Is this a special property of a def which returns Prop?

[Kyle Miller]

Whether or not this is the "right" way to implement rationals, it seems like a nice project, and I'm happy to have learned about this representation of positive rationals. I didn't realize you could store continued fractions with positive terms like this. $N^a D^b N^c ... = a + 1/(b + 1/(c + 1/\ldots))$

I've heard about Gosper's algorithms for arithmetic operations on continued fractions -- I was under the impression these weren't so horrible, but I've never seen running times.

[Kyle Miller]

@Lane Biocini It tends to be hard to debug errors without a #mwe, something that we can paste into an editor and see an error for ourselves.

[Kyle Miller]

I can guess what Qplus is, but I'm not sure about Qword. If I assume it's a typo for Qplus, then after replacing it I get no errors:

inductive Qplus
| one
| num (p : Qplus)
| den (p : Qplus)

def lt (w w' : Qplus) : Prop :=
  match (w : Qplus) with
  | Qplus.one =>
    match w' with
    | Qplus.one => False
    | Qplus.num x => True
    | Qplus.den x => False
  | Qplus.num y =>
    match w' with
    | Qplus.one => False
    | Qplus.num x => (lt y x)
    | Qplus.den x => True
  | Qplus.den y =>
    match w' with
    | Qplus.one => True
    | Qplus.num x => True
    | Qplus.den x => (lt y x)

[Lane Biocini]

wow @Kyle Williams ! I've clearly been staring at this code for too long thank you so much

[Lane Biocini]

Now as it turns out, my error is now something along the lines of "Failed to synthesize Decidable". When I finish implementing all the parts of this paper I will be uploading to github

[Lane Biocini]

A stretch goal for me is to be able to define exact arithmetic on the Calkin-Wilf numbers, but at the very least I have working functions that allow me to both construct and interpret rational number representations in it to and from their integer quotient equivalents. A secondary goal for me is to be able to construct paths from Calkin-Wilf numbers to their equivalents in Stern-Brocot and vice versa, because there are many nice properties the latter has and the translation from one to the other is trivial.

When I examine how the Rationals are constructed in mathlib, it uses a struct that includes the numerator, denominator, as well as two proofs that the denominator is non-zero and that both sides of the quotient are coprime. I see the wisdom in being able to carry out more efficient arithmetic on such integer representations.

I would like to then expand my approach, and construct my library such that it serves as a collection of translations between these rational representations. I can construct a similar struct as is implemented in mathlib; the advantage, as I see it, of building support for these binary representations of the rationals is that the construction of a number in either the Stern-Brocot or Calkin-Wilf representations is itself a proof that they are reduced and defined expressions in Q, because there is a bijection that exists between all three representations and a quotient is reduced when it is constructed in either binary representation. So the struct would simply be the following:

structure Rational where
  num : Int
  den : Nat
  pf: BinaryRat

Where in constructing it, one does math in integer form for arithmetic then constructs the binary representation which then supplies the values for numerator and denominator that are thereafter stored in the struct. For now I would focus on a chosen representative of BinaryRat, but eventually I would like to make a class which may be implemented by SternBrocot or CalkinWilk types.