Zulip Chat Archive

Stream: new members

Topic: formalizing definitions for real analysis


Patrick Thomas (Jul 24 2020 at 20:39):

I was wondering if someone might be able to suggest the best way to formalize the following, especially the definition of a partition.

1.1 Definition: A partition PP of a closed interval [a,b][a, b] is a finite sequence (x0,x1,,xn)(x_{0}, x_{1}, \ldots, x_{n}) such that a=x0<x1<<xn=ba = x_{0} < x_{1} < \ldots < x_{n} = b. The norm of PP, denoted P\left|\left|P\right|\right|, is defined by P=max1in(xixi1)\left|\left|P\right|\right| = \max_{1 \leq i \leq n} (x_{i} - x_{i-1}).

1.2 Definition: Let P=(x0,,xn)P = (x_{0}, \ldots, x_{n}) be a partition of [a,b][a, b], and let ff be defined on [a,b][a, b]. For each i=1,,ni = 1, \ldots, n, let xix_{i}* be an arbitrary point in the interval [xi1,xi][x_{i-1}, x_{i}]. Then any sum of the form R(f,P)=i=1nf(xi)(xixi1)R(f, P) = \sum_{i=1}^{n} f(x_{i}*)(x_{i} - x_{i-1}) is called a Riemann sum of ff relative to PP.

1.3 Definition: A function ff is Riemann integrable on [a,b][a, b] if there is a real number RR such that for any ϵ>0\epsilon > 0, there exists a δ>0\delta > 0 such that for any partition PP of [a,b][a, b] satisfying P<δ\left|\left|P\right|\right| < \delta, and for any Riemann sum R(f,P)R(f, P) of ff relative to PP, we have R(f,P)R<ϵ\left|R(f,P) - R\right| < \epsilon.

1.4 Definition: A function gg, defined on [a,b][a, b], is a step function if there is a partition P=(x0,x1,,xn)P = (x_{0}, x_{1}, \ldots, x_{n}) such that gg is constant on each open subinterval (xi1,xi)(x_{i-1}, x_{i}), for i=1,,ni = 1, \ldots, n.

Kenny Lau (Jul 24 2020 at 20:40):

just don't use backticks

Kenny Lau (Jul 24 2020 at 20:40):

and use double-dollar-signs, i.e. $$\LaTeX$$ for LaTeX\LaTeX

Patrick Thomas (Jul 24 2020 at 20:42):

Thank you.

Reid Barton (Jul 24 2020 at 20:49):

What theorems do you want to prove and how do the proofs go?

Reid Barton (Jul 24 2020 at 20:51):

I would probably be inclined to go for a fairly literal translation (and, in particular, not invent a custom inductive type for a partition) in order to avoid reinventing lots of finset sum stuff.

Patrick Thomas (Jul 24 2020 at 20:52):

I'm going through the exercises in the first chapter of "An Introduction to Lebesgue Integration and Fourier Series" by Howard J. Wilcox and David L. Myers. I'm attaching what I have done in latex. myers.dvi

Jalex Stark (Jul 24 2020 at 20:53):

(do you know that mathlib has lebesgue integration?)

Patrick Thomas (Jul 24 2020 at 20:55):

I saw that directory, but I didn't understand it.

Jalex Stark (Jul 24 2020 at 20:55):

yury gave some tutorials about this part of the library at lftcm2020

Jalex Stark (Jul 24 2020 at 20:56):

there are exercises you can get with leanproject get lftcm2020 and a video lecture

Jalex Stark (Jul 24 2020 at 20:57):

the rest of the talks are on the same youtube channel :)

Patrick Thomas (Jul 24 2020 at 20:57):

Cool. I'll take a look.

Kevin Buzzard (Jul 24 2020 at 21:14):

The ultimate aim of the work described here would be to formally define an integral which is strictly weaker than an integral we have already. However, if you write the proofs in tactic mode with comments then it would be an excellent pedagogical resource.

Kevin Buzzard (Jul 24 2020 at 21:17):

@Patrick Thomas if you're thinking of developing the theory with pedagogy in mind then you might want to make new notation for a partition. Reid's point is a partition is just a finset containing a and b, and that the moment things get tough you are going to be unfolding the definition of a partition because all the lemmas about finsets which you'll need won't be rewritable until we can see the finset.

Patrick Thomas (Jul 24 2020 at 21:20):

Yes, it is for pedagogy. Sorry, I'm not sure if you are saying if I should or should not define it as a finset in lean.

Kevin Buzzard (Jul 24 2020 at 21:21):

If you're trying to write golfy term mode proofs for mathlib, this (making a new definition) will become tedious. But if you're happy to write tactic mode proofs then this will not be a bother at all. Taking Reid's argument to its natural conclusion, the lean idiomatic way would be to think of a partition as a nonempty finset of reals and you then define a and b to be the min and max. No new definition needed. The computer scientists would argue that the definition in your maths book is lousy because it's inconvenient to use in term mode. They say the fewer definitions the better. But I'm coming to the conclusion that there's some merit in ignoring the computer scientists and developing things the normal maths way. I just did three live streams about topological spaces and compact sets etc and I never once used a filter, I did it all the way I was taught. It's not going in mathlib but it's instructive for mathematicians

Patrick Thomas (Jul 24 2020 at 21:24):

What are "golfy term mode proofs"?

Patrick Thomas (Jul 24 2020 at 21:25):

Does that just mean really compact proofs or something more?

Reid Barton (Jul 24 2020 at 21:26):

I really meant something like (n : nat) (x : fin (n+1) -> real) (h0 : x 0 = a) ...

Reid Barton (Jul 24 2020 at 21:27):

I would suggest trying to formulate and prove a theorem about telescoping sums which amounts to the calculation of a Riemann sum for a constant function

Patrick Thomas (Jul 24 2020 at 21:28):

Is that code a suggestion for the definition of a partition?

Reid Barton (Jul 24 2020 at 21:29):

Yes

Patrick Thomas (Jul 24 2020 at 21:30):

I see.

Patrick Thomas (Jul 24 2020 at 21:48):

Why this rather than a finite set of reals? I haven't worked with fin before.

Adam Topaz (Jul 24 2020 at 21:49):

You can think of fin n \to \R as an ordered n-tuple of real numbers.

Patrick Thomas (Jul 24 2020 at 21:49):

So the difference is to make it ordered?

Patrick Thomas (Jul 24 2020 at 21:51):

It might help to see what the full definition in Lean would look like.

Adam Topaz (Jul 24 2020 at 21:51):

Yes. Mathematically, it's the difference between (x1,,xn)(x_1,\ldots,x_n) and {x1,,xn}\{x_1,\ldots,x_n\}.

Patrick Thomas (Jul 24 2020 at 22:01):

Are we defining a proposition like, is_partition, or the partition itself?

Kevin Buzzard (Jul 24 2020 at 22:03):

I thought a bit more about this and I agree with Reid. The disadvantage with a finset is that there is no good interface to access the i'th element. Lists would also be a pain because you probably won't be concatenating them or appending to the left, you will be mostly using them via their i'th element, so Reid's suggestion of a map from fin(n+1) (to ensure non-emptiness) to real is I think the best. Make a new definition! When you use it you'll figure out what API you'll need for it. I would love to watch the progress of this one.

Dan Stanescu (Jul 24 2020 at 22:04):

Adam Topaz said:

Yes. Mathematically, it's the difference between (x1,,xn)(x_1,\ldots,x_n) and {x1,,xn}\{x_1,\ldots,x_n\}.

Wait, with this definition I don't see where's the proof that x0<x1<x_0 < x_1 < \ldots . Isn't it just a tuple, with no order between the values?

Adam Topaz (Jul 24 2020 at 22:04):

You can still do it inductively with fin.

Adam Topaz (Jul 24 2020 at 22:04):

Since fin.tail is a thing.

Adam Topaz (Jul 24 2020 at 22:05):

You can define a partition of [a,b][a,b] of length n as the data of a partition of length n1n-1 of [a1,b][a_1,b] for some a1(a,b)a_1 \in (a,b).

Adam Topaz (Jul 24 2020 at 22:06):

And defining the empty partition is easy :)

Dan Stanescu (Jul 24 2020 at 22:06):

That's what I thought. I had actually started doing that myself some time ago.
At that time I didn't know about fin.tail.

Adam Topaz (Jul 24 2020 at 22:07):

To do this inductive definition, you just need to get the element in fin (n+1) corresponding to the value 11, which is (0 : fin n).succ, I guess.

Kevin Buzzard (Jul 24 2020 at 22:08):

@Dan Stanescu yeah you have to add a proof that x_i < x_{i+1}. Reid wrote ..., he didn't finish the definition. He did the data part and left the other mathematicians to do the proof part.

Reid Barton (Jul 24 2020 at 22:09):

The rest is just the same, translate "for all ii, xi<xi+1x_i < x_{i+1}" as something involving ∀ i : fin n, ... or whatever.

Reid Barton (Jul 24 2020 at 22:10):

Maybe it would be convenient to extend x to all of nat or even int by setting it to a/b outside the range fin n

Adam Topaz (Jul 24 2020 at 22:10):

Unfortunately, (i : fin n).succ has type fin (n+1).

Kevin Buzzard (Jul 24 2020 at 22:10):

I'm not sure that it will help to do the definition inductively. You're going to have a lot of lemmas where P is a partition and i is less than n and you want to talk about the interval [x_i, x_{i+1}]. If you make some fancy inductive definition then you'll have to work to get to the x_i

Reid Barton (Jul 24 2020 at 22:11):

Adam Topaz said:

Unfortunately, (i : fin n).succ has type fin (n+1).

Yes, which is the input of x

Adam Topaz (Jul 24 2020 at 22:11):

Oh right :)

Adam Topaz (Jul 24 2020 at 22:11):

So yes, I agree this is the best option :)

Reid Barton (Jul 24 2020 at 22:12):

You do have to do some cast to turn i : fin n to i : fin (n+1)

Adam Topaz (Jul 24 2020 at 22:12):

Doesn't this exist as a coersion?

Reid Barton (Jul 24 2020 at 22:13):

Not sure but it certainly exists in some form

Patrick Thomas (Jul 24 2020 at 22:14):

I'm not sure I follow, but I think what Kevin said makes sense?

Dan Stanescu (Jul 24 2020 at 22:14):

A good place to ask, would Riemann integrals still have a place somewhere in mathlib now? Same for Dedekind cuts.

Kevin Buzzard (Jul 24 2020 at 22:14):

Do you think it's worth storing the differences of the x_i, instead of the x_i themselves? Then you could use a finsupp.

Reid Barton (Jul 24 2020 at 22:17):

You're also going to need to talk about points xi<x<xi+1x_i < x < x_{i+1}

Patrick Thomas (Jul 24 2020 at 22:18):

The partitions will at points probably need to be broken apart into sets of subintervals with sums over those sets.

Adam Topaz (Jul 24 2020 at 22:18):

Reid Barton said:

Not sure but it certainly exists in some form

src#fin.cast_succ

Kevin Buzzard (Jul 24 2020 at 22:19):

You can have a finsupp from nat or int to nnreal and then just define the x_i as partial sums.

Adam Topaz (Jul 24 2020 at 22:19):

Just in case it's helpful later.

Patrick Thomas (Jul 24 2020 at 22:21):

Why is the function from fin (n + 1) \to \real and not \nat \to \real?

Reid Barton (Jul 24 2020 at 22:22):

Well that's what your informal definition said right?

Patrick Thomas (Jul 24 2020 at 22:23):

I guess I'm not sure what fin (n + 1) to real means? Is fin (n+1) a set?

Kevin Buzzard (Jul 24 2020 at 22:23):

It is the canonical type with n+1 elements

Jalex Stark (Jul 24 2020 at 22:23):

did you ask lean what fin (n+1) means?

Kevin Buzzard (Jul 24 2020 at 22:24):

You need a list of reals with n+1 elements and you need easy access to the i'th element of the list, so why not store the list internally as a function from a type with n+1 elements with names like 0,1,2,..,n to the reals.

Kevin Buzzard (Jul 24 2020 at 22:25):

fin m is a type. A term of type fin m is a pair consisting of a natural number i and a proof that i<m. You take a term of this type apart with cases, which gives you the pair (the number and the proof), and you build terms of this type with the \<i, hi\> constructor, where i is a nat and hi is a proof that i<m.

Patrick Thomas (Jul 24 2020 at 22:32):

So fin m is not the type of finite ordered sets of natural numbers? I think I'm starting to see.

Jalex Stark (Jul 24 2020 at 22:33):

what would the m be doing there?

Kevin Buzzard (Jul 24 2020 at 22:33):

fin m is exactly what I said it is. You can just #check fin if you have any more questions.

Adam Topaz (Jul 24 2020 at 22:33):

or #print

Jalex Stark (Jul 24 2020 at 22:34):

to elaborate on kevin's point, there's a literal definition and it is not very long

Kevin Buzzard (Jul 24 2020 at 22:34):

sorry yeah -- #check fin and then right click on fin and go to definition!

Jalex Stark (Jul 24 2020 at 22:34):

so if you read the definition you should either understand it or be able to find a part of it you don't understand

Adam Topaz (Jul 24 2020 at 22:35):

In math notation: finn:={xN  x<n} \operatorname{fin} n := \{ x \in \mathbb{N} \ | \ x < n \}

Kevin Buzzard (Jul 24 2020 at 22:35):

except that it's a type, not a set

Adam Topaz (Jul 24 2020 at 22:35):

yeah, in lean fin n := { x : \N // x < n }

Kevin Buzzard (Jul 24 2020 at 22:36):

so in set theory you have fin n \subseteq fin (n+1) but in Lean this doesn't even make sense because \subseteq is for (sub)sets

Kevin Buzzard (Jul 24 2020 at 22:38):

You can see why fin n isn't a sub-thing of fin (n+1) because to give a term of type fin n is to give a pair (i,h) with h a proof that i<n, and so now you don't have immediate access to a proof that i<(n+1), you'll have to make this proof, and that is the content of the canonical map from fin n to fin(n+1) (it's not "the identity" -- work needs to be done)

Patrick Thomas (Jul 24 2020 at 22:39):

I think I get it.

Patrick Thomas (Jul 24 2020 at 22:41):

Thank you.

Adam Topaz (Jul 24 2020 at 22:42):

I think it's a good exercise to write this definition. And here are some components which you'll need:

  1. fin.succ is the successor function fin n \to fin (n+1).
  2. You can just write 0 for the first element of fin (n+1)
  3. You can write fin.last n for the last element of fin (n+1).
  4. fin.cast_succ is the obvious inclusion fin n \to fin (n+1) that Kevin mentioned.

src#fin.last src#fin.succ src#fin.cast_succ

Patrick Thomas (Jul 24 2020 at 22:45):

This would be an inductive definition? Kevin mentioned that maybe an inductive definition might not be ideal?

Adam Topaz (Jul 24 2020 at 22:45):

No. This is if you want to follow Reid's suggestion.

Patrick Thomas (Jul 24 2020 at 22:59):

To be honest, I'm not sure I have a good idea of what form that definition would take. What would be the final type returned?

Patrick Thomas (Jul 24 2020 at 22:59):

The function?

Adam Topaz (Jul 24 2020 at 23:05):

You probably want a function with two real numbers a and b and the tuple as : fin (n+1) \to \R as inputs, and a Prop as the output. This should say that the as are the endpoints of the intervals of a partition of the interval with endpoints a and b.

Patrick Thomas (Jul 24 2020 at 23:08):

Would it also take a proof that x_{0} < x_{1} < ... x_{n} as an input?

Patrick Thomas (Jul 24 2020 at 23:09):

No, I guess that proof would be part of the returned Prop?

Dan Stanescu (Jul 24 2020 at 23:10):

I was rather thinking about a function that takes a, b and n as inputs and returns a tuple.
And the proof(s) that the points in the tuple are ordered, the first is a etc.

Adam Topaz (Jul 24 2020 at 23:11):

But there are many partitions of any given interval

Dan Stanescu (Jul 24 2020 at 23:11):

True.

Patrick Thomas (Jul 24 2020 at 23:14):

I can still say things like "Let P be a partition such that ||P|| < \delta" right? I just need to prove that one exists, probably by constructing it?

Scott Morrison (Jul 24 2020 at 23:23):

Dan Stanescu said:

A good place to ask, would Riemann integrals still have a place somewhere in mathlib now? Same for Dedekind cuts.

I would say yes.

Dan Stanescu (Jul 24 2020 at 23:25):

Patrick Thomas said:

I can still say things like "Let P be a partition such that ||P|| < \delta" right? I just need to prove that one exists, probably by constructing it?

In my view you could, but I'm not sure you could do that if you have a Prop. @Adam Topaz ?

Adam Topaz (Jul 24 2020 at 23:27):

You can use this prop to define a subtype, etc.

Dan Stanescu (Jul 24 2020 at 23:31):

Scott Morrison said:

Dan Stanescu said:

A good place to ask, would Riemann integrals still have a place somewhere in mathlib now? Same for Dedekind cuts.

I would say yes.

@Scott Morrison Where would you see them going to? The archive?

Scott Morrison (Jul 24 2020 at 23:32):

I think just a subdirectory called riemann_integral somewhere. Obviously it should have a thorough explanation in the module doc-strings that the rest of mathlib is build on top of more general constructions of integration.

Scott Morrison (Jul 24 2020 at 23:32):

Others may have other opinions on this, however.

Patrick Thomas (Jul 24 2020 at 23:33):

Would it just be:

def is_partition (a : ) (b : ) (n : ) (x : fin (n + 1)  ) :=
n > 0  x 0 = a  x n = b   m : , m < n  x m < x (m + 1)

Scott Morrison (Jul 24 2020 at 23:33):

We've got ZFC even though we're working in type theory, why not have Riemann integrals even though we're using Bochner? :-)

Patrick Thomas (Jul 24 2020 at 23:57):

How do you make a type out of a proposition?

Bryan Gin-ge Chen (Jul 24 2020 at 23:58):

Propositions are types. Proofs of a proposition are terms of that type.

Patrick Thomas (Jul 25 2020 at 00:03):

I guess I'm not sure how I say let P be a partition of [a, b] such that...

Adam Topaz (Jul 25 2020 at 00:06):

Is you define is_partition {n} (a b : \R) (as : fin (n+1) \to \R) then you would have some as with a proof of that prop.

Adam Topaz (Jul 25 2020 at 00:07):

And the "such that" depends on what "such that" actually is.

Adam Topaz (Jul 25 2020 at 00:08):

If "such that" is another prop, just include a proof of that prop as a variable

Reid Barton (Jul 25 2020 at 00:08):

I would make a structure partition (a b : ℝ) := ...

Mario Carneiro (Jul 25 2020 at 00:22):

Also, how would you ever formalize the theorem that the riemann integral is weaker than the lebesgue integral without a formalization of the former?

Mario Carneiro (Jul 25 2020 at 00:22):

Same deal with dedekind reals being isomorphic to cauchy reals

Mario Carneiro (Jul 25 2020 at 00:23):

Turing machines are already in mathlib for this exact reason - even though the "official" foundations use partial recursive functions, we need the definition of a TM in order to state and prove the equivalence

Patrick Thomas (Jul 25 2020 at 01:03):

Reid Barton said:

I would make a structure partition (a b : ℝ) := ...

I'm not sure I follow. Does the structure use the proposition?

Reid Barton (Jul 25 2020 at 01:08):

n, x, all the n > 0 etc. would be fields.

Patrick Thomas (Jul 25 2020 at 01:18):

I'm not sure I understand how a value of type partition would be guaranteed to be a partition. I'm looking through the documentation on structures here: https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html

Jalex Stark (Jul 25 2020 at 01:19):

your structure will be a bundle of data and propositions about that data

Jalex Stark (Jul 25 2020 at 01:20):

the subtype notation used in the definition of fin n is an example of a structure

Patrick Thomas (Jul 25 2020 at 01:21):

So one of the fields would be the is_partition proposition for example?

Jalex Stark (Jul 25 2020 at 01:21):

right, and if your proposition has an and in it, you probably want to break it into two fields

Jalex Stark (Jul 25 2020 at 01:23):

fin n is an example of a structure

Patrick Thomas (Jul 25 2020 at 01:24):

Can I then define a variable of type partition like I define a variable of type real, or do I have to always provide the fields?

Jalex Stark (Jul 25 2020 at 01:24):

it's morally equivalent (maybe literally defeq) to

structure fin (n : \N) :=
(val : \N)
(property : val < n)

Jalex Stark (Jul 25 2020 at 01:24):

I don't understand your question

Patrick Thomas (Jul 25 2020 at 01:25):

I can say "let P be a partition" without constructing one?

Jalex Stark (Jul 25 2020 at 01:26):

Yes, e.g. if you have structure partition (a b : ℝ) := ... then later you can say

lemma partition_eq_foo (a b : \R) (p : partition a b) : p = foo

Jalex Stark (Jul 25 2020 at 01:26):

partition has type \R \to \R \to Type

Patrick Thomas (Jul 25 2020 at 01:27):

Cool. Do I have to show that there is such a thing as a partition? That is, that the definition is not self contradicting?

Jalex Stark (Jul 25 2020 at 01:27):

no

Jalex Stark (Jul 25 2020 at 01:28):

you could define a partition and then prove

lemma partition_eq_foo (a b : \R) (p : partition a b) : false

Bryan Gin-ge Chen (Jul 25 2020 at 01:28):

(If you PR it to mathlib, the inhabited linter might want you to construct an instance.)

Jalex Stark (Jul 25 2020 at 01:29):

of course it is a good idea to construct an example as part of convincing yourself the definition is correct

Jalex Stark (Jul 25 2020 at 01:29):

you should also try to prove lemmas that are mathematically obvious

Patrick Thomas (Jul 25 2020 at 01:30):

Interesting.

Jalex Stark (Jul 25 2020 at 01:31):

this is the same as saying that you don't have to prove a proposition in order to talk about it

Jalex Stark (Jul 25 2020 at 01:32):

You can write def fermat : Prop := \ex a b c n, n > 2 \and a \ne 0 \and a ^ n = b^n + c^n

Patrick Thomas (Jul 25 2020 at 01:34):

Makes sense I guess.

Jalex Stark (Jul 25 2020 at 01:35):

a def is like a 0-field structure

Patrick Thomas (Jul 25 2020 at 01:48):

def is_partition (a : ) (b : ) (n : ) (x : fin (n + 1)  ) :=
n > 0  x 0 = a  x n = b   m : , m < n  x m < x (m + 1)

structure partition (a : ) (b : ) :=
(n : ) (x : fin (n + 1)  ) (h0 : is_partition a b n x)

Patrick Thomas (Jul 25 2020 at 01:50):

Or is it better to combine them into just the structure?

Bryan Gin-ge Chen (Jul 25 2020 at 01:52):

Depends if you anticipate using is_partition outside of defining partition instances.

Patrick Thomas (Jul 25 2020 at 01:54):

True.

Yury G. Kudryashov (Jul 25 2020 at 02:19):

I think about formalizing Riemann integral too. Still not sure what is the best way to deal with it.

Yury G. Kudryashov (Jul 25 2020 at 02:20):

E.g., should I support baf(x)dx=abf(x)dx\int_b^a f(x)\,dx=-\int_a^b f(x)\,dx right away, or start with abf(x)dx\int_a^b f(x)\,dx for aba\le b.

Yury G. Kudryashov (Jul 25 2020 at 02:22):

If I'll formalize this, then I'll formalize Henstock-Kurzweil and McShane integrals as well.

Yury G. Kudryashov (Jul 25 2020 at 02:23):

Right now I'm trying to make a usable interval_integral based on Bochner integration.

Yury G. Kudryashov (Jul 25 2020 at 02:54):

BTW, I think it's better to assume only non-strict inequalities on xix_i because this way your definition will work for a=ba=b.

Patrick Thomas (Jul 25 2020 at 02:58):

I wanted to try to do the exercises in the book, so I wanted to use the book's definition. Wouldn't that also lead to partitions like {5,5,5}?

Jalex Stark (Jul 25 2020 at 03:08):

what's wrong with the partition {5,5,5}?

Patrick Thomas (Jul 25 2020 at 03:09):

Just not intuitive to me I guess.

Jalex Stark (Jul 25 2020 at 03:09):

i don't think it's good to wed yourself to a definition written on paper. if it's in a book that means it's battle tested as a way to get humans to learn math

Jalex Stark (Jul 25 2020 at 03:10):

but you should optimize your definitions to make it easy to write lean code with

Patrick Thomas (Jul 25 2020 at 03:12):

Maybe. I'm doing this for pedagogy though.

Yury G. Kudryashov (Jul 25 2020 at 03:14):

{5, 5} in a partition will add nothing to the Riemann sum, so it changes nothing.

Yury G. Kudryashov (Jul 25 2020 at 03:15):

But with the space of partitions has better properties.

Yury G. Kudryashov (Jul 25 2020 at 03:15):

E.g., you can insert a point without caring whether it's already in your set.

Yury G. Kudryashov (Jul 25 2020 at 03:15):

And the space of partitions of a given size is compact (not sure if it's important)

Jalex Stark (Jul 25 2020 at 03:17):

Sorry, I didn't mean to be adversarial. When I say you "should" do something, I just mean that I think that's the easiest path to having code that works

Patrick Thomas (Jul 25 2020 at 03:17):

No, that's fine. I appreciate the input.

Yury G. Kudryashov (Jul 25 2020 at 03:18):

Also I have to remind myself every few messages that some people write Lean code for a reason different from "PR it to mathlib".

Patrick Thomas (Jul 25 2020 at 03:18):

:)

Patrick Thomas (Jul 25 2020 at 03:19):

No problem.

Kevin Buzzard (Jul 25 2020 at 08:24):

Patrick your is_partition definition is not right: the implications after the colon should be and's, or moved before the colon. A structure is a better idea. I agree that <= will be much easier to work with than <. The theorem statements will be much neater. You'll find that the book-writers just use < for psychological reasons rather than anything else. There's no harm in having rectangles of width 0. Do you have a candidate structure definition yet?

Kevin Buzzard (Jul 25 2020 at 08:26):

I don't think n>0 should be there either in is_partition, and your quantifiers over m in nat are bad because you can't evaluate x at m. Remember x eats a term of type fin n+1 so it needs to be fed a pair consisting of a natural and a proof.

Patrick Thomas (Jul 25 2020 at 18:32):

The n > 0 is there to ensure that there are at least two points in the partition, a and b.

"Remember x eats a term of type fin n+1 so it needs to be fed a pair consisting of a natural and a proof." Does that mean that x 0 = a and x n = b are also wrong? I was following the example from earlier in the thread and Lean didn't complain. What should it be?

Reid Barton (Jul 25 2020 at 18:33):

a and b should be parameters anyways since you will constantly want to quantify over partitions of [a,b][a, b].

Reid Barton (Jul 25 2020 at 18:33):

If aba \ne b then n>0n > 0 is forced anyways

Reid Barton (Jul 25 2020 at 18:34):

If a=ba = b then you might as well allow n=0n = 0 I suppose.

Patrick Thomas (Jul 25 2020 at 18:36):

So if I want to keep the strict inequality then I should force a < b instead?

Patrick Thomas (Jul 25 2020 at 18:36):

a and b are parameters aren't they?

Reid Barton (Jul 25 2020 at 18:36):

Surely you don't want to force a < b though? Isn't aaf(x)dx\int_a^a f(x) \, dx well-defined (as zero)?

Reid Barton (Jul 25 2020 at 18:37):

Apparently there's a coercion from nat to fin n--I didn't realize this

Reid Barton (Jul 25 2020 at 18:37):

not sure what it does on out of range inputs

Patrick Thomas (Jul 25 2020 at 18:38):

I guess it isn't defined in this book. Interesting point.

Patrick Thomas (Jul 25 2020 at 18:39):

What would it look like without the coercion? That is, what should x 0 be replaced with?

Reid Barton (Jul 25 2020 at 18:41):

x 0 doesn't need a coercion because fin m has a has_zero instance (I guess I don't know what happens for m = 0 but anyways it's not possible here).

Reid Barton (Jul 25 2020 at 18:42):

Otherwise, use library functions for fin--these were discussed above

Patrick Thomas (Jul 25 2020 at 19:04):

Like this?

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(h0 : x 0 = a)
(h1 : x (fin.last n) = b)
(h2 :  m : fin n, x m.cast_succ  x m.succ)

Yury G. Kudryashov (Jul 25 2020 at 20:46):

Note that this will work for aba \le b. Textbooks often say something like "we can deal with aba \ge b in the same way" but you can't do this in Lean. If you want to deal with 10f(x)dx\int_1^0 f(x)\,dx, then you have (at least) three options:

  1. Support this in your definition right away. E.g., say something like cmp (x m.cast_succ) (x m.succ) = cmp a b in h2.
  2. def integral f a b := if a ≤ b then integral_aux f a b else -integral_aux f b a.
  3. If integral_aux f a b = 0 whenever a ≥ b, then you can also use def integral f a b := integral_aux f a b - integral_aux f b a.

Yury G. Kudryashov (Jul 25 2020 at 20:46):

Currently I use option 3 to define interval_integral based on Lebesgue integral.

Yury G. Kudryashov (Jul 25 2020 at 20:47):

The main issue with option 2 is that you can't prove anything without by_cases hab : a ≤ b.

Yury G. Kudryashov (Jul 25 2020 at 20:52):

Option 1 gives you the correct definition right away but it's harder to prove lemmas along the way.

Reid Barton (Jul 25 2020 at 20:54):

I guess a fourth option is abf(x)dx=01f(a+(ba)t)(ba)dt\int_a^b f(x)\, dx = \int_0^1 f(a+(b-a)t)\,(b-a)dt. But it doesn't look too good for composing intervals.

Yury G. Kudryashov (Jul 25 2020 at 21:01):

And option 4' is to use a partition of [0,1][0, 1] in the definition of ab\int_a^b.

Patrick Thomas (Jul 25 2020 at 21:07):

I'm trying to define the norm of P that is $$max_{i \leq 1 \leq n) (x_{i} - x_{i-1})$$. As a starting point I have:

def norm (n : ) : (fin (n + 1)  )  
| ...

But then I don't know how to induct on the function.

Jalex Stark (Jul 25 2020 at 21:10):

I'd probably use finset.sup

Mario Carneiro (Jul 25 2020 at 21:13):

I used option 2 in metamath. You don't need to case split everything, in particular once you have additivity of endpoints you can mostly forget about this detail

Mario Carneiro (Jul 25 2020 at 21:15):

Actually I didn't have any integral_aux in option 2, it was just the lebesgue integral over Ioo a b

Mario Carneiro (Jul 25 2020 at 21:19):

It's actually pretty important to have this function for stating the FTC

Patrick Thomas (Jul 25 2020 at 22:20):

Jalex Stark said:

I'd probably use finset.sup

I'm not sure what you mean. Do you mean something like def norm : finset ℝ → ℝ := ...?

Jalex Stark (Jul 25 2020 at 22:48):

i mean that finset.sup reduces the problem to writing an appropriate function

foo : (fin (n + 1)  )  finset \R

and composing this with finset.sup

Yury G. Kudryashov (Jul 25 2020 at 23:51):

I'm trying option 3 with Lebesgue integral over Ico a b. This way you can use any measure, not only Lebesgue.

Patrick Thomas (Jul 26 2020 at 00:55):

finset: "This file builds the basic theory of finset α, modelled as a multiset α without duplicates."
Then "multiset α is the quotient of list α by list permutation. The result is a type of finite sets with duplicates allowed."
I'm lost at quotient of a list.

Patrick Thomas (Jul 26 2020 at 00:57):

Does defining foo not still require induction on the function?

Adam Topaz (Jul 26 2020 at 00:58):

A multiset is a set but where repetition is allowed. In lean, it is represented by a lists modulo an equivalence relation where two lists are considered equivalent if one is a permutation of the other.

Bryan Gin-ge Chen (Jul 26 2020 at 00:58):

Quotient types are definitely a bit tricky. They're not explained until almost the very end of TPiL: https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients

@Kevin Buzzard wrote a tutorial that demonstrates quotients in Lean here: https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean

Reid Barton (Jul 26 2020 at 00:58):

These are just implementation details.

Adam Topaz (Jul 26 2020 at 00:59):

Yeah, in practice you don't need to worry about how things are implemented

Adam Topaz (Jul 26 2020 at 00:59):

As long as you know how to find/use the appropriate stuff in mathlib

Bryan Gin-ge Chen (Jul 26 2020 at 00:59):

I think that's still more "in theory" than "in practice", though things are getting better all the time.

Scott Morrison (Jul 26 2020 at 01:01):

Let's make lots more things @[irreducible]! :-)

Patrick Thomas (Jul 26 2020 at 01:21):

I can think of something like this, but replacing nat with fin n + 1, but this has a natural number to induct on (and it doesn't compile) (or terminate):

def norm (x :   ) :   
| n := max (x (n + 1) - x n) (norm (n + 1))

Reid Barton (Jul 26 2020 at 01:31):

Well, this type already doesn't make much sense because what are the finite number of things you want to take the max of?

Reid Barton (Jul 26 2020 at 01:32):

oh is that supposed to be the second argument?

Patrick Thomas (Jul 26 2020 at 01:32):

That it doesn't terminate. Yeah :)

Reid Barton (Jul 26 2020 at 01:34):

In general my advice is not to use induction for normal math

Reid Barton (Jul 26 2020 at 01:34):

I'm not sure what your goals are though.

Reid Barton (Jul 26 2020 at 01:35):

If you make a brand new recursive definition here, then you will have to prove all the lemmas about it by induction yourself.

Reid Barton (Jul 26 2020 at 01:35):

Maybe that's actually what you prefer though, I don't know.

Patrick Thomas (Jul 26 2020 at 01:35):

I'm happy not to use induction, it's confusing. I'm just not sure how to do it otherwise.

Reid Barton (Jul 26 2020 at 01:37):

The best advice I have is to just read the parts of the library that seem relevant, like data.finset. Maybe someone else has something more specific to suggest.

Patrick Thomas (Jul 26 2020 at 01:38):

How do you define a function on something that has a domain of the functions of type fin n + 1 to real?

Adam Topaz (Jul 26 2020 at 01:40):

If I had to guess, there is probably something in mathlib that gives you a finset \R that's the image of a map fin (n+1) \to \R, and something that gives you the max of a finset \R.

Patrick Thomas (Jul 26 2020 at 01:43):

So, in general, I got the impression that just about everything in a functional programming language is done by some form of recursion?

Jalex Stark (Jul 26 2020 at 01:44):

if you want to implement these things from scratch, you'll use recursion. If you just compose functions that are already available, you can avoid it.

Scott Morrison (Jul 26 2020 at 01:47):

But why reimplement everything from scratch? I think in your statement "everything" only means "all elementary exercises when learning a functional programming language". :-)

Yury G. Kudryashov (Jul 26 2020 at 01:48):

You can use (finset.univ : finset (fin n)).sup (λ j, (⟨x j.cast_succ - x j.succ, _⟩ : nnreal))

Yury G. Kudryashov (Jul 26 2020 at 01:48):

Or ⨆ i : fin n, x i.cast_succ - x i.succ

Patrick Thomas (Jul 26 2020 at 01:49):

What is the first symbol in the second one?

Patrick Thomas (Jul 26 2020 at 01:51):

The one that looks like a square U.

Adam Topaz (Jul 26 2020 at 01:53):

That's notation for max, essentially. You can copy and paste that into vscode, and hover over it to see what it is notation for. Maybe even control-click to jump to defn?

Yury G. Kudryashov (Jul 26 2020 at 01:59):

⨆ i, f i is mathlib notation for Sup (range f).

Yury G. Kudryashov (Jul 26 2020 at 02:01):

The relevant instance for reals is conditionally_complete_linear_order, and most theorems about will have csupr in their name, and assume [nonempty α] and/or bdd_above (range f), where f : α → real.

Yury G. Kudryashov (Jul 26 2020 at 02:01):

For empty or unbounded sets Sup is defined to be 0.

Yury G. Kudryashov (Jul 26 2020 at 02:02):

In most cases it doesn't matter which garbage value do we use for Sup empty but this way a few theorems don't need bdd_above/nonempty assumption.

Patrick Thomas (Jul 26 2020 at 02:04):

I didn't know about the control click.

Yury G. Kudryashov (Jul 26 2020 at 02:05):

We have both docs#finset.sup and docs#finset.max

Patrick Thomas (Jul 26 2020 at 02:06):

So def norm' (n : ℕ) (x : fin (n + 1) → ℝ) := ⨆ i : fin n, x i.cast_succ - x i.succ?
This gives me: definition 'norm'' is noncomputable, it depends on 'real.lattice.conditionally_complete_linear_order'

Yury G. Kudryashov (Jul 26 2020 at 02:07):

They have slightly different assumptions. E.g., sup takes a function as an argument, and for max you need to use map or image. Also sup assumes that there exists a minimal element of the type (bot) and max returns none for an empty finset and some x for a non-empty finset.

Yury G. Kudryashov (Jul 26 2020 at 02:07):

Try noncomputable theory at the top of your file.

Yury G. Kudryashov (Jul 26 2020 at 02:08):

Most probably you don't want to try developing computable integrals. E.g., because real numbers are noncomputable in Lean.

Patrick Thomas (Jul 26 2020 at 02:10):

Yes, that fixed it.
So I thought that if i is of type fin n, then i.cast_succ gives back i of type fin n + 1 and i.succ gives back i + 1 of type fin n + 1?

Yury G. Kudryashov (Jul 26 2020 at 02:11):

The "supremum" part is noncomputable.

Patrick Thomas (Jul 26 2020 at 02:17):

(deleted)

Patrick Thomas (Jul 26 2020 at 02:19):

The definition of norm above seems to be the other way around?

Patrick Thomas (Jul 26 2020 at 02:54):

So is x i.cast_succ - x i.succ the function passed to Sup (range f)? And i iterates over the domain of that function?

Yury G. Kudryashov (Jul 26 2020 at 03:02):

Yes. More precisely, the function λ i : fin n, x i.cast_succ - x i.succ is passed to Sup (range f).

Patrick Thomas (Jul 26 2020 at 03:12):

Cool. Am I misunderstanding the definition of cast_succ and succ? I'm guessing probably.

Adam Topaz (Jul 26 2020 at 03:14):

cast_succ is just the "obvious" inclusion from fin n to fin (n+1), while succ is the successor. So when you write x i.cast_succ - x i.succ it means, mathematically, xixi+1x_i - x_{i+1}.

Adam Topaz (Jul 26 2020 at 03:15):

You probably want i.succ - i.cast_succ

Patrick Thomas (Jul 26 2020 at 03:15):

That was what I was wondering.

Patrick Thomas (Jul 26 2020 at 03:17):

Thank you.

Adam Topaz (Jul 26 2020 at 03:17):

No problem!

Patrick Thomas (Jul 26 2020 at 03:53):

In summary:

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(h0 : x 0 = a)
(h1 : x (fin.last n) = b)
(h2 :  m : fin n, x m.cast_succ  x m.succ)

def partition_norm (a : ) (b : ) (P : partition a b) : 
:=  i : fin P.n, P.x i.succ - P.x i.cast_succ

Adam Topaz (Jul 26 2020 at 03:55):

Looks good. You can make the a and b implicit in partition_norm since they can be inferred from the type of P. You can also give the fields in partition some more descriptive names.

Patrick Thomas (Jul 26 2020 at 03:56):

Cool.

Adam Topaz (Jul 26 2020 at 03:57):

If you make a and b implicit in partition_norm, and P is a partition (for some a and b) you would be able to just write partition_norm P for the norm of P.

Patrick Thomas (Jul 26 2020 at 03:58):

Sounds good.

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(h0 : x 0 = a)
(h1 : x (fin.last n) = b)
(h2 :  m : fin n, x m.cast_succ  x m.succ)

def partition_norm {a : } {b : } (P : partition a b) : 
:=  i : fin P.n, P.x i.succ - P.x i.cast_succ

Adam Topaz (Jul 26 2020 at 03:59):

And if you're really up to it, look up how to write custom notation, so you can actually write something like P||P||

Patrick Thomas (Jul 26 2020 at 04:01):

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(h0 : x 0 = a)
(h1 : x (fin.last n) = b)
(h2 :  m : fin n, x m.cast_succ  x m.succ)

def partition_norm {a : } {b : } (P : partition a b) : 
:=  i : fin P.n, P.x i.succ - P.x i.cast_succ

notation `||`P`||` := partition_norm P

Adam Topaz (Jul 26 2020 at 04:04):

Alternatively, you can do something like this:

namespace partition
def norm {a b : \R} (P : partition a b) : \R := ...
end partition

which will allow you to write P.norm instead of partition.norm P.

Patrick Thomas (Jul 26 2020 at 04:05):

Good idea.

Adam Topaz (Jul 26 2020 at 04:06):

One thing to keep in mind when defining notation is the precedence levels.

Patrick Thomas (Jul 26 2020 at 04:08):

I might wait and look into that latter.

Patrick Thomas (Jul 26 2020 at 04:08):

I need to move on to Riemann sums :)

Patrick Thomas (Jul 26 2020 at 04:35):

For each i=1,,ni = 1, \ldots, n, let xix_{i}* be an arbitrary point in the interval [xi1,xi][x_{i-1}, x_{i}]:

structure needs_a_name {a : } {b : } (P : partition a b) (x : fin P.n  ) :=
(h0 :  m : fin P.n, (P.x m.cast_succ  x m)  (x m  P.x m.succ))

?

Yury G. Kudryashov (Jul 26 2020 at 07:20):

I'd extend the original structure adding fields x and x_mem_Icc

Kevin Buzzard (Jul 26 2020 at 07:50):

Cool. Am I misunderstanding the definition of cast_succ and succ? I'm guessing probably.

@Patrick Thomas you do know that you can just hover over a definition and see its docstring, and if it hasn't got one then you can right click on it and peek its definition, right? If you don't understand the definitions of cast_succ and succas written in the source code then you should probably figure them out because you're going to have to get used tofin m at some point. A term of type fin m is a pair, consisting of a natural i and a proof that i<m. That's all you need to know.

Kevin Buzzard (Jul 26 2020 at 07:53):

But in general you should be able to get away with not reading definitions, and hoping that the stuff in the source code just after the definition is the interface you'll need.

Kevin Buzzard (Jul 26 2020 at 08:14):

Patrick Thomas said:

So if I want to keep the strict inequality then I should force a < b instead?

Re this: if you don't need that inequality, and in most places you don't, then you should go rogue and generalize the book when making the definition (as you did), and just insert it into the lemmas which actually need it. You'll probably be surprised to find that essentially no lemmas need it, and the authors just put this assumption in for psychological reasons. There is a big disadvantage in putting in a random assumption 0<n which is almost never needed: then every proof by induction on n, you'll have to do a fake base case, where the result is probably trivially true but the hypotheses are false anyway, and then an actual base case n=1, where the result is true but a bit less trivially, and would follow from the inductive hypothesis and the case n=0 apart from the fact that you didn't prove the n=0 case because you made the mistake of copying from the book so you can't use the n=0 case, and then an inductive step which will be the same.

Re finset: if you're reading the definition finset you're doing the wrong thing. finset X is the type of finite subsets of X. This is what you need to know. If you want to learn more about how to use finset then go to data.finset.basic and read (only) the statements of the lemmas. Skip the first 100-200 lines because they might be messy ones you'll never need, and then start reading from there and you'll see that the lemmas are a bunch of basic mathematical results about finite sets all of which have incomprehensible proofs which you don't need to worry about, because you are not making the finset API, you are just going to use it, and it's very thorough. This is all moot because it looks like you're not going to use it anyway.

Finally, getting the definitions right is hard. Once the definitions are there, you can start proving theorems, and it doesn't matter how messy your proofs are because they are compiled and then forgotten. But definitions you have to implement them in such a way that they are usable in practice, and it's hard for an inexperienced Lean user to set these things up. You should make a little project github repo (usnig leanproject new) with just one file in src for now, so you can point people to your definitions more easily. This set-up is easier to work with than one random file on your computer. partition and partition_norm are looking good but as Adam says it should be called partition.norm, and your h0, h1, h2` hypotheses have lousy names -- what are you -- a mathematician? Give things descriptive names. Here's what Yury means:

import data.real.basic data.set.intervals

noncomputable theory

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

namespace partition

def norm {a b : } (P : partition a b) : 
:=  i : fin P.n, P.x i.succ - P.x i.cast_succ

notation `||`P`||` := P.norm

end partition

open set

structure pointed_partition (a b : ) extends partition a b :=
(y : fin n  )
(mem_block :  m : fin n, y m  Icc (x m.cast_succ) (x m.succ))

Calling something xx and then something else xx^* doesn't sound like a great idea to me. I called it y.

Patrick Thomas (Jul 26 2020 at 20:20):

Thank you. Do you have any advice for finding the things I need in mathlib? For example, I'm sure there must be a function in mathlib that allows me to easily take the sum over the range of the function on fin n, but I don't know of an easy way to find it.

Mario Carneiro (Jul 26 2020 at 20:33):

Yury G. Kudryashov said:

You can use (finset.univ : finset (fin n)).sup (λ j, (⟨x j.cast_succ - x j.succ, _⟩ : nnreal))
Or ⨆ i : fin n, x i.cast_succ - x i.succ

Patrick Thomas (Jul 26 2020 at 20:35):

That takes the max, not the sum right?

Kevin Buzzard (Jul 26 2020 at 20:35):

Hint: it's going to be called finset.sum

Kevin Buzzard (Jul 26 2020 at 20:37):

You could do worse than read through data.finset.basic just looking at the statements of the theorems, and reading docstrings of definitions. This will give you a feeling for what's there

Patrick Thomas (Jul 26 2020 at 20:38):

Alright.

Jalex Stark (Jul 26 2020 at 20:39):

you might prefer looking at it in the web browser
https://leanprover-community.github.io/mathlib_docs/

Jalex Stark (Jul 26 2020 at 20:39):

this will automatically hide the proofs and emphasize docstrings

Jalex Stark (Jul 26 2020 at 20:40):

reading mathlib_docs directly is kind of like reading a book where all the proofs are exercises

Patrick Thomas (Jul 26 2020 at 20:40):

Thanks. I didn't use finset earlier, is this a suggestion that I should have?

Jalex Stark (Jul 26 2020 at 20:40):

i don't know what you should do

Jalex Stark (Jul 26 2020 at 20:41):

if your goal is to get code reasonably quickly that expresses the mathematics you were talking about before, you should aim to take advantage of existing libraries

Patrick Thomas (Jul 26 2020 at 20:41):

I guess that was directed to Kevin, when he said it is called finset.sum.

Jalex Stark (Jul 26 2020 at 20:43):

i think a literal interpretation of his words would say that kevin suggests that you find some lemma in the library called finset.sum or similar, literally read the statement, and try to figure out whether it applies to your situation

Kevin Buzzard (Jul 26 2020 at 20:43):

The reason I'd go for finset.sum is that the API for it is much better developed than for the other sums, or at least that was true in the past when I wanted to do finite sums

Patrick Thomas (Jul 26 2020 at 20:44):

I see.

Kevin Buzzard (Jul 26 2020 at 20:44):

You can use finset.univ to make your finite subset of fin n

Kevin Buzzard (Jul 26 2020 at 20:45):

And if you read the relevant part of the finset API (and Jalex is right, you'd be much better off reading the docs than the source code) then you'd see it in action and also what the basic lemmas are

Anatole Dedecker (Jul 26 2020 at 20:46):

Kevin Buzzard said:

The reason I'd go for finset.sum is that the API for it is much better developed than for the other sums, or at least that was true in the past when I wanted to do finite sums

And it has a nice notation too

Kevin Buzzard (Jul 26 2020 at 20:46):

Which hopefully you'll see in the docs. Is it used there?

Anatole Dedecker (Jul 26 2020 at 20:49):

https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html

Kevin Buzzard (Jul 26 2020 at 20:49):

https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html#finset.sum

Kevin Buzzard (Jul 26 2020 at 20:50):

Start there and go down and hopefully you'll see enough to figure how to use this stuff

Bryan Gin-ge Chen (Jul 26 2020 at 20:52):

#mil should cover all this too, eventually.

Patrick Thomas (Jul 27 2020 at 04:03):

I wonder if it would be helpful to have examples of use in the mathlib documentation. It might help me.

Bryan Gin-ge Chen (Jul 27 2020 at 04:07):

Yes, I would support that. There are some usage examples in the docstrings in data.list.defs, but very few elsewhere. Contributions are welcome!

Patrick Thomas (Jul 27 2020 at 04:08):

I would contribute if I knew how to use them. :)

Bryan Gin-ge Chen (Jul 27 2020 at 04:12):

You can search mathlib itself for usage examples, sometimes that helps. But of course, questions here are always welcome too!

Patrick Thomas (Jul 31 2020 at 01:26):

This compiles:

def riemann_sum (a b : ) (P : pointed_partition a b) (f :   ) : 
:= (finset.univ : finset (fin P.n)).sum (λ i, f (P.y i) * (P.x i.succ - P.x i.cast_succ))

I'm not sure I understand what finset.univ does.

If I try this:

def riemann_sum (a b : ) (P : pointed_partition a b) (f :   ) : 
:= 

then I get 'unexpected token' for the summation symbol. I have tried various imports, but have not found one that fixes it.

Alex J. Best (Jul 31 2020 at 01:32):

Did you try open_locale big_operators?

Patrick Thomas (Jul 31 2020 at 01:35):

If I put that in front of the definition then I get a command expected error. Entire file:

import data.real.basic data.set.intervals data.finset algebra.big_operators

noncomputable theory

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

namespace partition

def norm {a b : } (P : partition a b) : 
-- := ⨆ i : fin P.n, P.x i.succ - P.x i.cast_succ
:= (finset.univ : finset (fin P.n)).sup (λ j, (P.x j.cast_succ - P.x j.succ))

notation `||`P`||` := P.norm

end partition

open set

structure pointed_partition (a b : ) extends partition a b :=
(y : fin n  )
(mem_block :  m : fin n, y m  Icc (x m.cast_succ) (x m.succ))

/-
def riemann_sum (a b : ℝ) (P : pointed_partition a b) (f : ℝ → ℝ) : ℝ
:= (finset.univ : finset (fin P.n)).sum (λ i, f (P.y i) * (P.x i.succ - P.x i.cast_succ))
-/

open_locale big_operators

def riemann_sum (a b : ) (P : pointed_partition a b) (f :   ) : 
:= 

Jalex Stark (Jul 31 2020 at 02:22):

the first error in the file is significantly before the definition of riemann sum

Alex J. Best (Jul 31 2020 at 02:35):

Yeah the notation for Sum needs some arguments after it.

Alex J. Best (Jul 31 2020 at 02:48):

So this should be what you want i think:

def riemann_sum (a b : ) (P : pointed_partition a b) (f :   ) : 
:=  n, f (P.y n) * (P.x n.succ - P.x n.cast_succ)

Patrick Thomas (Jul 31 2020 at 03:29):

Jalex Stark said:

the first error in the file is significantly before the definition of riemann sum

Yeah, it was fine in Visual Studio Code, but when I pasted it into the lean web page it gave a bunch of errors. I'm updating my OS, etc. now.

Alex J. Best (Jul 31 2020 at 03:38):

I think I had to add the import data.fintype.basic to makee it work on my mathlib

Patrick Thomas (Jul 31 2020 at 03:41):

In the web editor I get file 'data/fintype/basic' not found in the LEAN_PATH.

Alex J. Best (Jul 31 2020 at 03:43):

https://leanprover-community.github.io/lean-web-editor/#code=import%20data.real.basic%20data.set.intervals%20data.finset%20algebra.big_operators%20data.fintype.basic%0A%0Anoncomputable%20theory%0A%0Astructure%20partition%20%28a%20%3A%20%E2%84%9D%29%20%28b%20%3A%20%E2%84%9D%29%20%3A%3D%0A%28n%20%3A%20%E2%84%95%29%0A%28x%20%3A%20fin%20%28n%20%2B%201%29%20%E2%86%92%20%E2%84%9D%29%0A%28x_zero%20%3A%20x%200%20%3D%20a%29%0A%28x_last%20%3A%20x%20%28fin.last%20n%29%20%3D%20b%29%0A%28mono%20%3A%20%E2%88%80%20m%20%3A%20fin%20n%2C%20x%20m.cast_succ%20%E2%89%A4%20x%20m.succ%29%0A%0Anamespace%20partition%0A%0Adef%20norm%20%7Ba%20b%20%3A%20%E2%84%9D%7D%20%28P%20%3A%20partition%20a%20b%29%20%3A%20%E2%84%9D%0A--%20%3A%3D%20%E2%A8%86%20i%20%3A%20fin%20P.n%2C%20P.x%20i.succ%20-%20P.x%20i.cast_succ%0A%3A%3D%20%28finset.univ%20%3A%20finset%20%28fin%20P.n%29%29.sup%20%28%CE%BB%20j%2C%20%28P.x%20j.cast_succ%20-%20P.x%20j.succ%29%29%0A%0Anotation%20%60%7C%7C%60P%60%7C%7C%60%20%3A%3D%20P.norm%0A%0Aend%20partition%0A%0Aopen%20set%0A%0Astructure%20pointed_partition%20%28a%20b%20%3A%20%E2%84%9D%29%20extends%20partition%20a%20b%20%3A%3D%0A%28y%20%3A%20fin%20n%20%E2%86%92%20%E2%84%9D%29%0A%28mem_block%20%3A%20%E2%88%80%20m%20%3A%20fin%20n%2C%20y%20m%20%E2%88%88%20Icc%20%28x%20m.cast_succ%29%20%28x%20m.succ%29%29%0A%0Ainstance%20%28a%20b%20%3A%20%E2%84%9D%29%20%3A%20has_coe_to_fun%20%28pointed_partition%20a%20b%29%20%3A%3D%20%E2%9F%A8_%2C%20%CE%BB%20c%2C%20c.y%E2%9F%A9%0A%0A%2F-%0Adef%20riemann_sum%20%28a%20b%20%3A%20%E2%84%9D%29%20%28P%20%3A%20pointed_partition%20a%20b%29%20%28f%20%3A%20%E2%84%9D%20%E2%86%92%20%E2%84%9D%29%20%3A%20%E2%84%9D%0A%3A%3D%20%28finset.univ%20%3A%20finset%20%28fin%20P.n%29%29.sum%20%28%CE%BB%20i%2C%20f%20%28P.y%20i%29%20*%20%28P.x%20i.succ%20-%20P.x%20i.cast_succ%29%29%0A-%2F%0A%0Aopen_locale%20big_operators%0A%0Adef%20riemann_sum%20%28a%20b%20%3A%20%E2%84%9D%29%20%28P%20%3A%20pointed_partition%20a%20b%29%20%28f%20%3A%20%E2%84%9D%20%E2%86%92%20%E2%84%9D%29%20%3A%20%E2%84%9D%0A%3A%3D%20%E2%88%91%20n%2C%20f%20%28P%20n%29%20*%20%28P.x%20n.succ%20-%20P.x%20n.cast_succ%29%0A%0A%23print%20riemann_sum

Alex J. Best (Jul 31 2020 at 03:44):

works fine for me except it doesn't like your definition of norm, as it needs a bottom element for when the set is empty

Alex J. Best (Jul 31 2020 at 03:46):

A possible solution is to make (P.x j.cast_succ - P.x j.succ) land in nnreal so that the bottom element is 0.

Patrick Thomas (Jul 31 2020 at 03:46):

Huh, that is a different web editor than the one I was using. I get a failed to synthesize error on this line := (finset.univ : finset (fin P.n)).sup (λ j, (P.x j.cast_succ - P.x j.succ)) in that.

Alex J. Best (Jul 31 2020 at 03:48):

Yeah always use the community web editor!

Alex J. Best (Jul 31 2020 at 03:49):

And yes that's the error I'm talking about, if you want to take sup over a set the Type the set is valued in needs to have an infimum or bottom element so that if you take the sup of the empty set you get a decent value back.

Patrick Thomas (Jul 31 2020 at 03:56):

So I need a case for when (finset.univ : finset (fin P.n)) is empty?

Alex J. Best (Jul 31 2020 at 04:00):

Yeah or you can use max instead of sup, which returns none if the input is empty, so your norm would land in option real instead of real. But I think the nnreal way is nicer.

Alex J. Best (Jul 31 2020 at 04:03):

Actually I just tried to do this and noticed that your norm is negatively valued!

Alex J. Best (Jul 31 2020 at 04:05):

I guess that's not intentional so I switched it to this

import data.real.basic data.set.intervals data.finset algebra.big_operators data.fintype.basic data.real.nnreal

noncomputable theory

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

namespace partition
open_locale nnreal

def norm {a b : } (P : partition a b) : 0
-- := ⨆ i : fin P.n, P.x i.succ - P.x i.cast_succ
:= (finset.univ : finset (fin P.n)).sup (λ j, P.x j.succ - P.x j.cast_succ, by linarith [mono P j])

notation `||`P`||` := P.norm

end partition

open set

structure pointed_partition (a b : ) extends partition a b :=
(y : fin n  )
(mem_block :  m : fin n, y m  Icc (x m.cast_succ) (x m.succ))

instance (a b : ) : has_coe_to_fun (pointed_partition a b) := ⟨_, λ c, c.y

/-
def riemann_sum (a b : ℝ) (P : pointed_partition a b) (f : ℝ → ℝ) : ℝ
:= (finset.univ : finset (fin P.n)).sum (λ i, f (P.y i) * (P.x i.succ - P.x i.cast_succ))
-/

open_locale big_operators

def riemann_sum (a b : ) (P : pointed_partition a b) (f :   ) : 
:=  n, f (P n) * (P.x n.succ - P.x n.cast_succ)

#print riemann_sum

Patrick Thomas (Jul 31 2020 at 04:10):

There is a proof in the definition?

Alex J. Best (Jul 31 2020 at 04:12):

Yep, to give an element of the nonnegative reals (ℝ≥0) we give an element of and a proof that it is nonnegative, as this is defined as a subtype in lean.

Patrick Thomas (Jul 31 2020 at 04:15):

I see.

Patrick Thomas (Jul 31 2020 at 04:33):

Why does making it nnreal satisfy the need for an empty case?

Patrick Thomas (Jul 31 2020 at 04:34):

Because the nnreal are bounded below and hence have a sup?

Patrick Thomas (Jul 31 2020 at 04:34):

Actually an inf right?

Alex J. Best (Jul 31 2020 at 04:35):

Yeah exactly, because nnreal has a smallest element (0) so that when you give an empty set the supremum has something sensible to be. You would want reals with a negative infinity if you really wanted values in reals, but as your terms are all positive this seemed cleaner

Patrick Thomas (Jul 31 2020 at 04:37):

So the sup of an empty subset of the nnreals is 0?

Patrick Thomas (Jul 31 2020 at 04:37):

Is that by convention?

Patrick Thomas (Jul 31 2020 at 04:42):

No, I guess that makes sense. Every nnreal is an upper bound, so the least of those is 0.

Patrick Thomas (Aug 01 2020 at 23:00):

As an aside, does this make sense? Is using structures like this a reasonable way to define the upper bound and the least upper bound?

import data.real.basic

structure ub (S : set ) :=
(t : )
(is_ub : Prop :=  s  S, s  t)

structure lub (S : set ) extends ub S :=
(is_lub : Prop :=  r : , r < t  not is_ub)

Reid Barton (Aug 01 2020 at 23:02):

You mean

import data.real.basic

structure ub (S : set ) :=
(t : )
(is_ub :  s  S, s  t)

& similarly for lub

Patrick Thomas (Aug 01 2020 at 23:04):

If I take out the Prop it seems to break the use of is_ub in the definition of lub.

Reid Barton (Aug 01 2020 at 23:04):

oh yes, I didn't notice that part is separately wrong.

Patrick Thomas (Aug 01 2020 at 23:05):

What did I do wrong?

Reid Barton (Aug 01 2020 at 23:05):

It just doesn't make any sense.

Reid Barton (Aug 01 2020 at 23:05):

:= is for default values, it's rarely useful.

Reid Barton (Aug 01 2020 at 23:05):

You need to replace it with what it means to be a least upper bound

Patrick Thomas (Aug 01 2020 at 23:06):

So I want to say that the ub and the lub are real numbers. That is done by the t : \real right?

Reid Barton (Aug 01 2020 at 23:07):

In ub you're saying (with the corrected version) that an upper bound of a set S is a real number t such that ∀ s ∈ S, s ≤ t.

Reid Barton (Aug 01 2020 at 23:07):

Which is right.

Reid Barton (Aug 01 2020 at 23:08):

The original said that an upper bound is any real number t together with any proposition which, if you don't supply it, defaults to ∀ s ∈ S, s ≤ t.

Patrick Thomas (Aug 01 2020 at 23:09):

I see. Ok. So now I'm not sure how to make use of the is_ub in the lub. I tried not is_ub r, but that doesn't seem to work.

Reid Barton (Aug 01 2020 at 23:09):

You don't need to make use of it

Patrick Thomas (Aug 01 2020 at 23:09):

True. I thought it might be easier to read though.

Reid Barton (Aug 01 2020 at 23:09):

Maybe start with the definition in math?

Reid Barton (Aug 01 2020 at 23:10):

(you also can't use it in any sensible way)

Reid Barton (Aug 01 2020 at 23:10):

I mean, since the structure already contains the field is_ub you don't need to repeat the fact that it is an upper bound in the fact that it is a least upper bound, I guess.

Patrick Thomas (Aug 01 2020 at 23:12):

That isn't how I wanted to use it. I can write:

import data.real.basic

structure ub (S : set ) :=
(t : )
(is_ub :  s  S, s  t)

structure lub (S : set ) extends ub S :=
(is_lub :  r : , r < t  ¬ ( s  S, s  r))

but the last part is just stating that r is not an ub.

Patrick Thomas (Aug 01 2020 at 23:12):

ub of S that is.

Reid Barton (Aug 01 2020 at 23:15):

These extra ¬s are a little awkward (normal definition would be that if r is another upper bound, then t <= r) but that works.

Reid Barton (Aug 01 2020 at 23:15):

You could also reuse the whole structure ub

Patrick Thomas (Aug 01 2020 at 23:16):

What do you mean by reuse the whole structure ub?

Reid Barton (Aug 01 2020 at 23:20):

Quantify over all ub S in the type of is_lub, rather than writing out the two hypotheses separately

Reid Barton (Aug 01 2020 at 23:21):

Also, you might not really want a structure in the first place.

Reid Barton (Aug 01 2020 at 23:22):

mathlib style is more like def is_ub (S : set \R) (t : \R) : Prop := \all s \in S, s \le t and def is_lub (S : set \R) (t : \R) : Prop := ... (can use is_ub).

Patrick Thomas (Aug 01 2020 at 23:23):

I thought it might make things cleaner to say r : ub S, then both r : real and is_ub r S. It would look closer to proofs on paper.

Patrick Thomas (Aug 01 2020 at 23:24):

If I try to do:

import data.real.basic

structure ub (S : set ) :=
(t : )
(is_ub :  s  S, s  t)

structure lub (S : set ) extends ub S :=
--(is_lub : ∀ r : ℝ, r < t → ¬ (∀ s ∈ S, s ≤ r))
(is_lub :  r : ub S, t  r)

I get an error on the last leq.

Kenny Lau (Aug 01 2020 at 23:25):

abomination incoming:

import data.real.basic

structure ub (S : set ) :=
(t : )
(is_ub : Prop :=  s  S, s  t)
(t_is_ub : is_ub)

structure lub (S : set ) extends ub S :=
(is_lub : Prop :=  r : , r < t  not is_ub)
(t_is_lub : is_lub)

Reid Barton (Aug 01 2020 at 23:25):

that's because r : ub S and not r : \R

Kenny Lau (Aug 01 2020 at 23:25):

you would have to write r.t instead

Patrick Thomas (Aug 01 2020 at 23:26):

What does r.t mean?

Reid Barton (Aug 01 2020 at 23:26):

ub.t r

Reid Barton (Aug 01 2020 at 23:26):

i.e. the t field

Patrick Thomas (Aug 01 2020 at 23:26):

Oh.

Kenny Lau (Aug 01 2020 at 23:27):

#tpil

Kenny Lau (Aug 01 2020 at 23:27):

Ch. 9

Reid Barton (Aug 01 2020 at 23:28):

I don't really think the bundled structure is more like informal math. The big difference from informal math is in Lean you're generally forced to refer to statements you know (like "r is an upper bound of S") explicitly somehow--whether that statement is called r.is_ub or h, you still have to name it.

Reid Barton (Aug 01 2020 at 23:30):

The disadvantage of the structure is that it forces you to introduce both r and the hypothesis that it is the (least) upper bound of something simultaneously--if you already had an r you were interested in then you have to jump through extra hoops to just state that it is an upper bound.

Patrick Thomas (Aug 01 2020 at 23:30):

Why was it better to use a structure for the definition of a partition instead of saying is_partition?

Reid Barton (Aug 01 2020 at 23:31):

It's not necessarily better or worse

Reid Barton (Aug 01 2020 at 23:31):

just different

Reid Barton (Aug 01 2020 at 23:32):

But, it's probably not as frequent in math that you have a random collection of subsets of a set lying around and you want to talk about whether or not it is a partition

Reid Barton (Aug 01 2020 at 23:32):

but it does seem quite likely that you would have a random real number lying around and want to talk about whether or not it is an upper bound

Reid Barton (Aug 01 2020 at 23:33):

For example with the structure ub alone it's quite awkward to express "t is not an upper bound of S"

Patrick Thomas (Aug 01 2020 at 23:33):

I see.

Reid Barton (Aug 01 2020 at 23:34):

And somehow, talking about something not being an upper bound feels plausible in a way that talking about something not being a partition does not

Kenny Lau (Aug 01 2020 at 23:35):

I believe the correct answer is "you'll know which implementation is better as you go on proving things about it"

Kenny Lau (Aug 01 2020 at 23:36):

you want to say, if s is an LUB of A and t of B then s+t of A+B

Kenny Lau (Aug 01 2020 at 23:36):

which means the implementation without structure is better

Patrick Thomas (Aug 01 2020 at 23:39):

Alright. Just out of pure curiosity, is there a way to replace the ¬ ∀ s ∈ S, s ≤ t with the simpler statement that r is not an ub as previously defined?

import data.real.basic

-- upper bound
structure ub (S : set ) :=
(t : )
(is_ub :  s  S, s  t)

-- least upper bound
structure lub (S : set ) extends ub S :=
(is_lub :  r : , r < t  ¬  s  S, s  r)

Patrick Thomas (Aug 01 2020 at 23:42):

I imagine a similar question might come up in the definition of something else as a structure that makes more sense.

Reid Barton (Aug 01 2020 at 23:43):

you can say "there does not exist a ub whose t equals the given t"

Reid Barton (Aug 01 2020 at 23:43):

but as I mentioned above it's awkward

Reid Barton (Aug 01 2020 at 23:44):

this awkwardness would disappear with the usual definition

Patrick Thomas (Aug 01 2020 at 23:44):

Alright.

Patrick Thomas (Aug 01 2020 at 23:44):

Thank you.

Patrick Thomas (Aug 01 2020 at 23:50):

Since we can prove the lub is unique, is a there a way to say the lub S instead of t is_lub S without the structure?

Patrick Thomas (Aug 01 2020 at 23:57):

I end up defining things named lub_S to keep track that they are the lub of S. Just hoping there was a simpler way.

Kenny Lau (Aug 02 2020 at 00:03):

import data.real.basic

noncomputable theory
open_locale classical

namespace hidden

def is_ub (S : set ) (t : ) : Prop :=
 s  S, s  t

def is_lub (S : set ) (t : ) : Prop :=
is_ub S t   r : , is_ub S r  t  r

def lub (S : set ) :  :=
classical.epsilon $ is_lub S

end hidden

Patrick Thomas (Aug 02 2020 at 00:04):

What does classical.epsilon $ is_lub S mean?

Kenny Lau (Aug 02 2020 at 00:05):

is_lub S is a predicate on \R

Kenny Lau (Aug 02 2020 at 00:05):

classical.epsilon means, if there's some r : \R satisfying it, return r

Kenny Lau (Aug 02 2020 at 00:05):

otherwise return a default element

Kenny Lau (Aug 02 2020 at 00:09):

import data.real.basic

noncomputable theory
open_locale classical

namespace hidden

def is_ub (S : set ) (t : ) : Prop :=
 s  S, s  t

def is_lub (S : set ) (t : ) : Prop :=
is_ub S t   {r : }, is_ub S r  t  r

def lub (S : set ) :  :=
classical.epsilon $ is_lub S

theorem is_lub_unique {S : set } {t₁ t₂ : } (ht₁ : is_lub S t₁) (ht₂ : is_lub S t₂) : t₁ = t₂ :=
le_antisymm (ht₁.2 ht₂.1) (ht₂.2 ht₁.1)

theorem eq_lub (S : set ) (t : ) (ht : is_lub S t) : t = lub S :=
is_lub_unique ht $ classical.epsilon_spec t, ht

end hidden

Kenny Lau (Aug 02 2020 at 00:09):

any this is the API for lub

Kenny Lau (Aug 02 2020 at 00:09):

so you can forget about its definition

Patrick Thomas (Aug 02 2020 at 00:11):

What would happen if I used lub S in a proof, and one didn't exist? Would I get an error in Lean?

Jalex Stark (Aug 02 2020 at 00:12):

did you read the definition of lub? did you put it in your VSCode? do you know what classical.epsilon is?

Kenny Lau (Aug 02 2020 at 00:14):

Kenny Lau said:

otherwise return a default element

@Patrick Thomas

Kenny Lau (Aug 02 2020 at 00:14):

you wouldn't get any error

Kenny Lau (Aug 02 2020 at 00:14):

but you wouldn't be able to prove anything about it in that case

Kenny Lau (Aug 02 2020 at 00:15):

treat it as an unspecified constant

Patrick Thomas (Aug 02 2020 at 00:15):

I guess it isn't any different than saying t is_lub S. The assumption that t exists is in the statement.

Patrick Thomas (Aug 02 2020 at 00:16):

Why wouldn't I be able to prove anything about it?

Patrick Thomas (Aug 02 2020 at 00:19):

Jalex Stark said:

did you read the definition of lub? did you put it in your VSCode? do you know what classical.epsilon is?

Yes, but did not understand the result.

Jalex Stark (Aug 02 2020 at 00:21):

ah, it looks like the docstring for classical.epsilon just tells you the math name for the concept

Kenny Lau (Aug 02 2020 at 00:24):

Patrick Thomas said:

Why wouldn't I be able to prove anything about it?

because it has no definition

Kenny Lau (Aug 02 2020 at 00:24):

it uses classical.choice

Kenny Lau (Aug 02 2020 at 00:24):

which produces an element of any type A from a proof of nonempty A by fiat

Adam Topaz (Aug 02 2020 at 00:32):

(deleted)

Patrick Thomas (Aug 02 2020 at 00:37):

I'm not sure I entirely follow. I guess my worry is that it is something like the definition of 0 - 1 = 0 if 0 and 1 are natural numbers. That is, I might prove something that I didn't expect I could.

Kenny Lau (Aug 02 2020 at 00:38):

if S doesn't have an LUB, then lub S will be some real number whose value is outside of your knowledge

Kenny Lau (Aug 02 2020 at 00:38):

it will behave like an arbiratry real number

Patrick Thomas (Aug 02 2020 at 00:40):

I guess it isn't much different than saying t is_lub S then?

Patrick Thomas (Aug 02 2020 at 00:40):

That is t : \R and t is_lub S.

Patrick Thomas (Aug 02 2020 at 00:41):

Or is it actually safer?

Patrick Thomas (Aug 02 2020 at 00:42):

Because the arbitrary number won't have the properties of the lub to use?

Patrick Thomas (Aug 02 2020 at 01:16):

How do I get at the properties of lub S? That is, use the fact that it is an ub of S and it is leq to any ub of S in a proof.

Patrick Thomas (Aug 02 2020 at 03:34):

I guess I need to prove: example (S : set ℝ) : is_lub S (lub S) := ?

Kenny Lau (Aug 02 2020 at 03:36):

that would mean every set has lub

Patrick Thomas (Aug 02 2020 at 03:41):

How do I get at the properties of lub S?

Kenny Lau (Aug 02 2020 at 07:32):

import data.real.basic

noncomputable theory
open_locale classical

namespace hidden

def is_ub (S : set ) (t : ) : Prop :=
 s  S, s  t

def is_lub (S : set ) (t : ) : Prop :=
is_ub S t   {r : }, is_ub S r  t  r

def lub (S : set ) :  :=
classical.epsilon $ is_lub S

theorem is_lub_unique {S : set } {t₁ t₂ : } (ht₁ : is_lub S t₁) (ht₂ : is_lub S t₂) : t₁ = t₂ :=
le_antisymm (ht₁.2 ht₂.1) (ht₂.2 ht₁.1)

theorem is_lub_lub {S : set } {t : } (ht : is_lub S t) : is_lub S (lub S) :=
classical.epsilon_spec t, ht

theorem eq_lub (S : set ) (t : ) (ht : is_lub S t) : t = lub S :=
is_lub_unique ht $ is_lub_lub ht

end hidden

Kenny Lau (Aug 02 2020 at 07:32):

is this enough API?

Kenny Lau (Aug 02 2020 at 07:32):

@Patrick Thomas

Patrick Thomas (Aug 02 2020 at 18:15):

Thank you!

Daniel Shapero (Aug 04 2020 at 16:43):

I was curious about defining Riemann integration and started experimenting with it as well -- I was wondering whether it might be easier to define partitions as a vector of real numbers rather than a mapping from fin? If it's a vector, you can easily pull in some of the existing machinery for sorting lists; for example merging two partitions just reduces to a single library call

Patrick Thomas (Aug 06 2020 at 20:00):

That sounds simpler. I don't know though, I'm new at this.

Patrick Thomas (Aug 07 2020 at 23:04):

I would also be interested in hearing opinions on this.

Dan Stanescu (Aug 08 2020 at 00:04):

It may just largely be a matter of preference. After having used fin for one proof I realize that you need to have everything set up very well from the very beginning in order not to bump into nasty coercion problems. For people with computational background thinking in terms of vector will probably seem more natural. I'm curious what other people with more Lean experience have to say, but it's good to bear in mind that the interface/API (i.e. for fin and vector) is of utmost importance. Also, I don't think you'll have to "sort" in the classical computer-science meaning of the term, where you really handle list/vector elements (like in a "quicksort" algorithm, say). You'll just be dealing with proofs that your sequences are monotone.

Patrick Thomas (Aug 08 2020 at 03:36):

I'm trying to fill in the first sorry in this theorem. By using a rewrite and set.​mem_set_of_eq I can get toz ∈ Z = ∃ x ∈ X, ∃ y ∈ Y, z = x + y, but then I get stuck. I'm wondering it it would be simpler if I had stated the theorem differently, but I'm not sure how.

import data.real.basic

namespace hidden

def is_ub (S : set ) (t : ) : Prop :=
 s  S, s  t

def is_lub (S : set ) (t : ) : Prop :=
is_ub S t   r : , (is_ub S r  r  t)


theorem sum_of_lub
(X : set ) (a : ) (h0 : is_lub X a)
(Y : set ) (b : ) (h1 : is_lub Y b)
(Z = {z |  x  X,  y  Y, z = x + y})
: is_lub Z (a + b) :=
begin
have s1 : is_ub Z (a + b) :=
  begin
  assume z : ,
  assume a1 : z  Z,
  have s2 :  x  X,  y  Y, z = x + y := sorry,
  have s10 : z  a + b := sorry,
  exact s10,
  end,
have s100 : is_lub Z (a + b) := sorry,
exact s100,
end

end hidden

Patrick Thomas (Aug 08 2020 at 03:57):

I guess finish works. I don't understand the description of finish though.

Patrick Thomas (Aug 08 2020 at 05:42):

I'm not sure what I have done wrong here:

import data.real.basic


namespace hidden

def is_ub (S : set ) (t : ) : Prop :=
 s  S, s  t

def is_lub (S : set ) (t : ) : Prop :=
is_ub S t   r : , (is_ub S r  r  t)

example
(X : set ) (a : ) (h0 : is_lub X a)
(Y : set ) (b : ) (h1 : is_lub Y b)
(Z = {z |  x  X,  y  Y, z = x + y})
:  z  Z, z  a + b :=
  assume z : ,
  assume a1 : z  Z,
  have s2 :  x  X,  y  Y, z = x + y, by finish,
  exists.elim s2 (
    assume x' : ,
    assume a2 : x'  X,
    assume y' : ,
    assume a3 : y'  Y,
    assume a4 : z = x' + y',
    have s4 : is_ub X a, from h0.elim_left,
    have s5 : x'  a, from s4 x' a2,
    have s6 : is_ub Y b, from h1.elim_left,
    have s7 : y'  b, from s6 y' a3,
    show z  a + b, by linarith
  )

end hidden

Kenny Lau (Aug 08 2020 at 06:26):

(Z = {z | ∃ x ∈ X, ∃ y ∈ Y, z = x + y}) is just incorrect

Kenny Lau (Aug 08 2020 at 06:27):

ok, incorrect is a bit strong, but it doesn't have its intended meaning?

Kenny Lau (Aug 08 2020 at 06:28):

Lean treats it as (Z) (H : Z = {z | ∃ x ∈ X, ∃ y ∈ Y, z = x + y})

Kenny Lau (Aug 08 2020 at 06:28):

which I guess still works

Kenny Lau (Aug 08 2020 at 06:35):

import data.real.basic algebra.pointwise

namespace hidden

def is_ub (S : set ) (t : ) : Prop :=
 s⦄, s  S  s  t -- implicit argument

def is_lub (S : set ) (t : ) : Prop :=
is_ub S t   r : ⦄, is_ub S r  t  r -- we prefer `≤`; extra bracket removed; implicit

theorem is_lub_add
  (X : set ) (a : ) (h0 : is_lub X a)
  (Y : set ) (b : ) (h1 : is_lub Y b) :
  is_lub (X + Y) (a + b) := -- `X + Y := { z | ∃ x y, x ∈ X ∧ y ∈ Y ∧ x + y = z }`
⟨λ z hz, let x, y, hx, hy, hxy := hz in
  hxy  add_le_add (h0.1 hx) (h1.1 hy),
λ r hr, add_le_of_le_sub_left $ h1.2 $ λ y hy, le_sub.2 $ h0.2 $ λ x hx, le_sub_iff_add_le.2 $
  hr x, y, hx, hy, rfl⟩⟩

end hidden

Kenny Lau (Aug 08 2020 at 06:35):

@Kevin Buzzard deja vu?

Patrick Thomas (Aug 08 2020 at 07:19):

Do you know why I get type mismatch at application for the exists.elim s2?

Kenny Lau (Aug 08 2020 at 07:19):

don't use exists.elim

Kenny Lau (Aug 08 2020 at 07:19):

use let

Patrick Thomas (Aug 08 2020 at 07:22):

That works on existential elimination?

Patrick Thomas (Aug 08 2020 at 07:23):

Is there an example somewhere?

Utensil Song (Aug 08 2020 at 07:32):

Another more natural choice is to use tactic#obtain , example:

import tactic
import tactic.lint

open int

theorem le.antisymm :  {a b : }, a  b  b  a  a = b :=
begin
assume a b : , assume (H₁ : a  b) (H₂ : b  a),
obtain n, Hn := int.le.dest H₁,
obtain m, Hm := int.le.dest H₂,
have H₃ : a + of_nat (n + m) = a + 0, from
  calc
    a + of_nat (n + m) = a + (of_nat n + m) : rfl
      ... = a + (n + m)                     : by rw of_nat_eq_coe
      ... = a + n + m                       : by rw add_assoc
      ... = b + m                           : by rw Hn
      ... = a                               : Hm
      ... = a + 0                           : by rw add_zero,
have H₄ : of_nat (n + m) = of_nat 0, from add_left_cancel H₃,
have H₅ : n + m = 0,                 from of_nat.inj H₄,
have h₆ : n = 0,                     from nat.eq_zero_of_add_eq_zero_right H₅,
show a = b, from
  calc
    a = a + 0    : by simp_rw [add_zero]
  ... = a + n    : by simp_rw [h₆, int.coe_nat_zero]
  ... = b        : Hn
end

Kenny Lau (Aug 08 2020 at 07:36):

Patrick Thomas said:

Is there an example somewhere?

look at my proof

Kenny Lau (Aug 08 2020 at 07:36):

the let I used is the existential elimination

Ruben Van de Velde (Aug 08 2020 at 08:42):

Bit higher level than Kenny's:

  intros z a1,
  rw [H] at a1,
  obtain x, hx, y, hy, h := a1,
  linarith [h0.left x hx, h1.left y hy],

Patrick Thomas (Aug 08 2020 at 17:36):

Kenny Lau said:

Kevin Buzzard deja vu?

?

Patrick Thomas (Aug 08 2020 at 18:01):

Is there a way to make it more verbose? Something like obtain (x : ℝ, hx : x ∈ X, y : ℝ, hy : y ∈ Y, h : z = x + y) from a1,?

Ruben Van de Velde (Aug 08 2020 at 20:02):

Something like

obtain x, hx, y, hy, h :  x  X,  y  Y, z = x + y} := a1,

(untested)

Patrick Thomas (Aug 08 2020 at 20:07):

Sorry, I was thinking more along the lines of showing explicitly what hx, hy, and h get assigned to in the obtain statement.

Ruben Van de Velde (Aug 08 2020 at 20:17):

Yeah, I don't think that's possible

Patrick Thomas (Aug 08 2020 at 20:18):

:(

Patrick Thomas (Aug 08 2020 at 20:24):

I might prefer the exists.elim then, as it shows more of the details in the proof itself. I'm still not sure why I get type mismatch at application for the exists.elim s2 though.

Mario Carneiro (Aug 08 2020 at 20:29):

That's definitely possible

Mario Carneiro (Aug 08 2020 at 20:30):

use rcases a_eq : a1 with ⟨x, hx, y, hy, h⟩

Mario Carneiro (Aug 08 2020 at 20:30):

I don't know if obtain has a similar syntax

Patrick Thomas (Aug 08 2020 at 20:34):

Sorry, I'm not sure I see the difference. I still need to go to the other window to read what x, hx, etc. are?

Mario Carneiro (Aug 08 2020 at 20:34):

what's the mwe?

Mario Carneiro (Aug 08 2020 at 20:35):

Oh I misunderstood your question

Mario Carneiro (Aug 08 2020 at 20:36):

I've been planning to add support for type ascriptions in rcases/obtain, so that you could write

obtain x : , hx : x  X, y : , hy : y  Y, h : z = x + y from a1,

Patrick Thomas (Aug 08 2020 at 20:37):

Yes, that is what I meant. That would be great.

Mario Carneiro (Aug 08 2020 at 20:37):

you might have to put parentheses around the type ascriptions, for consistency with other uses of type ascription

Mario Carneiro (Aug 08 2020 at 20:38):

it also might interact with | in a weird way if you have a notation that uses |

Patrick Thomas (Aug 08 2020 at 20:49):

I don't mind using exists.elim, but I think I am applying it to the double exists wrong?

Patrick Thomas (Aug 08 2020 at 21:14):

I think I got it!

import data.real.basic algebra.pointwise

namespace hidden

def is_ub (S : set ) (t : ) : Prop :=
 s  S, s  t

def is_lub (S : set ) (t : ) : Prop :=
is_ub S t   r : , (is_ub S r  r  t)

theorem is_lub_add
  (X : set ) (a : ) (h0 : is_lub X a)
  (Y : set ) (b : ) (h1 : is_lub Y b)
  : is_ub (X + Y) (a + b) :=
  assume z : ,
  assume a1 : z  X + Y,
  have s1 :  x, ( y, x  X  y  Y  x + y = z), from a1,
  exists.elim s1 (
    assume x' : ,
    assume a2 :  y, x'  X  y  Y  x' + y = z,
      exists.elim a2 (
        assume y' : ,
        assume a3 : x'  X  y'  Y  x' + y' = z,
        have s2 : is_ub X a, from h0.left,
        have s3 : x'  a, from s2 x' a3.left,
        have s4 : is_ub Y b, from h1.left,
        have s5 : y'  b, from s4 y' a3.right.left,
        have s6 : x' + y'  a + b, by linarith,
        show z  a + b, by linarith
      )
  )

end hidden

Patrick Thomas (Aug 08 2020 at 22:32):

Where does this error come from?
Screenshot-from-2020-08-08-15-31-29.png

Anatole Dedecker (Aug 08 2020 at 22:33):

Oh

Anatole Dedecker (Aug 08 2020 at 22:33):

I got this one quite a lot, I was about to ask the same thing

Anatole Dedecker (Aug 08 2020 at 22:34):

Well, I know why this happens : the hypothesis is_ub (X+Y) r in the implication is implicitly named a, shadowing the a you want

Anatole Dedecker (Aug 08 2020 at 22:37):

But the only way to avoid this I know is writing the implication as a forall, namely \for (h : is_ub (X+Y) r), .... This way you can name the hypothesis so no problem of shadowing. But this is quite ugly, so maybe there's a better solution ?

Patrick Thomas (Aug 08 2020 at 22:41):

How are you able to tell that the hypothesis is implicitly named a?

Anatole Dedecker (Aug 08 2020 at 22:43):

By reading the error message :upside_down: The type of a is exactly the left side of your implication, which means precisely that a is a proof of is_ub (X+Y) r

Patrick Thomas (Aug 08 2020 at 22:44):

I see. Well, changing a and b to t0 and t1 fixes it. That works I guess.

Patrick Thomas (Aug 08 2020 at 22:45):

Thank you.

Anatole Dedecker (Aug 08 2020 at 22:48):

No problem ! It would be nice for this to be fixed at some point anyway, but maybe it's harder than I imagine

Kenny Lau (Aug 09 2020 at 05:24):

just use guard_hyp

Mario Carneiro (Aug 09 2020 at 05:28):

Mario Carneiro said:

I've been planning to add support for type ascriptions in rcases/obtain, so that you could write

obtain x : , hx : x  X, y : , hy : y  Y, h : z = x + y from a1,

This works now, as of #3730, which is a significant rewrite of rcases to support some more flexible pattern syntax. You can now use parentheses like (a | b) | c in patterns instead of the previous strict alternation of and/or

Patrick Massot (Aug 09 2020 at 10:06):

Build is failing.

Anatole Dedecker (Aug 09 2020 at 20:02):

Kenny Lau said:

just use guard_hyp

Could you explain a bit more what you meant ?

Kenny Lau (Aug 10 2020 at 05:14):

you can use guard_hyp to assert that a hypothesis has a certain type

Kenny Lau (Aug 10 2020 at 05:15):

so if you want to assert that hx has type x \in X then just use guard_hyp

Patrick Thomas (Sep 13 2020 at 16:02):

I'm trying to define a partition using a list. Is this a good definition?

structure partition (a : ) (b : ) :=
(x : list )
(x_head : list.head' x = option.some a)
(x_last : list.last' x = option.some b)
(mono   : list.chain' real.le x)

I think the x_head and x_last constructors ensure that the list is not empty?
Using that I am trying to define the norm. I looked at using list.foldr for taking the max, but it requires an initial accumulator value that I would like to avoid.

Patrick Thomas (Sep 13 2020 at 16:07):

I think maybe I need something like the foldr1 function in Haskell.

Patrick Thomas (Sep 13 2020 at 17:30):

Is there a way to have an option to show the types in the mathlib generated documentation?

Patrick Thomas (Sep 13 2020 at 17:35):

For example that l is a list in the definition of a vector?
https://leanprover-community.github.io/mathlib_docs/core/data/vector.html#vector

Kevin Buzzard (Sep 13 2020 at 17:36):

If you click on "source" you see def vector (α : Type u) (n : ℕ) := { l : list α // l.length = n } . Does this answer your question?

Patrick Thomas (Sep 13 2020 at 17:37):

I was being lazy and thought it might be nice to have an option to avoid that :)

Patrick Thomas (Sep 13 2020 at 17:39):

Sorry

Kevin Buzzard (Sep 13 2020 at 17:40):

#print vector within a Lean file should also tell you everything about it

Patrick Thomas (Sep 13 2020 at 17:41):

Even more work :)

Bryan Gin-ge Chen (Sep 13 2020 at 17:41):

If you hover over .length in l.length, you can see that the URL ends in list.length which is a clue. But feel free to open an issue here.

Patrick Thomas (Sep 13 2020 at 17:41):

Ok. Thank you.

Patrick Thomas (Sep 13 2020 at 17:52):

Added: https://github.com/leanprover-community/doc-gen/issues/63

Patrick Thomas (Sep 13 2020 at 18:56):

If a vector is based on a list, how do you use the functions defined for lists on it? Do you have to cast it to a list first?

Kevin Buzzard (Sep 13 2020 at 18:57):

A vector is a pair consisting of a list and a proof.

Patrick Thomas (Sep 13 2020 at 18:58):

vector α n = {l // l.length = n} defines a list and a proof?

Patrick Thomas (Sep 13 2020 at 18:59):

The proof comes from the type somehow?

Kevin Buzzard (Sep 13 2020 at 19:00):

https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html?highlight=subtype#inductively-defined-propositions

Kevin Buzzard (Sep 13 2020 at 19:00):

the proof comes from the proof which you'll supply that l.length=n when you're making the term. vector is a subtype -- see the link above.

Patrick Thomas (Sep 13 2020 at 19:34):

So I should be able to get at the list by using .val?

Patrick Thomas (Sep 13 2020 at 19:41):

Got it. Thank you.

Patrick Thomas (Sep 13 2020 at 20:14):

Is there a function defined similar to vector.head for getting the last element of the vector where you don't have to worry about the vector being nil?

Patrick Thomas (Sep 13 2020 at 20:48):

I'm trying to make something like this work:

structure partition (a : ) (b : ) :=
(n : )
(x : vector  (n + 1))
(x_zero : vector.head x = a)
(x_last : vector.last x = b)
(mono : list.chain' real.le x.val)

structure pointed_partition (a b : ) extends partition a b :=
(y : vector  n)
(mem_block :  m : , m  n  y.at m  set.Icc ((x.at m) (x.at (m + 1)))

Kevin Buzzard (Sep 13 2020 at 21:20):

Patrick Thomas said:

Is there a function defined similar to vector.head for getting the last element of the vector where you don't have to worry about the vector being nil?

I don't know the vector or list API's at all but why don't you just write the precise function you want and then ask whether this precise function is already there?

Patrick Thomas (Sep 13 2020 at 21:21):

I can write the type, but I'm having trouble defining it.

Patrick Thomas (Sep 13 2020 at 21:23):

The same as this but returns the last element instead of the first:

def head : vector α (nat.succ n)  α
|  [],    h  := by contradiction
|  a :: v, h  := a

Kyle Miller (Sep 13 2020 at 21:28):

It doesn't seem to exist already. One way is to define it with vector.nth:

import data.vector

def vector.last {α : Type*} {n : } (v : vector α n.succ) : α :=
v.nth n, nat.less_than_or_equal.refl

Patrick Thomas (Sep 13 2020 at 21:30):

Nice. Thank you.

Kyle Miller (Sep 13 2020 at 21:30):

Another is in terms of list.last:

import data.vector

def vector.last {α : Type*} {n : } : vector α n.succ  α
| [], h := by contradiction
| a :: v, h := (a :: v).last (by simp)

Patrick Thomas (Sep 13 2020 at 21:31):

In the first, should n be n + 1 in the body?

Kyle Miller (Sep 13 2020 at 21:33):

I don't think so, since if you have a vector of length n+1, since it's zero-indexed the last element will be indexed by n.

Patrick Thomas (Sep 13 2020 at 21:33):

Oh. Right.

Adam Topaz (Sep 13 2020 at 21:36):

I don't know how heavily you're invested in vector, but all of these things (I think) are already in the API for fin n, i.e. representations of n-tuples as fin n \to A.

Yakov Pechersky (Sep 13 2020 at 21:37):

And data.matrix.notation has nice notation for those

Patrick Thomas (Sep 13 2020 at 21:40):

Not completely invested. I just figured that since there is a lot of beginner documentation and tutorials on lists and vectors that I would understand it better by going with that.

Patrick Thomas (Sep 13 2020 at 21:41):

For example I don't understand (finset.univ : finset (fin P.n)).sup (λ j, (P.x j.cast_succ - P.x j.succ))

Adam Topaz (Sep 13 2020 at 21:43):

Where's that from?

Patrick Thomas (Sep 13 2020 at 21:44):

Much earlier in the thread.

Adam Topaz (Sep 13 2020 at 21:46):

Oh, I see. In the link for the lean web editor? Note the commented out notation there :)

Adam Topaz (Sep 13 2020 at 21:46):

That should be approximately familiar mathematical notation.

Patrick Thomas (Sep 13 2020 at 21:48):

Yeah. I'm going to have to prove things about it though.

Adam Topaz (Sep 13 2020 at 21:49):

This is another reason to use fin nif the API is more developed.

Patrick Thomas (Sep 13 2020 at 21:50):

True.

Patrick Thomas (Sep 13 2020 at 21:51):

If I understand the API :)

Patrick Thomas (Sep 13 2020 at 21:53):

I'll probably move on to it at some point.

Patrick Thomas (Sep 13 2020 at 22:00):

What is the * after Type by the way?

Adam Topaz (Sep 13 2020 at 22:00):

It tells lean to go and figure out the universe variable.

Patrick Thomas (Sep 13 2020 at 22:00):

Ah.

Yakov Pechersky (Sep 13 2020 at 22:40):

The finset.univ line says that, for all values of (fin P.n), that is, from 0 to n-1.

Yakov Pechersky (Sep 13 2020 at 22:41):

Then the supremum of the set of all those values, under the map taking each such value j to P.x[j + 1] - P.x[j]

Yakov Pechersky (Sep 13 2020 at 22:41):

In python list accession syntax

Yakov Pechersky (Sep 13 2020 at 22:44):

finset.univ means a finset (a finite set) of all the terms for a given type

Patrick Thomas (Sep 14 2020 at 03:30):

For my own understanding, this seemed to work? Is this right?

namespace hidden

inductive nat : Type
| zero : nat
| succ : nat  nat


inductive vector (α : Type) : nat  Type
| nil : vector nat.zero
| cons (a : α) (n : nat) (v : vector n) : vector (nat.succ n)
-- a : element to prepend, n : length of vector to prepend to, v : vector to prepend to
-- note the use of n in the type of v


def first (α : Type) :  n : nat, vector α (nat.succ n)  α
| _ (vector.cons a _ _) := a


def v1 : vector nat nat.zero := vector.nil
def v2 : vector nat nat.zero.succ := vector.cons nat.zero nat.zero v1
def v3 : vector nat nat.zero.succ.succ := vector.cons nat.zero.succ nat.zero.succ v2

#reduce first nat nat.zero v2
#reduce first nat nat.zero.succ v3


def last (α : Type) :  n : nat, vector α (nat.succ n)  α
| _ (vector.cons a (nat.zero) vector.nil) := a
| _ (vector.cons _ (nat.succ n) v) := last n v

end hidden

Patrick Thomas (Sep 14 2020 at 03:32):

first and last didn't seem to need a proof that the vector wasn't empty like the ones in the library, so I'm a little unsure. I am guessing that is because of the way that vector was defined?

Patrick Thomas (Sep 14 2020 at 03:33):

Functionally I think this is equivalent though?

Yakov Pechersky (Sep 14 2020 at 03:39):

The proof that it isn't empty in your definition is that the patterns you're matching on require a vector of length (n + 1)

Yakov Pechersky (Sep 14 2020 at 03:41):

If you want to play more with these definitions, you could make se arguments implicit, like making the length argument to cons or first or last implicit. Since it can be inferred from the type of vector.

Yakov Pechersky (Sep 14 2020 at 03:41):

Also, look into Pi types, which are type level foralls

Patrick Thomas (Sep 14 2020 at 03:44):

Yakov Pechersky said:

The proof that it isn't empty in your definition is that the patterns you're matching on require a vector of length (n + 1)

That is what I was guessing.

Patrick Thomas (Sep 14 2020 at 03:44):

Thank you.

Patrick Thomas (Sep 19 2020 at 14:40):

Yakov Pechersky said:

The finset.univ line says that, for all values of (fin P.n), that is, from 0 to n-1.

I'm sorry, I'm still not sure I get this. Maybe if the steps were broken apart it would be easier to see? How would it look if we first took the differences and then the sup? What would be the least abstract way to build this up from just the definition of fin?

Alex J. Best (Sep 19 2020 at 15:13):

fin n is the subtype of nat of nats which are less than n.
finset (fin n) is the type of all finite sets (unordered lists with no duplicates) whose members are all from fin n.
univ (or finset.univ if the namespace isn't open) is the term of finset X containing all terms of type X when X is a type with only finitely many terms (which fin n is).
If you just type #check finset.univ lean doesn't know what you want a finset of so (finset.univ : finset (fin n)) is the term representing the set of all the terms of fin n.
finset.sup then takes the supremum of the function (λ j, (P.x j.cast_succ - P.x j.succ)) over the specified set, with the dot notation so it comes after the set, in this case univ.

Alex J. Best (Sep 19 2020 at 15:16):

I think this code is taking the differences first then the sup already. The (λ j, (P.x j.cast_succ - P.x j.succ)) function is applied to each term of fin P.n and the sup is taken of those values as it goes.

Patrick Thomas (Sep 19 2020 at 15:21):

So finset (fin 3) has the terms [0, 1, 2], [0, 2, 1], [1, 0, 2] etc.?

Alex J. Best (Sep 19 2020 at 15:23):

By unordered I mean the ordering doesn't matter, so its
{}, {0}, {1}, {2}, {0,1}, {0,2}, {1,2}, {0,1,2}
and the last one there is univ.

Patrick Thomas (Sep 19 2020 at 15:29):

I see.
What happens if the set has only one element? If I'm reading the definition of partition correctly, I think it allows that?

Patrick Thomas (Sep 19 2020 at 16:01):

It looks like it is using some kind of fold. Maybe it defaults to some value?

Alex J. Best (Sep 19 2020 at 16:35):

If the partition has 1 element then n = 0 as it is a map from fin (n + 1) \to \R\ge0 so I think in that case its the sup over the empty set, which defaults to the infimum of the whole target. Which version of the code are you using, it changed a bit throughout this thread.

Patrick Thomas (Sep 19 2020 at 16:46):

I was thinking that since it is taking adjacent differences there would be a problem with the set of only one element, since that element does not have an adjacent element.

Patrick Thomas (Sep 19 2020 at 16:48):

I had been looking at the following code, but now it gives an error next to the .sup:

import data.real.basic data.set.intervals data.finset algebra.big_operators data.fintype.basic

noncomputable theory

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

namespace partition

def norm {a b : } (P : partition a b) : 
-- := ⨆ i : fin P.n, P.x i.succ - P.x i.cast_succ
:= (finset.univ : finset (fin P.n)).sup (λ j, (P.x j.cast_succ - P.x j.succ))

end partition

Patrick Thomas (Sep 19 2020 at 16:55):

Also, why is it (finset.univ : finset (fin P.n)) instead of (finset.univ (finset (fin P.n)))?

Alex J. Best (Sep 19 2020 at 16:58):

the colon is specifying the type of the term on the left. finset.univ takes no explicit arguments, if you type #check finset.univ you should see finset.univ : finset ?M_1, so there are no arguments to be filled in, but there is a metavariable in the type, which means that lean doesn't know what sort of finset the term  finset.univ  is without extra hints, which is what the : is doing, telling lean what type you expect it to be.

Alex J. Best (Sep 19 2020 at 17:00):

You could instead tell lean you want to specify implicit arguments as arguments directly, by using @finset.univ, the type of this is now finset.univ : Π {α : Type u_1} [_inst_1 : fintype α], finset α, which we see has 2 arguments, the type and the fact it is a fintype, so we could write instead, (@finset.univ (fin P.n)).sup ...

Patrick Thomas (Sep 19 2020 at 17:02):

I see. Thank you.

Alex J. Best (Sep 19 2020 at 17:02):

The error next to the sup is discussed somewhere above in the thread, but its basically the issue you are worried about, if there is only one thing in the partition lean want to assign some default value to the norm, as its a sup over an empty set, but it doesn't have a sensible choice, as \R has no minimal element. Thats why in the version I gave a while ago I switched it to  \R\ge0, which has a minimal element!

Alex J. Best (Sep 19 2020 at 17:04):

When the partition has n+1 points in it, the list of things we take the sup over only has n.

Patrick Thomas (Sep 19 2020 at 17:06):

I see.

Patrick Thomas (Oct 30 2020 at 00:34):

Sorry, I'm trying to define something from scratch so that I can better understand it. It seems that this does not work, and I am guessing it may be why finset is involved? Is there a way to fix this definition?

def norm :  (n : ) (f : fin n  ), 
| 0 f := 0
| m f := min (f (fin.mk m sorry) - f (fin.mk (m - 1) sorry)) (norm (m - 1) f)

Patrick Thomas (Oct 30 2020 at 00:35):

Not the sorrys, but the passing of m-1 to norm.

Yakov Pechersky (Oct 30 2020 at 00:54):

First comment, you probably want to do something that looks like:

import data.real.basic

def norm :  (n : ) (f : fin n  ), 
| 0 f := 0
| (m + 1) f := min (f (fin.mk (m + 1) sorry) - f (fin.mk m sorry)) (norm m f)

Yakov Pechersky (Oct 30 2020 at 00:54):

that is, once you've taken care of the 0 case, do the succ pattern. and avoid subtraction.

Yakov Pechersky (Oct 30 2020 at 00:54):

what's the error you get now?

Patrick Thomas (Oct 30 2020 at 00:59):

type mismatch at application
  norm m f
term
  f
has type
  fin (m + 1)  
but is expected to have type
  fin m  

Yakov Pechersky (Oct 30 2020 at 01:00):

What exactly are you trying to define? Can you describe it in words?

Patrick Thomas (Oct 30 2020 at 01:03):

I'm using a function from fin n to R to define an ordered list of real numbers. If there is only one element in that 'list' I want to return 0. If the 'list' is [a, b, c, ...] I want to return the minimum of {b -a, c - b, ...}.

Patrick Thomas (Oct 30 2020 at 01:06):

Oops, make that the max of those numbers.

Yakov Pechersky (Oct 30 2020 at 01:11):

Just so you know, fin 0 is isomorphic to the empty type. So in your wording, it would be the empty list.

Patrick Thomas (Oct 30 2020 at 01:13):

Ok.

Yakov Pechersky (Oct 30 2020 at 01:13):

Are you wedded to having it as a fin n \to R?

Yakov Pechersky (Oct 30 2020 at 01:13):

You might want to express this as a fold over lists.

Yakov Pechersky (Oct 30 2020 at 01:15):

In the meantime, maybe something like:

import data.real.basic

noncomputable def norm : Π (n : ) (f : fin n  ), 
| 0       f := 0
| 1       f := 0
| (m + 2) f := min (f 1 - f 0) (norm (m + 1) (λ i, f i.succ))

Patrick Thomas (Oct 30 2020 at 01:16):

Interesting. Thank you!

Patrick Thomas (Oct 30 2020 at 02:01):

For the standard definition of a list, how would you write something like "every element in the list is 0" or "every element in the list is 0 except for n elements that are 1"?

Patrick Thomas (Oct 30 2020 at 02:10):

I guess you would need to define a function that returns the nth element of the list.

Patrick Thomas (Oct 30 2020 at 02:15):

But then that function should take a proof that n is less than the length of the list, and I'm not sure how that proof would be supplied in something like forall n : nat, n < list.len -> list.at n (sorry) = 0.

Yakov Pechersky (Oct 30 2020 at 02:33):

import data.real.basic
import data.list.basic

example {l : list } {x : } : x  l  x = 0 := sorry

Yakov Pechersky (Oct 30 2020 at 02:33):

The functions you're thinking about are docs#list.nth and docs#list.nth_le

Yakov Pechersky (Oct 30 2020 at 02:33):

There's also docs#list.of_fn

Yakov Pechersky (Oct 30 2020 at 02:34):

And also docs#vector.

Yakov Pechersky (Oct 30 2020 at 02:34):

But which you should use is probably dependent on what you want to use this list for!

Patrick Thomas (Oct 30 2020 at 02:50):

Thank you.

Patrick Thomas (Oct 31 2020 at 00:40):

Is there a way to say that l is not list.nil because that case has been exhausted?

def last (α : Type) : Π l : list α, ¬ l = list.nil  α
| list.nil h := absurd (eq.refl list.nil) h
| (list.cons a list.nil) _ := a
| (list.cons a l) _ := last l sorry

Kevin Buzzard (Oct 31 2020 at 08:08):

Change that l to list.cons b m?

Patrick Thomas (Nov 01 2020 at 19:31):

I see. Thank you.

Patrick Thomas (Nov 01 2020 at 19:38):

I'm sorry, I'm still having a hard time understanding quotients and setoids. Is there a simpler way to define the norm and Riemann sum that doesn't rely on these? Perhaps casting fin n to a list?

import data.real.basic data.set.intervals data.finset algebra.big_operators data.fintype.basic data.real.nnreal

noncomputable theory

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

namespace partition
open_locale nnreal

def norm {a b : } (P : partition a b) : 0
:= (finset.univ : finset (fin P.n)).sup (λ j, P.x j.succ - P.x j.cast_succ, by linarith [mono P j]⟩)

notation `||`P`||` := P.norm

end partition

open set

structure pointed_partition (a b : ) extends partition a b :=
(y : fin n  )
(mem_block :  m : fin n, y m  Icc (x m.cast_succ) (x m.succ))

instance (a b : ) : has_coe_to_fun (pointed_partition a b) := _, λ c, c.y

open_locale big_operators

def riemann_sum (a b : ) (P : pointed_partition a b) (f :   ) : 
:=  n, f (P n) * (P.x n.succ - P.x n.cast_succ)

Mario Carneiro (Nov 01 2020 at 19:47):

you mean like this?

import data.real.basic data.set.intervals

inductive pointed_partition :     Type
| nil :  a, pointed_partition a a
| cons :  a b c (y  set.Icc a b), pointed_partition b c  pointed_partition a c

def riemann_sum :  {a b}, pointed_partition a b  (  )  
| _ _ (pointed_partition.nil a) f := 0
| _ _ (pointed_partition.cons a b c y _ P) f := f y * (b - a) + riemann_sum P f

Patrick Thomas (Nov 01 2020 at 19:51):

I was actually thinking of keeping the definition of partition and pointed partition the same, but casting fin n to a list in the definition of norm and sum.

Mario Carneiro (Nov 01 2020 at 19:55):

I guess it's not clear to me what you are optimizing then

Mario Carneiro (Nov 01 2020 at 19:55):

you have no theorems

Mario Carneiro (Nov 01 2020 at 19:55):

I don't see anything particularly gratuitous in the definitions of norm and sum, assuming the definition of a partition is fixed

Mario Carneiro (Nov 01 2020 at 19:56):

you can skip the linarith proof if you want, dunno if that's better

Patrick Thomas (Nov 01 2020 at 19:57):

Just trying to make definitions that I understand so that I know how to use them. When I follow the definition of finset in mathlib I still get lost.

Mario Carneiro (Nov 01 2020 at 19:57):

how do you want to use them?

Patrick Thomas (Nov 01 2020 at 19:58):

The definitions of norm and sum? To prove properties of the Riemann integral.

Mario Carneiro (Nov 01 2020 at 19:58):

okay, so pick a theorem and prove it

Mario Carneiro (Nov 01 2020 at 19:58):

you won't know if the definition is usable until you try to use it

Patrick Thomas (Nov 01 2020 at 19:59):

Won't it be a bad start if I don't understand the definitions I am using?

Patrick Thomas (Nov 01 2020 at 20:01):

Or do you mean try to make my own definitions and use them and see how it goes?

Yakov Pechersky (Nov 01 2020 at 20:03):

Easy way of making a list from a fin n is docs#list.of_fn. But proving things about it will be harder than what you have. Try to make the statement of a theorem you want to prove. That will require some sort of basic definitions. Then you can try proving it. Clunky definitions will make proving things difficult. You can then alternate changing definitions, proving a little more, refining the theorem statament, etc

Patrick Thomas (Nov 01 2020 at 20:14):

Alright.

Patrick Thomas (Nov 01 2020 at 21:13):

Maybe instead of extending the definition of partition, pointed_partition should take a partition as a parameter? Because P' in this definition has no reference to P right? And it needs to.

∀ ε : ℝ, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ P : partition a b, (partition.norm P) < δ → ∀ P' : pointed_partition a b, abs ((riemann_sum a b P' f) - R) < ε

Patrick Thomas (Nov 01 2020 at 21:28):

I guess I could do this, but it seems a little unnatural?

def is_integral (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0 
 δ : nnreal, δ > 0   P : pointed_partition a b, (partition.norm (pointed_partition.to_partition P)) < δ 
abs ((riemann_sum a b P f) - R) < ε

Mario Carneiro (Nov 01 2020 at 21:28):

like this?

def partition.points {a b : } (P : partition a b) :=
Π m : fin P.n, Icc (P.x m.cast_succ) (P.x m.succ)

Mario Carneiro (Nov 01 2020 at 21:32):

I also want to observe that if you just wanted to say norm P < delta then there is no need to define norm

Mario Carneiro (Nov 01 2020 at 21:33):

you can define that more simply as ∀ j, P.x j.succ - P.x j.cast_succ < delta

Patrick Thomas (Nov 01 2020 at 21:34):

Or like this?

structure pointed_partition' (a b : ) (P : partition a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  Icc (P.x m.cast_succ) (P.x m.succ))

Mario Carneiro (Nov 01 2020 at 21:34):

you could do that, yes

Patrick Thomas (Nov 01 2020 at 21:35):

Any foreseeable issues?

Mario Carneiro (Nov 01 2020 at 21:40):

well it's two things instead of one thing

Patrick Thomas (Nov 01 2020 at 22:18):

import data.real.basic data.set.intervals algebra.big_operators

noncomputable theory

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)


structure pointed_partition (a b : ) (P : partition a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  set.Icc (P.x m.cast_succ) (P.x m.succ))


open_locale big_operators

def riemann_sum (a b : ) (P : partition a b) (P' : pointed_partition a b P) (f :   ) : 
:=  n, f (P'.y n) * (P.x n.succ - P.x n.cast_succ)


def is_integral (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0 
 δ : , δ > 0   P : partition a b,  j : fin P.n, P.x j.succ - P.x j.cast_succ < δ 
 P' : pointed_partition a b P, abs ((riemann_sum a b P P' f) - R) < ε

Patrick Thomas (Nov 02 2020 at 04:16):

Why is the declaration of this example an invalid expression?

import data.real.basic data.set.intervals

structure part (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

structure pt_part {a b : } (P : part a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  set.Icc (P.x m.cast_succ) (P.x m.succ))

example {a b : } (P : part a b) :  P' : pt_part P := sorry

Yakov Pechersky (Nov 02 2020 at 04:24):

An exists statement can only state something that is a Prop. Your pt_part P is a structure that has data, not just propositions.

Yakov Pechersky (Nov 02 2020 at 04:25):

What would the P' do?

Patrick Thomas (Nov 02 2020 at 04:29):

It was going to be used in my theorem that the definition of the riemann integral is uniquely defined.

I guess maybe I should instead define a default p_part for an arbitrary part?

Yakov Pechersky (Nov 02 2020 at 04:31):

You could, but I'm not sure what you were trying to state with your example.

Patrick Thomas (Nov 02 2020 at 04:31):

import data.real.basic data.set.intervals


structure part (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)


noncomputable def norm_aux : Π (n : ) (f : fin (n + 1)  ), 
| 0       f := 0
| 1       f := 0
| (m + 2) f := max (f 1 - f 0) (norm_aux (m + 1) (fun i, f i))

noncomputable def norm {a b : } (P : part a b) :  := norm_aux P.n P.x

lemma blah {a b : } :  δ : , δ > 0   P : part a b, norm P < δ := sorry


structure pt_part {a b : } (P : part a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  set.Icc (P.x m.cast_succ) (P.x m.succ))

--lemma blah2 {a b : ℝ} (P : part a b) : ∃ P' : pt_part P := sorry

def rsum_aux : Π (n : ) (f : fin n  ), 
| 0       _ := 0
| (m + 1) f := f m + rsum_aux m (fun i, f i.succ)

def rsum {a b : } {P : part a b} (P' : pt_part P) (f :   ) : 
:= rsum_aux P.n (fun i : fin P.n, (P'.y i) * (P.x i.succ - P.x i.cast_succ))


def is_rint (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0   δ : , δ > 0   P : part a b, norm P < δ   P' : pt_part P, abs ((rsum P' f) - R) < ε


example (a b : ) (f :   ) (R₀ R₁ : ) (h0 : is_rint a b f R₀) (h1 : is_rint a b f R₁) : R₀ = R₁ :=
have s1 :  ε : , ε > 0  abs (R₀ - R₁) < ε := (
  assume ε : ,
  assume a1 : ε > 0,
  have s2 : ε / 2 > 0, by linarith,
  have s3 :  δ₀ : , δ₀ > 0   P : part a b, norm P < δ₀   P' : pt_part P, abs ((rsum P' f) - R₀) < ε / 2 := h0 (ε / 2) s2,
  have s4 :  δ₁ : , δ₁ > 0   P : part a b, norm P < δ₁   P' : pt_part P, abs ((rsum P' f) - R₁) < ε / 2 := h1 (ε / 2) s2,
  exists.elim s3 (
    assume δ₀ : ,
    assume a2 : δ₀ > 0   P : part a b, norm P < δ₀   P' : pt_part P, abs ((rsum P' f) - R₀) < ε / 2,
    exists.elim s4 (
      assume δ₁ : ,
      assume a3 : δ₁ > 0   P : part a b, norm P < δ₁   P' : pt_part P, abs ((rsum P' f) - R₁) < ε / 2,
      let δ := min δ₀ δ₁ in
      have s5 : δ > 0 := sorry,
      have s6 :  P : part a b, norm P < δ := blah δ s5,
      exists.elim s6 (
        assume P : part a b,
        assume a4 : norm P < δ,
        -- get an arbitrary p_part of P here.
      )
    )
  )
),
sorry

Yakov Pechersky (Nov 02 2020 at 04:32):

"Given P, a partition of [a, b], there exists a P' such that the pt_part of P is ...?"

Yakov Pechersky (Nov 02 2020 at 04:32):

What's the ... there?

Yakov Pechersky (Nov 02 2020 at 04:34):

Do you just want to say that for any P : part a b one can make a pt_part P?

Patrick Thomas (Nov 02 2020 at 04:34):

Yes. I just need an arbitrary riemann sum of P.

Yakov Pechersky (Nov 02 2020 at 04:37):

import data.real.basic data.set.intervals

structure part (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

structure pt_part {a b : } (P : part a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : part a b) : inhabited (pt_part P) :=
⟨{ y := _,
  mem_block := _ }⟩

Yakov Pechersky (Nov 02 2020 at 04:38):

Providing an inhabited instance allows you to use default for a default value, or arbitrary for a default value that one should not introspect

Patrick Thomas (Nov 02 2020 at 04:38):

You don't have to supply the definition of y and a proof of mem_block?

Yakov Pechersky (Nov 02 2020 at 04:39):

You do.

Yakov Pechersky (Nov 02 2020 at 04:39):

You have to fill in those underscores

Yakov Pechersky (Nov 02 2020 at 04:39):

But once you do it in that instance declaration, you don't have to do it again when you invoke default

Patrick Thomas (Nov 02 2020 at 04:39):

Ah. Ok. Thank you.

Yakov Pechersky (Nov 02 2020 at 04:40):

We'll see. This might not work because of the P argument

Patrick Thomas (Nov 02 2020 at 04:45):

What is the syntax to get the default?

Yakov Pechersky (Nov 02 2020 at 04:49):

import data.real.basic data.set.intervals

structure part (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

structure pt_part {a b : } (P : part a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : part a b) : inhabited (pt_part P) :=
⟨{ y := λ i, sorry,
  mem_block := sorry }⟩

example {a b : } {P : part a b} : pt_part P := default _

Yakov Pechersky (Nov 02 2020 at 04:49):

So in a place that would expect a pt_part P for some inferable P, you could just write default _

Yakov Pechersky (Nov 02 2020 at 04:50):

because default : Π (α : Sort u_1) [c : inhabited α], α

Yakov Pechersky (Nov 02 2020 at 04:50):

That is, default gives you some α if you tell it what α you want and it can find an instance of inhabited α. And in the example, we can use an underscore, because the type α is inferable from the context.

Patrick Thomas (Nov 02 2020 at 04:55):

Nice. Thank you.

Patrick Thomas (Nov 03 2020 at 01:38):

Is this a correct definition for saying that R is the Riemann integral of f on [a,b]? I'm not sure about the after the δ > 0.

def is_riemann_integral (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0   δ : , δ > 0   P : partition a b, norm P < δ   Q : pointed_partition P, abs ((riemann_sum Q f) - R) < ε

Patrick Thomas (Nov 03 2020 at 02:27):

Also, how can I state this correctly?

example (f := fun x : , if x = 1 then 1 else 0) : is_riemann_integral 0 2 f 0 := sorry

Alex J. Best (Nov 03 2020 at 03:08):

I'd say just do

example  : is_riemann_integral 0 2 (λ x : , if x = 1 then 1 else 0) 0 := sorry

Alex J. Best (Nov 03 2020 at 03:09):

But

example  : let f := (λ x : , if x = 1 then 1 else 0) in is_riemann_integral 0 2 f 0 := sorry

is more like what you had, if fis some long expression you want to use twice this can be helpful.

Patrick Thomas (Nov 03 2020 at 03:11):

Ok. Thank you!

Patrick Thomas (Nov 07 2020 at 04:43):

How would I set up the induction tactic for all_le_b so that it is decreasing?

import data.real.basic

namespace hidden

structure fin (n : ) :=
(i : )
(h : i < n)


lemma lt_succ_1 {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_2 {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ (n : ) : n < n + 1 := sorry
lemma zero_lt_succ {n : } : 0 < n + 1 := sorry


def cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.i (lt_succ_1 a.h)

def succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.i + 1) (lt_succ_2 a.h)

def fin_zero {n : } : fin (n + 1) :=
@fin.mk (n + 1) 0 zero_lt_succ

def fin_last {n : } : fin (n + 1) :=
@fin.mk (n + 1) n (lt_succ n)

/-
n = 0 :
x : 0 → ℝ
a = x 0 = b
n = 1 :
x : [0, 1] → ℝ
a = x 0 ≤ x 1 = b
-/
structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x fin_zero = a)
(x_last : x fin_last = b)
(mono :  m : fin n, x (cast_succ m)  x (succ m))


/-
nat.zero
Goal : a ≤ P.x {0, 0 < P.n + 1}

nat.succ
IH : m < P.n + 1 → a ≤ P.x {m, m < P.n + 1}
Goal : m + 1 < P.n + 1 → a ≤ P.x {m + 1, m + 1 < P.n + 1}
-/
lemma a_le_all {a b : } (P : partition a b) :  m : fin (P.n + 1), a  P.x m :=
begin
assume m : fin (P.n + 1),
induction m,
induction m_i,
case nat.zero {
  have s0 : a = P.x fin_zero := eq.symm P.x_zero,
  show a  P.x fin_zero, from sorry
},
case nat.succ : m IH {
  -- m_h : m.succ < P.n + 1
  -- IH : ∀ (m_h : m < P.n + 1), a ≤ P.x {i := m, h := m_h}
  have s0 : m + 1 < P.n + 1 := m_h,
  have s1 : m < P.n := sorry,
  have s2 : m < P.n + 1 := sorry,
  have s3 : a  P.x (cast_succ {i := m, h := s1}) := IH s2,
  have s4 : P.x (cast_succ {i := m, h := s1})  P.x (succ {i := m, h := s1}) := P.mono {i := m, h := s1},
  show a  P.x (succ {i := m, h := s1}), from le_trans s3 s4
}
end

lemma a_le_b {a b : } (P : partition a b) : a  b :=
have s0 : a  P.x (@fin_last P.n) := a_le_all P (@fin_last P.n),
have s1 : P.x (@fin_last P.n) = b := P.x_last,
show a  b, from sorry

lemma all_le_b {a b : } (P : partition a b) :  m : fin (P.n + 1), P.x m  b :=
begin
assume m : fin (P.n + 1),
induction m,
induction m_i using ?,
end

end hidden

Mario Carneiro (Nov 07 2020 at 07:37):

namespace fin

theorem lt_succ_iff {k} :  {m : fin (k+1)} {n : fin k},
  m < fin.succ n  m  cast_succ n
| m, _ n, _ := @nat.lt_succ_iff m n

end fin

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last _) = b)
(mono :  m : fin n, x (fin.cast_succ m)  x (fin.succ m))

lemma mono' {a b : } (P : partition a b) {i j : fin (P.n + 1)} : i  j  P.x i  P.x j :=
begin
  apply fin.induction_on j,
  { intro h, rw le_antisymm h (fin.zero_le _) },
  { intros j IH h,
    rcases lt_or_eq_of_le h with h | rfl,
    { exact (IH (fin.lt_succ_iff.1 h)).trans (P.mono _) },
    { refl } }
end

lemma a_le_all {a b : } (P : partition a b) (m : fin (P.n + 1)) : a  P.x m :=
by simpa [P.x_zero] using mono' P (fin.zero_le m)

lemma a_le_b {a b : } (P : partition a b) : a  b :=
by rw  P.x_last; apply a_le_all

lemma all_le_b {a b : } (P : partition a b) (m : fin (P.n + 1)) : P.x m  b :=
by simpa [P.x_last] using mono' P (fin.le_last m)

Patrick Thomas (Nov 07 2020 at 23:11):

Thank you.

Patrick Thomas (Nov 08 2020 at 00:17):

What is it in the mathlib definition of fin that allows for apply fin.induction_on j? It doesn't seem to work with my definition of fin.

Bryan Gin-ge Chen (Nov 08 2020 at 00:20):

docs#fin.induction_on is a lemma that's in mathlib about the mathlib definition of fin; you'd have to prove an analogue involving your fin for apply fin.induction_on to work with your type.

Patrick Thomas (Nov 08 2020 at 00:22):

Oh, right. Thank you.

Patrick Thomas (Nov 09 2020 at 05:19):

How would I get something that represents the maximum of an arbitrary choice of the ms in this example (that would be an upper bound for abs f on [a, b])?

import data.real.basic data.set.intervals

def is_bounded_on (a b : ) (f :   ) : Prop :=  M : ,  x  set.Icc a b, abs (f x)  M

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

example {a b : } (P : partition a b) (f :   ) :
( i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f)  is_bounded_on a b f :=
assume a0 :  i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
have s0 :  i : fin P.n,  m : ,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m := (
assume i : fin P.n,
a0 i
),
sorry

Patrick Thomas (Nov 10 2020 at 00:13):

Do I need to make some kind of inhabited data type?

Patrick Thomas (Nov 10 2020 at 03:48):

Hmm. Perhaps:

example {a b : } (P : partition a b) (f :   ) :
( i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f)  is_bounded_on a b f :=
assume a0 :  i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
let m := fun i : fin P.n, Exists.some (a0 i) in
sorry

Patrick Thomas (Nov 16 2020 at 03:02):

I was wondering if someone could help me understand what is going wrong with and how to fix s2:

import data.real.basic

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

example {a b : } (P : partition a b) : P.n = 0  a = b :=
assume a0 : P.n = 0,
have s0 : a = P.x 0 := eq.symm P.x_zero,
have s1 : P.x (fin.last P.n) = b := P.x_last,
have s2 : fin.last P.n = 0 := @eq.subst  (fun n : , fin.last P.n = fin.last n) P.n 0 a0 (eq.refl (fin.last P.n)),
have s3 : P.x 0 = b := eq.subst s2 s1,
eq.trans s0 s3

Patrick Thomas (Nov 16 2020 at 04:00):

I guess this works:

import data.real.basic

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

example {a b : } (P : partition a b) : P.n = 0  a = b :=
assume a0 : P.n = 0,
have s0 : a = P.x 0 := eq.symm P.x_zero,
have s1 : P.x (fin.last P.n) = b := P.x_last,
have s2 : fin.last P.n = 0 := fin.ext a0,
have s3 : P.x 0 = b := eq.subst s2 s1,
eq.trans s0 s3

Yakov Pechersky (Nov 16 2020 at 05:10):

Can I ask, is there a reason you prefer these tactic mode proofs?

Patrick Thomas (Nov 16 2020 at 05:12):

Do you mean non tactic? I just like to make it readable independent of Lean.

Yakov Pechersky (Nov 16 2020 at 06:53):

What parts of Lean would you consider lean dependent in reading? I find the "ext" and "eq.subst" more difficult to parse. I think of those to be pretty Lean dependent in reading.

Yakov Pechersky (Nov 16 2020 at 06:55):

Perhaps a calc style proof would be the most readable in such a case

Patrick Thomas (Nov 16 2020 at 18:26):

"I find the "ext" and "eq.subst" more difficult to parse. I think of those to be pretty Lean dependent in reading."
What would you replace them with?

Kevin Buzzard (Nov 16 2020 at 18:26):

tactics!

Patrick Thomas (Nov 16 2020 at 18:28):

I mean which tactics :)

Patrick Thomas (Nov 16 2020 at 18:28):

rw?

Kevin Buzzard (Nov 16 2020 at 18:30):

rw is the eq.subst tactic, yes. The tactic which does ext is in fact called ext :-)

Kevin Buzzard (Nov 16 2020 at 18:33):

import data.real.basic

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

example {a b : } (P : partition a b) : P.n = 0  a = b :=
begin
  rcases P with n, x, rfl, rfl, mono⟩,
  show n = 0  _,
  rintro rfl,
  congr',
end

Patrick Thomas (Nov 16 2020 at 18:34):

Personally I find that a lot harder to read, especially without Lean.

Kevin Buzzard (Nov 16 2020 at 18:35):

But you don't need to read this proof because the result is trivial.

Mario Carneiro (Nov 16 2020 at 18:36):

example {a b : } :  (P : partition a b), P.n = 0  a = b :=
by { rintro n, x, rfl, rfl, - (rfl : n = 0), refl }

Kevin Buzzard (Nov 16 2020 at 18:37):

example {a b : } (P : partition a b) : P.n = 0  a = b :=
begin
  -- Let n and x be the data associated to P
  rcases P with n, x, rfl, rfl, mono⟩,
  -- assume n = 0.
  show n = 0  _,
  rintro rfl,
  -- The goal is now to prove x 0 = x (fin.last 0)
  -- but this is trivial
  congr',
end

Reid Barton (Nov 16 2020 at 18:38):

(rfl : a = b) is a nice trick

Patrick Thomas (Nov 16 2020 at 18:38):

Kevin Buzzard said:

But you don't need to read this proof because the result is trivial.

Perhaps. I still like to though. Its too bad there isn't a mechanism to turn tactic proofs into something a mathematician without Lean could follow.

Kevin Buzzard (Nov 16 2020 at 18:39):

Well, I guess I can read some proofs fine without using Lean, because I can "be the compiler" (something Mario used to encourage me to do when I was a beginner).

Mario Carneiro (Nov 16 2020 at 18:39):

You can also do this in "term mode" using the equation compiler for a similar proof

example :  {a b : } (P : partition a b), P.n = 0  a = b
| _ _ n, x, rfl, rfl, _ rfl := rfl

Kevin Buzzard (Nov 16 2020 at 18:39):

But for long proofs, I agree, you are better off running a copy of Lean and looking at the code within it.

Mario Carneiro (Nov 16 2020 at 18:44):

But in case you haven't noticed yet, my strategy for making readable proofs is to get them over with as quickly as possible, which forces the proof to be pretty slick and hopefully convincing the reader that they didn't want to read the proof anyway

Mario Carneiro (Nov 16 2020 at 18:46):

For longer proofs, tactic mode is much better than term mode for conveying structure and order to the proof, and you don't really want to read these proofs without tool assistance anyway because the local context is super important and much harder to read in any static textual form

Mario Carneiro (Nov 16 2020 at 18:47):

The only static form I really think does the job is #explode / metamath proofs, which are crazy verbose unless you are really regimented about your context management

Patrick Thomas (Nov 16 2020 at 18:48):

What is #explode?

Mario Carneiro (Nov 16 2020 at 18:48):

It's a tactic that will print out a metamath style proof of any lean theorem

Patrick Thomas (Nov 16 2020 at 18:49):

Huh. Cool. I'll take a look.

Mario Carneiro (Nov 16 2020 at 18:49):

import tactic

#explode classical.em
classical.em :  (p : Prop), p  ¬p
0      p                                 Prop
1      _private.1778634979.not_uv_or_p   u p  v p  p
2      hne                                u p  v p
3      _private.4061111967.p_implies_uv   p  u p = v p
43,2   mt                                 ¬p
54     or.inr                             p  ¬p
62,5   I                                u p  v p  p  ¬p
7      or.inl                            p  p  ¬p
81,6,7 or.elim                           p  ¬p
90,8   I                                 (p : Prop), p  ¬p

Patrick Thomas (Nov 16 2020 at 18:52):

Interesting.

Yakov Pechersky (Nov 16 2020 at 19:02):

import data.real.basic

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

example {a b : } (P : partition a b) : P.n = 0  a = b :=
λ (h : P.n = 0),
have hn : fin.last P.n = 0, from fin.eq_of_veq h,
calc a = P.x 0 : P.x_zero.symm
...    = P.x (fin.last P.n) : congr_arg P.x hn.symm
...    = b : P.x_last

Yakov Pechersky (Nov 16 2020 at 19:06):

This gives the proof state explicitly, and the Lean steps to convert from one state to another. It's difficult to avoid "Lean-like" terms or syntax, because of fin.

Patrick Thomas (Nov 21 2020 at 03:58):

I'm a bit confused. Why does this compile, when s may not have type fin (n + 1)?

import data.real.basic

def blah (n : ) (f : fin (n + 1)  ) : Π (m : ), 
| 0        := f 0
| (s + 1)  := f s

Alex J. Best (Nov 21 2020 at 04:03):

You can do

#print blah._main

to see whats produced is

def polynomial.blah._main : Π (n : ), (fin (n + 1)  )     :=
λ (n : ) (f : fin (n + 1)  ) (m : ), m.cases_on (id_rhs  (f 0)) (λ (m : ), id_rhs  (f m))

Alex J. Best (Nov 21 2020 at 04:03):

So its coercing naturals to fin (n+1)

Patrick Thomas (Nov 21 2020 at 04:04):

What happens if m can not be coerced?

Alex J. Best (Nov 21 2020 at 04:06):

It always can be coerced, in this case it takes m mod n+1,

#eval ((7 : ) : fin 3) -- 1

Patrick Thomas (Nov 21 2020 at 04:07):

Huh. Why does it do that?

Patrick Thomas (Nov 21 2020 at 04:14):

I guess because it is defined to :)

Bryan Gin-ge Chen (Nov 21 2020 at 04:14):

Here's one way to find out:

import tactic
variables (n : )
#check (by apply_instance : has_coe_t  (fin (n+1)))
/-
nat.cast_coe : has_coe_t ℕ (fin (n + 1))
-/

That points to docs#nat.cast_coe, which is an instance that defines a coercion from to any type with has_zero, has_one and has_add.

Bryan Gin-ge Chen (Nov 21 2020 at 04:16):

Unfolding the definition, you get to src#nat.cast, which is defined as the following:

/-- Canonical homomorphism from `ℕ` to a type `α` with `0`, `1` and `+`. -/
protected def cast :   α
| 0     := 0
| (n+1) := cast n + 1

Bryan Gin-ge Chen (Nov 21 2020 at 04:19):

The way Lean finds coercions is explained in this section of TPiL.

Patrick Thomas (Nov 21 2020 at 04:29):

Thank you.

Mario Carneiro (Nov 21 2020 at 04:29):

FYI this cast is not recommended; you should use fin.last n instead

Patrick Thomas (Nov 21 2020 at 04:35):

Given a definition like the following, is there a way to supply some chosen parameters to it, and see what everything gets assigned to in each step as it unfolds, as a way to verify that it works as intended?

noncomputable def fin_max : Π (n : ) (f : fin (n + 1)  ), 
| 0       f := f 0
| (m + 1) f := max (f (m + 1)) (fin_max m (fun i : fin (m + 1), f i))

Mario Carneiro (Nov 21 2020 at 04:51):

Does it have to be ? That definition looks like it would work on any type

Mario Carneiro (Nov 21 2020 at 04:51):

If you use a computational type you can #eval it

Mario Carneiro (Nov 21 2020 at 04:53):

def fin_max {α} [linear_order α] : Π (n : ) (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (m + 1)) (fin_max m (fun i : fin (m + 1), f i))

#eval fin_max 5 (λ i, i.1 + 2) -- 7

Patrick Thomas (Nov 21 2020 at 04:53):

I was actually thinking in more general terms, for any inductive definition. Like it prints out:
iteration 0:
param_name_0 = ...
param_name_1 = ...

iteration 1:
param_name_0 = ...
param_name_1 = ...
...

Mario Carneiro (Nov 21 2020 at 04:56):

meta def fin_max {α} [linear_order α] [has_to_format α] : Π (n : ) (f : fin (n + 1)  α), α
| 0       f :=
  trace (to_string format!"iteration 0: {f 0}") $ f 0
| (m + 1) f :=
  let a := f (m + 1), b := fin_max m (fun i : fin (m + 1), f i) in
  trace (to_string format!"iteration {m + 1}: max {a} {b} = {max a b}") $
  max a b

#eval fin_max 5 (λ i, i.1 + 2) -- 7
-- iteration 0: 2
-- iteration 1: max 3 2 = 3
-- iteration 2: max 4 3 = 4
-- iteration 3: max 5 4 = 5
-- iteration 4: max 6 5 = 6
-- iteration 5: max 7 6 = 7

Patrick Thomas (Nov 21 2020 at 04:58):

Cool! Thanks!

Patrick Thomas (Nov 23 2020 at 02:49):

I can prove it, but is there an existing theorem that says that if i : fin 1 then i = 0? Is there also an existing theorem that breaks i : fin n + 1 into the cases i = fin.last n and i : fin n?

Kenny Lau (Nov 23 2020 at 02:51):

Probably Lean knows that fin 1 is a subsingleton

Kenny Lau (Nov 23 2020 at 02:52):

and the second question is probably answered by some sort of induction/cases

Yakov Pechersky (Nov 23 2020 at 02:59):

A recent commit added fin.eq_zero: https://github.com/leanprover-community/mathlib/commit/c4132e9ae950e8b28eafc964062311ff21fe4d08

Yakov Pechersky (Nov 23 2020 at 03:01):

What do you mean by breaking a fin (n + 1) into fin n? They're different types. Can you prove your statement for 0 : fin (n + 1) and using that, the inductive step? Then you can use fin.induction_on. Or if you have no need to induct, you can use refine fin.cases _ _ i. Do you need to break it into [0, n) and {n}? Then we can write fin.decreasing_induction

Patrick Thomas (Nov 23 2020 at 03:04):

I was thinking about an easier and more readable way to do the or.elim here:

import data.real.basic


def fin_max {α} [linear_order α] : Π (n : ) (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (fin.last (m + 1))) (fin_max m (fun i : fin (m + 1), f i.cast_succ))


example {α} [linear_order α] (n : ) (f : fin (n + 1)  α) :  i : fin (n + 1), f i  (fin_max n f) :=
begin
induction n,
case nat.zero {
  assume i : fin (0 + 1),
  have s0 : i.val  0 := fin.le_last i,
  have s1 : i.val = 0 := nat.eq_zero_of_le_zero s0,
  have s2 : i = 0 := fin.ext s1,
  have s3 : f i  f 0 := eq.subst s2 (le_refl (f i)),
  have s4 : fin_max 0 f = f 0 := eq.refl (fin_max 0 f),
  show f i  fin_max 0 f, from eq.subst (eq.symm s4) s3
},
case nat.succ : n IH {
  assume i : fin (n.succ + 1),
  let f' := fun i : fin n.succ, f i.cast_succ,

  have s5 : fin_max n.succ f = max (f (fin.last n.succ)) (fin_max n f') := eq.refl (fin_max n.succ f),

  have s6 : f (fin.last n.succ)  max (f (fin.last n.succ)) (fin_max n f') := le_max_left (f (fin.last n.succ)) (fin_max n f'),
  have s7 : f (fin.last n.succ)  fin_max n.succ f := eq.subst (eq.refl s5) s6,

  have s8 : fin_max n f'  max (f (fin.last n.succ)) (fin_max n f') := le_max_right (f (fin.last n.succ)) (fin_max n f'),
  have s9 : fin_max n f'  fin_max n.succ f := eq.subst (eq.refl s5) s8,

  have s10 : i.val  n.succ := fin.le_last i,
  have s11 : i.val < n.succ  i.val = n.succ := lt_or_eq_of_le s10,
  exact or.elim s11
  (
    assume a0 : i.val < n.succ,
    let i' := fin.mk i.val a0 in
    have s12 : f' i'  fin_max n f' := IH f' i',
    have s13 : f' i' = f i'.cast_succ := eq.refl (f' i'),
    have s14 : f i'.cast_succ  fin_max n f' := eq.subst s13 s12,
    have s15 : i'.cast_succ = i := fin.mk_coe i,
    have s16 : f i  fin_max n f' := eq.subst s15 s14,
    show f i  fin_max n.succ f, from le_trans s16 s9
  )
  (
    assume a1 : i.val = n.succ,
    have s17 : i = fin.last n.succ := fin.ext a1,
    show f i  fin_max n.succ f, from eq.subst (eq.symm s17) s7
  )
}
end

Yakov Pechersky (Nov 23 2020 at 03:25):

Does this help?

import data.real.basic

variables {α : Type*} [linear_order α] {n : }

def fin_max : Π {n : } (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (fin.last (m + 1))) (fin_max (fun i : fin (m + 1), f i.cast_succ))

example (f : fin (n + 1)  α) (i : fin (n + 1)) : f i  (fin_max f) :=
begin
  induction n with n hn,
  { have : i = 0 := by simp,
    simp only [this, fin_max] },
  {
    apply fin.induction_on i,
    { simp only [fin_max, le_max_iff],
      right,
      have : f 0 = (λ (k : fin (n + 1)), f k.cast_succ) 0 := rfl,
      rw this,
      apply hn },
    { sorry },
  }
end

Kenny Lau (Nov 23 2020 at 03:35):

import data.real.basic

variables {α : Type*} [linear_order α] {n : }

def fin_max : Π {n : } (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (fin.last (m + 1))) (fin_max (λ i : fin (m + 1), f i.cast_succ))

lemma le_fin_max (f : fin (n + 1)  α) (i : fin (n + 1)) : f i  fin_max f :=
begin
  induction n with n ih,
  { have : i = 0 := subsingleton.elim _ _,
    simp only [this, fin_max] },
  { by_cases hi : (i : ) < n.succ,
    { rw  fin.cast_succ_cast_lt i hi,
      exact le_max_right_of_le (ih (λ i : fin (n + 1), f i.cast_succ) (i.cast_lt hi)) },
    { rw fin.eq_last_of_not_lt hi,
      exact le_max_left _ _ } }
end

Patrick Thomas (Nov 23 2020 at 03:52):

Thank you both.

Patrick Thomas (Nov 28 2020 at 23:14):

How can I use my definition of fin.max in the last example? Should I change my definition or the statement of the lemmas somehow?

import algebra.order data.real.basic data.set.intervals

namespace hidden

structure fin (n : ) :=
(val : )
(prop : val < n)


lemma lt_lt_succ {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ {n : } : n < n + 1 := sorry
lemma succ_pos {n : } : 0 < n + 1 := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry


def fin.cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.val (lt_lt_succ a.prop)

def fin.succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.val + 1) (lt_succ_lt_succ a.prop)

instance {n : } : has_zero (fin (n + 1)) := {zero := @fin.mk (n + 1) 0 succ_pos}

def fin.last (n : ) : fin (n + 1) :=
@fin.mk (n + 1) n lt_succ


lemma fin.eq_of_veq {n : } {i j : fin n} : i.val = j.val  i = j := sorry


@[elab_as_eliminator] def fin.induction {n : } {C : fin (n + 1)  Sort*}
(h0 : C 0) (hs :  i : fin n, C i.cast_succ  C i.succ) : Π (i : fin (n + 1)), C i := sorry

@[elab_as_eliminator] def fin.induction_on {n : } (i : fin (n + 1)) {C : fin (n + 1)  Sort*}
(h0 : C 0) (hs :  i : fin n, C i.cast_succ  C i.succ) : C i := fin.induction h0 hs i


def fin.max {α} [linear_order α] : Π (n : ) (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (fin.last (m + 1))) (fin.max m (fun i : fin (m + 1), f (fin.cast_succ i)))


lemma fin.all_le_max {α} [linear_order α] (n : ) (f : fin (n + 1)  α) :  i : fin (n + 1), f i  (fin.max n f) :=
begin
induction n,
case nat.zero {
  -- f : fin (0 + 1) → α
  show  (i : fin (0 + 1)), f i  fin.max 0 f, from
  assume i : fin (0 + 1),
  have s0 : i.val < 1 := i.prop,
  have s1 : i.val = 0 := lt_one s0,
  have s2 : i = 0 := fin.eq_of_veq s1,
  have s3 : fin.max 0 f = f 0 := eq.refl (fin.max 0 f),
  have s4 : fin.max 0 f = f i := eq.subst (eq.symm s2) s3,
  show f i  fin.max 0 f, from eq.ge s4
},
case nat.succ : n IH {
  -- f : fin (n.succ + 1) → α
  -- IH : ∀ (f : fin (n + 1) → α) (i : fin (n + 1)), f i ≤ fin.max n f
  show  (i : fin (n.succ + 1)), f i  fin.max n.succ f, from
  assume i : fin (n.succ + 1),
  let f' : fin (n + 1)  α := fun i : fin n.succ, f (fin.cast_succ i) in
  have s5 : fin.max n.succ f = max (f (fin.last n.succ)) (fin.max n f') := eq.refl (fin.max n.succ f),
  have s6 : f (fin.last n.succ)  max (f (fin.last n.succ)) (fin.max n f') := le_max_left (f (fin.last n.succ)) (fin.max n f'),
  have s7 : f (fin.last n.succ)  fin.max n.succ f := eq.subst (eq.refl s5) s6,
  have s8 : fin.max n f'  max (f (fin.last n.succ)) (fin.max n f') := le_max_right (f (fin.last n.succ)) (fin.max n f'),
  have s9 : fin.max n f'  fin.max n.succ f := eq.subst (eq.refl s5) s8,
  have s10 : i.val < n.succ + 1 := i.prop,
  have s11 : i.val  n.succ := le_of_lt_succ s10,
  have s12 : i.val < n.succ  i.val = n.succ := lt_or_eq_of_le s11,
  show f i  fin.max n.succ f, from or.elim s12
  (
    assume a0 : i.val < n.succ,
    let i' : fin n.succ := fin.mk i.val a0 in
    have s13 : (fin.cast_succ i').val = i.val := eq.refl (fin.cast_succ i').val,
    have s14 : (fin.cast_succ i') = i := fin.eq_of_veq s13,
    have s15 : f' i'  fin.max n f' := IH f' i',
    have s16 : f' i' = f (fin.cast_succ i') := eq.refl (f' i'),
    have s17 : f (fin.cast_succ i')  fin.max n f' := eq.subst s16 s15,
    have s18 : f i  fin.max n f' := eq.subst s14 s15,
    show f i  fin.max n.succ f, from le_trans s18 s9
  )
  (
    assume a1 : i.val = n.succ,
    have s19 : i = fin.last n.succ := fin.eq_of_veq a1,
    show f i  fin.max n.succ f, from eq.subst (eq.symm s19) s7
  )
}
end


def is_bounded_on (a b : ) (f :   ) : Prop :=  M : ,  x  set.Icc a b, abs (f x)  M

lemma singleton_bounded (a : ) (f :   ) : is_bounded_on a a f :=
let M := abs (f a) in
have s0 :  x  set.Icc a a, abs (f x)  M := (
  assume x : ,
  assume a0 : x  set.Icc a a,
  have s1 : a  x  x  a := a0,
  have s2 : a  x := and.left s1,
  have s3 : x  a := and.right s1,
  have s4 : x = a := le_antisymm s3 s2,
  have s5 : abs (f x) = abs (f x) := eq.refl (abs (f x)),
  have s6 : abs (f x) = abs (f a) := eq.subst s4 s5,
  have s7 : abs (f x) = M := s6,
  eq.le s7
),
exists.intro M s0


structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)


lemma singleton_partition {a b : } (P : partition a b) : P.n = 0  a = b :=
assume a0 : P.n = 0,
have s0 : fin.last P.n = 0 := fin.eq_of_veq a0,
calc a = P.x 0              : eq.symm P.x_zero
...    = P.x (fin.last P.n) : congr_arg P.x (eq.symm s0)
...    = b                  : P.x_last


lemma partition_mem {a b : } (P : partition a b) : 0 < P.n   x  set.Icc a b,  i : fin P.n, x  set.Icc (P.x i.cast_succ) (P.x i.succ) :=
assume a0 : 0 < P.n,
assume x : ,
assume a1 : x  set.Icc a b,
by_contradiction (
  assume a2 : ¬  i : fin P.n, x  set.Icc (P.x i.cast_succ) (P.x i.succ),
  have s0 :  i : fin P.n, ¬ x  set.Icc (P.x i.cast_succ) (P.x i.succ) := sorry,
  have s1 : a  x := and.left a1,
  have s2 : a < x  a = x := lt_or_eq_of_le s1,
  or.elim s2
  (
    assume a3 : a < x,
    have s3 :  i : fin (P.n + 1), P.x i < x := (
      assume i : fin (P.n + 1),
      fin.induction_on i
      (
        have s4 : P.x 0 = a := P.x_zero,
        show P.x 0 < x, from eq.subst (eq.symm s4) a3
      )
      (
        assume i' : fin P.n,
        assume IH : P.x i'.cast_succ < x,
        have s5 : P.x i'.cast_succ  x := le_of_lt IH,
        have s6 : ¬ x  set.Icc (P.x i'.cast_succ) (P.x i'.succ) := s0 i',
        have s7 : ¬ ((P.x i'.cast_succ)  x  x  (P.x i'.succ)) := s6,
        have s8 : (P.x i'.cast_succ)  x  ¬ x  (P.x i'.succ) := sorry,
        have s9 : ¬ x  (P.x i'.succ) := s8 s5,
        show P.x i'.succ < x, from sorry
      )
    ),
    have s10 : P.x (fin.last P.n) < x := s3 (fin.last P.n),
    have s11 : P.x (fin.last P.n) = b := P.x_last,
    have s12 : b < x := eq.subst s11 s10,
    have s13 : ¬ x  b := sorry,
    have s14 : x  b := and.right a1,
    show false, from s13 s14
  )
  (
    assume a4 : a = x,
    have s15 : P.x (fin.mk 0 a0).cast_succ = a := P.x_zero,
    have s16 : P.x (fin.mk 0 a0).cast_succ  x := eq.trans_le s15 s1,
    have s17 : P.x (fin.mk 0 a0).cast_succ = x := eq.trans s15 a4,
    have s18 : P.x (fin.mk 0 a0).cast_succ  P.x (fin.mk 0 a0).succ := P.mono (fin.mk 0 a0),
    have s19 : x  P.x (fin.mk 0 a0).succ := eq.subst s17 s18,
    have s20 : x  set.Icc (P.x (fin.mk 0 a0).cast_succ) (P.x (fin.mk 0 a0).succ) := and.intro s16 s19,
    have s21 : ¬ x  set.Icc (P.x (fin.mk 0 a0).cast_succ) (P.x (fin.mk 0 a0).succ) := s0 (fin.mk 0 a0),
    show false, from s21 s20
  )
)


example {a b : } (P : partition a b) (f :   ) :
( i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f)  is_bounded_on a b f :=
assume a0 :  i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
have s0 :  i : fin P.n,  m : ,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m := a0,
have s1 : P.n = 0  0 < P.n := sorry,
or.elim s1
(
  assume a1 : P.n = 0,
  have s2 : a = b := singleton_partition P a1,
  have s3 : is_bounded_on a a f := singleton_bounded a f,
  eq.subst s2 s3
)
(
  assume a2 : 0 < P.n,
  let m := fun i : fin P.n, Exists.some (s0 i) in
  have s4 :  i : fin P.n,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m i := (
    assume i : fin P.n,
    Exists.some_spec (s0 i)
  ),
  let M := fin.max (P.n - 1) m in
  have s5 :  i : fin P.n, m i  M := fin.all_le_max (P.n - 1) m,
  have s6 :  x  set.Icc a b, abs (f x)  M := (
    assume x : ,
    assume a3 : x  set.Icc a b,
    have s7 :  i : fin P.n, x  set.Icc (P.x i.cast_succ) (P.x i.succ) := partition_mem P a2 x a3,
    exists.elim s7 (
      assume i : fin P.n,
      assume a4 : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
      have s8 : abs (f x)  m i := s4 i x a4,
      have s9 : m i  M := s5 i,
      show abs (f x)  M, from le_trans s8 s9
    )
  ),
  exists.intro M s6
)

end hidden

Kevin Buzzard (Nov 29 2020 at 00:59):

lemma lt_lt_succ {m n : } : m < n  m < n + 1 := by omega
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := by omega
lemma lt_succ {n : } : n < n + 1 := by omega
lemma succ_pos {n : } : 0 < n + 1 := by omega
lemma lt_one {n : } : n < 1  n = 0 := by omega
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := by omega

Kevin Buzzard (Nov 29 2020 at 01:00):

lemma fin.eq_of_veq {n : } {i j : fin n} : i.val = j.val  i = j :=
begin
  cases i, cases j,
  simp,
end

Kevin Buzzard (Nov 29 2020 at 01:04):

@[elab_as_eliminator] def fin.induction {n : } {C : fin (n + 1)  Sort*}
(h0 : C 0) (hs :  i : fin n, C i.cast_succ  C i.succ) : Π (i : fin (n + 1)), C i :=
begin
  rintro i, hi⟩,
  induction i with j hj,
    exact h0,
  convert hs j, _ (hj _),
  exact nat.lt_of_succ_lt_succ hi,
end

Kevin Buzzard (Nov 29 2020 at 01:15):

Your problem with fin.max can be seen from the error:

type mismatch at application
  fin.max (P.n - 1) m
term
  m
has type
  fin P.n → ℝ : Type
but is expected to have type
  fin (P.n - 1 + 1) → ?m_1 : Type ?

For a general natural number x, x-1+1 isn't equal to x. This is why you should avoid natural number subtraction. I would recommend using a2 : 0 < P.n to actually get your hands on some natural r such that P.n=r+1 and then using r instead. Like this: Add something like

lemma temp_lemma {n : } (hn : 0 < n) :  m : , n = m.succ :=
begin
  cases n, cases hn,
  use n,
end

(I'm surprised this isn't in the library) and then

...
    assume i : fin P.n,
    Exists.some_spec (s0 i)
  ),
  begin
    cases temp_lemma a2 with r hr,
    rw hr at m,
    set M := fin.max r m with hM,
    sorry
  end

(I'm switching to tactic mode because this proof is massive, doing it in term mode seems crazy to me).

Patrick Thomas (Nov 29 2020 at 01:22):

Thank you!

Patrick Thomas (Nov 29 2020 at 01:50):

Sorry, if you don't mind, how would you handle the rw hr at m without tactics?

Patrick Thomas (Nov 29 2020 at 04:00):

I think I got it.

example {a b : } (P : partition a b) (f :   ) :
( i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f)  is_bounded_on a b f :=
assume a0 :  i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
have s0 :  i : fin P.n,  m : ,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m := a0,
have s1 : P.n = 0  0 < P.n := sorry,
or.elim s1
(
  assume a1 : P.n = 0,
  have s2 : a = b := singleton_partition P a1,
  have s3 : is_bounded_on a a f := singleton_bounded a f,
  eq.subst s2 s3
)
(
  assume a2 : 0 < P.n,
  let m := fun i : fin P.n, Exists.some (s0 i) in
  have s4 :  i : fin P.n,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m i := (
    assume i : fin P.n,
    Exists.some_spec (s0 i)
  ),
  have s5 :  r : , P.n = r + 1 := exists_succ_eq a2,
  exists.elim s5
  (
    assume r : ,
    assume a3 : P.n = r + 1,
    let m' := fun i : fin (r + 1), m (@fin.mk P.n i.val (eq.subst (eq.symm a3) (i.prop))) in
    let M := fin.max r m' in
    have s6 :  i : fin P.n, m i  M := (
      assume i : fin P.n,
      have s7 : i.val < P.n := i.prop,
      have s8 : i.val < (r + 1) := eq.subst a3 s7,
      let i' := @fin.mk (r + 1) i.val s8 in
      have s9 : m' i' = m i := eq.refl (m' i'),
      have s10 : m' i'  M := fin.all_le_max r m' i',
      show m i  M, from eq.subst s9 s10
    ),
    have s11 :  x  set.Icc a b, abs (f x)  M := (
      assume x : ,
      assume a4 : x  set.Icc a b,
      have s12 :  i : fin P.n, x  set.Icc (P.x i.cast_succ) (P.x i.succ) := partition_mem P a2 x a4,
      exists.elim s12 (
        assume i : fin P.n,
        assume a4 : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
        have s13 : abs (f x)  m i := s4 i x a4,
        have s14 : m i  M := s6 i,
        show abs (f x)  M, from le_trans s13 s14
      )
    ),
    exists.intro M s11
  )
)

Patrick Thomas (Nov 29 2020 at 19:47):

What is the correct way to define the function t here?

example (a b : ) (f :   ) : ( R : , is_riemann_integral a b f R)  is_bounded_on a b f :=
assume a0 :  R : , is_riemann_integral a b f R,
by_contradiction (
  assume a1 : ¬ is_bounded_on a b f,
  exists.elim a0 (
    assume R : ,
    assume a2 : is_riemann_integral a b f R,
    let ε :  := 1 in
    have s0 : ε > 0 := sorry,
    have s1 :  δ : , δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := a2 ε s0,
    exists.elim s1 (
      assume δ : ,
      assume a3 : δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε,
      have s2 : δ > 0 := and.left a3,
      have s3 :  P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := and.right a3,
      have s4 :  P : partition a b, norm P < δ := norm_delta_exists δ s2,
      exists.elim s4 (
        assume P : partition a b,
        assume a4 : norm P < δ,
        have s5 :  Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := s3 P a4,
        have s6 :  i : fin P.n, ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f := sorry,
        exists.elim s6 (
          assume i : fin P.n,
          assume a5 : ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
          let Q := default (tagged_partition P) in
          let R := riemann_sum Q f in
          let S := f (Q.t i) * ((P.x i.succ) - (P.x i.cast_succ)) in
          let T := R - S in
          have s7 :  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε := sorry,
          exists.elim s7 (
            assume x : ,
            assume a6 :  (H : x  set.Icc (P.x i.cast_succ) (P.x i.succ)), abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε,
            exists.elim a6 (
              assume H : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
              assume a7 : abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε,
              let t : (fin P.n)   := fun j : (fin P.n), if j = i then x else Q.t j in
            )
          )
        )
      )
    )
  )
)

Kevin Buzzard (Nov 29 2020 at 21:55):

I can't make this compile. Can you give a #mwe ?

Patrick Thomas (Nov 29 2020 at 22:12):

I'm trying to fix the error in the definition of t. Actually, I think this is going to be a mess dealing with rearranging the sum, but I don't know of a way to make it any easier.

import algebra.order data.real.basic data.set.intervals

namespace hidden

structure fin (n : ) :=
(val : )
(prop : val < n)


lemma lt_lt_succ {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ {n : } : n < n + 1 := sorry
lemma succ_pos {n : } : 0 < n + 1 := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry
lemma exists_succ_eq {n : } (hn : 0 < n) :  m : , n = m + 1 := sorry
lemma zero_le {n : } : 0  n := sorry

def fin.cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.val (lt_lt_succ a.prop)

def fin.succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.val + 1) (lt_succ_lt_succ a.prop)

instance {n : } : has_zero (fin (n + 1)) := {zero := @fin.mk (n + 1) 0 succ_pos}

def fin.last (n : ) : fin (n + 1) :=
@fin.mk (n + 1) n lt_succ


def is_bounded_on (a b : ) (f :   ) : Prop :=  M : ,  x  set.Icc a b, abs (f x)  M


structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)


noncomputable def norm {a b : } (P : partition a b) :  := sorry

lemma norm_delta_exists {a b : } :  δ : , δ > 0   P : partition a b, norm P < δ := sorry


structure tagged_partition {a b : } (P : partition a b) :=
(t : fin P.n  )
(mem_block :  m : fin P.n, t m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : partition a b) : inhabited (tagged_partition P) := sorry


def riemann_sum {a b : } {P : partition a b} (Q : tagged_partition P) (f :   ) :  := sorry


def is_riemann_integral (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0   δ : , δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε


example (a b : ) (f :   ) : ( R : , is_riemann_integral a b f R)  is_bounded_on a b f :=
assume a0 :  R : , is_riemann_integral a b f R,
by_contradiction (
  assume a1 : ¬ is_bounded_on a b f,
  exists.elim a0 (
    assume R : ,
    assume a2 : is_riemann_integral a b f R,
    let ε :  := 1 in
    have s0 : ε > 0 := sorry,
    have s1 :  δ : , δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := a2 ε s0,
    exists.elim s1 (
      assume δ : ,
      assume a3 : δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε,
      have s2 : δ > 0 := and.left a3,
      have s3 :  P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := and.right a3,
      have s4 :  P : partition a b, norm P < δ := norm_delta_exists δ s2,
      exists.elim s4 (
        assume P : partition a b,
        assume a4 : norm P < δ,
        have s5 :  Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := s3 P a4,
        have s6 :  i : fin P.n, ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f := sorry,
        exists.elim s6 (
          assume i : fin P.n,
          assume a5 : ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
          let Q := default (tagged_partition P) in
          let R := riemann_sum Q f in
          let S := f (Q.t i) * ((P.x i.succ) - (P.x i.cast_succ)) in
          let T := R - S in
          have s7 :  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε := sorry,
          exists.elim s7 (
            assume x : ,
            assume a6 :  (H : x  set.Icc (P.x i.cast_succ) (P.x i.succ)), abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε,
            exists.elim a6 (
              assume H : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
              assume a7 : abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε,
              let t : (fin P.n)   := fun j : (fin P.n), if j = i then x else Q.t j in
            )
          )
        )
      )
    )
  )
)

end hidden

Yakov Pechersky (Nov 29 2020 at 23:19):

Here's a close to your state, but in tactic format, which is easier for me to parse:

example (a b : ) (f :   ) : ( R : , is_riemann_integral a b f R)  is_bounded_on a b f :=
begin
  rintro sum, hsum⟩,
  by_contra H,
  set ε :  := 1 with ,
  have εpos : 0 < ε := by { rw , exact zero_lt_one },
  obtain δ, δpos,  :  δ : , 0 < δ 
     (P : partition a b), norm P < δ   (tP : tagged_partition P), abs ((riemann_sum tP f) - sum) < ε := hsum ε εpos,
  obtain P, hP :  (P : partition a b), norm P < δ := norm_delta_exists δ δpos,
  have htag :  (tP : tagged_partition P), abs ((riemann_sum tP f) - sum) < ε :=  P hP,
  obtain i, hi :  (i : fin P.n), ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f := sorry,
  set tP : tagged_partition P := default _ with htP,
  set tagged_sum :  := riemann_sum tP f with htsum,
  set rect :  := f (tP.t i) * ((P.x i.succ) - (P.x i.cast_succ)) with hrect,
  set overflow :  := tagged_sum - rect with hover,
  have htpmem : tP.t i  set.Icc (P.x i.cast_succ) (P.x i.succ) := tP.mem_block i,
  obtain x, hx, hx' :  x  set.Icc (P.x i.cast_succ) (P.x i.succ),
    ε  abs ((overflow + (f x) * ((P.x i.succ - P.x i.cast_succ))) - sum) := sorry,
  unfold is_bounded_on at H hi,
  push_neg at H hi,
  sorry
end

Patrick Thomas (Nov 30 2020 at 05:05):

Now we need to create a new tagged partition that uses the x from the last obtain right? That is what I am struggling with.

Yakov Pechersky (Nov 30 2020 at 07:03):

Well I think that you would have to make that definition and associated API outside of the proof context.

Yakov Pechersky (Nov 30 2020 at 07:03):

Right now you have no formalized way of constructing tagged partitions at all, your inhabited instance (which really encodes data, and not proof) is sorried.

Patrick Thomas (Nov 30 2020 at 22:05):

Does this work?

instance {a b : } (P : partition a b) : inhabited (tagged_partition P) := {
  default := {
    t := fun i : fin P.n, P.x i.cast_succ,
    mem_block := (
      assume m : fin P.n,
      have s0 : P.x m.cast_succ  P.x m.cast_succ := le_refl (P.x m.cast_succ),
      have s1 : P.x m.cast_succ  P.x m.succ := P.mono m,
      and.intro s0 s1
    )
  }
}

I'm still not sure how to construct a new tagged partition using x. I think that has to be done? Is there a better approach to this proof? Different definitions or statements of the theorems?

Patrick Thomas (Nov 30 2020 at 23:06):

A possibly more minimal MWE:

import algebra.order data.real.basic data.set.intervals

namespace hidden

structure fin (n : ) :=
(val : )
(prop : val < n)


lemma lt_lt_succ {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ {n : } : n < n + 1 := sorry
lemma succ_pos {n : } : 0 < n + 1 := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry
lemma exists_succ_eq {n : } (hn : 0 < n) :  m : , n = m + 1 := sorry
lemma zero_le {n : } : 0  n := sorry

def fin.cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.val (lt_lt_succ a.prop)

def fin.succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.val + 1) (lt_succ_lt_succ a.prop)

instance {n : } : has_zero (fin (n + 1)) := {zero := @fin.mk (n + 1) 0 succ_pos}

def fin.last (n : ) : fin (n + 1) :=
@fin.mk (n + 1) n lt_succ


structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)


structure tagged_partition {a b : } (P : partition a b) :=
(t : fin P.n  )
(mem_block :  m : fin P.n, t m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : partition a b) : inhabited (tagged_partition P) := {
  default := {
    t := fun i : fin P.n, P.x i.cast_succ,
    mem_block := (
      assume m : fin P.n,
      have s0 : P.x m.cast_succ  P.x m.cast_succ := le_refl (P.x m.cast_succ),
      have s1 : P.x m.cast_succ  P.x m.succ := P.mono m,
      and.intro s0 s1
    )
  }
}

def tagged_partition_replace {a b : } {P : partition a b} (Q : tagged_partition P)
(i : fin P.n) (x : ) (h0 : x  set.Icc (P.x i.cast_succ) (P.x i.succ)) : tagged_partition P := {
  t := fun j : (fin P.n), if j = i then x else Q.t j,
  mem_block := sorry
}

end hidden

Yakov Pechersky (Nov 30 2020 at 23:20):

You still need to come up with a way of generating a tagged_partition P to begin with

Patrick Thomas (Nov 30 2020 at 23:22):

import algebra.order data.real.basic data.set.intervals

namespace hidden

structure fin (n : ) :=
(val : )
(prop : val < n)


lemma lt_lt_succ {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ {n : } : n < n + 1 := sorry
lemma succ_pos {n : } : 0 < n + 1 := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry
lemma exists_succ_eq {n : } (hn : 0 < n) :  m : , n = m + 1 := sorry
lemma zero_le {n : } : 0  n := sorry

def fin.cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.val (lt_lt_succ a.prop)

def fin.succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.val + 1) (lt_succ_lt_succ a.prop)

instance {n : } : has_zero (fin (n + 1)) := {zero := @fin.mk (n + 1) 0 succ_pos}

def fin.last (n : ) : fin (n + 1) :=
@fin.mk (n + 1) n lt_succ


structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)


structure tagged_partition {a b : } (P : partition a b) :=
(t : fin P.n  )
(mem_block :  m : fin P.n, t m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : partition a b) : inhabited (tagged_partition P) := {
  default := {
    t := fun i : fin P.n, P.x i.cast_succ,
    mem_block := (
      assume m : fin P.n,
      have s0 : P.x m.cast_succ  P.x m.cast_succ := le_refl (P.x m.cast_succ),
      have s1 : P.x m.cast_succ  P.x m.succ := P.mono m,
      and.intro s0 s1
    )
  }
}

def tagged_partition_replace {a b : } {P : partition a b} (Q : tagged_partition P)
(i : fin P.n) (x : ) (h0 : x  set.Icc (P.x i.cast_succ) (P.x i.succ)) : tagged_partition P := {
  t := fun j : (fin P.n), if j = i then x else Q.t j,
  mem_block := sorry
}

end hidden

Patrick Thomas (Nov 30 2020 at 23:30):

I'm trying to resolve this error:

failed to synthesize type class instance for
a b : ,
P : partition a b,
Q : tagged_partition P,
i : fin P.n,
x : ,
h0 : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
j : fin P.n
 decidable (j = i)

Kevin Buzzard (Nov 30 2020 at 23:31):

open_locale classical will make it go away

Yakov Pechersky (Nov 30 2020 at 23:32):

And not defining your own fin.

Yakov Pechersky (Nov 30 2020 at 23:33):

In fact, you don't need open_locale classical if you don't define your own fin

Patrick Thomas (Nov 30 2020 at 23:33):

What is different about my fin that causes this?

Yakov Pechersky (Nov 30 2020 at 23:35):

You didn't prove a decidable equality instance for it. Which, you have two options for, either assume classical, or say that decidable equality of the values makes them equal.

Patrick Thomas (Nov 30 2020 at 23:38):

What actually does it mean for two instances of a structure to be equal in Lean? Is that a built in definition somewhere?

Kevin Buzzard (Nov 30 2020 at 23:39):

Normally if you make a new structure then straight afterwards you prove an extensionality lemma, which is a practical way to prove that two instances are equal.

Kevin Buzzard (Nov 30 2020 at 23:40):

But more recently people got sick of this and so now you can put @[derive ext] just before your structure definition, and then the exttactic will do the best it can to prove a sensible theorem of the form "if the data parts are equal, then the instances are equal"

Yakov Pechersky (Nov 30 2020 at 23:40):

import algebra.order data.real.basic data.set.intervals

namespace hidden

structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x 0 = a)
(x_last : x (fin.last n) = b)
(mono :  m : fin n, x m.cast_succ  x m.succ)

structure tagged_partition {a b : } (P : partition a b) :=
(t : fin P.n  )
(mem_block :  m : fin P.n, t m  set.Icc (P.x m.cast_succ) (P.x m.succ))

def default_tp {a b : } (P : partition a b) : tagged_partition P :=
λ i, P.x i.cast_succ, λ m, le_rfl, P.mono m⟩⟩

instance {a b : } {P : partition a b} : inhabited (tagged_partition P) := default_tp P

def tagged_partition_replace {a b : } {P : partition a b} (Q : tagged_partition P)
(i : fin P.n) (x : ) (h0 : x  set.Icc (P.x i.cast_succ) (P.x i.succ)) : tagged_partition P :=
function.update Q.t i x, begin
  intros m,
  by_cases hm : (m = i),
  { simpa only [hm, function.update_apply, if_true, eq_self_iff_true] using h0 },
  { simpa only [hm, function.update_noteq, ne.def, not_false_iff] using Q.mem_block m},
end

end hidden

Patrick Thomas (Nov 30 2020 at 23:42):

Kevin Buzzard said:

But more recently people got sick of this and so now you can put @[derive ext] just before your structure definition, and then the exttactic will do the best it can to prove a sensible theorem of the form "if the data parts are equal, then the instances are equal"

What is the definition of 'the instances are equal' that has to be proven?

Kevin Buzzard (Nov 30 2020 at 23:43):

the data fields are equal.

Patrick Thomas (Nov 30 2020 at 23:44):

What is the difference between 'the data parts are equal' and 'the data fields are equal'?

Kevin Buzzard (Nov 30 2020 at 23:44):

nothing

Kevin Buzzard (Nov 30 2020 at 23:44):

two complex numbers are equal if and only if their real and imaginary parts are equal

Kevin Buzzard (Nov 30 2020 at 23:45):

two terms of type fin n are equal if the natural parts are equal, I don't need to worry about whether the proofs are equal.

Patrick Thomas (Nov 30 2020 at 23:45):

I thought you said we have to prove that 'if the data parts are equal, then the instances are equal'.

Kevin Buzzard (Nov 30 2020 at 23:45):

Yes.

Patrick Thomas (Nov 30 2020 at 23:46):

Um, sorry, this seems circular.

Kevin Buzzard (Nov 30 2020 at 23:47):

There's an example

Kevin Buzzard (Nov 30 2020 at 23:47):

It's the point in mathlib where it is proved that two complex numbers are equal if their real and imaginary parts are equal.

Kevin Buzzard (Nov 30 2020 at 23:48):

But it needed to be proved.

Yakov Pechersky (Nov 30 2020 at 23:48):

Here's how core Lean does it for fin:

instance (n : nat) : decidable_eq (fin n) :=
λ i j, decidable_of_decidable_of_iff
  (nat.decidable_eq i.val j.val) eq_of_veq, veq_of_eq

Kevin Buzzard (Nov 30 2020 at 23:49):

If you make a new structure, it's your job to make a useful test for equality of terms of that structure.

Yakov Pechersky (Nov 30 2020 at 23:50):

In any case, just use regular ol' fin instead of spinning your own

Yakov Pechersky (Nov 30 2020 at 23:50):

Unless you have some issues with it?

Kevin Buzzard (Nov 30 2020 at 23:50):

Yakov's code is a proof that there's an algorithm to determine equality of two terms of type fin n, and the proof is "we already know there's an algorithm to check to see if two natural numbers are equal, and all the rest is noise"

Yakov Pechersky (Nov 30 2020 at 23:50):

I mean, you're using \R for reals, so why not use fin as provided?

Yakov Pechersky (Nov 30 2020 at 23:51):

I don't agree that it's "just noise", someone does have to write the eq_of_veq and veq_of_eq, which is what is needed for the custom fin

Kevin Buzzard (Nov 30 2020 at 23:52):

If you don't use mathlib's fin then it's your job to make all the bells and whistles which you'll need to make your fin usable.

Yakov Pechersky (Nov 30 2020 at 23:52):

It's just the tedium of formalization, even more tedious than plain old real analysis

Yakov Pechersky (Nov 30 2020 at 23:54):

In any case, this is all a detour from your partition question, to which I provided a definition that works above. In this sort of formalization, you have to choose how far "down the rabbit hole" you want to go. I think it's fine to sorry the lemmas about fin behavior, etc, just know that function.update expects a decidable_eq instance (which you can also sorry, or do open_locale_classical or whatever). Since you aren't really working on formalizing fin, but something about the summability of partitions, I think it's fine to sorry it.

Patrick Thomas (Nov 30 2020 at 23:55):

I was just using my own fin to make sure I understood how it worked. I can abandon it I guess.

Yakov Pechersky (Nov 30 2020 at 23:55):

I used function.update because it comes with nice lemmas and API about how to deal with when things are equal or not. If you prefer the if j = i then x else ... that forces a classical context anyway.

Yakov Pechersky (Nov 30 2020 at 23:56):

And then you would use if_pos and if_neg instead of function.update_apply and function.update_noteq

Yakov Pechersky (Nov 30 2020 at 23:56):

"how it worked" is a scary hole to go down..., but laden with great questions!

Yakov Pechersky (Nov 30 2020 at 23:57):

I hope that some of that explanation re fin was useful. If you're interested, we can discuss that more, or focus more on the partition problem

Yakov Pechersky (Nov 30 2020 at 23:57):

I've looked down a lot of the fin hole, but haven't looked at all how the reals are defined...

Patrick Thomas (Nov 30 2020 at 23:58):

I guess I'll focus on the partition problem for now.

Patrick Thomas (Nov 30 2020 at 23:59):

Thank you!

Yakov Pechersky (Dec 01 2020 at 00:00):

Even if we use if ... then ... else ... it still is unhappy about decidable. So you can just do open_locale classical to avoid that

Yakov Pechersky (Dec 01 2020 at 00:00):

In any case, here's an equivalent definition in if then else style:

def tagged_partition_replace' {a b : } {P : partition a b} (Q : tagged_partition P)
(i : fin P.n) (x : ) (h0 : x  set.Icc (P.x i.cast_succ) (P.x i.succ)) : tagged_partition P :=
λ j, if j = i then x else Q.t j, begin
  intros m,
  split_ifs with hm,
  { simpa [hm] using h0 },
  { exact Q.mem_block m },
end

Patrick Thomas (Dec 01 2020 at 00:02):

Cool.

Yakov Pechersky (Dec 01 2020 at 00:03):

where split_ifs knows how to break the if then else into two cases and give you the resulting goals

Reid Barton (Dec 01 2020 at 00:05):

Patrick Thomas said:

Kevin Buzzard said:

But more recently people got sick of this and so now you can put @[derive ext] just before your structure definition, and then the exttactic will do the best it can to prove a sensible theorem of the form "if the data parts are equal, then the instances are equal"

What is the definition of 'the instances are equal' that has to be proven?

Equal as in =, which is defined uniformly for all types, as an inductive type

Patrick Thomas (Dec 01 2020 at 00:11):

Hmm. Ok.

Patrick Thomas (Dec 01 2020 at 00:12):

I had looked at the definition of equal earlier, and had been surprised to see that it was defined inductively, but had set aside worrying about it until later :)

Kevin Buzzard (Dec 01 2020 at 00:13):

Looking at the definition doesn't really help. Equality in type theory is something you just get used to.

Kevin Buzzard (Dec 01 2020 at 00:13):

N=Z\mathbb{N}=\mathbb{Z} is neither provable nor disprovable in Lean.

Patrick Thomas (Dec 01 2020 at 00:14):

Is that a statement that the types are equal?

Reid Barton (Dec 01 2020 at 00:14):

You can just think of = as built-in, as the thing that lets you subst (or rw, etc.)

Kevin Buzzard (Dec 01 2020 at 00:14):

Right. Equality of types is really random.

Kevin Buzzard (Dec 01 2020 at 00:15):

Equality of terms is a bit saner, but even then it's still quite random. If you've played the natural number game you'll know that if n : nat then 0 + n = n and n + 0 = n, but one of these can be proved by refl and the other can't, because the internal definition of + is asymmetric.

Patrick Thomas (Dec 01 2020 at 00:16):

Yes, I remember that.

Kevin Buzzard (Dec 01 2020 at 00:16):

Both are true, but they're true for different reasons.

Kevin Buzzard (Dec 01 2020 at 00:17):

So when you're talking about whether two instances of a structure are equal, you can ask whether they're equal by definition, or whether they can be proved to be equal, and these are two different questions. As a mathematician I tend to disregard definitional equality, this is some implementation-dependent question. This is why I tag my structures with @[derive ext] and take the theorem which is on offer.

Patrick Thomas (Dec 01 2020 at 00:20):

Is equal by definition the same as the lamba calculus equality? I forget what it is called, beta reduction or something?

Kevin Buzzard (Dec 01 2020 at 00:20):

Lean just has some random set of rules about what is equal by definition. Just above that complex.ext link above is the definition of complex.eta, which is the theorem that if you start with a complex number z, and then make the complex number whose real part is re(z) and whose imaginary part is im(z), then the complex number you get is z. These two complex numbers are not definitionally equal however. Why not? Don't ask me, this is all part of Lean's definition of definitionally equal, and the issues here are well beyond my understanding of type theory.

Kevin Buzzard (Dec 01 2020 at 00:21):

Yeah exactly, this reduction and that reduction. I guess the thing I just said must be eta reduction if the lemma is called eta. In the reference manual there's a list of which greek letter reductions are true by definition, and then the other ones aren't.

Kevin Buzzard (Dec 01 2020 at 00:21):

https://leanprover.github.io/reference/expressions.html#computation

Kevin Buzzard (Dec 01 2020 at 00:22):

This is a really careful definition of what definitional equality is (although I'm always confused by it because there is some theorem about quotients whose proof is rfl and it's not mentioned there)

Kevin Buzzard (Dec 01 2020 at 00:22):

eta equivalence for functions is on the list, eta equivalence for structures is not. Go figure. These are subtle design issues.

Kevin Buzzard (Dec 01 2020 at 00:23):

What matters (to me) is not what is true by definition, but what is true (or more precisely what is provable).

Yakov Pechersky (Dec 01 2020 at 00:31):

Kevin Buzzard said:

[...] then make the complex number whose real part is re(z) and whose imaginary part is im(z), then the complex number you get is z. These two complex numbers are not definitionally equal however.

In my mind, I hand-wave that as the difference between:

mk (re (mk a b)) (im (mk a b)) = mk a b

and

mk a b = mk a b

Kevin Buzzard (Dec 01 2020 at 00:32):

But mk (re (mk a b)) (im (mk a b)) = mk a b probably _is_ definitional!

Kevin Buzzard (Dec 01 2020 at 00:32):

import data.complex.basic

open complex

example (a b : ) :
  mk (re (mk a b)) (im (mk a b)) = mk a b := rfl

Kevin Buzzard (Dec 01 2020 at 00:33):

import data.complex.basic

open complex

example (z : ) :
  mk (re z) (im z) = z := rfl -- fails

Kevin Buzzard (Dec 01 2020 at 00:33):

import data.complex.basic

open complex

example (z : ) :
  mk (re z) (im z) = z := by cases z; refl -- works

Yakov Pechersky (Dec 01 2020 at 00:34):

Is some lemma somewhere tagged with [refl]in one case and not in another?

Kevin Buzzard (Dec 01 2020 at 00:34):

no, the difference is simply the difference between z : \C and complex.mk a b : \C

Kevin Buzzard (Dec 01 2020 at 00:35):

This is exactly how you prove the ext lemmas: if you have a b : X where X is your structure, then you do cases on a and b and then let the dust settle.

Yakov Pechersky (Dec 01 2020 at 00:35):

Fascinating

Kevin Buzzard (Dec 01 2020 at 00:35):

crazy, if you ask me

Yakov Pechersky (Dec 01 2020 at 00:35):

type mismatch, term
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  {re := z.re, im := z.im} = z

Kevin Buzzard (Dec 01 2020 at 00:36):

right. But if you take z apart, it works fine.

Kevin Buzzard (Dec 01 2020 at 00:36):

because re (mk a b) = a is definitional, because some greek letter happens to be in some set of definitional greek letters.

Kevin Buzzard (Dec 01 2020 at 00:37):

I think this might all go back to all those fractions which stop me getting past page 1 of Mario's thesis.

Kevin Buzzard (Dec 01 2020 at 00:38):

https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf

Kevin Buzzard (Dec 01 2020 at 00:39):

Oh it's p6 where the fractions start.

Kevin Buzzard (Dec 01 2020 at 00:41):

Maybe something on page 8, 9 or 10 says re (mk a b) = a is definitional. But for me definitional equality is not important, the only things I know about it are things I've randomly picked up when making stuff like the complex number game.

Yakov Pechersky (Dec 01 2020 at 00:42):

I guess mk a b is a nice pleasant structured z unlike z \in

0=n=11nz{\displaystyle 0 =\sum _{n=1}^{\infty }{\frac {1}{n^{z}}}}

Reid Barton (Dec 01 2020 at 00:44):

Kevin Buzzard said:

Maybe something on page 8, 9 or 10 says re (mk a b) = a is definitional. But for me definitional equality is not important, the only things I know about it are things I've randomly picked up when making stuff like the complex number game.

fwiw, it's the first "fraction" (inference rule) in section 2.6.4, on page 12

Kevin Buzzard (Dec 01 2020 at 00:45):

After failed attempts at explaining to undergraduate mathematicians why 0 + n = n needed a proof but n + 0 = n was true by definition, I gave up, told them that add_zero was an axiom, disabled post-refl testing in rw and the natural number game in its current form was born, where people have to rw add_zero, refl to prove n + 0 = n even though refl would do it (but they don't know this, although people discover it by accident and file bug reports).

Reid Barton (Dec 01 2020 at 00:46):

You could even use constant/axiom to introduce +, but maybe it would be too disruptive

Kevin Buzzard (Dec 01 2020 at 00:47):

maybe I'll try that for the filter game.

Kevin Buzzard (Dec 01 2020 at 00:48):

maybe not.

Kevin Buzzard (Dec 01 2020 at 00:48):

Aah! So it's iota reduction.

Patrick Thomas (Dec 01 2020 at 03:27):

I'm guessing there are already theorems for this example, and others, like rearranging sums, splitting sums, etc, in mathlib using finset or fintype?

def fin.sum {α : Type} [has_add α] : Π (n : ) (x : fin (n + 1)  α), α
| 0       x := x 0
| (m + 1) x := x (fin.last (m + 1)) + (fin.sum m (fun i : fin (m + 1), x (fin.cast_succ i)))

example {α : Type} [has_add α] [has_sub α] (n : ) (x₀ x₁ : fin (n + 1)  α) (j : fin (n + 1))
(h0 :  i : fin (n + 1), ¬ i = j  x₁ i = x₀ i) :
fin.sum n x₁ = fin.sum n x₀ - x₀ j + x₁ j := sorry

Patrick Thomas (Dec 01 2020 at 03:44):

Hmm. Could probably use finset.add_sum_diff_singleton.

Patrick Thomas (Dec 01 2020 at 03:49):

How do you make a finset from fin using finset.mk?

Patrick Thomas (Dec 01 2020 at 04:01):

If I click on the source for https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html#finset.sum it takes me to the definition for finset.prod, and I can't seem to find the definition for finset.sum.

Alex J. Best (Dec 01 2020 at 04:34):

It's defined automatically from the prod definition via the to_additive attribute. This is a metaprogram that converts addition symbols in the definition to multiplication and defines the analogous definition with the word prod replaced with sum

Patrick Thomas (Dec 01 2020 at 04:35):

Oh. Ok. Thank you.

Bryan Gin-ge Chen (Dec 01 2020 at 04:36):

Related: attr#to_additive

Patrick Thomas (Dec 01 2020 at 05:19):

Is this actually not possible, because there is no guarantee that the function maps to all unique values?

def fin_fn_to_finset {α : Type} {n : } (f : fin n  α) : finset α :=
finset.mk (list.of_fn f) sorry

Patrick Thomas (Dec 01 2020 at 05:20):

And if I forced it, then the sums etc. using finset would not be as expected.

Patrick Thomas (Dec 01 2020 at 05:23):

(deleted)

Kevin Buzzard (Dec 01 2020 at 09:30):

I think the sum stuff in algebra.big_operators will work over any fintype (and fin n is a fintype), but it might be worth writing explicit stuff for fin anyway because there are more possibilities for induction principlles.

Yakov Pechersky (Dec 02 2020 at 01:21):

@Patrick Thomas

import data.fintype.card

open_locale big_operators

example {α : Type*} [ring α] {n : } (x₀ x₁ : fin (n + 1)  α) (j : fin (n + 1))
  (h0 :  i : fin (n + 1), ¬ i = j  x₁ i = x₀ i) :
  ( i, x₁ i) = ( i, x₀ i) - x₀ j + x₁ j :=
begin
  rw fin.sum_univ_succ_above _ j,
  rw fin.sum_univ_succ_above _ j,
  rw add_comm,
  rw add_comm (x₀ j),
  rw add_sub_assoc,
  rw sub_self,
  rw add_zero,
  rw add_right_cancel_iff,
  rw finset.sum_congr,
  { refl },
  { intros i hi,
    rw h0,
    exact fin.succ_above_ne j i },
end

Yakov Pechersky (Dec 02 2020 at 01:22):

I expanded out all the rw steps as opposed to a simp so that you can see the way the proof state is transformed.

Yakov Pechersky (Dec 02 2020 at 01:23):

In simp style:

import data.fintype.card

open_locale big_operators

example {α : Type*} [ring α] {n : } (x₀ x₁ : fin (n + 1)  α) (j : fin (n + 1))
  (h0 :  i : fin (n + 1), ¬ i = j  x₁ i = x₀ i) :
  ( i, x₁ i) = ( i, x₀ i) - x₀ j + x₁ j :=
by simp [fin.sum_univ_succ_above _ j, h0, fin.succ_above_ne, add_comm]

Yakov Pechersky (Dec 02 2020 at 01:24):

In fact, it's true even for fin n:

import data.fintype.card

open_locale big_operators

example {α : Type*} [ring α] {n : } (x₀ x₁ : fin n  α) (j : fin n)
  (h0 :  i : fin n, ¬ i = j  x₁ i = x₀ i) :
  ( i, x₁ i) = ( i, x₀ i) - x₀ j + x₁ j :=
begin
  cases n,
  { exact fin_zero_elim j },
  { simp [fin.sum_univ_succ_above _ j, h0, fin.succ_above_ne, add_comm] }
end

Patrick Thomas (Dec 02 2020 at 02:02):

Nice! Thank you!
Do you think it is still worth writing explicit stuff for fin as Kevin suggested? It could be fun and informative.

Kevin Buzzard (Dec 02 2020 at 02:06):

I learnt a lot about Lean by making my own natural numbers, complex numbers, and groups. In fact me and some undergraduates have developed more group theory using our own version of groups than there is in Lean right now!

Yakov Pechersky (Dec 02 2020 at 03:32):

It could be - the main complexity with fin is coercions to nat and back, in my opinion. And learning how to provide the coercion instances in a way that works well with other lemmas can be tricky.

Patrick Thomas (Dec 06 2020 at 00:33):

I'm trying to figure out why neither attempt at s1 works. I think it has something to do with casting, but I'm not sure.

import data.fin

def fin.sum {α : Type} [has_add α] : Π (n : ) (x : fin (n + 1)  α), α
| 0       x := x 0
| (m + 1) x := x (fin.last (m + 1)) + (fin.sum m (fun i : fin (m + 1), x (fin.cast_succ i)))

example {α : Type} [ring α] (n : ) (x : fin (n + 1)  α) (c : α) (h :  i : fin (n + 1), x i = c) :
fin.sum n x = c * (n + 1) :=
begin
induction n,
case nat.zero {
  show fin.sum 0 x = c * (0 + 1), from
  have s0 : 1 = 0 + 1 := zero_add 1,
  -- have s1 : c * 1 = c * (0 + 1) := @eq.subst α (fun x : α, c * 1 = c * x) 1 (0 + 1) s0 (eq.refl (c * 1)),
  -- have s1 : c * 1 = c * (0 + 1), by rw s0,
  calc
  fin.sum 0 x = x 0 : eq.refl (fin.sum 0 x)
  ...         = c : h 0
  ...         = c * 1 : (eq.symm (mul_one c))
  ...         = c * (0 + 1) : sorry
},
case nat.succ : n IH {
  /-
  IH : ∀ (x : fin (n + 1) → α), (∀ (i : fin (n + 1)), x i = c) → fin.sum n x = c * (↑n + 1),
  x : fin (n.succ + 1) → α,
  h : ∀ (i : fin (n.succ + 1)), x i = c
  -/
  show fin.sum n.succ x = c * (n.succ + 1), from
  let x' := fun i : fin n.succ, x (fin.cast_succ i) in
  have s0 : x (fin.last n.succ) = c := h (fin.last n.succ),
  have s1 : fin.sum n.succ x = x (fin.last n.succ) + fin.sum n x' := eq.refl (fin.sum n.succ x),
  have s2 : fin.sum n.succ x = c + fin.sum n x' := eq.subst s0 s1,
  have s3 : ( i : fin (n + 1), x' i = c)  fin.sum n x' = c * (n + 1) := IH x',
  have s4 :  i : fin (n + 1), x' i = c := (
    assume i : fin (n + 1),
    have s5 : x' i = x i.cast_succ := eq.refl (x' i),
    have s6 : x i.cast_succ = c := h i.cast_succ,
    eq.trans s5 s6
  ),
  have s7 : fin.sum n x' = c * (n + 1) := s3 s4,
  have s8 : fin.sum n.succ x = c + c * (n + 1) := eq.subst s7 s2,
  have s9 : c + c * (n + 1) = c * (n.succ + 1) := sorry,
  eq.trans s8 s9
}
end

Alex J. Best (Dec 06 2020 at 00:40):

  have s1 : c * 1 = c * (0 + 1), by simp,

works, the rw s0 version doesn't as s0 is an equality of natural numbers, you probably want

  have s0 : (1 : α) = 0 + 1 := (zero_add 1).symm,

instead

Patrick Thomas (Dec 06 2020 at 00:45):

That works. Thank you!

Patrick Thomas (Dec 06 2020 at 03:20):

Is there a single tactic that would work for the last sorry?

import data.fin


def fin.sum {α : Type} [has_add α] : Π (n : ) (x : fin (n + 1)  α), α
| 0       x := x 0
| (m + 1) x := x (fin.last (m + 1)) + (fin.sum m (fun i : fin (m + 1), x (fin.cast_succ i)))


example {α : Type} [ring α] (n : ) (x : fin (n + 1)  α) (c : α) (h :  i : fin (n + 1), x i = c) :
fin.sum n x = c * (n + 1) :=
begin
induction n,
case nat.zero {
  /-
  x : fin (0 + 1) → α,
  h : ∀ (i : fin (0 + 1)), x i = c
  -/
  show fin.sum 0 x = c * (0 + 1), from
  calc
  fin.sum 0 x = x 0         : by refl
  ...         = c           : h 0
  ...         = c * (0 + 1) : by simp
},
case nat.succ : n IH {
  /-
  IH : ∀ (x : fin (n + 1) → α), (∀ (i : fin (n + 1)), x i = c) → fin.sum n x = c * (↑n + 1),
  x : fin (n.succ + 1) → α,
  h : ∀ (i : fin (n.succ + 1)), x i = c
  -/
  show fin.sum n.succ x = c * (n.succ + 1), from
  let x' := fun i : fin n.succ, x (fin.cast_succ i) in
  have s0 :  i : fin (n + 1), x' i = c := (
    assume i : fin (n + 1),
    calc
    x' i = x i.cast_succ : by refl
    ...  = c             : h i.cast_succ
  ),
  have s1 : fin.sum n x' = c * (n + 1) := IH x' s0,
  have s2 : x (fin.last n.succ) = c := h (fin.last n.succ),
  calc
  fin.sum n.succ x = x (fin.last n.succ) + fin.sum n x' : by refl
  ...              = x (fin.last n.succ) + c * (n + 1)  : by rw s1
  ...              = c + c * (n + 1)                    : by rw s2
  ...              = c * ((n + 1) + 1)                  : by sorry
}
end

Alex J. Best (Dec 06 2020 at 03:22):

by noncomm_ring does it

Kenny Lau (Dec 06 2020 at 03:22):

by rw [mul_add, nat.cast_one, mul_one, add_comm] should work (haven't tested)

Kenny Lau (Dec 06 2020 at 03:22):

if you count that as "one tactic"

Patrick Thomas (Dec 06 2020 at 03:23):

noncomm_ring worked. Thank you!

Patrick Thomas (Dec 13 2020 at 20:03):

Any recommendations on which sum definition to go with, or something else?

import data.fin tactic algebra.order


def fin.sum {α : Type} [has_add α] : Π (n : ) (x : fin (n + 1)  α), α
| 0       x := x 0
| (m + 1) x := x (fin.last (m + 1)) + (fin.sum m (fun i : fin (m + 1), x (fin.cast_succ i)))

example {β : Type} [add_comm_monoid β] {n : } (f : fin (n + 2)  β) (x : fin (n + 2)) :
fin.sum (n + 1) f = f x + fin.sum n (fun i : fin (n + 1), ite (fin.cast_succ i < x) (f i.cast_succ) (f i.succ)) := sorry


def fin.sum' {α : Type} [has_add α] [has_zero α] : Π (n : ) (x : fin n  α), α
| 0       x := 0
| (m + 1) x := x (fin.last m) + (fin.sum m (fun i : fin (m + 1), x (fin.cast_succ i)))

example {β : Type} [add_comm_monoid β] {n : } (f : fin (n + 1)  β) (x : fin (n + 1)) :
fin.sum' (n + 1) f = f x + fin.sum' n (fun i : fin n, ite (fin.cast_succ i < x) (f i.cast_succ) (f i.succ)) := sorry

Kevin Buzzard (Dec 13 2020 at 20:28):

Go with the one that's already in the library! Unless you want to go through the whole process of proving sum(a_n + b_n) = sum a_n + sum b_n, sum(c)=N*c, a_n <= b_n implies sum a_n <= sum b_n and the 100 other lemmas you need to make a working sum theory by yourself (which you might want to do -- I have made group theory in Lean from first principle with undergraduates and it was rewarding from a teaching perspective)

Patrick Thomas (Dec 13 2020 at 20:31):

I was trying your suggestion: "I think the sum stuff in algebra.big_operators will work over any fintype (and fin n is a fintype), but it might be worth writing explicit stuff for fin anyway because there are more possibilities for induction principlles."

Patrick Thomas (Dec 13 2020 at 20:36):

I'm not sure in what sense "there are more possibilities for induction principlles." Would you have an example?

Kevin Buzzard (Dec 13 2020 at 20:38):

Maybe I mean "there are more possibilities for lemmas". For example a sum over fin(a+b) is a sum over fin(a) plus an appropriately shifted sum over fin(b). I don't know what I was talking about with induction principles.

Eric Wieser (Dec 13 2020 at 20:57):

I found that when I thought I had special cases for fin, what I actually had were lemmas about sum types (not to be confused with summations), and the fin (n + m) case fell out of docs#sum_fin_sum_equiv

Patrick Thomas (Dec 13 2020 at 21:28):

What is a sum type? I'm not sure I follow the idea from the definition.

Patrick Thomas (Dec 30 2020 at 01:25):

Is there a tactic that will break an equality into separate goals for each subexpression?
For example to change |- a + (b + c) = d + (e + f) into |- a = d |- b = e |- c = f.

Yakov Pechersky (Dec 30 2020 at 01:26):

congr

Yakov Pechersky (Dec 30 2020 at 01:26):

or more cleanly, likely congr' 1

Patrick Thomas (Dec 30 2020 at 01:28):

Nice. Thank you!

Patrick Thomas (Dec 30 2020 at 02:14):

Is there a tactic to compute instances of function application?

Patrick Thomas (Dec 30 2020 at 02:19):

For example, to change

   let x' := fin.mk x.val a0 in
   let f' := fun i : fin n.succ, f i.cast_succ in
   |- f' x' = f x

to f x'.cast_succ = f x.

Alex J. Best (Dec 30 2020 at 02:28):

try tactic#dsimp if that doesn't do what you want please post a #mwe

Patrick Thomas (Dec 30 2020 at 02:52):

I'm not sure how to fix the syntax to make a mwe. Something like

example (α : Type) (n : ) (f : fin (n + 1)  α) (x : fin (n.succ + 1)) (h0 : x.val < n.succ)
(x' := fin.mk x.val h0) (f' := fun i : fin n.succ, f i.cast_succ) :
f' x' = f x := sorry

Alex J. Best (Dec 30 2020 at 02:56):

Is

import data.fin
example (α : Type) (n : ) (f : fin (n + 1)  α) (x : fin (n.succ + 1)) (h0 : x.val < n.succ) :
let x' := fin.mk x.val h0, f' := fun i : fin n.succ, f i.cast_succ in
f' x' = f x := begin
dsimp,
refl,
end

what you meant then?

Alex J. Best (Dec 30 2020 at 02:56):

So tactic#dsimp does work?

Patrick Thomas (Dec 30 2020 at 03:03):

Hmm. I thought that would be a mwe. This is what doesn't work:

import data.fin tactic

lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry

lemma fin.lt_one_eq_zero (x : fin 1) : x = 0 :=
have s0 : x.val < 1 := x.prop,
have s1 : x.val = 0 := lt_one s0,
fin.eq_of_veq s1


def fin.sum {α : Type} [has_add α] [has_zero α] : Π (n : ) (x : fin n  α), α
| 0       x := 0
| (m + 1) x := x (fin.last m) + fin.sum m (fun i : fin m, x i.cast_succ)


example {α : Type} [ring α] {n : } (f : fin (n + 1)  α) (x : fin (n + 1)) :
fin.sum (n + 1) f = f x + fin.sum n (fun i : fin n, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) :=
begin
induction n,
case nat.zero {
  show fin.sum (0 + 1) f = f x + fin.sum 0 (fun i : fin 0, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)), from
  have s0 : x = 0 := fin.lt_one_eq_zero x,
  calc
  fin.sum (0 + 1) f = f (fin.last 0) + fin.sum 0 (fun i : fin 0, f i.cast_succ)                         : by refl
  ...               = f 0 + fin.sum 0 (fun i : fin 0, f i.cast_succ)                                    : by refl
  ...               = f x + fin.sum 0 (fun i : fin 0, f i.cast_succ)                                    : by rw s0
  ...               = f x + 0                                                                           : by refl
  ...               = f x + fin.sum 0 (fun i : fin 0, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) : by refl
},
case nat.succ : n IH {
  show fin.sum (n.succ + 1) f = f x + fin.sum n.succ (fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)), from
  have s1 : x.val < n.succ  x.val = n.succ := lt_or_eq_of_le (le_of_lt_succ x.prop),
  or.elim s1
  (
    assume a0 : x.val < n.succ,
    let x' := fin.mk x.val a0 in
    let f' := fun i : fin n.succ, f i.cast_succ in
    have s2 : fin.sum n.succ f' = f' x' + fin.sum n (fun i : fin n, ite (i.cast_succ < x') (f' i.cast_succ) (f' i.succ)) := IH f' x',
    calc
    fin.sum (n.succ + 1) f = f (fin.last n.succ) + fin.sum n.succ f' : by refl
    ...                    = f (fin.last n.succ) + (f' x' + fin.sum n (fun i : fin n, ite (i.cast_succ < x') (f' i.cast_succ) (f' i.succ))) : by rw s2
    ...                    = f' x' + (f (fin.last n.succ) + fin.sum n (fun i : fin n, ite (i.cast_succ < x') (f' i.cast_succ) (f' i.succ))) : by noncomm_ring
    ...                    = f x
                           + ((fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) (fin.last n)
                           + fin.sum n (fun i : fin n, (fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) i.cast_succ)) :
                           begin
                           congr,
                           dsimp,

                           end


    ...                    = f x + fin.sum n.succ (fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) : by refl
  )
  (
    assume a1 : x.val = n.succ,
    calc
    fin.sum (n.succ + 1) f = f (fin.last n.succ) + fin.sum n.succ (fun i : fin n.succ, f i.cast_succ) : by refl
    ...                    = f x + fin.sum n.succ (fun i : fin n.succ, f i.cast_succ) : sorry
    ...                    = f x + fin.sum n.succ (fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) : sorry
  )
}
end

Alex J. Best (Dec 30 2020 at 03:12):

I see, there are no lets in the goal, when you wrote

   let x' := fin.mk x.val a0 in
   let f' := fun i : fin n.succ, f i.cast_succ in
   |- f' x' = f x

it looked like there would be, its really helpful to post actual lean code in this case, the working + example parts are more helpful then being minimal in this case :smile:.
Anyway you can do those substitutions with simp like

import data.fin tactic

lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry

lemma fin.lt_one_eq_zero (x : fin 1) : x = 0 :=
have s0 : x.val < 1 := x.prop,
have s1 : x.val = 0 := lt_one s0,
fin.eq_of_veq s1


def fin.sum {α : Type} [has_add α] [has_zero α] : Π (n : ) (x : fin n  α), α
| 0       x := 0
| (m + 1) x := x (fin.last m) + fin.sum m (fun i : fin m, x i.cast_succ)


example {α : Type} [ring α] {n : } (f : fin (n + 1)  α) (x : fin (n + 1)) :
fin.sum (n + 1) f = f x + fin.sum n (fun i : fin n, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) :=
begin
induction n,
case nat.zero {
  show fin.sum (0 + 1) f = f x + fin.sum 0 (fun i : fin 0, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)), from
  have s0 : x = 0 := fin.lt_one_eq_zero x,
  calc
  fin.sum (0 + 1) f = f (fin.last 0) + fin.sum 0 (fun i : fin 0, f i.cast_succ)                         : by refl
  ...               = f 0 + fin.sum 0 (fun i : fin 0, f i.cast_succ)                                    : by refl
  ...               = f x + fin.sum 0 (fun i : fin 0, f i.cast_succ)                                    : by rw s0
  ...               = f x + 0                                                                           : by refl
  ...               = f x + fin.sum 0 (fun i : fin 0, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) : by refl
},
case nat.succ : n IH {
  show fin.sum (n.succ + 1) f = f x + fin.sum n.succ (fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)), from
  have s1 : x.val < n.succ  x.val = n.succ := lt_or_eq_of_le (le_of_lt_succ x.prop),
  or.elim s1
  (
    assume a0 : x.val < n.succ,
    let x' := fin.mk x.val a0 in
    let f' := fun i : fin n.succ, f i.cast_succ in
    have s2 : fin.sum n.succ f' = f' x' + fin.sum n (fun i : fin n, ite (i.cast_succ < x') (f' i.cast_succ) (f' i.succ)) := IH f' x',
    calc
    fin.sum (n.succ + 1) f = f (fin.last n.succ) + fin.sum n.succ f' : by refl
    ...                    = f (fin.last n.succ) + (f' x' + fin.sum n (fun i : fin n, ite (i.cast_succ < x') (f' i.cast_succ) (f' i.succ))) : by rw s2
    ...                    = f' x' + (f (fin.last n.succ) + fin.sum n (fun i : fin n, ite (i.cast_succ < x') (f' i.cast_succ) (f' i.succ))) : by noncomm_ring
    ...                    = f x
                           + ((fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) (fin.last n)
                           + fin.sum n (fun i : fin n, (fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) i.cast_succ)) :
                           begin
                           congr,
                           simp [f', x'],
                           congr,
                           exact fin.eta x _,
                           end


    ...                    = f x + fin.sum n.succ (fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) : by refl
  )
  (
    assume a1 : x.val = n.succ,
    calc
    fin.sum (n.succ + 1) f = f (fin.last n.succ) + fin.sum n.succ (fun i : fin n.succ, f i.cast_succ) : by refl
    ...                    = f x + fin.sum n.succ (fun i : fin n.succ, f i.cast_succ) : sorry
    ...                    = f x + fin.sum n.succ (fun i : fin n.succ, ite (i.cast_succ < x) (f i.cast_succ) (f i.succ)) : sorry
  )
}
end

Patrick Thomas (Dec 30 2020 at 03:16):

Thank you!

Alex J. Best (Dec 30 2020 at 03:16):

                           begin
                           simp [f', x'],
                           congr,
                           exact fin.eta x _,
                           rw if_neg,
                           simp,
                           exact le_of_lt_succ a0,
                           ext,congr,
                           exact fin.cast_succ_fin_succ _ _,
                           end

does that inner goal completely :smile:, these goals are very messy though, I wonder if there are some lemmas that need splitting out ?

Patrick Thomas (Dec 30 2020 at 03:20):

Maybe, I'm not sure.

Patrick Thomas (Dec 30 2020 at 03:54):

I agree, it does seem rather messy. I'm not sure what to pull out for lemmas though.

Eric Wieser (Dec 30 2020 at 10:06):

I think your fin.lt_one_eq_zero is docs#subsingleton.elim or similar

Patrick Thomas (Dec 30 2020 at 19:45):

Looks like it might be fin.eq_zero.

Patrick Thomas (Dec 30 2020 at 19:46):

Is there a fold operation defined for fin? I wonder if that would make it simpler.

Johan Commelin (Dec 30 2020 at 19:49):

There is finset.fold which you could apply on univ. Not sure if that is helpful.

Patrick Thomas (Dec 30 2020 at 20:23):

Yeah, I should probably just move to the library definition anyway. I had started this lemma, so I had wanted to finish it first.


Last updated: Dec 20 2023 at 11:08 UTC