Equiv on sums with IsLeft Invariant

Stream: Is there code for X?

[Wrenna Robson]

Hi.

https://gist.github.com/linesthatinterlace/f1faa2a1c8379b1273397175fe40e056

I have a gist here which ends with an equiv thus: {e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ // ∀ x, (e x).isLeft = x.isLeft} ≃ (α₁ ≃ α₂) × (β₁ ≃ β₂).

Essentially I want to define the equivalence that Equiv.sumCongr is one component of, so that I can move between permutations on sum types which are invariant on IsLeft (that is, they send Sum.inl to Sum.inl and Sum.inr to Sum.inr), and permutations between each component.

Do we have this? It seems a natural enough idea.

I actually wanted it in the special case where α₁ = α₂ = β₁ = β₂ = FIn (2^m), as I really wanted an equivalence between "permutations on Fin (2^(m+1) that fix bit i" and "pairs of permutations on Fin(2^m)". It's just that Fin (2^(m+1) is naturally equivalent to Bool \times Fin (2^m) which is in turn equivalent to Fin (2^m) ⊕ Fin (2^m), and the above is broadly equivalent to that. But the above gist is totally extracted from my context.

I'd love thoughts.

[Antoine Chambert-Loir]

It doesn't look correct, it seems there are many more equivalences on the left hand side, for the second component may depend on the first one.

[Eric Wieser]

I think a more interesting result would be

{e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ // ∀ x, Sum.LiftRel ra rb (e x) x}
  ≃
{ea : α₁ ≃ α₂ // ∀ x, ra (ea x) x} × {eb : β₁ ≃ β₂ // ∀ x, rb (eb x) x}

for which your version is a special case with ra = rb = \top

[Eric Wieser]

(@Antoine Chambert-Loir, the linked code appear to be sorry-free, so I'm pretty sure it's true :smile:)

[Wrenna Robson]

Yes, it's possible I've mis-stated it above but I'm fairly sure I didn't. And my code is complete.

[Wrenna Robson]

I'm not sure sure I see why my result is that with \top

[Eric Wieser]

Because Sum.LiftRel \top \top x y is the same as x.is_right = y.is_right

[Wrenna Robson]

Aha, I see, yes.

[Wrenna Robson]

That is nicer, and less symmetry-breaking than specifying left or right.

[Eric Wieser]

Symmetry was indeed my motivation

[Wrenna Robson]

I originally started wanting to find the natural equivalence between {x : α \times β // x.fst = a} (for fixed a) and β.

[Wrenna Robson]

Which this is somewhat related to, though I went a different route. I'm not sure what the generalisation of that is.

[Wrenna Robson]

(It is related because of the Bool \times α ≃ α ⊕α equivalence I mention above.)

[Wrenna Robson]

Is "getLeft" the correct way to extract values of something that is provably left?

[Wrenna Robson]

I have updated the above gist with this result. @Eric Wieser, do you think this is PR-able? I am not sure about names and style. https://gist.github.com/linesthatinterlace/f1faa2a1c8379b1273397175fe40e056

[Eric Wieser]

Wrenna Robson said:

Is "getLeft" the correct way to extract values of something that is provably left?

Another option is match h : x with | .inl _ := sorry | .inr _ => (h _).elim end

[Wrenna Robson]

I like that less I think.

[Wrenna Robson]

Just on the basis that I don't like deliberate sorries.

[Wrenna Robson]

it would be nice if there was a fusion of getLeft and Option.get, where you directly get something, but have to provide a proof that it isLeft.

[Eric Wieser]

def equivOfLiftRelToEquivLeft (e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂) (ra : α₂ → α₁ → Prop) (rb : β₂ → β₁ → Prop)
    (he : ∀ ab, Sum.LiftRel ra rb (e ab) ab) : α₁ ≃ α₂ where
  toFun  a₁ := match e (Sum.inl a₁), he (Sum.inl a₁) with | Sum.inl a₂, h => a₂
  invFun a₂ :=
    have he' : ∀ ab, Sum.LiftRel ra rb ab (e.symm ab) := fun ab => by simpa using he (e.symm ab)
    match e.symm (Sum.inl a₂), he' (Sum.inl a₂) with | Sum.inl a₁, h => a₁

[Eric Wieser]

Though I can't work out how to prove things about those matches, split makes a mess

[Eric Wieser]

Wrenna Robson said:

I have updated the above gist with this result. Eric Wieser, do you think this is PR-able? I am not sure about names and style. https://gist.github.com/linesthatinterlace/f1faa2a1c8379b1273397175fe40e056

I think this could be PR-able; though right now the whitespace style is pretty jarring compared to some mathlib code; I recommend looking at how the whitespace is handled for other Equivs in mathlib

[Eric Wieser]

I also wonder whether ∀ x, r (f x) x has a name somewhere already

[Wrenna Robson]

It's a shame we don't have some tool to auto-fix the whitespace.

[Wrenna Robson]

It might. It also occurs that you could as well write r x (f x) and perhaps you'd want that version too.

[Wrenna Robson]

Though fundamentally I believe it's just a case of using Function.swap.

[Wrenna Robson]

On a core level this is the new thing I think. The equiv stuff is just the natural extension of this idea to the end state.

def foo (f : α₁ ⊕ β₁ →  α₂ ⊕ β₂) (ra : α₂ → α₁ → Prop) (rb : β₂ → β₁ → Prop)
(he : ∀ ab, Sum.LiftRel ra rb (f ab) ab) : α₁ → α₂ :=
fun a => (f (Sum.inl a)).getLeft.get (
  by  rcases h : f ((Sum.inl a)) with _ | _
      · simp_rw [ Sum.getLeft_inl, Option.isSome_some ]
      · specialize he (Sum.inl a)
        simp_rw [h, Sum.not_liftRel_inr_inl] at he)

[Eric Wieser]

That's fun a => match f (Sum.inl a₁), he (Sum.inl a₁) with | Sum.inl a₂, h => a₂

[Wrenna Robson]

Indeed, though as you say, hard to prove stuff about in that form...

[Wrenna Robson]

def equivBarFoo : {f : γ → α ⊕ β // ∀ c, (f c).isLeft} ≃ (γ → α) where
  toFun := fun ⟨f, hf⟩ => fun c => (f c).getLeft.get (by specialize hf c ; rw [Sum.isLeft_iff] at hf
                                                         rcases hf with ⟨a, ha⟩ ; rw [ha] ; rfl)
  invFun := fun g => ⟨Sum.inl ∘ g, by simp only [Function.comp_apply, Sum.isLeft_inl, implies_true]⟩
  left_inv := fun ⟨f, hf⟩ => by
                ext c ; specialize hf c ; rw [Sum.isLeft_iff] at hf ; rcases hf with ⟨a, ha⟩
                simp_rw [Function.comp_apply, ha, Sum.getLeft_inl, Option.get_some]
  right_inv := fun g => rfl

[Wrenna Robson]

Here's the equiv-analogue for it.

[Wrenna Robson]

Because we have Equiv.sumArrowEquivProdArrow, I think this is probably the more fundamental content of the above.

[Wrenna Robson]

I can't quite see how to relationify this - if you can, that would be nice.

[Wrenna Robson]

The analogy for products would be the equivalence between maps which do not depend on one component (f(a,b) = f(a,b') for all a b b') and maps from A (with a:A).

I think this is the duality between non-dependence and invariance?

[Wrenna Robson]

def equivProdLeftMap [Inhabited β] : {f : α × β → γ  // ∀ a b b', f (a, b) = f (a, b')} ≃ (α → γ) where
  toFun := fun ⟨f, _⟩ => fun a => f (a, default)
  invFun := fun g => ⟨fun ⟨a, _⟩ => g a, fun a b _ => rfl⟩
  left_inv := fun ⟨f, hf⟩ => by ext ⟨a, b⟩ ; dsimp ; rw [hf a b]
  right_inv := fun g => rfl

As in, this.

[Wrenna Robson]

What this means is that I'm a little unsure what results to include.

[Wrenna Robson]

Amusingly there is another such equivalence with a useless precondition.

def equivProdLeftMap' [IsEmpty α] : {f : α × β → γ  // ∀ a b b', f (a, b) = f (a, b')} ≃ (α → γ) where
  toFun := fun ⟨_, _⟩ => fun a => (IsEmpty.false a).elim
  invFun := fun _ => ⟨fun ⟨a, _⟩ => (IsEmpty.false a).elim, fun a _ _ => (IsEmpty.false a).elim⟩
  left_inv := fun ⟨_, _⟩ => by ext ⟨a, _⟩ ; exact (IsEmpty.false a).elim
  right_inv := fun _ => by ext a ; exact (IsEmpty.false a).elim

(Observed by thinking about multiplying by zero.)

[Wrenna Robson]

@Eric Wieser I did another iteration. In particular I think there is a case for having a Sum.getLeft and Sum.getRight which work more like Option.get, and rename the current functions as Sum.getLeft? and Sum.getRight?, analogous to List.get?

These can be defined using that match construction, and then with suitable simp lemmas, it makes the later proofs much easier - you fiddle with cases a lot less by defining things that way.

[Eric Wieser]

Adding question marks to the names seems like a good standalone PR

[Wrenna Robson]

Yes, I agree.

[Wrenna Robson]

What's the Mathlib4 PR process?

[Alex J. Best]

Basically the same as the mathlib 3 one was at this point

[Wrenna Robson]

Grand.

[Wrenna Robson]

Now, I must admit I can't remember how that worked. But I think it was written down somewhere...

[Alex J. Best]

https://leanprover-community.github.io/contribute/index.html is still approximately correct, except you change mathlib to mathlib4 in all the URLs. And you should request permission to push to the main repo rather than forking.

[Alex J. Best]

And you can ignore all mention of leanproject

[Anatole Dedecker]

Since I'm here, what's your GitHub username?

[Wrenna Robson]

linesthatinterlace

[Anatole Dedecker]

Well you alreadt have access since you contributed to the port!

[Anatole Dedecker]

Here is the usual workflow. It won't cover all the details that were cover on the "contribute" page, but it should at least get you started.

• if you haven't already, clone the mathlib repo using ssh
• on master, run git pull && lake exe cache get to get the current version and cache
• then do git checkout -b name_of_the_branch to create a new branch from there
• do your things in VSCode, commit and push (using the VSCode interface or the command line)
• then go to https://github.com/leanprover-community/mathlib4 and it should invite you to create a PR

[Wrenna Robson]

Thanks

[Wrenna Robson]

https://github.com/leanprover-community/mathlib4/pull/6663

[Anatole Dedecker]

Tip: you can link it as #6663

[Wrenna Robson]

Ah thanks.