Zulip Chat Archive
Stream: general
Topic: pi instances
Patrick Massot (Mar 12 2018 at 08:04):
@Mario Carneiro and @Johannes Hölzl could you have a look at the wonderful tactics that @Simon Hudon wrote for me in https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/indexed_product.lean and tell me whether this is suitable for mathlib? Remember the mathematical goals is to have instances of algebraic structures for Pi products of groups, rings, modules etc. and the Lean goal is to avoids writing tons of lines like https://github.com/PatrickMassot/lean-differential-topology/blob/f47348abf8515e23bd485683d8b351c7fd89c70f/src/indexed_product.lean#L92
Mario Carneiro (Mar 12 2018 at 08:07):
It seems a bit overkill, but it is clearly effective and I'd hate to throw a nice tactic like that away. Sure, PR away
Mario Carneiro (Mar 12 2018 at 08:09):
(Re: overkill, consider that the tactic + proofs have actually increased the overall size of the file, from 100 to 156 lines, and it looks like you already have covered most of the algebraic hierarchy there, so I think that's nearly its complete applicability.)
Patrick Massot (Mar 12 2018 at 08:11):
I think the psychological impact will be different when those instances will be spread over five files instead of one
Simon Hudon (Mar 12 2018 at 08:11):
Would it make more worthwhile if we used the same tactic to prove that vector n α conforms to a given structure if α does and that it is true for other applicative functors than vector n?
Patrick Massot (Mar 12 2018 at 08:12):
And also, I think this is really cool tactic. I can't wait for the making of tutorial that Simon promised to write soon.
Simon Hudon (Mar 12 2018 at 08:14):
:) I'll get right on that. I might procrastinate a bit with the mono tactic, I hope you'll forgive me
Mario Carneiro (Mar 12 2018 at 08:23):
I can see how this would generalize to all applicative functors, and I agree that would increase the applicability. (Again, I'm not actually rejecting the tactic version, it is always nice to have a new tactic if only as a future example and base for later expermentation. I just probably would have tried to find a more efficient way to write the proofs, say by using refine, rather than automating the entire process.)
Simon Hudon (Mar 12 2018 at 08:26):
Cool
Simon Hudon (Mar 12 2018 at 08:27):
I do take your point that it's making more code rather than less. It should withstand a lot of reengineering of the hierarchy though.
Simon Hudon (Mar 12 2018 at 08:31):
I'm not sure you could do much better than the one-line proofs that were there. For me, I think that was an interesting exercise. I'm especially interested to see how the code can be improved now
Mario Carneiro (Mar 12 2018 at 08:31):
since all the proofs follow the same script, you can abbreviate it with refine {..}; funext; simp or what have you
Simon Hudon (Mar 12 2018 at 08:32):
but for simp to work, don't you need all the laws of all the involved classes to be labelled simp?
Simon Hudon (Mar 12 2018 at 08:34):
I don't know how I'd implement it but if we could use the same tag system that the case system relies on, when we call refine { .. } we could tag each goal with the field that it responds to.
Simon Hudon (Mar 12 2018 at 08:34):
It would be more generally applicable and would probably shrink those scripts
Mario Carneiro (Mar 12 2018 at 08:35):
I would just add anything that isn't a simp lemma to the bracket list until it works
Mario Carneiro (Mar 12 2018 at 08:36):
Here obviously I'm thinking as a proof writer not a tactic writer
Mario Carneiro (Mar 12 2018 at 08:37):
It's a cool idea to use tags with refine {..}. You would have to ask @Sebastian Ullrich about that
Simon Hudon (Mar 12 2018 at 08:37):
That makes sense and that's robust enough
Simon Hudon (Mar 12 2018 at 08:38):
Glad you like it :) I'll talk to him about it
Kevin Buzzard (Mar 12 2018 at 10:05):
(Re: overkill, consider that the tactic + proofs have actually increased the overall size of the file, from 100 to 156 lines, and it looks like you already have covered most of the algebraic hierarchy there, so I think that's nearly its complete applicability.)
Kenny and I had to prove that a slightly complicated structure was a ring, and our current effort looks like this:
Kevin Buzzard (Mar 12 2018 at 10:05):
Kevin Buzzard (Mar 12 2018 at 10:06):
There's a lot of repeating λ _, structure_presheaf_value.ext _ _ _ _ $ λ _ _, which I felt might have been better dealt with by a general "maps to a ring with certain properties form a ring" tactic.
Simon Hudon (Mar 12 2018 at 10:10):
I can have a look and see if the same tactics could apply
Simon Hudon (Mar 12 2018 at 10:14):
I'll have a look tomorrow. Time for bed now
Yury G. Kudryashov (Feb 12 2020 at 15:25):
Hi, pi.monoid defines one := eq.mpr monoid._proof_2 (λ (_x : I), monoid.one (f _x)) where monoid._proof_2 is a rfl. I tried to understand which line in pi_instances creates this eq.mpr but failed to understand the code of derive_field. @Simon Hudon Could you please explain what happens there?
Last updated: Dec 20 2023 at 11:08 UTC