formalizing definitions for real analysis

Stream: new members

[Patrick Thomas]

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 $P$ of a closed interval $[a, b]$ is a finite sequence $(x_{0}, x_{1}, \ldots, x_{n})$ such that $a = x_{0} < x_{1} < \ldots < x_{n} = b$. The norm of $P$, denoted $\left|\left|P\right|\right|$, is defined by $\left|\left|P\right|\right| = \max_{1 \leq i \leq n} (x_{i} - x_{i-1})$.

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

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

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

[Kenny Lau]

just don't use backticks

[Kenny Lau]

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

[Patrick Thomas]

Thank you.

[Reid Barton]

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

[Reid Barton]

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]

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]

(do you know that mathlib has lebesgue integration?)

[Patrick Thomas]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Patrick Thomas]

Cool. I'll take a look.

[Kevin Buzzard]

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]

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

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]

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]

What are "golfy term mode proofs"?

[Patrick Thomas]

Does that just mean really compact proofs or something more?

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

Yes

[Patrick Thomas]

I see.

[Patrick Thomas]

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

[Adam Topaz]

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

[Patrick Thomas]

So the difference is to make it ordered?

[Patrick Thomas]

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

[Adam Topaz]

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

[Patrick Thomas]

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

[Kevin Buzzard]

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]

Adam Topaz said:

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

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

[Adam Topaz]

You can still do it inductively with fin.

[Adam Topaz]

Since fin.tail is a thing.

[Adam Topaz]

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

[Adam Topaz]

And defining the empty partition is easy :)

[Dan Stanescu]

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]

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

[Kevin Buzzard]

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

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

Adam Topaz said:

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

Yes, which is the input of x

[Adam Topaz]

Oh right :)

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

Doesn't this exist as a coersion?

[Reid Barton]

Not sure but it certainly exists in some form

[Patrick Thomas]

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

[Dan Stanescu]

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

[Kevin Buzzard]

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]

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

[Patrick Thomas]

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

[Adam Topaz]

Reid Barton said:

Not sure but it certainly exists in some form

src#fin.cast_succ

[Kevin Buzzard]

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

[Adam Topaz]

Just in case it's helpful later.

[Patrick Thomas]

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

[Reid Barton]

Well that's what your informal definition said right?

[Patrick Thomas]

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

[Kevin Buzzard]

It is the canonical type with n+1 elements

[Jalex Stark]

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

[Kevin Buzzard]

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]

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]

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

[Jalex Stark]

what would the m be doing there?

[Kevin Buzzard]

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

[Adam Topaz]

or #print

[Jalex Stark]

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

[Kevin Buzzard]

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

[Jalex Stark]

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]

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

[Kevin Buzzard]

except that it's a type, not a set

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

I think I get it.

[Patrick Thomas]

Thank you.

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Patrick Thomas]

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]

The function?

[Adam Topaz]

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]

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

[Patrick Thomas]

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

[Dan Stanescu]

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]

But there are many partitions of any given interval

[Dan Stanescu]

True.

[Patrick Thomas]

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]

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]

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]

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

[Dan Stanescu]

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]

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]

Others may have other opinions on this, however.

[Patrick Thomas]

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]

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]

How do you make a type out of a proposition?

[Bryan Gin-ge Chen]

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

[Patrick Thomas]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Reid Barton]

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

[Mario Carneiro]

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]

Same deal with dedekind reals being isomorphic to cauchy reals

[Mario Carneiro]

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]

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]

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

[Patrick Thomas]

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]

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

[Jalex Stark]

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

[Patrick Thomas]

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

[Jalex Stark]

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

[Jalex Stark]

fin n is an example of a structure

[Patrick Thomas]

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]

it's morally equivalent (maybe literally defeq) to

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

[Jalex Stark]

I don't understand your question

[Patrick Thomas]

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

[Jalex Stark]

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]

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

[Patrick Thomas]

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]

no

[Jalex Stark]

you could define a partition and then prove

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

[Bryan Gin-ge Chen]

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

[Jalex Stark]

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

[Jalex Stark]

you should also try to prove lemmas that are mathematically obvious

[Patrick Thomas]

Interesting.

[Jalex Stark]

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

[Jalex Stark]

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]

Makes sense I guess.

[Jalex Stark]

a def is like a 0-field structure

[Patrick Thomas]

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]

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

[Bryan Gin-ge Chen]

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

[Patrick Thomas]

True.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Patrick Thomas]

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]

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

[Patrick Thomas]

Just not intuitive to me I guess.

[Jalex Stark]

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]

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

[Patrick Thomas]

Maybe. I'm doing this for pedagogy though.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

But with ≤ the space of partitions has better properties.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Jalex Stark]

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]

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

[Yury G. Kudryashov]

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]

:)

[Patrick Thomas]

No problem.

[Kevin Buzzard]

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]

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]

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]

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

[Reid Barton]

If $a \ne b$ then $n > 0$ is forced anyways

[Reid Barton]

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

[Patrick Thomas]

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

[Patrick Thomas]

a and b are parameters aren't they?

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

not sure what it does on out of range inputs

[Patrick Thomas]

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

[Patrick Thomas]

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

[Reid Barton]

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]

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

[Patrick Thomas]

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]

Note that this will work for $a \le b$. Textbooks often say something like "we can deal with $a \ge b$ in the same way" but you can't do this in Lean. If you want to deal with $\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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Reid Barton]

I guess a fourth option is $\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]

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

[Patrick Thomas]

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]

I'd probably use finset.sup

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Patrick Thomas]

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]

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]

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

[Patrick Thomas]

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]

Does defining foo not still require induction on the function?

[Adam Topaz]

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]

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]

These are just implementation details.

[Adam Topaz]

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

[Adam Topaz]

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

[Bryan Gin-ge Chen]

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

[Scott Morrison]

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

[Patrick Thomas]

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]

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]

oh is that supposed to be the second argument?

[Patrick Thomas]

That it doesn't terminate. Yeah :)

[Reid Barton]

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

[Reid Barton]

I'm not sure what your goals are though.

[Reid Barton]

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]

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

[Patrick Thomas]

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

[Reid Barton]

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]

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

[Adam Topaz]

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]

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]

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]

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]

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

[Yury G. Kudryashov]

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

[Patrick Thomas]

What is the first symbol in the second one?

[Patrick Thomas]

The one that looks like a square U.

[Adam Topaz]

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]

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

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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]

I didn't know about the control click.

[Yury G. Kudryashov]

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

[Patrick Thomas]

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]

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]

Try noncomputable theory at the top of your file.

[Yury G. Kudryashov]

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

[Patrick Thomas]

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]

The "supremum" part is noncomputable.

[Patrick Thomas]

(deleted)

[Patrick Thomas]

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

[Patrick Thomas]

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]

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

[Patrick Thomas]

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

[Adam Topaz]

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, $x_i - x_{i+1}$.

[Adam Topaz]

You probably want i.succ - i.cast_succ

[Patrick Thomas]

That was what I was wondering.

[Patrick Thomas]

Thank you.

[Adam Topaz]

No problem!

[Patrick Thomas]

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]

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]

Cool.

[Adam Topaz]

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]

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]

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

[Patrick Thomas]

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]

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]

Good idea.

[Adam Topaz]

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

[Patrick Thomas]

I might wait and look into that latter.

[Patrick Thomas]

I need to move on to Riemann sums :)

[Patrick Thomas]

For each $i = 1, \ldots, n$, let $x_{i}*$ be an arbitrary point in the interval $[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]

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

[Kevin Buzzard]

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]

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]

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 $x$ and then something else $x^*$ doesn't sound like a great idea to me. I called it y.

[Patrick Thomas]

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]

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]

That takes the max, not the sum right?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Alright.

[Jalex Stark]

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

[Jalex Stark]

this will automatically hide the proofs and emphasize docstrings

[Jalex Stark]

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

[Patrick Thomas]

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

[Jalex Stark]

i don't know what you should do

[Jalex Stark]

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]

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

[Jalex Stark]

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]

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]

I see.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Anatole Dedecker]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

#mil should cover all this too, eventually.

[Patrick Thomas]

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

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

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

[Patrick Thomas]

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]

Did you try open_locale big_operators?

[Patrick Thomas]

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]

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

[Alex J. Best]

Yeah the notation for Sum needs some arguments after it.

[Alex J. Best]

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]

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]

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

[Patrick Thomas]

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

[Alex J. Best]

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]

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]

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]

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]

Yeah always use the community web editor!

[Alex J. Best]

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]

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

[Alex J. Best]

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]

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

[Alex J. Best]

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]

There is a proof in the definition?

[Alex J. Best]

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]

I see.

[Patrick Thomas]

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

[Patrick Thomas]

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

[Patrick Thomas]

Actually an inf right?

[Alex J. Best]

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]

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

[Patrick Thomas]

Is that by convention?

[Patrick Thomas]

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

[Patrick Thomas]

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]

You mean

import data.real.basic

structure ub (S : set ℝ) :=
(t : ℝ)
(is_ub : ∀ s ∈ S, s ≤ t)

& similarly for lub

[Patrick Thomas]

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

[Reid Barton]

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

[Patrick Thomas]

What did I do wrong?

[Reid Barton]

It just doesn't make any sense.

[Reid Barton]

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

[Reid Barton]

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

[Patrick Thomas]

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

[Reid Barton]

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]

Which is right.

[Reid Barton]

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]

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]

You don't need to make use of it

[Patrick Thomas]

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

[Reid Barton]

Maybe start with the definition in math?

[Reid Barton]

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

[Reid Barton]

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]

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]

ub of S that is.

[Reid Barton]

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]

You could also reuse the whole structure ub

[Patrick Thomas]

What do you mean by reuse the whole structure ub?

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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]

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

[Kenny Lau]

you would have to write r.t instead

[Patrick Thomas]

What does r.t mean?

[Reid Barton]

ub.t r

[Reid Barton]

i.e. the t field

[Patrick Thomas]

Oh.

[Kenny Lau]

#tpil

[Kenny Lau]

Ch. 9

[Reid Barton]

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]

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]

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

[Reid Barton]

It's not necessarily better or worse

[Reid Barton]

just different

[Reid Barton]

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]

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]

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

[Patrick Thomas]

I see.

[Reid Barton]

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]

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

[Kenny Lau]

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

[Kenny Lau]

which means the implementation without structure is better

[Patrick Thomas]

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]

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

[Reid Barton]

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

[Reid Barton]

but as I mentioned above it's awkward

[Reid Barton]

this awkwardness would disappear with the usual definition

[Patrick Thomas]

Alright.

[Patrick Thomas]

Thank you.

[Patrick Thomas]

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]

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]

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]

What does classical.epsilon $ is_lub S mean?

[Kenny Lau]

is_lub S is a predicate on \R

[Kenny Lau]

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

[Kenny Lau]

otherwise return a default element

[Kenny Lau]

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]

any this is the API for lub

[Kenny Lau]

so you can forget about its definition

[Patrick Thomas]

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]

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

[Kenny Lau]

Kenny Lau said:

otherwise return a default element

@Patrick Thomas

[Kenny Lau]

you wouldn't get any error

[Kenny Lau]

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

[Kenny Lau]

treat it as an unspecified constant

[Patrick Thomas]

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

[Patrick Thomas]

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

[Patrick Thomas]

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]

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

[Kenny Lau]

Patrick Thomas said:

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

because it has no definition

[Kenny Lau]

it uses classical.choice

[Kenny Lau]

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

[Adam Topaz]

(deleted)

[Patrick Thomas]

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]

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

[Kenny Lau]

it will behave like an arbiratry real number

[Patrick Thomas]

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

[Patrick Thomas]

That is t : \R and t is_lub S.

[Patrick Thomas]

Or is it actually safer?

[Patrick Thomas]

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

[Patrick Thomas]

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]

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

[Kenny Lau]

that would mean every set has lub

[Patrick Thomas]

How do I get at the properties of lub S?

[Kenny Lau]

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]

is this enough API?

[Kenny Lau]

@Patrick Thomas

[Patrick Thomas]

Thank you!

[Daniel Shapero]

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]

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

[Patrick Thomas]

I would also be interested in hearing opinions on this.

[Dan Stanescu]

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]

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]

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

[Patrick Thomas]

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]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

which I guess still works

[Kenny Lau]

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]

@Kevin Buzzard deja vu?

[Patrick Thomas]

Do you know why I get type mismatch at application for the exists.elim s2?

[Kenny Lau]

don't use exists.elim

[Kenny Lau]

use let

[Patrick Thomas]

That works on existential elimination?

[Patrick Thomas]

Is there an example somewhere?

[Utensil Song]

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]

Patrick Thomas said:

Is there an example somewhere?

look at my proof

[Kenny Lau]

the let I used is the existential elimination

[Ruben Van de Velde]

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]

Kenny Lau said:

Kevin Buzzard deja vu?

?

[Patrick Thomas]

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]

Something like

obtain ⟨x, hx, y, hy, h⟩ : ∃ x ∈ X, ∃ y ∈ Y, z = x + y} := a1,

(untested)

[Patrick Thomas]

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]

Yeah, I don't think that's possible

[Patrick Thomas]

:(

[Patrick Thomas]

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]

That's definitely possible

[Mario Carneiro]

use rcases a_eq : a1 with ⟨x, hx, y, hy, h⟩

[Mario Carneiro]

I don't know if obtain has a similar syntax

[Patrick Thomas]

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]

what's the mwe?

[Mario Carneiro]

Oh I misunderstood your question

[Mario Carneiro]

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]

Yes, that is what I meant. That would be great.

[Mario Carneiro]

you might have to put parentheses around the type ascriptions, for consistency with other uses of type ascription

[Mario Carneiro]

it also might interact with | in a weird way if you have a notation that uses |

[Patrick Thomas]

I don't mind using exists.elim, but I think I am applying it to the double exists wrong?

[Patrick Thomas]

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]

Where does this error come from?
Screenshot-from-2020-08-08-15-31-29.png

[Anatole Dedecker]

Oh

[Anatole Dedecker]

I got this one quite a lot, I was about to ask the same thing

[Anatole Dedecker]

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]

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]

How are you able to tell that the hypothesis is implicitly named a?

[Anatole Dedecker]

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]

I see. Well, changing a and b to t0 and t1 fixes it. That works I guess.

[Patrick Thomas]

Thank you.

[Anatole Dedecker]

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]

just use guard_hyp

[Mario Carneiro]

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]

Build is failing.

[Anatole Dedecker]

Kenny Lau said:

just use guard_hyp

Could you explain a bit more what you meant ?

[Kenny Lau]

you can use guard_hyp to assert that a hypothesis has a certain type

[Kenny Lau]

so if you want to assert that hx has type x \in X then just use guard_hyp

[Patrick Thomas]

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]

I think maybe I need something like the foldr1 function in Haskell.

[Patrick Thomas]

Is there a way to have an option to show the types in the mathlib generated documentation?

[Patrick Thomas]

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]

If you click on "source" you see def vector (α : Type u) (n : ℕ) := { l : list α // l.length = n } . Does this answer your question?

[Patrick Thomas]

I was being lazy and thought it might be nice to have an option to avoid that :)

[Patrick Thomas]

Sorry

[Kevin Buzzard]

#print vector within a Lean file should also tell you everything about it

[Patrick Thomas]

Even more work :)

[Bryan Gin-ge Chen]

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]

Ok. Thank you.

[Patrick Thomas]

Added: https://github.com/leanprover-community/doc-gen/issues/63

[Patrick Thomas]

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]

A vector is a pair consisting of a list and a proof.

[Patrick Thomas]

vector α n = {l // l.length = n} defines a list and a proof?

[Patrick Thomas]

The proof comes from the type somehow?

[Kevin Buzzard]

https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html?highlight=subtype#inductively-defined-propositions

[Kevin Buzzard]

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]

So I should be able to get at the list by using .val?

[Patrick Thomas]

Got it. Thank you.

[Patrick Thomas]

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]

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]

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]

I can write the type, but I'm having trouble defining it.

[Patrick Thomas]

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]

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]

Nice. Thank you.

[Kyle Miller]

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]

In the first, should n be n + 1 in the body?

[Kyle Miller]

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]

Oh. Right.

[Adam Topaz]

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]

And data.matrix.notation has nice notation for those

[Patrick Thomas]

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]

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]

Where's that from?

[Patrick Thomas]

Much earlier in the thread.

[Adam Topaz]

Oh, I see. In the link for the lean web editor? Note the commented out notation there :)

[Adam Topaz]

That should be approximately familiar mathematical notation.

[Patrick Thomas]

Yeah. I'm going to have to prove things about it though.

[Adam Topaz]

This is another reason to use fin nif the API is more developed.

[Patrick Thomas]

True.

[Patrick Thomas]

If I understand the API :)

[Patrick Thomas]

I'll probably move on to it at some point.

[Patrick Thomas]

What is the * after Type by the way?

[Adam Topaz]

It tells lean to go and figure out the universe variable.

[Patrick Thomas]

Ah.

[Yakov Pechersky]

The finset.univ line says that, for all values of (fin P.n), that is, from 0 to n-1.

[Yakov Pechersky]

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]

In python list accession syntax

[Yakov Pechersky]

finset.univ means a finset (a finite set) of all the terms for a given type

[Patrick Thomas]

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]

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]

Functionally I think this is equivalent though?

[Yakov Pechersky]

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]

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]

Also, look into Pi types, which are type level foralls

[Patrick Thomas]

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]

Thank you.

[Patrick Thomas]

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]

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]

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]

So finset (fin 3) has the terms [0, 1, 2], [0, 2, 1], [1, 0, 2] etc.?

[Alex J. Best]

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]

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]

It looks like it is using some kind of fold. Maybe it defaults to some value?

[Alex J. Best]

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]

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]

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]

Also, why is it (finset.univ : finset (fin P.n)) instead of (finset.univ (finset (fin P.n)))?

[Alex J. Best]

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]

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]

I see. Thank you.

[Alex J. Best]

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]

When the partition has n+1 points in it, the list of things we take the sup over only has n.

[Patrick Thomas]

I see.

[Patrick Thomas]

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]

Not the sorrys, but the passing of m-1 to norm.

[Yakov Pechersky]

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]

that is, once you've taken care of the 0 case, do the succ pattern. and avoid subtraction.

[Yakov Pechersky]

what's the error you get now?

[Patrick Thomas]

type mismatch at application
  norm m f
term
  f
has type
  fin (m + 1) → ℝ
but is expected to have type
  fin m → ℝ

[Yakov Pechersky]

What exactly are you trying to define? Can you describe it in words?

[Patrick Thomas]

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]

Oops, make that the max of those numbers.

[Yakov Pechersky]

Just so you know, fin 0 is isomorphic to the empty type. So in your wording, it would be the empty list.

[Patrick Thomas]

Ok.

[Yakov Pechersky]

Are you wedded to having it as a fin n \to R?

[Yakov Pechersky]

You might want to express this as a fold over lists.

[Yakov Pechersky]

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]

Interesting. Thank you!

[Patrick Thomas]

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]

I guess you would need to define a function that returns the nth element of the list.

[Patrick Thomas]

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]

import data.real.basic
import data.list.basic

example {l : list ℝ} {x : ℝ} : x ∈ l → x = 0 := sorry

[Yakov Pechersky]

The functions you're thinking about are docs#list.nth and docs#list.nth_le

[Yakov Pechersky]

There's also docs#list.of_fn

[Yakov Pechersky]

And also docs#vector.

[Yakov Pechersky]

But which you should use is probably dependent on what you want to use this list for!

[Patrick Thomas]

Thank you.

[Patrick Thomas]

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]

Change that l to list.cons b m?

[Patrick Thomas]

I see. Thank you.

[Patrick Thomas]

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]

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]

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]

I guess it's not clear to me what you are optimizing then

[Mario Carneiro]

you have no theorems

[Mario Carneiro]

I don't see anything particularly gratuitous in the definitions of norm and sum, assuming the definition of a partition is fixed

[Mario Carneiro]

you can skip the linarith proof if you want, dunno if that's better

[Patrick Thomas]

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]

how do you want to use them?

[Patrick Thomas]

The definitions of norm and sum? To prove properties of the Riemann integral.

[Mario Carneiro]

okay, so pick a theorem and prove it

[Mario Carneiro]

you won't know if the definition is usable until you try to use it

[Patrick Thomas]

Won't it be a bad start if I don't understand the definitions I am using?

[Patrick Thomas]

Or do you mean try to make my own definitions and use them and see how it goes?

[Yakov Pechersky]

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]

Alright.

[Patrick Thomas]

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]

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]

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]

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]

you can define that more simply as ∀ j, P.x j.succ - P.x j.cast_succ < delta

[Patrick Thomas]

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]

you could do that, yes

[Patrick Thomas]

Any foreseeable issues?

[Mario Carneiro]

well it's two things instead of one thing

[Patrick Thomas]

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]

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]

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]

What would the P' do?

[Patrick Thomas]

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]

You could, but I'm not sure what you were trying to state with your example.

[Patrick Thomas]

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]

"Given P, a partition of [a, b], there exists a P' such that the pt_part of P is ...?"

[Yakov Pechersky]

What's the ... there?

[Yakov Pechersky]

Do you just want to say that for any P : part a b one can make a pt_part P?

[Patrick Thomas]

Yes. I just need an arbitrary riemann sum of P.

[Yakov Pechersky]

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]

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]

You don't have to supply the definition of y and a proof of mem_block?

[Yakov Pechersky]

You do.

[Yakov Pechersky]

You have to fill in those underscores

[Yakov Pechersky]

But once you do it in that instance declaration, you don't have to do it again when you invoke default

[Patrick Thomas]

Ah. Ok. Thank you.

[Yakov Pechersky]

We'll see. This might not work because of the P argument

[Patrick Thomas]

What is the syntax to get the default?

[Yakov Pechersky]

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]

So in a place that would expect a pt_part P for some inferable P, you could just write default _

[Yakov Pechersky]

because default : Π (α : Sort u_1) [c : inhabited α], α

[Yakov Pechersky]

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]

Nice. Thank you.

[Patrick Thomas]

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]

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]

I'd say just do

example  : is_riemann_integral 0 2 (λ x : ℝ, if x = 1 then 1 else 0) 0 := sorry

[Alex J. Best]

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]

Ok. Thank you!

[Patrick Thomas]

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]

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]

Thank you.

[Patrick Thomas]

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]

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]

Oh, right. Thank you.

[Patrick Thomas]

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]

Do I need to make some kind of inhabited data type?

[Patrick Thomas]

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]

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]

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]

Can I ask, is there a reason you prefer these tactic mode proofs?

[Patrick Thomas]

Do you mean non tactic? I just like to make it readable independent of Lean.

[Yakov Pechersky]

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]

Perhaps a calc style proof would be the most readable in such a case

[Patrick Thomas]

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

tactics!

[Patrick Thomas]

I mean which tactics :)

[Patrick Thomas]

rw?

[Kevin Buzzard]

rw is the eq.subst tactic, yes. The tactic which does ext is in fact called ext :-)

[Kevin Buzzard]

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]

Personally I find that a lot harder to read, especially without Lean.

[Kevin Buzzard]

But you don't need to read this proof because the result is trivial.

[Mario Carneiro]

example {a b : ℝ} : ∀ (P : partition a b), P.n = 0 → a = b :=
by { rintro ⟨n, x, rfl, rfl, -⟩ (rfl : n = 0), refl }

[Kevin Buzzard]

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]

(rfl : a = b) is a nice trick

[Patrick Thomas]

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]

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]

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]

But for long proofs, I agree, you are better off running a copy of Lean and looking at the code within it.

[Mario Carneiro]

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]

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]

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]

What is #explode?

[Mario Carneiro]

It's a tactic that will print out a metamath style proof of any lean theorem

[Patrick Thomas]

Huh. Cool. I'll take a look.

[Mario Carneiro]

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
4│3,2  │ mt                               │ │ ¬p
5│4    │ or.inr                           │ │ p ∨ ¬p
6│2,5  │ ∀I                               │ u p ≠ v p → p ∨ ¬p
7│     │ or.inl                           │ p → p ∨ ¬p
8│1,6,7│ or.elim                          │ p ∨ ¬p
9│0,8  │ ∀I                               │ ∀ (p : Prop), p ∨ ¬p

[Patrick Thomas]

Interesting.

[Yakov Pechersky]

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]

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]

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]

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]

So its coercing naturals to fin (n+1)

[Patrick Thomas]

What happens if m can not be coerced?

[Alex J. Best]

It always can be coerced, in this case it takes m mod n+1,

#eval (↑(7 : ℕ) : fin 3) -- 1

[Patrick Thomas]

Huh. Why does it do that?

[Patrick Thomas]

I guess because it is defined to :)

[Bryan Gin-ge Chen]

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]

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]

The way Lean finds coercions is explained in this section of TPiL.

[Patrick Thomas]

Thank you.

[Mario Carneiro]

FYI this cast is not recommended; you should use fin.last n instead

[Patrick Thomas]

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]

Does it have to be ℝ? That definition looks like it would work on any type

[Mario Carneiro]

If you use a computational type you can #eval it

[Mario Carneiro]

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]

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]

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]

Cool! Thanks!

[Patrick Thomas]

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]

Probably Lean knows that fin 1 is a subsingleton

[Kenny Lau]

and the second question is probably answered by some sort of induction/cases

[Yakov Pechersky]

A recent commit added fin.eq_zero: https://github.com/leanprover-community/mathlib/commit/c4132e9ae950e8b28eafc964062311ff21fe4d08

[Yakov Pechersky]

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]

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]

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]

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]

Thank you both.

[Patrick Thomas]

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]

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]

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]

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

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]

Thank you!

[Patrick Thomas]

Sorry, if you don't mind, how would you handle the rw hr at m without tactics?

[Patrick Thomas]

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]

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]

I can't make this compile. Can you give a #mwe ?

[Patrick Thomas]

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]

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 hε,
  have εpos : 0 < ε := by { rw hε, exact zero_lt_one },
  obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ, 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) < ε := hδ 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]

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]

Well I think that you would have to make that definition and associated API outside of the proof context.

[Yakov Pechersky]

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]

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]

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]

You still need to come up with a way of generating a tagged_partition P to begin with

[Patrick Thomas]

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]

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]

open_locale classical will make it go away

[Yakov Pechersky]

And not defining your own fin.

[Yakov Pechersky]

In fact, you don't need open_locale classical if you don't define your own fin

[Patrick Thomas]

What is different about my fin that causes this?

[Yakov Pechersky]

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]

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]

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]

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]

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]

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]

the data fields are equal.

[Patrick Thomas]

What is the difference between 'the data parts are equal' and 'the data fields are equal'?

[Kevin Buzzard]

nothing

[Kevin Buzzard]

two complex numbers are equal if and only if their real and imaginary parts are equal

[Kevin Buzzard]

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]

I thought you said we have to prove that 'if the data parts are equal, then the instances are equal'.

[Kevin Buzzard]

Yes.

[Patrick Thomas]

Um, sorry, this seems circular.

[Kevin Buzzard]

There's an example

[Kevin Buzzard]

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]

But it needed to be proved.

[Yakov Pechersky]

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]

If you make a new structure, it's your job to make a useful test for equality of terms of that structure.

[Yakov Pechersky]

In any case, just use regular ol' fin instead of spinning your own

[Yakov Pechersky]

Unless you have some issues with it?

[Kevin Buzzard]

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]

I mean, you're using \R for reals, so why not use fin as provided?

[Yakov Pechersky]

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]

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]

It's just the tedium of formalization, even more tedious than plain old real analysis

[Yakov Pechersky]

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]

I was just using my own fin to make sure I understood how it worked. I can abandon it I guess.

[Yakov Pechersky]

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]

And then you would use if_pos and if_neg instead of function.update_apply and function.update_noteq

[Yakov Pechersky]

"how it worked" is a scary hole to go down..., but laden with great questions!

[Yakov Pechersky]

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]

I've looked down a lot of the fin hole, but haven't looked at all how the reals are defined...

[Patrick Thomas]

I guess I'll focus on the partition problem for now.

[Patrick Thomas]

Thank you!

[Yakov Pechersky]

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]

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]

Cool.

[Yakov Pechersky]

where split_ifs knows how to break the if then else into two cases and give you the resulting goals

[Reid Barton]

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]

Hmm. Ok.

[Patrick Thomas]

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]

Looking at the definition doesn't really help. Equality in type theory is something you just get used to.

[Kevin Buzzard]

$\mathbb{N}=\mathbb{Z}$ is neither provable nor disprovable in Lean.

[Patrick Thomas]

Is that a statement that the types are equal?

[Reid Barton]

You can just think of = as built-in, as the thing that lets you subst (or rw, etc.)

[Kevin Buzzard]

Right. Equality of types is really random.

[Kevin Buzzard]

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]

Yes, I remember that.

[Kevin Buzzard]

Both are true, but they're true for different reasons.

[Kevin Buzzard]

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]

Is equal by definition the same as the lamba calculus equality? I forget what it is called, beta reduction or something?

[Kevin Buzzard]

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]

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]

https://leanprover.github.io/reference/expressions.html#computation

[Kevin Buzzard]

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]

eta equivalence for functions is on the list, eta equivalence for structures is not. Go figure. These are subtle design issues.

[Kevin Buzzard]

What matters (to me) is not what is true by definition, but what is true (or more precisely what is provable).

[Yakov Pechersky]

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]

But mk (re (mk a b)) (im (mk a b)) = mk a b probably _is_ definitional!

[Kevin Buzzard]

import data.complex.basic

open complex

example (a b : ℝ) :
  mk (re (mk a b)) (im (mk a b)) = mk a b := rfl

[Kevin Buzzard]

import data.complex.basic

open complex

example (z : ℂ) :
  mk (re z) (im z) = z := rfl -- fails

[Kevin Buzzard]

import data.complex.basic

open complex

example (z : ℂ) :
  mk (re z) (im z) = z := by cases z; refl -- works

[Yakov Pechersky]

Is some lemma somewhere tagged with [refl]in one case and not in another?

[Kevin Buzzard]

no, the difference is simply the difference between z : \C and complex.mk a b : \C

[Kevin Buzzard]

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]

Fascinating

[Kevin Buzzard]

crazy, if you ask me

[Yakov Pechersky]

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]

right. But if you take z apart, it works fine.

[Kevin Buzzard]

because re (mk a b) = a is definitional, because some greek letter happens to be in some set of definitional greek letters.

[Kevin Buzzard]

I think this might all go back to all those fractions which stop me getting past page 1 of Mario's thesis.

[Kevin Buzzard]

https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf

[Kevin Buzzard]

Oh it's p6 where the fractions start.

[Kevin Buzzard]

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]

I guess mk a b is a nice pleasant structured z unlike z \in

$${\displaystyle 0 =\sum _{n=1}^{\infty }{\frac {1}{n^{z}}}}$$

[Reid Barton]

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]

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]

You could even use constant/axiom to introduce +, but maybe it would be too disruptive

[Kevin Buzzard]

maybe I'll try that for the filter game.

[Kevin Buzzard]

maybe not.

[Kevin Buzzard]

Aah! So it's iota reduction.

[Patrick Thomas]

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]

Hmm. Could probably use finset.add_sum_diff_singleton.

[Patrick Thomas]

How do you make a finset from fin using finset.mk?

[Patrick Thomas]

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]

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]

Oh. Ok. Thank you.

[Bryan Gin-ge Chen]

Related: attr#to_additive

[Patrick Thomas]

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]

And if I forced it, then the sums etc. using finset would not be as expected.

[Patrick Thomas]

(deleted)

[Kevin Buzzard]

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]

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

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]

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]

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]

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]

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]

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]

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]

  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]

That works. Thank you!

[Patrick Thomas]

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]

by noncomm_ring does it

[Kenny Lau]

by rw [mul_add, nat.cast_one, mul_one, add_comm] should work (haven't tested)

[Kenny Lau]

if you count that as "one tactic"

[Patrick Thomas]

noncomm_ring worked. Thank you!

[Patrick Thomas]

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]

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]

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]

I'm not sure in what sense "there are more possibilities for induction principlles." Would you have an example?

[Kevin Buzzard]

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]

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]

What is a sum type? I'm not sure I follow the idea from the definition.

[Patrick Thomas]

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]

congr

[Yakov Pechersky]

or more cleanly, likely congr' 1

[Patrick Thomas]

Nice. Thank you!

[Patrick Thomas]

Is there a tactic to compute instances of function application?

[Patrick Thomas]

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]

try tactic#dsimp if that doesn't do what you want please post a #mwe

[Patrick Thomas]

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]

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]

So tactic#dsimp does work?

[Patrick Thomas]

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]

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]

Thank you!

[Alex J. Best]

                           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]

Maybe, I'm not sure.

[Patrick Thomas]

I agree, it does seem rather messy. I'm not sure what to pull out for lemmas though.

[Eric Wieser]

I think your fin.lt_one_eq_zero is docs#subsingleton.elim or similar

[Patrick Thomas]

Looks like it might be fin.eq_zero.

[Patrick Thomas]

Is there a fold operation defined for fin? I wonder if that would make it simpler.

[Johan Commelin]

There is finset.fold which you could apply on univ. Not sure if that is helpful.

[Patrick Thomas]

Yeah, I should probably just move to the library definition anyway. I had started this lemma, so I had wanted to finish it first.