## Stream: maths

### Topic: bigop

#### Patrick Massot (Apr 21 2018 at 23:34):

I proved the first lemma of my new bigop lib!

#### Patrick Massot (Apr 21 2018 at 23:34):

I'm so happy :smile:

#### Patrick Massot (Apr 21 2018 at 23:35):

@Mario Carneiro Could you have a look to tell me if I started wrong, before I try to prove 50 more lemmas of this kind?

#### Patrick Massot (Apr 21 2018 at 23:35):

I think you can simply copy and paste the content of this file

#### Patrick Massot (Apr 21 2018 at 23:36):

It depends on nothing but mathlib

#### Patrick Massot (Apr 21 2018 at 23:37):

I'm especially curious about what you think about using is_associative and is_left_id here

#### Patrick Massot (Apr 21 2018 at 23:38):

Usually I love the old algebraic hierarchy but here it seems to me I wanted something directly attached to the operation

#### Kenny Lau (Apr 21 2018 at 23:38):

btw [∀ i, decidable \$ P i] is just [decidable_pred P]

#### Patrick Massot (Apr 21 2018 at 23:39):

Good to know, thanks!

#### Patrick Massot (Apr 21 2018 at 23:40):

I hope you noticed my effort not to use the usual non computable theory/local attribute [instance] classical.prop_decidable

#### Patrick Massot (Apr 21 2018 at 23:40):

Actually I needed it in order to compute 5! in the examples...

:D

did you?

#### Kenny Lau (Apr 21 2018 at 23:41):

I removed the open classical at the top and everything worked fine

#### Kenny Lau (Apr 21 2018 at 23:41):

and how does noncomputable things help with computation

#### Patrick Massot (Apr 21 2018 at 23:41):

Right, I forgot to erase that line

#### Patrick Massot (Apr 21 2018 at 23:42):

Which is the third line that is normally on top of all my Lean file before I start writing anything else

#### Kenny Lau (Apr 21 2018 at 23:43):

feature request: make it work with finset if your op is commutative

#### Patrick Massot (Apr 21 2018 at 23:45):

@Assia Mahboubi could you have a look at this https://github.com/PatrickMassot/lean-scratchpad/blob/01776fcb1eedc65df32e457427d06feacb321910/src/bigop.lean and tell me if this tiny starts means I can forget about the canonical instance propaganda, and Lean type class is doing just fine for the purpose of porting the bigop lib from Coq to Lean?

#### Patrick Massot (Apr 21 2018 at 23:46):

feature request: make it work with finset if your op is commutative

Of course that on the TODO list

#### Mario Carneiro (Apr 22 2018 at 00:07):

I think that apply_bigop can be removed and replaced by list.foldr of list.filter, although the notations seem okay (very stylish)

#### Mario Carneiro (Apr 22 2018 at 00:08):

I wonder if the new lean 4 parser will permit stuff like python list comprehensions

#### Mario Carneiro (Apr 22 2018 at 00:14):

comparison:

/- python
>>> [(x, y) for x in [1,2,3] for y in [3,1,4] if x != y]
[(1, 3), (1, 4), (2, 3), (2, 1), (2, 4), (3, 1), (3, 4)]
-/
#eval do x ← [1,2,3], y ← [3,1,4], guard (x ≠ y), return (x, y)
-- [(1, 3), (1, 4), (2, 3), (2, 1), (2, 4), (3, 1), (3, 4)]


#### Patrick Massot (Apr 22 2018 at 09:29):

I think that apply_bigop can be removed and replaced by list.foldr of list.filter, although the notations seem okay (very stylish)

Do you suggest I write def apply_bigop := foldr (λ i, op (F i)) nil (filter P r) or completely remove apply_bigop and copy-paste the RHS everywhere I had apply_bigop?

#### Patrick Massot (Apr 22 2018 at 09:29):

I wonder if the new lean 4 parser will permit stuff like python list comprehensions

If this happens it will become very hard to come up with something that Lean doesn't do great.

#### Patrick Massot (Apr 22 2018 at 14:50):

I created a separate repo, the new place to look at is https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean

#### Patrick Massot (Apr 22 2018 at 14:50):

Every help is welcome

#### Patrick Massot (Apr 23 2018 at 14:03):

Writing lemmas with minimal hypotheses is so fun. I find myself having lemmas assuming op is associative with an element nil which is a left identity (op nil a = a for all a) but not a right identity. Then I keep the same hypothesis for the next lemma I find myself surprised to see I actually need right identity this time.

#### Patrick Massot (Apr 23 2018 at 14:03):

I feel I'm Bourbaki

#### Kenny Lau (Apr 23 2018 at 14:03):

I thought someone doesn't care about which axioms we use

aha

#### Kenny Lau (Apr 23 2018 at 14:04):

I fail to see any difference

#### Kenny Lau (Apr 23 2018 at 14:05):

assuming AoC, omega <= a implies a^2 = a

#### Kevin Buzzard (Apr 23 2018 at 15:59):

hypotheses are what you need to make your lemmas work. Axioms are what you need to make everything work.

#### Patrick Massot (Apr 23 2018 at 16:01):

Oh, I have proof containing rw assoc op, rw ← assoc op,

#### Patrick Massot (Apr 23 2018 at 16:02):

and it's not simplifiable

#### Kevin Buzzard (Apr 23 2018 at 16:24):

That can happen if you have more than two multiplications

#### Kevin Buzzard (Apr 23 2018 at 16:24):

because it just finds the first match

sure

#### Patrick Massot (Apr 23 2018 at 16:24):

that's what is happening here

#### Kevin Buzzard (Apr 23 2018 at 16:24):

I suspect a * (b * c) = (d * e) * f would work, right?

#### Kevin Buzzard (Apr 23 2018 at 16:24):

But I agree it looks funny :-)

#### Patrick Massot (Apr 23 2018 at 16:24):

it still looks funny

heh

#### Patrick Massot (Apr 23 2018 at 16:29):

That one is also cute in a different direction: simp [H', H h (by simp)]

#### Patrick Massot (Apr 23 2018 at 16:29):

nested simp!

#### Patrick Massot (Apr 24 2018 at 00:22):

Two more lemmas tonight, culminating with https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean#L165. The needs some polishing but the statement is nice.

#### Andrew Ashworth (Apr 24 2018 at 00:27):

Will you eventually also formalize Kantorovitch’s theorem? The bigop paper mentions a whole bunch of results that seem to follow easily

#### Patrick Massot (Apr 24 2018 at 08:11):

I'm not interested in numerical analysis but I certainly intend to continue working on (multi-variable) calculus at some point. And I really hope we will have some linear algebra in the not too far distant future (it's a bit embarrassing to have schemes but no finite dimensional vector spaces...)

#### Kevin Buzzard (Apr 24 2018 at 09:00):

Did you see the short proof of Cayley-Hamilton Patrick? I can't remember where I saw it -- was it actually in the paper you're reading?

#### Patrick Massot (Apr 24 2018 at 09:36):

It's mentioned in that paper but not spelled out

#### Patrick Massot (Apr 24 2018 at 09:37):

But now I really need to work (understand an old paper by DBA Epstein which is not formalized, not even in automath)

#### Assia Mahboubi (May 28 2018 at 09:51):

HI @Patrick Massot! Cool, this looks really promising! However, I am afraid that the potential problems will not show up at this stage (if ever). The tricky part is the predictability and robustness of the algorithm inferring the instances. So for instance (foobar example) when writing \sum_(1 < p <= n | p prime) f ( \prod(x \ I_n) x), i.e. you have to infer and combine different instances of monoids, on different types.

#### Patrick Massot (May 28 2018 at 09:58):

Hi Assia! Of course I have no idea how predictable and robust is the algorithm here. I only tried to use my lemmas in https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/support.lean where I got completely stuck because of natural numbers arithmetic (with the crazy non-properties of substraction). So I gave up and wait for https://github.com/skbaek/qelim to become usable

#### Assia Mahboubi (May 28 2018 at 09:59):

Thinking about more concrete benchmarks. A first test case could be the definition of the determinant of a matrix, as the sum over the elements of the symetric group, etc. Another good one might be Cayley Hamilton and friends (juggling with matrices of polynomials and polynomials over matrices).

#### Patrick Massot (May 28 2018 at 10:03):

Ok, I will probably try to define determinants. Of course the problem is everything takes forever, and I also have real work to do...

#### Patrick Massot (May 28 2018 at 10:04):

And it's lunch time

Last updated: May 09 2021 at 10:11 UTC