Functions into sums

Stream: Is there code for X?

[Paul Rowe]

I have a function f : α → β ⊕ γ and I'm looking to define a function left_restrict f whose domain is the terms a : α such that f a = inl b for some b : β. I have cobbled together something that (I think) does the right thing, but I get stuck trying to prove the most basic fact about it.

import data.sum.order
open sum
variables {α β γ: Type*}

def pre_left (f : α → β ⊕ γ) :=
{ a : α // ∃ b : β, f a = sum.inl b}

lemma lr_aux (f : α → β ⊕ γ) (a : (pre_left f)) :
(option.is_some (sum.get_left (f a.val))) :=
begin
  cases (a.property) with b p,
  rw p, simp,
end

def left_restrict (f : α → β ⊕ γ) :
(pre_left f) → β :=
λ a, option.get (lr_aux f a)

lemma lr_def (f : α → β ⊕ γ) {a : pre_left f} {b} (h : f a.val = inl b) :
left_restrict f a = b :=
begin
  have h1 := lr_aux f a,
  have g : left_restrict f a = option.get h1, by refl,
  rw g,
  rw h at h1,  --creates a second hypothesis with name h1 but keeps the first one
  simp only [get_left] at h1,  --alters the new copy of h1
  simp, -- seems to simplify option.get h1 using the first copy of h1?
end

A few questions: First, why doesn't the final simp finish the goal? option.get h1 should simplify to b. Also, if there is already code that does this, or if there's a better approach, I'm open to suggestions.

[Yaël Dillies]

∃ b : β, f a = sum.inl b could be rephrased nicely with docs#sum.is_left. Maybe that helps?

[Paul Rowe]

That sounds promising.

[Yaël Dillies]

Second, rewriting data indeed keeps the original thing around. Maybe you should instead use docs#eq.mp, docs#eq.mpr

[Paul Rowe]

That one didn't work. It complains

clear tactic failed, target type depends on 'h1'

[Yaël Dillies]

What exactly do you need left_restrict for? Maybe you can totally forget about it and instead throw junk values?

[Paul Rowe]

It's all related to the thing of mine you were reading the other day. I have managed to define a preorder on preorders (P \le P' iff there is an order homomorphism from P to P'). I'm trying to prove a result about how downward closures in this preorder distribute across the "distributive product" (second equality of Lemma 1 from that paper.

[Yaël Dillies]

Oh that shouldn't require such things

[Paul Rowe]

Basically, a key step of the proof should be to recognize that P ≤ S ⊕ T ↔ ∃ P1 P2, P = P1 ⊕ P2 ∧ P1 ≤ S ∧ P2 ≤ T. But the ≤ s on the right correspond to order homomorphisms that I have to build.

[Paul Rowe]

Tell me more!

[Yaël Dillies]

There's something however that I'm not getting. What did you define your preorder of preorders on?

[Yaël Dillies]

It's gonna be hard to prove stuff about, and in particular I suspect your result is wrong so long as you don't quotient by order isomorphism.

[Yaël Dillies]

Try filling in this sorry. It should be a good training for whatever awaits you.

import order.ideal

def equiv.sum_ideal_exp {α β : Type*} [preorder α] [preorder β] :
  order.ideal (α ⊕ β) ≃o order.ideal α × order.ideal β := sorry

[Paul Rowe]

So if P1 and P2 are preorders then P1 ≤ P2 if and only if there is a monotone function h : P1 \to P2

[Yaël Dillies]

Yes, but on what type did you put this preorder? What is ? in instance : preorder ? := your_preorder_of_preorders?

[Yaël Dillies]

If you're feeling like it, a second much harder level is

def equiv.sum_lex_ideal_distrib {α β : Type*} [partial_order α] [partial_order β] [order_top α]
  [order_bot β] :
  order.ideal (α ⊕ₗ β) ≃o (⊤ : order.ideal α) ⊕ₚ (⊥ : order.ideal β) :=

where the ⊕ₚ comes from branch#twop.

[Paul Rowe]

Oh, I see. Relating back to this thread, I ended up defining a type whose elements were evsys that were also preorders. The preorder is on that type.

[Yaël Dillies]

Hmm... That seems hard to manage.

[Paul Rowe]

Yikes! I'll give those exercises a go. I'm sure they will help me gain facility in manipulating what I need to.

[Paul Rowe]

Yaël Dillies said:

Hmm... That seems hard to manage.

Can confirm! :laughing: I'm not sure how to make it easier though.

[Yaël Dillies]

(please really only try the second one after having done the first, I suspect it's really hard because I have proved barely anything about ⊕ₚ yet!)

[Paul Rowe]

Hahaha. Honestly, my facility with git repos is such that it will already be a challenge to get that branch going without messing anything else up first! I'll definitely start with the first one.

[Yaël Dillies]

PS: Those should actually be order isomorphisms!

[Paul Rowe]

You mean it should use ≃o instead of ≃?

[Paul Rowe]

And it took me a while to process your comment about the result being false unless I quotient by order isomorphisms. Yes, I was sloppy in what I wrote above, but my current statement in Lean does have P ≃o P1 ⊕ P2 instead of P = P1 ⊕ P2.

[Yaël Dillies]

Still, I fear that's not the best way to state it.

[Yaël Dillies]

Whoops sorry @Paul Rowe I just noticed I gave you the wrong statement. You want down_set (which doesn't yet exist) instead of ideal.

[Paul Rowe]

Yes, I noticed that. I was also surprised that down_set didn't exist yet! After obsessively playing around with various approaches for a weekend, I decided I needed a break from it all. But translating your statement about ideal into one about down_set should be pretty straightforward since ideals are also downsets.

[Yaël Dillies]

Yeah! I also happen to need down_set to express Birkhoff's representation theorem. So if you aren't interested in defining them, I can do it.

[Paul Rowe]

If I had more time and focus, I might've wanted to take a crack at them, but you should go ahead and do it. It'll all be much better and quicker! :grinning_face_with_smiling_eyes:

[Yaël Dillies]

Heads up: downsets are now in mathlib! docs#lower_set

[Yaël Dillies]

cc @Paul Rowe