Zulip Chat Archive

Stream: maths

Topic: algebra on subtypes

Patrick Massot (Jul 19 2018 at 09:57):

@Johan Commelin Simon has been working for us, and Mario promptly merged. You can update mathlib to at least c2f54ad03 and try to understand how to use the magic in https://gist.github.com/PatrickMassot/8afef3917a917300cf31c1396a895705

Johan Commelin (Jul 19 2018 at 11:04):

Looks interesting! I'm updating (-;

Johan Commelin (Jul 19 2018 at 11:11):

I really like where this is going! You give it the data (zero, addition, ...) and for the properties (assoc, comm, ...) you just tell Lean: look, follow your nose and you'll get there.

Patrick Massot (Jul 19 2018 at 11:18):

Indeed. This now really looks like what you would wrote on paper: explain why operations make sense and then write either nothing or "algebraic axioms follow from the parent structure axiom"

Patrick Massot (Jul 19 2018 at 11:18):

And this will be reused a lot. Each algebraic structure need subtype instances

Patrick Massot (Jul 19 2018 at 11:20):

Note that refine_struct is an ongoing long-term collaboration effort using all available strengths: I do the whining and Simon does the coding. It started with the pi_instance tactic back in February I think

Johan Commelin (Jul 19 2018 at 11:24):

Ok, so here are some explicit kudos to @Simon Hudon :thumbs_up: :tada: :octopus: :cake: :hammer_and_wrench: :muscle:

Johan Commelin (Jul 19 2018 at 11:27):

I do wonder, in how far is this overlapping with Scott's tactics? I don't fully understand what his obviously does, but it is also related to deriving obvious results from fields in structures and such, right?

Mario Carneiro (Jul 19 2018 at 11:29):

obviously is one of several "hammer" style tactics by scott

Mario Carneiro (Jul 19 2018 at 11:29):

i.e. "throw every automation we have at the problem until it buckles"

Mario Carneiro (Jul 19 2018 at 11:30):

I don't think refine_struct does anything like this

Johan Commelin (Jul 19 2018 at 11:31):

Agreed, but vice versa? Would most of these goals buckle under ~~Thor's~~ Scott's hammer?

Patrick Massot (Jul 19 2018 at 11:33):

No, refine_struct by itself carefully understand and name what Lean wants to be proved. Then specialized automation like https://github.com/leanprover/mathlib/blob/master/algebra/pi_instances.lean#L16 or https://gist.github.com/PatrickMassot/8afef3917a917300cf31c1396a895705#file-subtypes-lean-L9 take over.

Johan Commelin (Jul 19 2018 at 11:34):

Since Lean supports unicode, I think we really should have a tactic called Mjölnir.

Kevin Buzzard (Jul 19 2018 at 11:38):

You should propose a unicode character for that thing

Patrick Massot (Jul 19 2018 at 11:39):

Let's ask google how to spell that in runes

Patrick Massot (Jul 19 2018 at 11:39):

And then we can email Jasmin and give him one more incentive to bring us that hammer thing

Patrick Massot (Jul 19 2018 at 11:40):

Looks like this could be our winner: https://static1.fjcdn.com/comments/Spelled+the+right+way+_47df3c7a85289a0912599c30d252cf08.jpg

Kenny Lau (Jul 19 2018 at 11:42):

Let's ask google how to spell that in runes

ᛗᛃᛟᛚᚾᛁᚱ

Mario Carneiro (Jul 19 2018 at 11:42):

def ᛗᛃᛟᛚᚾᛁᚱ := by ᛗᛃᛟᛚᚾᛁᚱ

Patrick Massot (Jul 19 2018 at 11:43):

Too bad: I tried meta def ᛗᛃᛟᛚᚾᛁᚱ : tactic unit := sorry but Lean complains invalid declaration, identifier expected

Patrick Massot (Jul 19 2018 at 11:44):

It seems we'll need some help from @Sebastian Ullrich

Mario Carneiro (Jul 19 2018 at 11:44):

meta def «ᛗᛃᛟᛚᚾᛁᚱ» : tactic unit := sorry

Sean Leather (Jul 19 2018 at 11:45):

Guillemets: how appropriate.

Mario Carneiro (Jul 19 2018 at 11:45):

problem solved:

meta def «ᛗᛃᛟᛚᚾᛁᚱ» : tactic unit := sorry
notation `ᛗᛃᛟᛚᚾᛁᚱ` := «ᛗᛃᛟᛚᚾᛁᚱ»
example : true := by ᛗᛃᛟᛚᚾᛁᚱ

Patrick Massot (Jul 19 2018 at 11:46):

This works! We're almost set. It only remains to whine long enough for someone to unsorry this

Mario Carneiro (Jul 19 2018 at 11:47):

obviously meta def «ᛗᛃᛟᛚᚾᛁᚱ» : tactic unit := by ᛗᛃᛟᛚᚾᛁᚱ

Johan Commelin (Jul 19 2018 at 11:47):

I like your use of "obviously"

Patrick Massot (Jul 19 2018 at 11:48):

We shouldn't forget the PR to https://github.com/leanprover/vscode-lean/blob/master/translations.json

Last updated: Dec 20 2023 at 11:08 UTC