Zulip Chat Archive

Stream: maths

Topic: algebra on subtypes


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

view this post on Zulip Johan Commelin (Jul 19 2018 at 11:04):

Looks interesting! I'm updating (-;

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

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

view this post on Zulip Patrick Massot (Jul 19 2018 at 11:18):

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

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

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

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 11:29):

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 11:29):

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 11:30):

I don't think refine_struct does anything like this

view this post on Zulip Johan Commelin (Jul 19 2018 at 11:31):

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

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

view this post on Zulip Johan Commelin (Jul 19 2018 at 11:34):

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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 11:38):

You should propose a unicode character for that thing

view this post on Zulip Patrick Massot (Jul 19 2018 at 11:39):

Let's ask google how to spell that in runes

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

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

view this post on Zulip Kenny Lau (Jul 19 2018 at 11:42):

Let's ask google how to spell that in runes

ᛗᛃᛟᛚᚾᛁᚱ

view this post on Zulip Mario Carneiro (Jul 19 2018 at 11:42):

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

view this post on Zulip Patrick Massot (Jul 19 2018 at 11:43):

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

view this post on Zulip Patrick Massot (Jul 19 2018 at 11:44):

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 11:44):

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

view this post on Zulip Sean Leather (Jul 19 2018 at 11:45):

Guillemets: how appropriate.

view this post on Zulip Mario Carneiro (Jul 19 2018 at 11:45):

problem solved:

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

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

view this post on Zulip Mario Carneiro (Jul 19 2018 at 11:47):

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

view this post on Zulip Johan Commelin (Jul 19 2018 at 11:47):

I like your use of "obviously"

view this post on Zulip 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: May 12 2021 at 08:14 UTC