Zulip Chat Archive

Stream: maths

Topic: should monotone be a class?

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)...

Johan Commelin (May 28 2018 at 09:13):

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

Johan Commelin (May 28 2018 at 09:13):

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

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?

Johan Commelin (May 28 2018 at 09:25):

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

Johan Commelin (May 28 2018 at 09:25):

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

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

Johan Commelin (May 28 2018 at 09:51):

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

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

Johan Commelin (May 28 2018 at 09:51):

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

Johan Commelin (May 28 2018 at 09:51):

I have no idea how to do that.

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.

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

Johan Commelin (May 28 2018 at 11:54):

How do I remove the final sorry in my file?

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"

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.

Patrick Massot (May 28 2018 at 11:58):

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

Johan Commelin (May 28 2018 at 11:58):

I linked them a few posts up

Johan Commelin (May 28 2018 at 11:59):

But generic pointers are also welcome

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 δ?

Johan Commelin (May 28 2018 at 12:06):

Why the underscores?

Johan Commelin (May 28 2018 at 12:06):

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

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₁]

Johan Commelin (May 28 2018 at 12:12):

Brilliant!

Johan Commelin (May 28 2018 at 12:12):

I need to understand finish

Johan Commelin (May 28 2018 at 12:12):

But this is awesome, thanks!

Patrick Massot (May 28 2018 at 12:12):

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

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

Mario Carneiro (May 28 2018 at 19:27):

You can enable proof printing with set_option pp.proofs true

Johan Commelin (May 28 2018 at 19:29):

Ok, thanks for the explanation!

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

Kevin Buzzard (May 28 2018 at 21:32):

All proofs are the same

Kevin Buzzard (May 28 2018 at 21:32):

and are instantly forgotten

Kevin Buzzard (May 28 2018 at 21:32):

so don't even get names

Kevin Buzzard (May 28 2018 at 21:32):

and this is kind of good but kind of annoying

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,_>

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>"