Zulip Chat Archive

Stream: new members

Topic: formalizing definitions for real analysis


view this post on Zulip Patrick Thomas (Jul 24 2020 at 20:39):

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

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

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

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

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

view this post on Zulip Kenny Lau (Jul 24 2020 at 20:40):

just don't use backticks

view this post on Zulip Kenny Lau (Jul 24 2020 at 20:40):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 20:42):

Thank you.

view this post on Zulip Reid Barton (Jul 24 2020 at 20:49):

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

view this post on Zulip Reid Barton (Jul 24 2020 at 20:51):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 20:52):

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

view this post on Zulip Jalex Stark (Jul 24 2020 at 20:53):

(do you know that mathlib has lebesgue integration?)

view this post on Zulip Patrick Thomas (Jul 24 2020 at 20:55):

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

view this post on Zulip Jalex Stark (Jul 24 2020 at 20:55):

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

view this post on Zulip Jalex Stark (Jul 24 2020 at 20:56):

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

view this post on Zulip Jalex Stark (Jul 24 2020 at 20:57):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 20:57):

Cool. I'll take a look.

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 21:14):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 21:17):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 21:20):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 21:21):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 21:24):

What are "golfy term mode proofs"?

view this post on Zulip Patrick Thomas (Jul 24 2020 at 21:25):

Does that just mean really compact proofs or something more?

view this post on Zulip Reid Barton (Jul 24 2020 at 21:26):

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

view this post on Zulip Reid Barton (Jul 24 2020 at 21:27):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 21:28):

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

view this post on Zulip Reid Barton (Jul 24 2020 at 21:29):

Yes

view this post on Zulip Patrick Thomas (Jul 24 2020 at 21:30):

I see.

view this post on Zulip Patrick Thomas (Jul 24 2020 at 21:48):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 21:49):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 21:49):

So the difference is to make it ordered?

view this post on Zulip Patrick Thomas (Jul 24 2020 at 21:51):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 21:51):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:01):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:03):

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

view this post on Zulip Dan Stanescu (Jul 24 2020 at 22:04):

Adam Topaz said:

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

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:04):

You can still do it inductively with fin.

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:04):

Since fin.tail is a thing.

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:05):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:06):

And defining the empty partition is easy :)

view this post on Zulip Dan Stanescu (Jul 24 2020 at 22:06):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:07):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:08):

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

view this post on Zulip Reid Barton (Jul 24 2020 at 22:09):

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

view this post on Zulip Reid Barton (Jul 24 2020 at 22:10):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:10):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:10):

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

view this post on Zulip Reid Barton (Jul 24 2020 at 22:11):

Adam Topaz said:

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

Yes, which is the input of x

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:11):

Oh right :)

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:11):

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

view this post on Zulip Reid Barton (Jul 24 2020 at 22:12):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:12):

Doesn't this exist as a coersion?

view this post on Zulip Reid Barton (Jul 24 2020 at 22:13):

Not sure but it certainly exists in some form

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:14):

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

view this post on Zulip Dan Stanescu (Jul 24 2020 at 22:14):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:14):

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

view this post on Zulip Reid Barton (Jul 24 2020 at 22:17):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:18):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:18):

Reid Barton said:

Not sure but it certainly exists in some form

src#fin.cast_succ

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:19):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:19):

Just in case it's helpful later.

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:21):

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

view this post on Zulip Reid Barton (Jul 24 2020 at 22:22):

Well that's what your informal definition said right?

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:23):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:23):

It is the canonical type with n+1 elements

view this post on Zulip Jalex Stark (Jul 24 2020 at 22:23):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:24):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:25):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:32):

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

view this post on Zulip Jalex Stark (Jul 24 2020 at 22:33):

what would the m be doing there?

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:33):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:33):

or #print

view this post on Zulip Jalex Stark (Jul 24 2020 at 22:34):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:34):

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

view this post on Zulip Jalex Stark (Jul 24 2020 at 22:34):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:35):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:35):

except that it's a type, not a set

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:35):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:36):

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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:38):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:39):

I think I get it.

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:41):

Thank you.

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:42):

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

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

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:45):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 22:45):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:59):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 22:59):

The function?

view this post on Zulip Adam Topaz (Jul 24 2020 at 23:05):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 23:08):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 23:09):

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

view this post on Zulip Dan Stanescu (Jul 24 2020 at 23:10):

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 23:11):

But there are many partitions of any given interval

view this post on Zulip Dan Stanescu (Jul 24 2020 at 23:11):

True.

view this post on Zulip Patrick Thomas (Jul 24 2020 at 23:14):

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

view this post on Zulip Scott Morrison (Jul 24 2020 at 23:23):

Dan Stanescu said:

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

I would say yes.

view this post on Zulip Dan Stanescu (Jul 24 2020 at 23:25):

Patrick Thomas said:

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

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

view this post on Zulip Adam Topaz (Jul 24 2020 at 23:27):

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

view this post on Zulip Dan Stanescu (Jul 24 2020 at 23:31):

Scott Morrison said:

Dan Stanescu said:

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

I would say yes.

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

view this post on Zulip Scott Morrison (Jul 24 2020 at 23:32):

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

view this post on Zulip Scott Morrison (Jul 24 2020 at 23:32):

Others may have other opinions on this, however.

view this post on Zulip Patrick Thomas (Jul 24 2020 at 23:33):

Would it just be:

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

view this post on Zulip Scott Morrison (Jul 24 2020 at 23:33):

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

view this post on Zulip Patrick Thomas (Jul 24 2020 at 23:57):

How do you make a type out of a proposition?

view this post on Zulip Bryan Gin-ge Chen (Jul 24 2020 at 23:58):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 00:03):

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

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:06):

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

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:07):

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

view this post on Zulip Adam Topaz (Jul 25 2020 at 00:08):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 00:08):

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

view this post on Zulip Mario Carneiro (Jul 25 2020 at 00:22):

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

view this post on Zulip Mario Carneiro (Jul 25 2020 at 00:22):

Same deal with dedekind reals being isomorphic to cauchy reals

view this post on Zulip Mario Carneiro (Jul 25 2020 at 00:23):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:03):

Reid Barton said:

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

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

view this post on Zulip Reid Barton (Jul 25 2020 at 01:08):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:18):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:19):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:20):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:21):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:21):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:23):

fin n is an example of a structure

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:24):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:24):

it's morally equivalent (maybe literally defeq) to

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:24):

I don't understand your question

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:25):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:26):

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

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:26):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:27):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:27):

no

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:28):

you could define a partition and then prove

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

view this post on Zulip Bryan Gin-ge Chen (Jul 25 2020 at 01:28):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:29):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:29):

you should also try to prove lemmas that are mathematically obvious

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:30):

Interesting.

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:31):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:32):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:34):

Makes sense I guess.

view this post on Zulip Jalex Stark (Jul 25 2020 at 01:35):

a def is like a 0-field structure

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:48):

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

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:50):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 25 2020 at 01:52):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 01:54):

True.

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 02:19):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 02:20):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 02:22):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 02:23):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 02:54):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 02:58):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 03:08):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 03:09):

Just not intuitive to me I guess.

view this post on Zulip Jalex Stark (Jul 25 2020 at 03:09):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 03:10):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 03:12):

Maybe. I'm doing this for pedagogy though.

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 03:14):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 03:15):

But with the space of partitions has better properties.

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 03:15):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 03:15):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 03:17):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 03:17):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 03:18):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 03:18):

:)

view this post on Zulip Patrick Thomas (Jul 25 2020 at 03:19):

No problem.

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 08:24):

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

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 08:26):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 18:32):

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

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

view this post on Zulip Reid Barton (Jul 25 2020 at 18:33):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 18:33):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 18:34):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 18:36):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 18:36):

a and b are parameters aren't they?

view this post on Zulip Reid Barton (Jul 25 2020 at 18:36):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 18:37):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 18:37):

not sure what it does on out of range inputs

view this post on Zulip Patrick Thomas (Jul 25 2020 at 18:38):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 18:39):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 18:41):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 18:42):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 19:04):

Like this?

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 20:46):

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

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 20:46):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 20:47):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 20:52):

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

view this post on Zulip Reid Barton (Jul 25 2020 at 20:54):

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

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 21:01):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 21:07):

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

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

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 21:10):

I'd probably use finset.sup

view this post on Zulip Mario Carneiro (Jul 25 2020 at 21:13):

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

view this post on Zulip Mario Carneiro (Jul 25 2020 at 21:15):

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

view this post on Zulip Mario Carneiro (Jul 25 2020 at 21:19):

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

view this post on Zulip Patrick Thomas (Jul 25 2020 at 22:20):

Jalex Stark said:

I'd probably use finset.sup

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 22:48):

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

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

and composing this with finset.sup

view this post on Zulip Yury G. Kudryashov (Jul 25 2020 at 23:51):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 00:55):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 00:57):

Does defining foo not still require induction on the function?

view this post on Zulip Adam Topaz (Jul 26 2020 at 00:58):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 26 2020 at 00:58):

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

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

view this post on Zulip Reid Barton (Jul 26 2020 at 00:58):

These are just implementation details.

view this post on Zulip Adam Topaz (Jul 26 2020 at 00:59):

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

view this post on Zulip Adam Topaz (Jul 26 2020 at 00:59):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 26 2020 at 00:59):

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

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:01):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 01:21):

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

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

view this post on Zulip Reid Barton (Jul 26 2020 at 01:31):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 01:32):

oh is that supposed to be the second argument?

view this post on Zulip Patrick Thomas (Jul 26 2020 at 01:32):

That it doesn't terminate. Yeah :)

view this post on Zulip Reid Barton (Jul 26 2020 at 01:34):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 01:34):

I'm not sure what your goals are though.

view this post on Zulip Reid Barton (Jul 26 2020 at 01:35):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 01:35):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 01:35):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 01:37):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 01:38):

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

view this post on Zulip Adam Topaz (Jul 26 2020 at 01:40):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 01:43):

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

view this post on Zulip Jalex Stark (Jul 26 2020 at 01:44):

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

view this post on Zulip Scott Morrison (Jul 26 2020 at 01:47):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 01:48):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 01:48):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 01:49):

What is the first symbol in the second one?

view this post on Zulip Patrick Thomas (Jul 26 2020 at 01:51):

The one that looks like a square U.

view this post on Zulip Adam Topaz (Jul 26 2020 at 01:53):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 01:59):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 02:01):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 02:01):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 02:02):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 02:04):

I didn't know about the control click.

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 02:05):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 02:06):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 02:07):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 02:07):

Try noncomputable theory at the top of your file.

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 02:08):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 02:10):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 02:11):

The "supremum" part is noncomputable.

view this post on Zulip Patrick Thomas (Jul 26 2020 at 02:17):

(deleted)

view this post on Zulip Patrick Thomas (Jul 26 2020 at 02:19):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 02:54):

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

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 03:02):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 03:12):

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

view this post on Zulip Adam Topaz (Jul 26 2020 at 03:14):

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

view this post on Zulip Adam Topaz (Jul 26 2020 at 03:15):

You probably want i.succ - i.cast_succ

view this post on Zulip Patrick Thomas (Jul 26 2020 at 03:15):

That was what I was wondering.

view this post on Zulip Patrick Thomas (Jul 26 2020 at 03:17):

Thank you.

view this post on Zulip Adam Topaz (Jul 26 2020 at 03:17):

No problem!

view this post on Zulip Patrick Thomas (Jul 26 2020 at 03:53):

In summary:

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

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

view this post on Zulip Adam Topaz (Jul 26 2020 at 03:55):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 03:56):

Cool.

view this post on Zulip Adam Topaz (Jul 26 2020 at 03:57):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 03:58):

Sounds good.

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

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

view this post on Zulip Adam Topaz (Jul 26 2020 at 03:59):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 04:01):

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

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

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

view this post on Zulip Adam Topaz (Jul 26 2020 at 04:04):

Alternatively, you can do something like this:

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

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 04:05):

Good idea.

view this post on Zulip Adam Topaz (Jul 26 2020 at 04:06):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 04:08):

I might wait and look into that latter.

view this post on Zulip Patrick Thomas (Jul 26 2020 at 04:08):

I need to move on to Riemann sums :)

view this post on Zulip Patrick Thomas (Jul 26 2020 at 04:35):

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

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

?

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 07:20):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 07:50):

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

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 07:53):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 08:14):

Patrick Thomas said:

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

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

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

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

import data.real.basic data.set.intervals

noncomputable theory

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

namespace partition

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

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

end partition

open set

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

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 20:20):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 20:33):

Yury G. Kudryashov said:

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 20:35):

That takes the max, not the sum right?

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 20:35):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 20:37):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 20:38):

Alright.

view this post on Zulip Jalex Stark (Jul 26 2020 at 20:39):

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

view this post on Zulip Jalex Stark (Jul 26 2020 at 20:39):

this will automatically hide the proofs and emphasize docstrings

view this post on Zulip Jalex Stark (Jul 26 2020 at 20:40):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 20:40):

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

view this post on Zulip Jalex Stark (Jul 26 2020 at 20:40):

i don't know what you should do

view this post on Zulip Jalex Stark (Jul 26 2020 at 20:41):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 20:41):

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

view this post on Zulip Jalex Stark (Jul 26 2020 at 20:43):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 20:43):

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

view this post on Zulip Patrick Thomas (Jul 26 2020 at 20:44):

I see.

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 20:44):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 20:45):

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

view this post on Zulip Anatole Dedecker (Jul 26 2020 at 20:46):

Kevin Buzzard said:

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

And it has a nice notation too

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 20:46):

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

view this post on Zulip Anatole Dedecker (Jul 26 2020 at 20:49):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 20:49):

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

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 20:50):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 26 2020 at 20:52):

#mil should cover all this too, eventually.

view this post on Zulip Patrick Thomas (Jul 27 2020 at 04:03):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 27 2020 at 04:07):

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

view this post on Zulip Patrick Thomas (Jul 27 2020 at 04:08):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 27 2020 at 04:12):

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 01:26):

This compiles:

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

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

If I try this:

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

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 01:32):

Did you try open_locale big_operators?

view this post on Zulip Patrick Thomas (Jul 31 2020 at 01:35):

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

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

noncomputable theory

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

namespace partition

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

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

end partition

open set

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

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

open_locale big_operators

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

view this post on Zulip Jalex Stark (Jul 31 2020 at 02:22):

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 02:35):

Yeah the notation for Sum needs some arguments after it.

view this post on Zulip Alex J. Best (Jul 31 2020 at 02:48):

So this should be what you want i think:

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 03:29):

Jalex Stark said:

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

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 03:38):

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 03:41):

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 03:43):

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 03:44):

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 03:46):

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 03:46):

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 03:48):

Yeah always use the community web editor!

view this post on Zulip Alex J. Best (Jul 31 2020 at 03:49):

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 03:56):

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 04:00):

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 04:03):

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

view this post on Zulip Alex J. Best (Jul 31 2020 at 04:05):

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

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

noncomputable theory

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

namespace partition
open_locale nnreal

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

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

end partition

open set

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

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

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

open_locale big_operators

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

#print riemann_sum

view this post on Zulip Patrick Thomas (Jul 31 2020 at 04:10):

There is a proof in the definition?

view this post on Zulip Alex J. Best (Jul 31 2020 at 04:12):

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 04:15):

I see.

view this post on Zulip Patrick Thomas (Jul 31 2020 at 04:33):

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 04:34):

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 04:34):

Actually an inf right?

view this post on Zulip Alex J. Best (Jul 31 2020 at 04:35):

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 04:37):

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

view this post on Zulip Patrick Thomas (Jul 31 2020 at 04:37):

Is that by convention?

view this post on Zulip Patrick Thomas (Jul 31 2020 at 04:42):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:00):

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

import data.real.basic

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

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:02):

You mean

import data.real.basic

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

& similarly for lub

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:04):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:04):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:05):

What did I do wrong?

view this post on Zulip Reid Barton (Aug 01 2020 at 23:05):

It just doesn't make any sense.

view this post on Zulip Reid Barton (Aug 01 2020 at 23:05):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:05):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:06):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:07):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:07):

Which is right.

view this post on Zulip Reid Barton (Aug 01 2020 at 23:08):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:09):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:09):

You don't need to make use of it

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:09):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:09):

Maybe start with the definition in math?

view this post on Zulip Reid Barton (Aug 01 2020 at 23:10):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:10):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:12):

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

import data.real.basic

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

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

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:12):

ub of S that is.

view this post on Zulip Reid Barton (Aug 01 2020 at 23:15):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:15):

You could also reuse the whole structure ub

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:16):

What do you mean by reuse the whole structure ub?

view this post on Zulip Reid Barton (Aug 01 2020 at 23:20):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:21):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:22):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:23):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:24):

If I try to do:

import data.real.basic

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

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

I get an error on the last leq.

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:25):

abomination incoming:

import data.real.basic

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

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:25):

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

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:25):

you would have to write r.t instead

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:26):

What does r.t mean?

view this post on Zulip Reid Barton (Aug 01 2020 at 23:26):

ub.t r

view this post on Zulip Reid Barton (Aug 01 2020 at 23:26):

i.e. the t field

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:26):

Oh.

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:27):

#tpil

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:27):

Ch. 9

view this post on Zulip Reid Barton (Aug 01 2020 at 23:28):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:30):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:30):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:31):

It's not necessarily better or worse

view this post on Zulip Reid Barton (Aug 01 2020 at 23:31):

just different

view this post on Zulip Reid Barton (Aug 01 2020 at 23:32):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:32):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:33):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:33):

I see.

view this post on Zulip Reid Barton (Aug 01 2020 at 23:34):

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

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:35):

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

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:36):

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

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:36):

which means the implementation without structure is better

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:39):

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

import data.real.basic

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

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:42):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:43):

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

view this post on Zulip Reid Barton (Aug 01 2020 at 23:43):

but as I mentioned above it's awkward

view this post on Zulip Reid Barton (Aug 01 2020 at 23:44):

this awkwardness would disappear with the usual definition

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:44):

Alright.

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:44):

Thank you.

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:50):

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

view this post on Zulip Patrick Thomas (Aug 01 2020 at 23:57):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:03):

import data.real.basic

noncomputable theory
open_locale classical

namespace hidden

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

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

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

end hidden

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:04):

What does classical.epsilon $ is_lub S mean?

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:05):

is_lub S is a predicate on \R

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:05):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:05):

otherwise return a default element

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:09):

import data.real.basic

noncomputable theory
open_locale classical

namespace hidden

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

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

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

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

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

end hidden

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:09):

any this is the API for lub

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:09):

so you can forget about its definition

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:11):

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

view this post on Zulip Jalex Stark (Aug 02 2020 at 00:12):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:14):

Kenny Lau said:

otherwise return a default element

@Patrick Thomas

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:14):

you wouldn't get any error

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:14):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:15):

treat it as an unspecified constant

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:15):

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

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:16):

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

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:19):

Jalex Stark said:

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

Yes, but did not understand the result.

view this post on Zulip Jalex Stark (Aug 02 2020 at 00:21):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:24):

Patrick Thomas said:

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

because it has no definition

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:24):

it uses classical.choice

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:24):

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

view this post on Zulip Adam Topaz (Aug 02 2020 at 00:32):

(deleted)

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:37):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:38):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:38):

it will behave like an arbiratry real number

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:40):

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

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:40):

That is t : \R and t is_lub S.

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:41):

Or is it actually safer?

view this post on Zulip Patrick Thomas (Aug 02 2020 at 00:42):

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

view this post on Zulip Patrick Thomas (Aug 02 2020 at 01:16):

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

view this post on Zulip Patrick Thomas (Aug 02 2020 at 03:34):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 03:36):

that would mean every set has lub

view this post on Zulip Patrick Thomas (Aug 02 2020 at 03:41):

How do I get at the properties of lub S?

view this post on Zulip Kenny Lau (Aug 02 2020 at 07:32):

import data.real.basic

noncomputable theory
open_locale classical

namespace hidden

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

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

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

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

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

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

end hidden

view this post on Zulip Kenny Lau (Aug 02 2020 at 07:32):

is this enough API?

view this post on Zulip Kenny Lau (Aug 02 2020 at 07:32):

@Patrick Thomas

view this post on Zulip Patrick Thomas (Aug 02 2020 at 18:15):

Thank you!

view this post on Zulip Daniel Shapero (Aug 04 2020 at 16:43):

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

view this post on Zulip Patrick Thomas (Aug 06 2020 at 20:00):

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

view this post on Zulip Patrick Thomas (Aug 07 2020 at 23:04):

I would also be interested in hearing opinions on this.

view this post on Zulip Dan Stanescu (Aug 08 2020 at 00:04):

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

view this post on Zulip Patrick Thomas (Aug 08 2020 at 03:36):

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

import data.real.basic

namespace hidden

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

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


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

end hidden

view this post on Zulip Patrick Thomas (Aug 08 2020 at 03:57):

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

view this post on Zulip Patrick Thomas (Aug 08 2020 at 05:42):

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

import data.real.basic


namespace hidden

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

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

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

end hidden

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:26):

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

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:27):

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

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:28):

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

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:28):

which I guess still works

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:35):

import data.real.basic algebra.pointwise

namespace hidden

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

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

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

end hidden

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:35):

@Kevin Buzzard deja vu?

view this post on Zulip Patrick Thomas (Aug 08 2020 at 07:19):

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

view this post on Zulip Kenny Lau (Aug 08 2020 at 07:19):

don't use exists.elim

view this post on Zulip Kenny Lau (Aug 08 2020 at 07:19):

use let

view this post on Zulip Patrick Thomas (Aug 08 2020 at 07:22):

That works on existential elimination?

view this post on Zulip Patrick Thomas (Aug 08 2020 at 07:23):

Is there an example somewhere?

view this post on Zulip Utensil Song (Aug 08 2020 at 07:32):

Another more natural choice is to use tactic#obtain , example:

import tactic
import tactic.lint

open int

theorem le.antisymm :  {a b : }, a  b  b  a  a = b :=
begin
assume a b : , assume (H₁ : a  b) (H₂ : b  a),
obtain n, Hn := int.le.dest H₁,
obtain m, Hm := int.le.dest H₂,
have H₃ : a + of_nat (n + m) = a + 0, from
  calc
    a + of_nat (n + m) = a + (of_nat n + m) : rfl
      ... = a + (n + m)                     : by rw of_nat_eq_coe
      ... = a + n + m                       : by rw add_assoc
      ... = b + m                           : by rw Hn
      ... = a                               : Hm
      ... = a + 0                           : by rw add_zero,
have H₄ : of_nat (n + m) = of_nat 0, from add_left_cancel H₃,
have H₅ : n + m = 0,                 from of_nat.inj H₄,
have h₆ : n = 0,                     from nat.eq_zero_of_add_eq_zero_right H₅,
show a = b, from
  calc
    a = a + 0    : by simp_rw [add_zero]
  ... = a + n    : by simp_rw [h₆, int.coe_nat_zero]
  ... = b        : Hn
end

view this post on Zulip Kenny Lau (Aug 08 2020 at 07:36):

Patrick Thomas said:

Is there an example somewhere?

look at my proof

view this post on Zulip Kenny Lau (Aug 08 2020 at 07:36):

the let I used is the existential elimination

view this post on Zulip Ruben Van de Velde (Aug 08 2020 at 08:42):

Bit higher level than Kenny's:

  intros z a1,
  rw [H] at a1,
  obtain x, hx, y, hy, h := a1,
  linarith [h0.left x hx, h1.left y hy],

view this post on Zulip Patrick Thomas (Aug 08 2020 at 17:36):

Kenny Lau said:

Kevin Buzzard deja vu?

?

view this post on Zulip Patrick Thomas (Aug 08 2020 at 18:01):

Is there a way to make it more verbose? Something like obtain (x : ℝ, hx : x ∈ X, y : ℝ, hy : y ∈ Y, h : z = x + y) from a1,?

view this post on Zulip Ruben Van de Velde (Aug 08 2020 at 20:02):

Something like

obtain x, hx, y, hy, h :  x  X,  y  Y, z = x + y} := a1,

(untested)

view this post on Zulip Patrick Thomas (Aug 08 2020 at 20:07):

Sorry, I was thinking more along the lines of showing explicitly what hx, hy, and h get assigned to in the obtain statement.

view this post on Zulip Ruben Van de Velde (Aug 08 2020 at 20:17):

Yeah, I don't think that's possible

view this post on Zulip Patrick Thomas (Aug 08 2020 at 20:18):

:(

view this post on Zulip Patrick Thomas (Aug 08 2020 at 20:24):

I might prefer the exists.elim then, as it shows more of the details in the proof itself. I'm still not sure why I get type mismatch at application for the exists.elim s2 though.

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:29):

That's definitely possible

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:30):

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

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:30):

I don't know if obtain has a similar syntax

view this post on Zulip Patrick Thomas (Aug 08 2020 at 20:34):

Sorry, I'm not sure I see the difference. I still need to go to the other window to read what x, hx, etc. are?

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:34):

what's the mwe?

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:35):

Oh I misunderstood your question

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:36):

I've been planning to add support for type ascriptions in rcases/obtain, so that you could write

obtain x : , hx : x  X, y : , hy : y  Y, h : z = x + y from a1,

view this post on Zulip Patrick Thomas (Aug 08 2020 at 20:37):

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

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:37):

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

view this post on Zulip Mario Carneiro (Aug 08 2020 at 20:38):

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

view this post on Zulip Patrick Thomas (Aug 08 2020 at 20:49):

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

view this post on Zulip Patrick Thomas (Aug 08 2020 at 21:14):

I think I got it!

import data.real.basic algebra.pointwise

namespace hidden

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

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

theorem is_lub_add
  (X : set ) (a : ) (h0 : is_lub X a)
  (Y : set ) (b : ) (h1 : is_lub Y b)
  : is_ub (X + Y) (a + b) :=
  assume z : ,
  assume a1 : z  X + Y,
  have s1 :  x, ( y, x  X  y  Y  x + y = z), from a1,
  exists.elim s1 (
    assume x' : ,
    assume a2 :  y, x'  X  y  Y  x' + y = z,
      exists.elim a2 (
        assume y' : ,
        assume a3 : x'  X  y'  Y  x' + y' = z,
        have s2 : is_ub X a, from h0.left,
        have s3 : x'  a, from s2 x' a3.left,
        have s4 : is_ub Y b, from h1.left,
        have s5 : y'  b, from s4 y' a3.right.left,
        have s6 : x' + y'  a + b, by linarith,
        show z  a + b, by linarith
      )
  )

end hidden

view this post on Zulip Patrick Thomas (Aug 08 2020 at 22:32):

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

view this post on Zulip Anatole Dedecker (Aug 08 2020 at 22:33):

Oh

view this post on Zulip Anatole Dedecker (Aug 08 2020 at 22:33):

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

view this post on Zulip Anatole Dedecker (Aug 08 2020 at 22:34):

Well, I know why this happens : the hypothesis is_ub (X+Y) r in the implication is implicitly named a, shadowing the a you want

view this post on Zulip Anatole Dedecker (Aug 08 2020 at 22:37):

But the only way to avoid this I know is writing the implication as a forall, namely \for (h : is_ub (X+Y) r), .... This way you can name the hypothesis so no problem of shadowing. But this is quite ugly, so maybe there's a better solution ?

view this post on Zulip Patrick Thomas (Aug 08 2020 at 22:41):

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

view this post on Zulip Anatole Dedecker (Aug 08 2020 at 22:43):

By reading the error message :upside_down: The type of a is exactly the left side of your implication, which means precisely that a is a proof of is_ub (X+Y) r

view this post on Zulip Patrick Thomas (Aug 08 2020 at 22:44):

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

view this post on Zulip Patrick Thomas (Aug 08 2020 at 22:45):

Thank you.

view this post on Zulip Anatole Dedecker (Aug 08 2020 at 22:48):

No problem ! It would be nice for this to be fixed at some point anyway, but maybe it's harder than I imagine

view this post on Zulip Kenny Lau (Aug 09 2020 at 05:24):

just use guard_hyp

view this post on Zulip Mario Carneiro (Aug 09 2020 at 05:28):

Mario Carneiro said:

I've been planning to add support for type ascriptions in rcases/obtain, so that you could write

obtain x : , hx : x  X, y : , hy : y  Y, h : z = x + y from a1,

This works now, as of #3730, which is a significant rewrite of rcases to support some more flexible pattern syntax. You can now use parentheses like (a | b) | c in patterns instead of the previous strict alternation of and/or

view this post on Zulip Patrick Massot (Aug 09 2020 at 10:06):

Build is failing.

view this post on Zulip Anatole Dedecker (Aug 09 2020 at 20:02):

Kenny Lau said:

just use guard_hyp

Could you explain a bit more what you meant ?

view this post on Zulip Kenny Lau (Aug 10 2020 at 05:14):

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

view this post on Zulip Kenny Lau (Aug 10 2020 at 05:15):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 16:02):

I'm trying to define a partition using a list. Is this a good definition?

structure partition (a : ) (b : ) :=
(x : list )
(x_head : list.head' x = option.some a)
(x_last : list.last' x = option.some b)
(mono   : list.chain' real.le x)

I think the x_head and x_last constructors ensure that the list is not empty?
Using that I am trying to define the norm. I looked at using list.foldr for taking the max, but it requires an initial accumulator value that I would like to avoid.

view this post on Zulip Patrick Thomas (Sep 13 2020 at 16:07):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 17:30):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 17:35):

For example that l is a list in the definition of a vector?
https://leanprover-community.github.io/mathlib_docs/core/data/vector.html#vector

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 17:36):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 17:37):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 17:39):

Sorry

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 17:40):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 17:41):

Even more work :)

view this post on Zulip Bryan Gin-ge Chen (Sep 13 2020 at 17:41):

If you hover over .length in l.length, you can see that the URL ends in list.length which is a clue. But feel free to open an issue here.

view this post on Zulip Patrick Thomas (Sep 13 2020 at 17:41):

Ok. Thank you.

view this post on Zulip Patrick Thomas (Sep 13 2020 at 17:52):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 18:56):

If a vector is based on a list, how do you use the functions defined for lists on it? Do you have to cast it to a list first?

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 18:57):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 18:58):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 18:59):

The proof comes from the type somehow?

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 19:00):

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

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 19:00):

the proof comes from the proof which you'll supply that l.length=n when you're making the term. vector is a subtype -- see the link above.

view this post on Zulip Patrick Thomas (Sep 13 2020 at 19:34):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 19:41):

Got it. Thank you.

view this post on Zulip Patrick Thomas (Sep 13 2020 at 20:14):

Is there a function defined similar to vector.head for getting the last element of the vector where you don't have to worry about the vector being nil?

view this post on Zulip Patrick Thomas (Sep 13 2020 at 20:48):

I'm trying to make something like this work:

structure partition (a : ) (b : ) :=
(n : )
(x : vector  (n + 1))
(x_zero : vector.head x = a)
(x_last : vector.last x = b)
(mono : list.chain' real.le x.val)

structure pointed_partition (a b : ) extends partition a b :=
(y : vector  n)
(mem_block :  m : , m  n  y.at m  set.Icc ((x.at m) (x.at (m + 1)))

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 21:20):

Patrick Thomas said:

Is there a function defined similar to vector.head for getting the last element of the vector where you don't have to worry about the vector being nil?

I don't know the vector or list API's at all but why don't you just write the precise function you want and then ask whether this precise function is already there?

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:21):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:23):

The same as this but returns the last element instead of the first:

def head : vector α (nat.succ n)  α
|  [],    h  := by contradiction
|  a :: v, h  := a

view this post on Zulip Kyle Miller (Sep 13 2020 at 21:28):

It doesn't seem to exist already. One way is to define it with vector.nth:

import data.vector

def vector.last {α : Type*} {n : } (v : vector α n.succ) : α :=
v.nth n, nat.less_than_or_equal.refl

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:30):

Nice. Thank you.

view this post on Zulip Kyle Miller (Sep 13 2020 at 21:30):

Another is in terms of list.last:

import data.vector

def vector.last {α : Type*} {n : } : vector α n.succ  α
| [], h := by contradiction
| a :: v, h := (a :: v).last (by simp)

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:31):

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

view this post on Zulip Kyle Miller (Sep 13 2020 at 21:33):

I don't think so, since if you have a vector of length n+1, since it's zero-indexed the last element will be indexed by n.

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:33):

Oh. Right.

view this post on Zulip Adam Topaz (Sep 13 2020 at 21:36):

I don't know how heavily you're invested in vector, but all of these things (I think) are already in the API for fin n, i.e. representations of n-tuples as fin n \to A.

view this post on Zulip Yakov Pechersky (Sep 13 2020 at 21:37):

And data.matrix.notation has nice notation for those

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:40):

Not completely invested. I just figured that since there is a lot of beginner documentation and tutorials on lists and vectors that I would understand it better by going with that.

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:41):

For example I don't understand (finset.univ : finset (fin P.n)).sup (λ j, (P.x j.cast_succ - P.x j.succ))

view this post on Zulip Adam Topaz (Sep 13 2020 at 21:43):

Where's that from?

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:44):

Much earlier in the thread.

view this post on Zulip Adam Topaz (Sep 13 2020 at 21:46):

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

view this post on Zulip Adam Topaz (Sep 13 2020 at 21:46):

That should be approximately familiar mathematical notation.

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:48):

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

view this post on Zulip Adam Topaz (Sep 13 2020 at 21:49):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:50):

True.

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:51):

If I understand the API :)

view this post on Zulip Patrick Thomas (Sep 13 2020 at 21:53):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 22:00):

What is the * after Type by the way?

view this post on Zulip Adam Topaz (Sep 13 2020 at 22:00):

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

view this post on Zulip Patrick Thomas (Sep 13 2020 at 22:00):

Ah.

view this post on Zulip Yakov Pechersky (Sep 13 2020 at 22:40):

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

view this post on Zulip Yakov Pechersky (Sep 13 2020 at 22:41):

Then the supremum of the set of all those values, under the map taking each such value j to P.x[j + 1] - P.x[j]

view this post on Zulip Yakov Pechersky (Sep 13 2020 at 22:41):

In python list accession syntax

view this post on Zulip Yakov Pechersky (Sep 13 2020 at 22:44):

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

view this post on Zulip Patrick Thomas (Sep 14 2020 at 03:30):

For my own understanding, this seemed to work? Is this right?

namespace hidden

inductive nat : Type
| zero : nat
| succ : nat  nat


inductive vector (α : Type) : nat  Type
| nil : vector nat.zero
| cons (a : α) (n : nat) (v : vector n) : vector (nat.succ n)
-- a : element to prepend, n : length of vector to prepend to, v : vector to prepend to
-- note the use of n in the type of v


def first (α : Type) :  n : nat, vector α (nat.succ n)  α
| _ (vector.cons a _ _) := a


def v1 : vector nat nat.zero := vector.nil
def v2 : vector nat nat.zero.succ := vector.cons nat.zero nat.zero v1
def v3 : vector nat nat.zero.succ.succ := vector.cons nat.zero.succ nat.zero.succ v2

#reduce first nat nat.zero v2
#reduce first nat nat.zero.succ v3


def last (α : Type) :  n : nat, vector α (nat.succ n)  α
| _ (vector.cons a (nat.zero) vector.nil) := a
| _ (vector.cons _ (nat.succ n) v) := last n v

end hidden

view this post on Zulip Patrick Thomas (Sep 14 2020 at 03:32):

first and last didn't seem to need a proof that the vector wasn't empty like the ones in the library, so I'm a little unsure. I am guessing that is because of the way that vector was defined?

view this post on Zulip Patrick Thomas (Sep 14 2020 at 03:33):

Functionally I think this is equivalent though?

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 03:39):

The proof that it isn't empty in your definition is that the patterns you're matching on require a vector of length (n + 1)

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 03:41):

If you want to play more with these definitions, you could make se arguments implicit, like making the length argument to cons or first or last implicit. Since it can be inferred from the type of vector.

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 03:41):

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

view this post on Zulip Patrick Thomas (Sep 14 2020 at 03:44):

Yakov Pechersky said:

The proof that it isn't empty in your definition is that the patterns you're matching on require a vector of length (n + 1)

That is what I was guessing.

view this post on Zulip Patrick Thomas (Sep 14 2020 at 03:44):

Thank you.

view this post on Zulip Patrick Thomas (Sep 19 2020 at 14:40):

Yakov Pechersky said:

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

I'm sorry, I'm still not sure I get this. Maybe if the steps were broken apart it would be easier to see? How would it look if we first took the differences and then the sup? What would be the least abstract way to build this up from just the definition of fin?

view this post on Zulip Alex J. Best (Sep 19 2020 at 15:13):

fin n is the subtype of nat of nats which are less than n.
finset (fin n) is the type of all finite sets (unordered lists with no duplicates) whose members are all from fin n.
univ (or finset.univ if the namespace isn't open) is the term of finset X containing all terms of type X when X is a type with only finitely many terms (which fin n is).
If you just type #check finset.univ lean doesn't know what you want a finset of so (finset.univ : finset (fin n)) is the term representing the set of all the terms of fin n.
finset.sup then takes the supremum of the function (λ j, (P.x j.cast_succ - P.x j.succ)) over the specified set, with the dot notation so it comes after the set, in this case univ.

view this post on Zulip Alex J. Best (Sep 19 2020 at 15:16):

I think this code is taking the differences first then the sup already. The (λ j, (P.x j.cast_succ - P.x j.succ)) function is applied to each term of fin P.n and the sup is taken of those values as it goes.

view this post on Zulip Patrick Thomas (Sep 19 2020 at 15:21):

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

view this post on Zulip Alex J. Best (Sep 19 2020 at 15:23):

By unordered I mean the ordering doesn't matter, so its
{}, {0}, {1}, {2}, {0,1}, {0,2}, {1,2}, {0,1,2}
and the last one there is univ.

view this post on Zulip Patrick Thomas (Sep 19 2020 at 15:29):

I see.
What happens if the set has only one element? If I'm reading the definition of partition correctly, I think it allows that?

view this post on Zulip Patrick Thomas (Sep 19 2020 at 16:01):

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

view this post on Zulip Alex J. Best (Sep 19 2020 at 16:35):

If the partition has 1 element then n = 0 as it is a map from fin (n + 1) \to \R\ge0 so I think in that case its the sup over the empty set, which defaults to the infimum of the whole target. Which version of the code are you using, it changed a bit throughout this thread.

view this post on Zulip Patrick Thomas (Sep 19 2020 at 16:46):

I was thinking that since it is taking adjacent differences there would be a problem with the set of only one element, since that element does not have an adjacent element.

view this post on Zulip Patrick Thomas (Sep 19 2020 at 16:48):

I had been looking at the following code, but now it gives an error next to the .sup:

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

noncomputable theory

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

namespace partition

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

end partition

view this post on Zulip Patrick Thomas (Sep 19 2020 at 16:55):

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

view this post on Zulip Alex J. Best (Sep 19 2020 at 16:58):

the colon is specifying the type of the term on the left. finset.univ takes no explicit arguments, if you type #check finset.univ you should see finset.univ : finset ?M_1, so there are no arguments to be filled in, but there is a metavariable in the type, which means that lean doesn't know what sort of finset the term  finset.univ  is without extra hints, which is what the : is doing, telling lean what type you expect it to be.

view this post on Zulip Alex J. Best (Sep 19 2020 at 17:00):

You could instead tell lean you want to specify implicit arguments as arguments directly, by using @finset.univ, the type of this is now finset.univ : Π {α : Type u_1} [_inst_1 : fintype α], finset α, which we see has 2 arguments, the type and the fact it is a fintype, so we could write instead, (@finset.univ (fin P.n)).sup ...

view this post on Zulip Patrick Thomas (Sep 19 2020 at 17:02):

I see. Thank you.

view this post on Zulip Alex J. Best (Sep 19 2020 at 17:02):

The error next to the sup is discussed somewhere above in the thread, but its basically the issue you are worried about, if there is only one thing in the partition lean want to assign some default value to the norm, as its a sup over an empty set, but it doesn't have a sensible choice, as \R has no minimal element. Thats why in the version I gave a while ago I switched it to  \R\ge0, which has a minimal element!

view this post on Zulip Alex J. Best (Sep 19 2020 at 17:04):

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

view this post on Zulip Patrick Thomas (Sep 19 2020 at 17:06):

I see.

view this post on Zulip Patrick Thomas (Oct 30 2020 at 00:34):

Sorry, I'm trying to define something from scratch so that I can better understand it. It seems that this does not work, and I am guessing it may be why finset is involved? Is there a way to fix this definition?

def norm :  (n : ) (f : fin n  ), 
| 0 f := 0
| m f := min (f (fin.mk m sorry) - f (fin.mk (m - 1) sorry)) (norm (m - 1) f)

view this post on Zulip Patrick Thomas (Oct 30 2020 at 00:35):

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

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 00:54):

First comment, you probably want to do something that looks like:

import data.real.basic

def norm :  (n : ) (f : fin n  ), 
| 0 f := 0
| (m + 1) f := min (f (fin.mk (m + 1) sorry) - f (fin.mk m sorry)) (norm m f)

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 00:54):

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

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 00:54):

what's the error you get now?

view this post on Zulip Patrick Thomas (Oct 30 2020 at 00:59):

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

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 01:00):

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

view this post on Zulip Patrick Thomas (Oct 30 2020 at 01:03):

I'm using a function from fin n to R to define an ordered list of real numbers. If there is only one element in that 'list' I want to return 0. If the 'list' is [a, b, c, ...] I want to return the minimum of {b -a, c - b, ...}.

view this post on Zulip Patrick Thomas (Oct 30 2020 at 01:06):

Oops, make that the max of those numbers.

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 01:11):

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

view this post on Zulip Patrick Thomas (Oct 30 2020 at 01:13):

Ok.

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 01:13):

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

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 01:13):

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

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 01:15):

In the meantime, maybe something like:

import data.real.basic

noncomputable def norm : Π (n : ) (f : fin n  ), 
| 0       f := 0
| 1       f := 0
| (m + 2) f := min (f 1 - f 0) (norm (m + 1) (λ i, f i.succ))

view this post on Zulip Patrick Thomas (Oct 30 2020 at 01:16):

Interesting. Thank you!

view this post on Zulip Patrick Thomas (Oct 30 2020 at 02:01):

For the standard definition of a list, how would you write something like "every element in the list is 0" or "every element in the list is 0 except for n elements that are 1"?

view this post on Zulip Patrick Thomas (Oct 30 2020 at 02:10):

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

view this post on Zulip Patrick Thomas (Oct 30 2020 at 02:15):

But then that function should take a proof that n is less than the length of the list, and I'm not sure how that proof would be supplied in something like forall n : nat, n < list.len -> list.at n (sorry) = 0.

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 02:33):

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

example {l : list } {x : } : x  l  x = 0 := sorry

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 02:33):

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

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 02:33):

There's also docs#list.of_fn

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 02:34):

And also docs#vector.

view this post on Zulip Yakov Pechersky (Oct 30 2020 at 02:34):

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

view this post on Zulip Patrick Thomas (Oct 30 2020 at 02:50):

Thank you.

view this post on Zulip Patrick Thomas (Oct 31 2020 at 00:40):

Is there a way to say that l is not list.nil because that case has been exhausted?

def last (α : Type) : Π l : list α, ¬ l = list.nil  α
| list.nil h := absurd (eq.refl list.nil) h
| (list.cons a list.nil) _ := a
| (list.cons a l) _ := last l sorry

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 08:08):

Change that l to list.cons b m?

view this post on Zulip Patrick Thomas (Nov 01 2020 at 19:31):

I see. Thank you.

view this post on Zulip Patrick Thomas (Nov 01 2020 at 19:38):

I'm sorry, I'm still having a hard time understanding quotients and setoids. Is there a simpler way to define the norm and Riemann sum that doesn't rely on these? Perhaps casting fin n to a list?

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

noncomputable theory

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

namespace partition
open_locale nnreal

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

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

end partition

open set

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

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

open_locale big_operators

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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 19:47):

you mean like this?

import data.real.basic data.set.intervals

inductive pointed_partition :     Type
| nil :  a, pointed_partition a a
| cons :  a b c (y  set.Icc a b), pointed_partition b c  pointed_partition a c

def riemann_sum :  {a b}, pointed_partition a b  (  )  
| _ _ (pointed_partition.nil a) f := 0
| _ _ (pointed_partition.cons a b c y _ P) f := f y * (b - a) + riemann_sum P f

view this post on Zulip Patrick Thomas (Nov 01 2020 at 19:51):

I was actually thinking of keeping the definition of partition and pointed partition the same, but casting fin n to a list in the definition of norm and sum.

view this post on Zulip Mario Carneiro (Nov 01 2020 at 19:55):

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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 19:55):

you have no theorems

view this post on Zulip Mario Carneiro (Nov 01 2020 at 19:55):

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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 19:56):

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

view this post on Zulip Patrick Thomas (Nov 01 2020 at 19:57):

Just trying to make definitions that I understand so that I know how to use them. When I follow the definition of finset in mathlib I still get lost.

view this post on Zulip Mario Carneiro (Nov 01 2020 at 19:57):

how do you want to use them?

view this post on Zulip Patrick Thomas (Nov 01 2020 at 19:58):

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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 19:58):

okay, so pick a theorem and prove it

view this post on Zulip Mario Carneiro (Nov 01 2020 at 19:58):

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

view this post on Zulip Patrick Thomas (Nov 01 2020 at 19:59):

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

view this post on Zulip Patrick Thomas (Nov 01 2020 at 20:01):

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

view this post on Zulip Yakov Pechersky (Nov 01 2020 at 20:03):

Easy way of making a list from a fin n is docs#list.of_fn. But proving things about it will be harder than what you have. Try to make the statement of a theorem you want to prove. That will require some sort of basic definitions. Then you can try proving it. Clunky definitions will make proving things difficult. You can then alternate changing definitions, proving a little more, refining the theorem statament, etc

view this post on Zulip Patrick Thomas (Nov 01 2020 at 20:14):

Alright.

view this post on Zulip Patrick Thomas (Nov 01 2020 at 21:13):

Maybe instead of extending the definition of partition, pointed_partition should take a partition as a parameter? Because P' in this definition has no reference to P right? And it needs to.

∀ ε : ℝ, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ P : partition a b, (partition.norm P) < δ → ∀ P' : pointed_partition a b, abs ((riemann_sum a b P' f) - R) < ε

view this post on Zulip Patrick Thomas (Nov 01 2020 at 21:28):

I guess I could do this, but it seems a little unnatural?

def is_integral (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0 
 δ : nnreal, δ > 0   P : pointed_partition a b, (partition.norm (pointed_partition.to_partition P)) < δ 
abs ((riemann_sum a b P f) - R) < ε

view this post on Zulip Mario Carneiro (Nov 01 2020 at 21:28):

like this?

def partition.points {a b : } (P : partition a b) :=
Π m : fin P.n, Icc (P.x m.cast_succ) (P.x m.succ)

view this post on Zulip Mario Carneiro (Nov 01 2020 at 21:32):

I also want to observe that if you just wanted to say norm P < delta then there is no need to define norm

view this post on Zulip Mario Carneiro (Nov 01 2020 at 21:33):

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

view this post on Zulip Patrick Thomas (Nov 01 2020 at 21:34):

Or like this?

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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 21:34):

you could do that, yes

view this post on Zulip Patrick Thomas (Nov 01 2020 at 21:35):

Any foreseeable issues?

view this post on Zulip Mario Carneiro (Nov 01 2020 at 21:40):

well it's two things instead of one thing

view this post on Zulip Patrick Thomas (Nov 01 2020 at 22:18):

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

noncomputable theory

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


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


open_locale big_operators

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


def is_integral (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0 
 δ : , δ > 0   P : partition a b,  j : fin P.n, P.x j.succ - P.x j.cast_succ < δ 
 P' : pointed_partition a b P, abs ((riemann_sum a b P P' f) - R) < ε

view this post on Zulip Patrick Thomas (Nov 02 2020 at 04:16):

Why is the declaration of this example an invalid expression?

import data.real.basic data.set.intervals

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

structure pt_part {a b : } (P : part a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  set.Icc (P.x m.cast_succ) (P.x m.succ))

example {a b : } (P : part a b) :  P' : pt_part P := sorry

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:24):

An exists statement can only state something that is a Prop. Your pt_part P is a structure that has data, not just propositions.

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:25):

What would the P' do?

view this post on Zulip Patrick Thomas (Nov 02 2020 at 04:29):

It was going to be used in my theorem that the definition of the riemann integral is uniquely defined.

I guess maybe I should instead define a default p_part for an arbitrary part?

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:31):

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

view this post on Zulip Patrick Thomas (Nov 02 2020 at 04:31):

import data.real.basic data.set.intervals


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


noncomputable def norm_aux : Π (n : ) (f : fin (n + 1)  ), 
| 0       f := 0
| 1       f := 0
| (m + 2) f := max (f 1 - f 0) (norm_aux (m + 1) (fun i, f i))

noncomputable def norm {a b : } (P : part a b) :  := norm_aux P.n P.x

lemma blah {a b : } :  δ : , δ > 0   P : part a b, norm P < δ := sorry


structure pt_part {a b : } (P : part a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  set.Icc (P.x m.cast_succ) (P.x m.succ))

--lemma blah2 {a b : ℝ} (P : part a b) : ∃ P' : pt_part P := sorry

def rsum_aux : Π (n : ) (f : fin n  ), 
| 0       _ := 0
| (m + 1) f := f m + rsum_aux m (fun i, f i.succ)

def rsum {a b : } {P : part a b} (P' : pt_part P) (f :   ) : 
:= rsum_aux P.n (fun i : fin P.n, (P'.y i) * (P.x i.succ - P.x i.cast_succ))


def is_rint (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0   δ : , δ > 0   P : part a b, norm P < δ   P' : pt_part P, abs ((rsum P' f) - R) < ε


example (a b : ) (f :   ) (R₀ R₁ : ) (h0 : is_rint a b f R₀) (h1 : is_rint a b f R₁) : R₀ = R₁ :=
have s1 :  ε : , ε > 0  abs (R₀ - R₁) < ε := (
  assume ε : ,
  assume a1 : ε > 0,
  have s2 : ε / 2 > 0, by linarith,
  have s3 :  δ₀ : , δ₀ > 0   P : part a b, norm P < δ₀   P' : pt_part P, abs ((rsum P' f) - R₀) < ε / 2 := h0 (ε / 2) s2,
  have s4 :  δ₁ : , δ₁ > 0   P : part a b, norm P < δ₁   P' : pt_part P, abs ((rsum P' f) - R₁) < ε / 2 := h1 (ε / 2) s2,
  exists.elim s3 (
    assume δ₀ : ,
    assume a2 : δ₀ > 0   P : part a b, norm P < δ₀   P' : pt_part P, abs ((rsum P' f) - R₀) < ε / 2,
    exists.elim s4 (
      assume δ₁ : ,
      assume a3 : δ₁ > 0   P : part a b, norm P < δ₁   P' : pt_part P, abs ((rsum P' f) - R₁) < ε / 2,
      let δ := min δ₀ δ₁ in
      have s5 : δ > 0 := sorry,
      have s6 :  P : part a b, norm P < δ := blah δ s5,
      exists.elim s6 (
        assume P : part a b,
        assume a4 : norm P < δ,
        -- get an arbitrary p_part of P here.
      )
    )
  )
),
sorry

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:32):

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

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:32):

What's the ... there?

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:34):

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

view this post on Zulip Patrick Thomas (Nov 02 2020 at 04:34):

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

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:37):

import data.real.basic data.set.intervals

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

structure pt_part {a b : } (P : part a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : part a b) : inhabited (pt_part P) :=
⟨{ y := _,
  mem_block := _ }⟩

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:38):

Providing an inhabited instance allows you to use default for a default value, or arbitrary for a default value that one should not introspect

view this post on Zulip Patrick Thomas (Nov 02 2020 at 04:38):

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

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:39):

You do.

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:39):

You have to fill in those underscores

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:39):

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

view this post on Zulip Patrick Thomas (Nov 02 2020 at 04:39):

Ah. Ok. Thank you.

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:40):

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

view this post on Zulip Patrick Thomas (Nov 02 2020 at 04:45):

What is the syntax to get the default?

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:49):

import data.real.basic data.set.intervals

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

structure pt_part {a b : } (P : part a b) :=
(y : fin P.n  )
(mem_block :  m : fin P.n, y m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : part a b) : inhabited (pt_part P) :=
⟨{ y := λ i, sorry,
  mem_block := sorry }⟩

example {a b : } {P : part a b} : pt_part P := default _

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:49):

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

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:50):

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

view this post on Zulip Yakov Pechersky (Nov 02 2020 at 04:50):

That is, default gives you some α if you tell it what α you want and it can find an instance of inhabited α. And in the example, we can use an underscore, because the type α is inferable from the context.

view this post on Zulip Patrick Thomas (Nov 02 2020 at 04:55):

Nice. Thank you.

view this post on Zulip Patrick Thomas (Nov 03 2020 at 01:38):

Is this a correct definition for saying that R is the Riemann integral of f on [a,b]? I'm not sure about the after the δ > 0.

def is_riemann_integral (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0   δ : , δ > 0   P : partition a b, norm P < δ   Q : pointed_partition P, abs ((riemann_sum Q f) - R) < ε

view this post on Zulip Patrick Thomas (Nov 03 2020 at 02:27):

Also, how can I state this correctly?

example (f := fun x : , if x = 1 then 1 else 0) : is_riemann_integral 0 2 f 0 := sorry

view this post on Zulip Alex J. Best (Nov 03 2020 at 03:08):

I'd say just do

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

view this post on Zulip Alex J. Best (Nov 03 2020 at 03:09):

But

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

is more like what you had, if fis some long expression you want to use twice this can be helpful.

view this post on Zulip Patrick Thomas (Nov 03 2020 at 03:11):

Ok. Thank you!

view this post on Zulip Patrick Thomas (Nov 07 2020 at 04:43):

How would I set up the induction tactic for all_le_b so that it is decreasing?

import data.real.basic

namespace hidden

structure fin (n : ) :=
(i : )
(h : i < n)


lemma lt_succ_1 {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_2 {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ (n : ) : n < n + 1 := sorry
lemma zero_lt_succ {n : } : 0 < n + 1 := sorry


def cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.i (lt_succ_1 a.h)

def succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.i + 1) (lt_succ_2 a.h)

def fin_zero {n : } : fin (n + 1) :=
@fin.mk (n + 1) 0 zero_lt_succ

def fin_last {n : } : fin (n + 1) :=
@fin.mk (n + 1) n (lt_succ n)

/-
n = 0 :
x : 0 → ℝ
a = x 0 = b
n = 1 :
x : [0, 1] → ℝ
a = x 0 ≤ x 1 = b
-/
structure partition (a : ) (b : ) :=
(n : )
(x : fin (n + 1)  )
(x_zero : x fin_zero = a)
(x_last : x fin_last = b)
(mono :  m : fin n, x (cast_succ m)  x (succ m))


/-
nat.zero
Goal : a ≤ P.x {0, 0 < P.n + 1}

nat.succ
IH : m < P.n + 1 → a ≤ P.x {m, m < P.n + 1}
Goal : m + 1 < P.n + 1 → a ≤ P.x {m + 1, m + 1 < P.n + 1}
-/
lemma a_le_all {a b : } (P : partition a b) :  m : fin (P.n + 1), a  P.x m :=
begin
assume m : fin (P.n + 1),
induction m,
induction m_i,
case nat.zero {
  have s0 : a = P.x fin_zero := eq.symm P.x_zero,
  show a  P.x fin_zero, from sorry
},
case nat.succ : m IH {
  -- m_h : m.succ < P.n + 1
  -- IH : ∀ (m_h : m < P.n + 1), a ≤ P.x {i := m, h := m_h}
  have s0 : m + 1 < P.n + 1 := m_h,
  have s1 : m < P.n := sorry,
  have s2 : m < P.n + 1 := sorry,
  have s3 : a  P.x (cast_succ {i := m, h := s1}) := IH s2,
  have s4 : P.x (cast_succ {i := m, h := s1})  P.x (succ {i := m, h := s1}) := P.mono {i := m, h := s1},
  show a  P.x (succ {i := m, h := s1}), from le_trans s3 s4
}
end

lemma a_le_b {a b : } (P : partition a b) : a  b :=
have s0 : a  P.x (@fin_last P.n) := a_le_all P (@fin_last P.n),
have s1 : P.x (@fin_last P.n) = b := P.x_last,
show a  b, from sorry

lemma all_le_b {a b : } (P : partition a b) :  m : fin (P.n + 1), P.x m  b :=
begin
assume m : fin (P.n + 1),
induction m,
induction m_i using ?,
end

end hidden

view this post on Zulip Mario Carneiro (Nov 07 2020 at 07:37):

namespace fin

theorem lt_succ_iff {k} :  {m : fin (k+1)} {n : fin k},
  m < fin.succ n  m  cast_succ n
| m, _ n, _ := @nat.lt_succ_iff m n

end fin

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

lemma mono' {a b : } (P : partition a b) {i j : fin (P.n + 1)} : i  j  P.x i  P.x j :=
begin
  apply fin.induction_on j,
  { intro h, rw le_antisymm h (fin.zero_le _) },
  { intros j IH h,
    rcases lt_or_eq_of_le h with h | rfl,
    { exact (IH (fin.lt_succ_iff.1 h)).trans (P.mono _) },
    { refl } }
end

lemma a_le_all {a b : } (P : partition a b) (m : fin (P.n + 1)) : a  P.x m :=
by simpa [P.x_zero] using mono' P (fin.zero_le m)

lemma a_le_b {a b : } (P : partition a b) : a  b :=
by rw  P.x_last; apply a_le_all

lemma all_le_b {a b : } (P : partition a b) (m : fin (P.n + 1)) : P.x m  b :=
by simpa [P.x_last] using mono' P (fin.le_last m)

view this post on Zulip Patrick Thomas (Nov 07 2020 at 23:11):

Thank you.

view this post on Zulip Patrick Thomas (Nov 08 2020 at 00:17):

What is it in the mathlib definition of fin that allows for apply fin.induction_on j? It doesn't seem to work with my definition of fin.

view this post on Zulip Bryan Gin-ge Chen (Nov 08 2020 at 00:20):

docs#fin.induction_on is a lemma that's in mathlib about the mathlib definition of fin; you'd have to prove an analogue involving your fin for apply fin.induction_on to work with your type.

view this post on Zulip Patrick Thomas (Nov 08 2020 at 00:22):

Oh, right. Thank you.

view this post on Zulip Patrick Thomas (Nov 09 2020 at 05:19):

How would I get something that represents the maximum of an arbitrary choice of the ms in this example (that would be an upper bound for abs f on [a, b])?

import data.real.basic data.set.intervals

def is_bounded_on (a b : ) (f :   ) : Prop :=  M : ,  x  set.Icc a b, abs (f x)  M

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

example {a b : } (P : partition a b) (f :   ) :
( i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f)  is_bounded_on a b f :=
assume a0 :  i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
have s0 :  i : fin P.n,  m : ,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m := (
assume i : fin P.n,
a0 i
),
sorry

view this post on Zulip Patrick Thomas (Nov 10 2020 at 00:13):

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

view this post on Zulip Patrick Thomas (Nov 10 2020 at 03:48):

Hmm. Perhaps:

example {a b : } (P : partition a b) (f :   ) :
( i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f)  is_bounded_on a b f :=
assume a0 :  i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
let m := fun i : fin P.n, Exists.some (a0 i) in
sorry

view this post on Zulip Patrick Thomas (Nov 16 2020 at 03:02):

I was wondering if someone could help me understand what is going wrong with and how to fix s2:

import data.real.basic

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

example {a b : } (P : partition a b) : P.n = 0  a = b :=
assume a0 : P.n = 0,
have s0 : a = P.x 0 := eq.symm P.x_zero,
have s1 : P.x (fin.last P.n) = b := P.x_last,
have s2 : fin.last P.n = 0 := @eq.subst  (fun n : , fin.last P.n = fin.last n) P.n 0 a0 (eq.refl (fin.last P.n)),
have s3 : P.x 0 = b := eq.subst s2 s1,
eq.trans s0 s3

view this post on Zulip Patrick Thomas (Nov 16 2020 at 04:00):

I guess this works:

import data.real.basic

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

example {a b : } (P : partition a b) : P.n = 0  a = b :=
assume a0 : P.n = 0,
have s0 : a = P.x 0 := eq.symm P.x_zero,
have s1 : P.x (fin.last P.n) = b := P.x_last,
have s2 : fin.last P.n = 0 := fin.ext a0,
have s3 : P.x 0 = b := eq.subst s2 s1,
eq.trans s0 s3

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 05:10):

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

view this post on Zulip Patrick Thomas (Nov 16 2020 at 05:12):

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

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 06:53):

What parts of Lean would you consider lean dependent in reading? I find the "ext" and "eq.subst" more difficult to parse. I think of those to be pretty Lean dependent in reading.

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 06:55):

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

view this post on Zulip Patrick Thomas (Nov 16 2020 at 18:26):

"I find the "ext" and "eq.subst" more difficult to parse. I think of those to be pretty Lean dependent in reading."
What would you replace them with?

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 18:26):

tactics!

view this post on Zulip Patrick Thomas (Nov 16 2020 at 18:28):

I mean which tactics :)

view this post on Zulip Patrick Thomas (Nov 16 2020 at 18:28):

rw?

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 18:30):

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

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 18:33):

import data.real.basic

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

example {a b : } (P : partition a b) : P.n = 0  a = b :=
begin
  rcases P with n, x, rfl, rfl, mono⟩,
  show n = 0  _,
  rintro rfl,
  congr',
end

view this post on Zulip Patrick Thomas (Nov 16 2020 at 18:34):

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

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 18:35):

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

view this post on Zulip Mario Carneiro (Nov 16 2020 at 18:36):

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

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 18:37):

example {a b : } (P : partition a b) : P.n = 0  a = b :=
begin
  -- Let n and x be the data associated to P
  rcases P with n, x, rfl, rfl, mono⟩,
  -- assume n = 0.
  show n = 0  _,
  rintro rfl,
  -- The goal is now to prove x 0 = x (fin.last 0)
  -- but this is trivial
  congr',
end

view this post on Zulip Reid Barton (Nov 16 2020 at 18:38):

(rfl : a = b) is a nice trick

view this post on Zulip Patrick Thomas (Nov 16 2020 at 18:38):

Kevin Buzzard said:

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

Perhaps. I still like to though. Its too bad there isn't a mechanism to turn tactic proofs into something a mathematician without Lean could follow.

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 18:39):

Well, I guess I can read some proofs fine without using Lean, because I can "be the compiler" (something Mario used to encourage me to do when I was a beginner).

view this post on Zulip Mario Carneiro (Nov 16 2020 at 18:39):

You can also do this in "term mode" using the equation compiler for a similar proof

example :  {a b : } (P : partition a b), P.n = 0  a = b
| _ _ n, x, rfl, rfl, _ rfl := rfl

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 18:39):

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

view this post on Zulip Mario Carneiro (Nov 16 2020 at 18:44):

But in case you haven't noticed yet, my strategy for making readable proofs is to get them over with as quickly as possible, which forces the proof to be pretty slick and hopefully convincing the reader that they didn't want to read the proof anyway

view this post on Zulip Mario Carneiro (Nov 16 2020 at 18:46):

For longer proofs, tactic mode is much better than term mode for conveying structure and order to the proof, and you don't really want to read these proofs without tool assistance anyway because the local context is super important and much harder to read in any static textual form

view this post on Zulip Mario Carneiro (Nov 16 2020 at 18:47):

The only static form I really think does the job is #explode / metamath proofs, which are crazy verbose unless you are really regimented about your context management

view this post on Zulip Patrick Thomas (Nov 16 2020 at 18:48):

What is #explode?

view this post on Zulip Mario Carneiro (Nov 16 2020 at 18:48):

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

view this post on Zulip Patrick Thomas (Nov 16 2020 at 18:49):

Huh. Cool. I'll take a look.

view this post on Zulip Mario Carneiro (Nov 16 2020 at 18:49):

import tactic

#explode classical.em
classical.em :  (p : Prop), p  ¬p
0      p                                 Prop
1      _private.1778634979.not_uv_or_p   u p  v p  p
2      hne                                u p  v p
3      _private.4061111967.p_implies_uv   p  u p = v p
43,2   mt                                 ¬p
54     or.inr                             p  ¬p
62,5   I                                u p  v p  p  ¬p
7      or.inl                            p  p  ¬p
81,6,7 or.elim                           p  ¬p
90,8   I                                 (p : Prop), p  ¬p

view this post on Zulip Patrick Thomas (Nov 16 2020 at 18:52):

Interesting.

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 19:02):

import data.real.basic

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

example {a b : } (P : partition a b) : P.n = 0  a = b :=
λ (h : P.n = 0),
have hn : fin.last P.n = 0, from fin.eq_of_veq h,
calc a = P.x 0 : P.x_zero.symm
...    = P.x (fin.last P.n) : congr_arg P.x hn.symm
...    = b : P.x_last

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 19:06):

This gives the proof state explicitly, and the Lean steps to convert from one state to another. It's difficult to avoid "Lean-like" terms or syntax, because of fin.

view this post on Zulip Patrick Thomas (Nov 21 2020 at 03:58):

I'm a bit confused. Why does this compile, when s may not have type fin (n + 1)?

import data.real.basic

def blah (n : ) (f : fin (n + 1)  ) : Π (m : ), 
| 0        := f 0
| (s + 1)  := f s

view this post on Zulip Alex J. Best (Nov 21 2020 at 04:03):

You can do

#print blah._main

to see whats produced is

def polynomial.blah._main : Π (n : ), (fin (n + 1)  )     :=
λ (n : ) (f : fin (n + 1)  ) (m : ), m.cases_on (id_rhs  (f 0)) (λ (m : ), id_rhs  (f m))

view this post on Zulip Alex J. Best (Nov 21 2020 at 04:03):

So its coercing naturals to fin (n+1)

view this post on Zulip Patrick Thomas (Nov 21 2020 at 04:04):

What happens if m can not be coerced?

view this post on Zulip Alex J. Best (Nov 21 2020 at 04:06):

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

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

view this post on Zulip Patrick Thomas (Nov 21 2020 at 04:07):

Huh. Why does it do that?

view this post on Zulip Patrick Thomas (Nov 21 2020 at 04:14):

I guess because it is defined to :)

view this post on Zulip Bryan Gin-ge Chen (Nov 21 2020 at 04:14):

Here's one way to find out:

import tactic
variables (n : )
#check (by apply_instance : has_coe_t  (fin (n+1)))
/-
nat.cast_coe : has_coe_t ℕ (fin (n + 1))
-/

That points to docs#nat.cast_coe, which is an instance that defines a coercion from to any type with has_zero, has_one and has_add.

view this post on Zulip Bryan Gin-ge Chen (Nov 21 2020 at 04:16):

Unfolding the definition, you get to src#nat.cast, which is defined as the following:

/-- Canonical homomorphism from `ℕ` to a type `α` with `0`, `1` and `+`. -/
protected def cast :   α
| 0     := 0
| (n+1) := cast n + 1

view this post on Zulip Bryan Gin-ge Chen (Nov 21 2020 at 04:19):

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

view this post on Zulip Patrick Thomas (Nov 21 2020 at 04:29):

Thank you.

view this post on Zulip Mario Carneiro (Nov 21 2020 at 04:29):

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

view this post on Zulip Patrick Thomas (Nov 21 2020 at 04:35):

Given a definition like the following, is there a way to supply some chosen parameters to it, and see what everything gets assigned to in each step as it unfolds, as a way to verify that it works as intended?

noncomputable def fin_max : Π (n : ) (f : fin (n + 1)  ), 
| 0       f := f 0
| (m + 1) f := max (f (m + 1)) (fin_max m (fun i : fin (m + 1), f i))

view this post on Zulip Mario Carneiro (Nov 21 2020 at 04:51):

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

view this post on Zulip Mario Carneiro (Nov 21 2020 at 04:51):

If you use a computational type you can #eval it

view this post on Zulip Mario Carneiro (Nov 21 2020 at 04:53):

def fin_max {α} [linear_order α] : Π (n : ) (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (m + 1)) (fin_max m (fun i : fin (m + 1), f i))

#eval fin_max 5 (λ i, i.1 + 2) -- 7

view this post on Zulip Patrick Thomas (Nov 21 2020 at 04:53):

I was actually thinking in more general terms, for any inductive definition. Like it prints out:
iteration 0:
param_name_0 = ...
param_name_1 = ...

iteration 1:
param_name_0 = ...
param_name_1 = ...
...

view this post on Zulip Mario Carneiro (Nov 21 2020 at 04:56):

meta def fin_max {α} [linear_order α] [has_to_format α] : Π (n : ) (f : fin (n + 1)  α), α
| 0       f :=
  trace (to_string format!"iteration 0: {f 0}") $ f 0
| (m + 1) f :=
  let a := f (m + 1), b := fin_max m (fun i : fin (m + 1), f i) in
  trace (to_string format!"iteration {m + 1}: max {a} {b} = {max a b}") $
  max a b

#eval fin_max 5 (λ i, i.1 + 2) -- 7
-- iteration 0: 2
-- iteration 1: max 3 2 = 3
-- iteration 2: max 4 3 = 4
-- iteration 3: max 5 4 = 5
-- iteration 4: max 6 5 = 6
-- iteration 5: max 7 6 = 7

view this post on Zulip Patrick Thomas (Nov 21 2020 at 04:58):

Cool! Thanks!

view this post on Zulip Patrick Thomas (Nov 23 2020 at 02:49):

I can prove it, but is there an existing theorem that says that if i : fin 1 then i = 0? Is there also an existing theorem that breaks i : fin n + 1 into the cases i = fin.last n and i : fin n?

view this post on Zulip Kenny Lau (Nov 23 2020 at 02:51):

Probably Lean knows that fin 1 is a subsingleton

view this post on Zulip Kenny Lau (Nov 23 2020 at 02:52):

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

view this post on Zulip Yakov Pechersky (Nov 23 2020 at 02:59):

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

view this post on Zulip Yakov Pechersky (Nov 23 2020 at 03:01):

What do you mean by breaking a fin (n + 1) into fin n? They're different types. Can you prove your statement for 0 : fin (n + 1) and using that, the inductive step? Then you can use fin.induction_on. Or if you have no need to induct, you can use refine fin.cases _ _ i. Do you need to break it into [0, n) and {n}? Then we can write fin.decreasing_induction

view this post on Zulip Patrick Thomas (Nov 23 2020 at 03:04):

I was thinking about an easier and more readable way to do the or.elim here:

import data.real.basic


def fin_max {α} [linear_order α] : Π (n : ) (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (fin.last (m + 1))) (fin_max m (fun i : fin (m + 1), f i.cast_succ))


example {α} [linear_order α] (n : ) (f : fin (n + 1)  α) :  i : fin (n + 1), f i  (fin_max n f) :=
begin
induction n,
case nat.zero {
  assume i : fin (0 + 1),
  have s0 : i.val  0 := fin.le_last i,
  have s1 : i.val = 0 := nat.eq_zero_of_le_zero s0,
  have s2 : i = 0 := fin.ext s1,
  have s3 : f i  f 0 := eq.subst s2 (le_refl (f i)),
  have s4 : fin_max 0 f = f 0 := eq.refl (fin_max 0 f),
  show f i  fin_max 0 f, from eq.subst (eq.symm s4) s3
},
case nat.succ : n IH {
  assume i : fin (n.succ + 1),
  let f' := fun i : fin n.succ, f i.cast_succ,

  have s5 : fin_max n.succ f = max (f (fin.last n.succ)) (fin_max n f') := eq.refl (fin_max n.succ f),

  have s6 : f (fin.last n.succ)  max (f (fin.last n.succ)) (fin_max n f') := le_max_left (f (fin.last n.succ)) (fin_max n f'),
  have s7 : f (fin.last n.succ)  fin_max n.succ f := eq.subst (eq.refl s5) s6,

  have s8 : fin_max n f'  max (f (fin.last n.succ)) (fin_max n f') := le_max_right (f (fin.last n.succ)) (fin_max n f'),
  have s9 : fin_max n f'  fin_max n.succ f := eq.subst (eq.refl s5) s8,

  have s10 : i.val  n.succ := fin.le_last i,
  have s11 : i.val < n.succ  i.val = n.succ := lt_or_eq_of_le s10,
  exact or.elim s11
  (
    assume a0 : i.val < n.succ,
    let i' := fin.mk i.val a0 in
    have s12 : f' i'  fin_max n f' := IH f' i',
    have s13 : f' i' = f i'.cast_succ := eq.refl (f' i'),
    have s14 : f i'.cast_succ  fin_max n f' := eq.subst s13 s12,
    have s15 : i'.cast_succ = i := fin.mk_coe i,
    have s16 : f i  fin_max n f' := eq.subst s15 s14,
    show f i  fin_max n.succ f, from le_trans s16 s9
  )
  (
    assume a1 : i.val = n.succ,
    have s17 : i = fin.last n.succ := fin.ext a1,
    show f i  fin_max n.succ f, from eq.subst (eq.symm s17) s7
  )
}
end

view this post on Zulip Yakov Pechersky (Nov 23 2020 at 03:25):

Does this help?

import data.real.basic

variables {α : Type*} [linear_order α] {n : }

def fin_max : Π {n : } (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (fin.last (m + 1))) (fin_max (fun i : fin (m + 1), f i.cast_succ))

example (f : fin (n + 1)  α) (i : fin (n + 1)) : f i  (fin_max f) :=
begin
  induction n with n hn,
  { have : i = 0 := by simp,
    simp only [this, fin_max] },
  {
    apply fin.induction_on i,
    { simp only [fin_max, le_max_iff],
      right,
      have : f 0 = (λ (k : fin (n + 1)), f k.cast_succ) 0 := rfl,
      rw this,
      apply hn },
    { sorry },
  }
end

view this post on Zulip Kenny Lau (Nov 23 2020 at 03:35):

import data.real.basic

variables {α : Type*} [linear_order α] {n : }

def fin_max : Π {n : } (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (fin.last (m + 1))) (fin_max (λ i : fin (m + 1), f i.cast_succ))

lemma le_fin_max (f : fin (n + 1)  α) (i : fin (n + 1)) : f i  fin_max f :=
begin
  induction n with n ih,
  { have : i = 0 := subsingleton.elim _ _,
    simp only [this, fin_max] },
  { by_cases hi : (i : ) < n.succ,
    { rw  fin.cast_succ_cast_lt i hi,
      exact le_max_right_of_le (ih (λ i : fin (n + 1), f i.cast_succ) (i.cast_lt hi)) },
    { rw fin.eq_last_of_not_lt hi,
      exact le_max_left _ _ } }
end

view this post on Zulip Patrick Thomas (Nov 23 2020 at 03:52):

Thank you both.

view this post on Zulip Patrick Thomas (Nov 28 2020 at 23:14):

How can I use my definition of fin.max in the last example? Should I change my definition or the statement of the lemmas somehow?

import algebra.order data.real.basic data.set.intervals

namespace hidden

structure fin (n : ) :=
(val : )
(prop : val < n)


lemma lt_lt_succ {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ {n : } : n < n + 1 := sorry
lemma succ_pos {n : } : 0 < n + 1 := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry


def fin.cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.val (lt_lt_succ a.prop)

def fin.succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.val + 1) (lt_succ_lt_succ a.prop)

instance {n : } : has_zero (fin (n + 1)) := {zero := @fin.mk (n + 1) 0 succ_pos}

def fin.last (n : ) : fin (n + 1) :=
@fin.mk (n + 1) n lt_succ


lemma fin.eq_of_veq {n : } {i j : fin n} : i.val = j.val  i = j := sorry


@[elab_as_eliminator] def fin.induction {n : } {C : fin (n + 1)  Sort*}
(h0 : C 0) (hs :  i : fin n, C i.cast_succ  C i.succ) : Π (i : fin (n + 1)), C i := sorry

@[elab_as_eliminator] def fin.induction_on {n : } (i : fin (n + 1)) {C : fin (n + 1)  Sort*}
(h0 : C 0) (hs :  i : fin n, C i.cast_succ  C i.succ) : C i := fin.induction h0 hs i


def fin.max {α} [linear_order α] : Π (n : ) (f : fin (n + 1)  α), α
| 0       f := f 0
| (m + 1) f := max (f (fin.last (m + 1))) (fin.max m (fun i : fin (m + 1), f (fin.cast_succ i)))


lemma fin.all_le_max {α} [linear_order α] (n : ) (f : fin (n + 1)  α) :  i : fin (n + 1), f i  (fin.max n f) :=
begin
induction n,
case nat.zero {
  -- f : fin (0 + 1) → α
  show  (i : fin (0 + 1)), f i  fin.max 0 f, from
  assume i : fin (0 + 1),
  have s0 : i.val < 1 := i.prop,
  have s1 : i.val = 0 := lt_one s0,
  have s2 : i = 0 := fin.eq_of_veq s1,
  have s3 : fin.max 0 f = f 0 := eq.refl (fin.max 0 f),
  have s4 : fin.max 0 f = f i := eq.subst (eq.symm s2) s3,
  show f i  fin.max 0 f, from eq.ge s4
},
case nat.succ : n IH {
  -- f : fin (n.succ + 1) → α
  -- IH : ∀ (f : fin (n + 1) → α) (i : fin (n + 1)), f i ≤ fin.max n f
  show  (i : fin (n.succ + 1)), f i  fin.max n.succ f, from
  assume i : fin (n.succ + 1),
  let f' : fin (n + 1)  α := fun i : fin n.succ, f (fin.cast_succ i) in
  have s5 : fin.max n.succ f = max (f (fin.last n.succ)) (fin.max n f') := eq.refl (fin.max n.succ f),
  have s6 : f (fin.last n.succ)  max (f (fin.last n.succ)) (fin.max n f') := le_max_left (f (fin.last n.succ)) (fin.max n f'),
  have s7 : f (fin.last n.succ)  fin.max n.succ f := eq.subst (eq.refl s5) s6,
  have s8 : fin.max n f'  max (f (fin.last n.succ)) (fin.max n f') := le_max_right (f (fin.last n.succ)) (fin.max n f'),
  have s9 : fin.max n f'  fin.max n.succ f := eq.subst (eq.refl s5) s8,
  have s10 : i.val < n.succ + 1 := i.prop,
  have s11 : i.val  n.succ := le_of_lt_succ s10,
  have s12 : i.val < n.succ  i.val = n.succ := lt_or_eq_of_le s11,
  show f i  fin.max n.succ f, from or.elim s12
  (
    assume a0 : i.val < n.succ,
    let i' : fin n.succ := fin.mk i.val a0 in
    have s13 : (fin.cast_succ i').val = i.val := eq.refl (fin.cast_succ i').val,
    have s14 : (fin.cast_succ i') = i := fin.eq_of_veq s13,
    have s15 : f' i'  fin.max n f' := IH f' i',
    have s16 : f' i' = f (fin.cast_succ i') := eq.refl (f' i'),
    have s17 : f (fin.cast_succ i')  fin.max n f' := eq.subst s16 s15,
    have s18 : f i  fin.max n f' := eq.subst s14 s15,
    show f i  fin.max n.succ f, from le_trans s18 s9
  )
  (
    assume a1 : i.val = n.succ,
    have s19 : i = fin.last n.succ := fin.eq_of_veq a1,
    show f i  fin.max n.succ f, from eq.subst (eq.symm s19) s7
  )
}
end


def is_bounded_on (a b : ) (f :   ) : Prop :=  M : ,  x  set.Icc a b, abs (f x)  M

lemma singleton_bounded (a : ) (f :   ) : is_bounded_on a a f :=
let M := abs (f a) in
have s0 :  x  set.Icc a a, abs (f x)  M := (
  assume x : ,
  assume a0 : x  set.Icc a a,
  have s1 : a  x  x  a := a0,
  have s2 : a  x := and.left s1,
  have s3 : x  a := and.right s1,
  have s4 : x = a := le_antisymm s3 s2,
  have s5 : abs (f x) = abs (f x) := eq.refl (abs (f x)),
  have s6 : abs (f x) = abs (f a) := eq.subst s4 s5,
  have s7 : abs (f x) = M := s6,
  eq.le s7
),
exists.intro M s0


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


lemma singleton_partition {a b : } (P : partition a b) : P.n = 0  a = b :=
assume a0 : P.n = 0,
have s0 : fin.last P.n = 0 := fin.eq_of_veq a0,
calc a = P.x 0              : eq.symm P.x_zero
...    = P.x (fin.last P.n) : congr_arg P.x (eq.symm s0)
...    = b                  : P.x_last


lemma partition_mem {a b : } (P : partition a b) : 0 < P.n   x  set.Icc a b,  i : fin P.n, x  set.Icc (P.x i.cast_succ) (P.x i.succ) :=
assume a0 : 0 < P.n,
assume x : ,
assume a1 : x  set.Icc a b,
by_contradiction (
  assume a2 : ¬  i : fin P.n, x  set.Icc (P.x i.cast_succ) (P.x i.succ),
  have s0 :  i : fin P.n, ¬ x  set.Icc (P.x i.cast_succ) (P.x i.succ) := sorry,
  have s1 : a  x := and.left a1,
  have s2 : a < x  a = x := lt_or_eq_of_le s1,
  or.elim s2
  (
    assume a3 : a < x,
    have s3 :  i : fin (P.n + 1), P.x i < x := (
      assume i : fin (P.n + 1),
      fin.induction_on i
      (
        have s4 : P.x 0 = a := P.x_zero,
        show P.x 0 < x, from eq.subst (eq.symm s4) a3
      )
      (
        assume i' : fin P.n,
        assume IH : P.x i'.cast_succ < x,
        have s5 : P.x i'.cast_succ  x := le_of_lt IH,
        have s6 : ¬ x  set.Icc (P.x i'.cast_succ) (P.x i'.succ) := s0 i',
        have s7 : ¬ ((P.x i'.cast_succ)  x  x  (P.x i'.succ)) := s6,
        have s8 : (P.x i'.cast_succ)  x  ¬ x  (P.x i'.succ) := sorry,
        have s9 : ¬ x  (P.x i'.succ) := s8 s5,
        show P.x i'.succ < x, from sorry
      )
    ),
    have s10 : P.x (fin.last P.n) < x := s3 (fin.last P.n),
    have s11 : P.x (fin.last P.n) = b := P.x_last,
    have s12 : b < x := eq.subst s11 s10,
    have s13 : ¬ x  b := sorry,
    have s14 : x  b := and.right a1,
    show false, from s13 s14
  )
  (
    assume a4 : a = x,
    have s15 : P.x (fin.mk 0 a0).cast_succ = a := P.x_zero,
    have s16 : P.x (fin.mk 0 a0).cast_succ  x := eq.trans_le s15 s1,
    have s17 : P.x (fin.mk 0 a0).cast_succ = x := eq.trans s15 a4,
    have s18 : P.x (fin.mk 0 a0).cast_succ  P.x (fin.mk 0 a0).succ := P.mono (fin.mk 0 a0),
    have s19 : x  P.x (fin.mk 0 a0).succ := eq.subst s17 s18,
    have s20 : x  set.Icc (P.x (fin.mk 0 a0).cast_succ) (P.x (fin.mk 0 a0).succ) := and.intro s16 s19,
    have s21 : ¬ x  set.Icc (P.x (fin.mk 0 a0).cast_succ) (P.x (fin.mk 0 a0).succ) := s0 (fin.mk 0 a0),
    show false, from s21 s20
  )
)


example {a b : } (P : partition a b) (f :   ) :
( i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f)  is_bounded_on a b f :=
assume a0 :  i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
have s0 :  i : fin P.n,  m : ,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m := a0,
have s1 : P.n = 0  0 < P.n := sorry,
or.elim s1
(
  assume a1 : P.n = 0,
  have s2 : a = b := singleton_partition P a1,
  have s3 : is_bounded_on a a f := singleton_bounded a f,
  eq.subst s2 s3
)
(
  assume a2 : 0 < P.n,
  let m := fun i : fin P.n, Exists.some (s0 i) in
  have s4 :  i : fin P.n,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m i := (
    assume i : fin P.n,
    Exists.some_spec (s0 i)
  ),
  let M := fin.max (P.n - 1) m in
  have s5 :  i : fin P.n, m i  M := fin.all_le_max (P.n - 1) m,
  have s6 :  x  set.Icc a b, abs (f x)  M := (
    assume x : ,
    assume a3 : x  set.Icc a b,
    have s7 :  i : fin P.n, x  set.Icc (P.x i.cast_succ) (P.x i.succ) := partition_mem P a2 x a3,
    exists.elim s7 (
      assume i : fin P.n,
      assume a4 : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
      have s8 : abs (f x)  m i := s4 i x a4,
      have s9 : m i  M := s5 i,
      show abs (f x)  M, from le_trans s8 s9
    )
  ),
  exists.intro M s6
)

end hidden

view this post on Zulip Kevin Buzzard (Nov 29 2020 at 00:59):

lemma lt_lt_succ {m n : } : m < n  m < n + 1 := by omega
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := by omega
lemma lt_succ {n : } : n < n + 1 := by omega
lemma succ_pos {n : } : 0 < n + 1 := by omega
lemma lt_one {n : } : n < 1  n = 0 := by omega
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := by omega

view this post on Zulip Kevin Buzzard (Nov 29 2020 at 01:00):

lemma fin.eq_of_veq {n : } {i j : fin n} : i.val = j.val  i = j :=
begin
  cases i, cases j,
  simp,
end

view this post on Zulip Kevin Buzzard (Nov 29 2020 at 01:04):

@[elab_as_eliminator] def fin.induction {n : } {C : fin (n + 1)  Sort*}
(h0 : C 0) (hs :  i : fin n, C i.cast_succ  C i.succ) : Π (i : fin (n + 1)), C i :=
begin
  rintro i, hi⟩,
  induction i with j hj,
    exact h0,
  convert hs j, _ (hj _),
  exact nat.lt_of_succ_lt_succ hi,
end

view this post on Zulip Kevin Buzzard (Nov 29 2020 at 01:15):

Your problem with fin.max can be seen from the error:

type mismatch at application
  fin.max (P.n - 1) m
term
  m
has type
  fin P.n → ℝ : Type
but is expected to have type
  fin (P.n - 1 + 1) → ?m_1 : Type ?

For a general natural number x, x-1+1 isn't equal to x. This is why you should avoid natural number subtraction. I would recommend using a2 : 0 < P.n to actually get your hands on some natural r such that P.n=r+1 and then using r instead. Like this: Add something like

lemma temp_lemma {n : } (hn : 0 < n) :  m : , n = m.succ :=
begin
  cases n, cases hn,
  use n,
end

(I'm surprised this isn't in the library) and then

...
    assume i : fin P.n,
    Exists.some_spec (s0 i)
  ),
  begin
    cases temp_lemma a2 with r hr,
    rw hr at m,
    set M := fin.max r m with hM,
    sorry
  end

(I'm switching to tactic mode because this proof is massive, doing it in term mode seems crazy to me).

view this post on Zulip Patrick Thomas (Nov 29 2020 at 01:22):

Thank you!

view this post on Zulip Patrick Thomas (Nov 29 2020 at 01:50):

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

view this post on Zulip Patrick Thomas (Nov 29 2020 at 04:00):

I think I got it.

example {a b : } (P : partition a b) (f :   ) :
( i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f)  is_bounded_on a b f :=
assume a0 :  i : fin P.n, is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
have s0 :  i : fin P.n,  m : ,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m := a0,
have s1 : P.n = 0  0 < P.n := sorry,
or.elim s1
(
  assume a1 : P.n = 0,
  have s2 : a = b := singleton_partition P a1,
  have s3 : is_bounded_on a a f := singleton_bounded a f,
  eq.subst s2 s3
)
(
  assume a2 : 0 < P.n,
  let m := fun i : fin P.n, Exists.some (s0 i) in
  have s4 :  i : fin P.n,  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs (f x)  m i := (
    assume i : fin P.n,
    Exists.some_spec (s0 i)
  ),
  have s5 :  r : , P.n = r + 1 := exists_succ_eq a2,
  exists.elim s5
  (
    assume r : ,
    assume a3 : P.n = r + 1,
    let m' := fun i : fin (r + 1), m (@fin.mk P.n i.val (eq.subst (eq.symm a3) (i.prop))) in
    let M := fin.max r m' in
    have s6 :  i : fin P.n, m i  M := (
      assume i : fin P.n,
      have s7 : i.val < P.n := i.prop,
      have s8 : i.val < (r + 1) := eq.subst a3 s7,
      let i' := @fin.mk (r + 1) i.val s8 in
      have s9 : m' i' = m i := eq.refl (m' i'),
      have s10 : m' i'  M := fin.all_le_max r m' i',
      show m i  M, from eq.subst s9 s10
    ),
    have s11 :  x  set.Icc a b, abs (f x)  M := (
      assume x : ,
      assume a4 : x  set.Icc a b,
      have s12 :  i : fin P.n, x  set.Icc (P.x i.cast_succ) (P.x i.succ) := partition_mem P a2 x a4,
      exists.elim s12 (
        assume i : fin P.n,
        assume a4 : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
        have s13 : abs (f x)  m i := s4 i x a4,
        have s14 : m i  M := s6 i,
        show abs (f x)  M, from le_trans s13 s14
      )
    ),
    exists.intro M s11
  )
)

view this post on Zulip Patrick Thomas (Nov 29 2020 at 19:47):

What is the correct way to define the function t here?

example (a b : ) (f :   ) : ( R : , is_riemann_integral a b f R)  is_bounded_on a b f :=
assume a0 :  R : , is_riemann_integral a b f R,
by_contradiction (
  assume a1 : ¬ is_bounded_on a b f,
  exists.elim a0 (
    assume R : ,
    assume a2 : is_riemann_integral a b f R,
    let ε :  := 1 in
    have s0 : ε > 0 := sorry,
    have s1 :  δ : , δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := a2 ε s0,
    exists.elim s1 (
      assume δ : ,
      assume a3 : δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε,
      have s2 : δ > 0 := and.left a3,
      have s3 :  P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := and.right a3,
      have s4 :  P : partition a b, norm P < δ := norm_delta_exists δ s2,
      exists.elim s4 (
        assume P : partition a b,
        assume a4 : norm P < δ,
        have s5 :  Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := s3 P a4,
        have s6 :  i : fin P.n, ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f := sorry,
        exists.elim s6 (
          assume i : fin P.n,
          assume a5 : ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
          let Q := default (tagged_partition P) in
          let R := riemann_sum Q f in
          let S := f (Q.t i) * ((P.x i.succ) - (P.x i.cast_succ)) in
          let T := R - S in
          have s7 :  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε := sorry,
          exists.elim s7 (
            assume x : ,
            assume a6 :  (H : x  set.Icc (P.x i.cast_succ) (P.x i.succ)), abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε,
            exists.elim a6 (
              assume H : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
              assume a7 : abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε,
              let t : (fin P.n)   := fun j : (fin P.n), if j = i then x else Q.t j in
            )
          )
        )
      )
    )
  )
)

view this post on Zulip Kevin Buzzard (Nov 29 2020 at 21:55):

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

view this post on Zulip Patrick Thomas (Nov 29 2020 at 22:12):

I'm trying to fix the error in the definition of t. Actually, I think this is going to be a mess dealing with rearranging the sum, but I don't know of a way to make it any easier.

import algebra.order data.real.basic data.set.intervals

namespace hidden

structure fin (n : ) :=
(val : )
(prop : val < n)


lemma lt_lt_succ {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ {n : } : n < n + 1 := sorry
lemma succ_pos {n : } : 0 < n + 1 := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry
lemma exists_succ_eq {n : } (hn : 0 < n) :  m : , n = m + 1 := sorry
lemma zero_le {n : } : 0  n := sorry

def fin.cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.val (lt_lt_succ a.prop)

def fin.succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.val + 1) (lt_succ_lt_succ a.prop)

instance {n : } : has_zero (fin (n + 1)) := {zero := @fin.mk (n + 1) 0 succ_pos}

def fin.last (n : ) : fin (n + 1) :=
@fin.mk (n + 1) n lt_succ


def is_bounded_on (a b : ) (f :   ) : Prop :=  M : ,  x  set.Icc a b, abs (f x)  M


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


noncomputable def norm {a b : } (P : partition a b) :  := sorry

lemma norm_delta_exists {a b : } :  δ : , δ > 0   P : partition a b, norm P < δ := sorry


structure tagged_partition {a b : } (P : partition a b) :=
(t : fin P.n  )
(mem_block :  m : fin P.n, t m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : partition a b) : inhabited (tagged_partition P) := sorry


def riemann_sum {a b : } {P : partition a b} (Q : tagged_partition P) (f :   ) :  := sorry


def is_riemann_integral (a b : ) (f :   ) (R : ) : Prop :=
 ε : , ε > 0   δ : , δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε


example (a b : ) (f :   ) : ( R : , is_riemann_integral a b f R)  is_bounded_on a b f :=
assume a0 :  R : , is_riemann_integral a b f R,
by_contradiction (
  assume a1 : ¬ is_bounded_on a b f,
  exists.elim a0 (
    assume R : ,
    assume a2 : is_riemann_integral a b f R,
    let ε :  := 1 in
    have s0 : ε > 0 := sorry,
    have s1 :  δ : , δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := a2 ε s0,
    exists.elim s1 (
      assume δ : ,
      assume a3 : δ > 0   P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε,
      have s2 : δ > 0 := and.left a3,
      have s3 :  P : partition a b, norm P < δ   Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := and.right a3,
      have s4 :  P : partition a b, norm P < δ := norm_delta_exists δ s2,
      exists.elim s4 (
        assume P : partition a b,
        assume a4 : norm P < δ,
        have s5 :  Q : tagged_partition P, abs ((riemann_sum Q f) - R) < ε := s3 P a4,
        have s6 :  i : fin P.n, ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f := sorry,
        exists.elim s6 (
          assume i : fin P.n,
          assume a5 : ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f,
          let Q := default (tagged_partition P) in
          let R := riemann_sum Q f in
          let S := f (Q.t i) * ((P.x i.succ) - (P.x i.cast_succ)) in
          let T := R - S in
          have s7 :  x  set.Icc (P.x i.cast_succ) (P.x i.succ), abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε := sorry,
          exists.elim s7 (
            assume x : ,
            assume a6 :  (H : x  set.Icc (P.x i.cast_succ) (P.x i.succ)), abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε,
            exists.elim a6 (
              assume H : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
              assume a7 : abs ((T + (f x) * ((P.x i.succ) - (P.x i.cast_succ))) - R)  ε,
              let t : (fin P.n)   := fun j : (fin P.n), if j = i then x else Q.t j in
            )
          )
        )
      )
    )
  )
)

end hidden

view this post on Zulip Yakov Pechersky (Nov 29 2020 at 23:19):

Here's a close to your state, but in tactic format, which is easier for me to parse:

example (a b : ) (f :   ) : ( R : , is_riemann_integral a b f R)  is_bounded_on a b f :=
begin
  rintro sum, hsum⟩,
  by_contra H,
  set ε :  := 1 with ,
  have εpos : 0 < ε := by { rw , exact zero_lt_one },
  obtain δ, δpos,  :  δ : , 0 < δ 
     (P : partition a b), norm P < δ   (tP : tagged_partition P), abs ((riemann_sum tP f) - sum) < ε := hsum ε εpos,
  obtain P, hP :  (P : partition a b), norm P < δ := norm_delta_exists δ δpos,
  have htag :  (tP : tagged_partition P), abs ((riemann_sum tP f) - sum) < ε :=  P hP,
  obtain i, hi :  (i : fin P.n), ¬ is_bounded_on (P.x i.cast_succ) (P.x i.succ) f := sorry,
  set tP : tagged_partition P := default _ with htP,
  set tagged_sum :  := riemann_sum tP f with htsum,
  set rect :  := f (tP.t i) * ((P.x i.succ) - (P.x i.cast_succ)) with hrect,
  set overflow :  := tagged_sum - rect with hover,
  have htpmem : tP.t i  set.Icc (P.x i.cast_succ) (P.x i.succ) := tP.mem_block i,
  obtain x, hx, hx' :  x  set.Icc (P.x i.cast_succ) (P.x i.succ),
    ε  abs ((overflow + (f x) * ((P.x i.succ - P.x i.cast_succ))) - sum) := sorry,
  unfold is_bounded_on at H hi,
  push_neg at H hi,
  sorry
end

view this post on Zulip Patrick Thomas (Nov 30 2020 at 05:05):

Now we need to create a new tagged partition that uses the x from the last obtain right? That is what I am struggling with.

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 07:03):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 07:03):

Right now you have no formalized way of constructing tagged partitions at all, your inhabited instance (which really encodes data, and not proof) is sorried.

view this post on Zulip Patrick Thomas (Nov 30 2020 at 22:05):

Does this work?

instance {a b : } (P : partition a b) : inhabited (tagged_partition P) := {
  default := {
    t := fun i : fin P.n, P.x i.cast_succ,
    mem_block := (
      assume m : fin P.n,
      have s0 : P.x m.cast_succ  P.x m.cast_succ := le_refl (P.x m.cast_succ),
      have s1 : P.x m.cast_succ  P.x m.succ := P.mono m,
      and.intro s0 s1
    )
  }
}

I'm still not sure how to construct a new tagged partition using x. I think that has to be done? Is there a better approach to this proof? Different definitions or statements of the theorems?

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:06):

A possibly more minimal MWE:

import algebra.order data.real.basic data.set.intervals

namespace hidden

structure fin (n : ) :=
(val : )
(prop : val < n)


lemma lt_lt_succ {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ {n : } : n < n + 1 := sorry
lemma succ_pos {n : } : 0 < n + 1 := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry
lemma exists_succ_eq {n : } (hn : 0 < n) :  m : , n = m + 1 := sorry
lemma zero_le {n : } : 0  n := sorry

def fin.cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.val (lt_lt_succ a.prop)

def fin.succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.val + 1) (lt_succ_lt_succ a.prop)

instance {n : } : has_zero (fin (n + 1)) := {zero := @fin.mk (n + 1) 0 succ_pos}

def fin.last (n : ) : fin (n + 1) :=
@fin.mk (n + 1) n lt_succ


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


structure tagged_partition {a b : } (P : partition a b) :=
(t : fin P.n  )
(mem_block :  m : fin P.n, t m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : partition a b) : inhabited (tagged_partition P) := {
  default := {
    t := fun i : fin P.n, P.x i.cast_succ,
    mem_block := (
      assume m : fin P.n,
      have s0 : P.x m.cast_succ  P.x m.cast_succ := le_refl (P.x m.cast_succ),
      have s1 : P.x m.cast_succ  P.x m.succ := P.mono m,
      and.intro s0 s1
    )
  }
}

def tagged_partition_replace {a b : } {P : partition a b} (Q : tagged_partition P)
(i : fin P.n) (x : ) (h0 : x  set.Icc (P.x i.cast_succ) (P.x i.succ)) : tagged_partition P := {
  t := fun j : (fin P.n), if j = i then x else Q.t j,
  mem_block := sorry
}

end hidden

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:20):

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

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:22):

import algebra.order data.real.basic data.set.intervals

namespace hidden

structure fin (n : ) :=
(val : )
(prop : val < n)


lemma lt_lt_succ {m n : } : m < n  m < n + 1 := sorry
lemma lt_succ_lt_succ {m n : } : m < n  m + 1 < n + 1 := sorry
lemma lt_succ {n : } : n < n + 1 := sorry
lemma succ_pos {n : } : 0 < n + 1 := sorry
lemma lt_one {n : } : n < 1  n = 0 := sorry
lemma le_of_lt_succ {m n : } : m < n + 1  m  n := sorry
lemma exists_succ_eq {n : } (hn : 0 < n) :  m : , n = m + 1 := sorry
lemma zero_le {n : } : 0  n := sorry

def fin.cast_succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) a.val (lt_lt_succ a.prop)

def fin.succ {n : } (a : fin n) : fin (n + 1) :=
@fin.mk (n + 1) (a.val + 1) (lt_succ_lt_succ a.prop)

instance {n : } : has_zero (fin (n + 1)) := {zero := @fin.mk (n + 1) 0 succ_pos}

def fin.last (n : ) : fin (n + 1) :=
@fin.mk (n + 1) n lt_succ


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


structure tagged_partition {a b : } (P : partition a b) :=
(t : fin P.n  )
(mem_block :  m : fin P.n, t m  set.Icc (P.x m.cast_succ) (P.x m.succ))

instance {a b : } (P : partition a b) : inhabited (tagged_partition P) := {
  default := {
    t := fun i : fin P.n, P.x i.cast_succ,
    mem_block := (
      assume m : fin P.n,
      have s0 : P.x m.cast_succ  P.x m.cast_succ := le_refl (P.x m.cast_succ),
      have s1 : P.x m.cast_succ  P.x m.succ := P.mono m,
      and.intro s0 s1
    )
  }
}

def tagged_partition_replace {a b : } {P : partition a b} (Q : tagged_partition P)
(i : fin P.n) (x : ) (h0 : x  set.Icc (P.x i.cast_succ) (P.x i.succ)) : tagged_partition P := {
  t := fun j : (fin P.n), if j = i then x else Q.t j,
  mem_block := sorry
}

end hidden

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:30):

I'm trying to resolve this error:

failed to synthesize type class instance for
a b : ,
P : partition a b,
Q : tagged_partition P,
i : fin P.n,
x : ,
h0 : x  set.Icc (P.x i.cast_succ) (P.x i.succ),
j : fin P.n
 decidable (j = i)

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:31):

open_locale classical will make it go away

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:32):

And not defining your own fin.

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:33):

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

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:33):

What is different about my fin that causes this?

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:35):

You didn't prove a decidable equality instance for it. Which, you have two options for, either assume classical, or say that decidable equality of the values makes them equal.

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:38):

What actually does it mean for two instances of a structure to be equal in Lean? Is that a built in definition somewhere?

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:39):

Normally if you make a new structure then straight afterwards you prove an extensionality lemma, which is a practical way to prove that two instances are equal.

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:40):

But more recently people got sick of this and so now you can put @[derive ext] just before your structure definition, and then the exttactic will do the best it can to prove a sensible theorem of the form "if the data parts are equal, then the instances are equal"

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:40):

import algebra.order data.real.basic data.set.intervals

namespace hidden

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

structure tagged_partition {a b : } (P : partition a b) :=
(t : fin P.n  )
(mem_block :  m : fin P.n, t m  set.Icc (P.x m.cast_succ) (P.x m.succ))

def default_tp {a b : } (P : partition a b) : tagged_partition P :=
λ i, P.x i.cast_succ, λ m, le_rfl, P.mono m⟩⟩

instance {a b : } {P : partition a b} : inhabited (tagged_partition P) := default_tp P

def tagged_partition_replace {a b : } {P : partition a b} (Q : tagged_partition P)
(i : fin P.n) (x : ) (h0 : x  set.Icc (P.x i.cast_succ) (P.x i.succ)) : tagged_partition P :=
function.update Q.t i x, begin
  intros m,
  by_cases hm : (m = i),
  { simpa only [hm, function.update_apply, if_true, eq_self_iff_true] using h0 },
  { simpa only [hm, function.update_noteq, ne.def, not_false_iff] using Q.mem_block m},
end

end hidden

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:42):

Kevin Buzzard said:

But more recently people got sick of this and so now you can put @[derive ext] just before your structure definition, and then the exttactic will do the best it can to prove a sensible theorem of the form "if the data parts are equal, then the instances are equal"

What is the definition of 'the instances are equal' that has to be proven?

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:43):

the data fields are equal.

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:44):

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

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:44):

nothing

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:44):

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

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:45):

two terms of type fin n are equal if the natural parts are equal, I don't need to worry about whether the proofs are equal.

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:45):

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

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:45):

Yes.

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:46):

Um, sorry, this seems circular.

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:47):

There's an example

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:47):

It's the point in mathlib where it is proved that two complex numbers are equal if their real and imaginary parts are equal.

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:48):

But it needed to be proved.

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:48):

Here's how core Lean does it for fin:

instance (n : nat) : decidable_eq (fin n) :=
λ i j, decidable_of_decidable_of_iff
  (nat.decidable_eq i.val j.val) eq_of_veq, veq_of_eq

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:49):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:50):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:50):

Unless you have some issues with it?

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:50):

Yakov's code is a proof that there's an algorithm to determine equality of two terms of type fin n, and the proof is "we already know there's an algorithm to check to see if two natural numbers are equal, and all the rest is noise"

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:50):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:51):

I don't agree that it's "just noise", someone does have to write the eq_of_veq and veq_of_eq, which is what is needed for the custom fin

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 23:52):

If you don't use mathlib's fin then it's your job to make all the bells and whistles which you'll need to make your fin usable.

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:52):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:54):

In any case, this is all a detour from your partition question, to which I provided a definition that works above. In this sort of formalization, you have to choose how far "down the rabbit hole" you want to go. I think it's fine to sorry the lemmas about fin behavior, etc, just know that function.update expects a decidable_eq instance (which you can also sorry, or do open_locale_classical or whatever). Since you aren't really working on formalizing fin, but something about the summability of partitions, I think it's fine to sorry it.

view this post on Zulip Patrick Thomas (Nov 30 2020 at 23:55):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:55):

I used function.update because it comes with nice lemmas and API about how to deal with when things are equal or not. If you prefer the if j = i then x else ... that forces a classical context anyway.

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:56):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:56):

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

view this post on Zulip Yakov Pechersky (Nov 30 2020 at 23:57):

I hope that some of that explanation re fin was useful. If you're interested, we can discuss that more, or focus more on the partition problem

view this post on Zulip Yakov Pechersky