Zulip Chat Archive

@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

Patrick Massot (Apr 23 2018 at 14:04):

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

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

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

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

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

Kevin Buzzard (Apr 23 2018 at 16:25):

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:36):

I've already seen it though

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: Dec 20 2023 at 11:08 UTC