Zulip Chat Archive

Stream: maths

Topic: bigop


view this post on Zulip Patrick Massot (Apr 21 2018 at 23:34):

I proved the first lemma of my new bigop lib!

view this post on Zulip Patrick Massot (Apr 21 2018 at 23:34):

https://github.com/PatrickMassot/lean-scratchpad/blob/01776fcb1eedc65df32e457427d06feacb321910/src/bigop.lean#L107

view this post on Zulip Patrick Massot (Apr 21 2018 at 23:34):

I'm so happy :smile:

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Apr 21 2018 at 23:35):

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

view this post on Zulip Patrick Massot (Apr 21 2018 at 23:36):

It depends on nothing but mathlib

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 23:38):

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

view this post on Zulip Patrick Massot (Apr 21 2018 at 23:39):

Good to know, thanks!

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 21 2018 at 23:40):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 23:40):

:D

view this post on Zulip Kenny Lau (Apr 21 2018 at 23:41):

did you?

view this post on Zulip Kenny Lau (Apr 21 2018 at 23:41):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 23:41):

and how does noncomputable things help with computation

view this post on Zulip Patrick Massot (Apr 21 2018 at 23:41):

Right, I forgot to erase that line

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 23:43):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 22 2018 at 00:08):

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

view this post on Zulip 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)]

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 22 2018 at 14:50):

Every help is welcome

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 23 2018 at 14:03):

I feel I'm Bourbaki

view this post on Zulip Kenny Lau (Apr 23 2018 at 14:03):

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

view this post on Zulip Patrick Massot (Apr 23 2018 at 14:04):

It's not about axioms, it's about hypotheses

view this post on Zulip Kenny Lau (Apr 23 2018 at 14:04):

aha

view this post on Zulip Kenny Lau (Apr 23 2018 at 14:04):

I fail to see any difference

view this post on Zulip Kenny Lau (Apr 23 2018 at 14:05):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:01):

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

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:02):

and it's not simplifiable

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:24):

That can happen if you have more than two multiplications

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:24):

because it just finds the first match

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:24):

sure

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:24):

that's what is happening here

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:24):

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

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:24):

But I agree it looks funny :-)

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:24):

it still looks funny

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:25):

heh

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:29):

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

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:29):

nested simp!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...)

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Apr 24 2018 at 09:36):

It's mentioned in that paper but not spelled out

view this post on Zulip Patrick Massot (Apr 24 2018 at 09:36):

I've already seen it though

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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...

view this post on Zulip Patrick Massot (May 28 2018 at 10:04):

And it's lunch time


Last updated: May 09 2021 at 10:11 UTC