Zulip Chat Archive

Stream: maths

Topic: should monotone be a class?


view this post on Zulip Johan Commelin (May 28 2018 at 09:12):

Should

def monotone (f : α  β) := a b⦄, a  b  f a  f b

be a class? I need compositions of these guys (and then applying a functor to them)...

view this post on Zulip Johan Commelin (May 28 2018 at 09:13):

I wouldn't mind if the type class inference system helped me a bit (-;

view this post on Zulip Johan Commelin (May 28 2018 at 09:13):

Ooh, this is line 37 of order/basic.lean

view this post on Zulip Andrew Ashworth (May 28 2018 at 09:21):

would type class inference even help? don't you just need a lemma that says the composition of two monotonically increasing functions is also monotonic?

view this post on Zulip Johan Commelin (May 28 2018 at 09:25):

That exists. But now I need to explicitly refer to it every time I use functoriality

view this post on Zulip Johan Commelin (May 28 2018 at 09:25):

I'dd rather just have that transparently dealt with by Lean

view this post on Zulip Andrew Ashworth (May 28 2018 at 09:32):

ahhh. I'm surprised you would reach for type class inference in this case, it's not my first choice. I would try parameters in sections, auto params, and figuring out how to write a mini tactic or helper lemma as well

view this post on Zulip Johan Commelin (May 28 2018 at 09:51):

Ok, I don't really understand what you mean.

view this post on Zulip Johan Commelin (May 28 2018 at 09:51):

I have proved that the simplicial complex is a complex, up to 1 sorry: https://github.com/jcommelin/mathlib/blob/simplicial/algebraic_topology/simplicial_set.lean#L15-L22

view this post on Zulip Johan Commelin (May 28 2018 at 09:51):

The only thing in that proof is pulling some identity through a functor

view this post on Zulip Johan Commelin (May 28 2018 at 09:51):

I have no idea how to do that.

view this post on Zulip Johan Commelin (May 28 2018 at 09:52):

See https://github.com/jcommelin/mathlib/blob/simplicial/algebraic_topology/simplex_category.lean#L80 for the corresponding identity in the source category.

view this post on Zulip Johan Commelin (May 28 2018 at 11:54):

class simplicial_set :=
(objs : Π n : , Type*)
(maps {m n : } {f : [m]  [n]} (hf : monotone f) : objs n  objs m)
(comp {l m n : } {f : [l]  [m]} {g : [m]  [n]} (hf : monotone f) (hg : monotone g) :
  (maps hf)  (maps hg) = (maps (monotone_comp hf hg)))

namespace simplicial_set
def δ {X : simplicial_set} {n : } (i : [n+1]) :=
maps (simplex_category.δ_monotone i)

lemma simplicial_identity₁ {X : simplicial_set} {n : } (i j : [n + 1]) (H : i  j) :
(@δ X n) i  δ j.succ = δ j  δ i.raise :=
begin
unfold δ,
rw comp,
rw comp,
sorry
end

view this post on Zulip Johan Commelin (May 28 2018 at 11:54):

How do I remove the final sorry in my file?

view this post on Zulip Johan Commelin (May 28 2018 at 11:56):

In simplex_category.lean, I have

lemma simplicial_identity₁ (i j : [n+1]) (H : i  j) : δ j.succ  δ i = δ i.raise  δ j := "long proof"

view this post on Zulip Johan Commelin (May 28 2018 at 11:56):

I just want to pull this through maps, but I have no clue at all how to do it.

view this post on Zulip Patrick Massot (May 28 2018 at 11:58):

I would need to get your files to try to help you

view this post on Zulip Johan Commelin (May 28 2018 at 11:58):

I linked them a few posts up

view this post on Zulip Johan Commelin (May 28 2018 at 11:59):

But generic pointers are also welcome

view this post on Zulip Johan Commelin (May 28 2018 at 12:05):

Also, why does my state look like

X : simplicial_set,
n : ,
i j : fin (n + 1 + 1),
H : i  j
 maps _  maps _ = maps _  maps _

after I unfold δ?

view this post on Zulip Johan Commelin (May 28 2018 at 12:06):

Why the underscores?

view this post on Zulip Johan Commelin (May 28 2018 at 12:06):

I expected something more useful, like maps (simplex_category.δ_monotone i) ∘ maps (simplex_category ... etc

view this post on Zulip Patrick Massot (May 28 2018 at 12:08):

lemma simplicial_identity₁ {X : simplicial_set} {n : } (i j : [n + 1]) (H : i  j) :
(@δ X n) i  δ j.succ = δ j  δ i.raise :=
by finish [δ, comp, simplex_category.simplicial_identity₁]

view this post on Zulip Johan Commelin (May 28 2018 at 12:12):

Brilliant!

view this post on Zulip Johan Commelin (May 28 2018 at 12:12):

I need to understand finish

view this post on Zulip Johan Commelin (May 28 2018 at 12:12):

But this is awesome, thanks!

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

No! Don't try to understand it, it's magic!

view this post on Zulip Mario Carneiro (May 28 2018 at 19:27):

Why the underscores?

The only explicit arg in maps is monotone f, which is a proof. Lean hides proof arguments by default, but this makes it hard to understand these goals unless the f is explicit too

view this post on Zulip Mario Carneiro (May 28 2018 at 19:27):

You can enable proof printing with set_option pp.proofs true

view this post on Zulip Johan Commelin (May 28 2018 at 19:29):

Ok, thanks for the explanation!

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:32):

Johan, those _s used to really confuse me. Everyone has told you all the right things but let me tell you the stupid version

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:32):

All proofs are the same

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:32):

and are instantly forgotten

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:32):

so don't even get names

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:32):

and this is kind of good but kind of annoying

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:32):

because if you have a subtype, so a value and then a proof, it might well just get displayed as <a,_>

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:33):

and this is annoying because sometimes you want to change the goal to something defeq with show, so you cut and paste the output from the pretty printer and write "show <the goal>"

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:33):

and it doesn't work

view this post on Zulip Mario Carneiro (May 28 2018 at 21:33):

it's not instantly forgotten

view this post on Zulip Mario Carneiro (May 28 2018 at 21:33):

it's there, it's a term

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:33):

because Lean can't reconstruct the _s

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:33):

yes so Lean is only pretending it forgot

view this post on Zulip Mario Carneiro (May 28 2018 at 21:33):

it's just a big and ugly term

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:34):

and if you set_option pp.proofs true

view this post on Zulip Mario Carneiro (May 28 2018 at 21:34):

lean can reconstruct the _

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:34):

then you can see them all and cut and paste them all again

view this post on Zulip Kevin Buzzard (May 28 2018 at 21:34):

and it turns out sometimes they're really ugly and long


Last updated: May 11 2021 at 17:39 UTC