Beginner issue: how to transport equality?

Stream: new members

[Franklin Pezzuti Dyer]

Hello! I'm a brand-new Lean user, coming in with some experience using Agda. I was wondering if there's a function in Lean/mathlib that works analogously to the transport function from Homotopy Type Theory, which, given a type family P and an equality p : x = y, allows you to produce an element of P y from an element of P x. If not, what kind of construction would you use to do "substitution" of two quantities that have been proven equal?

For more context, here's what I'm trying to prove. Following the vein of how a "closure operator" is defined in mathlib, I've written my own definition of an "interior operator":

structure interior_operator [preorder α] extends α →o α :=
(le_interior' : ∀ x, to_fun x ≤ x)
(idempotent' : ∀ x, to_fun (to_fun x) = to_fun x)

and I am trying to prove that for any interior operator i and any closure operator c, we have that i ∘ c ∘ i = i ∘ c ∘ i ∘ c ∘ i (i.e. these two functions take on the same values at all points). This is a generalization of an interesting theorem from topology. My plan is to prove this using a "sandwich" argument, i.e. by proving that i ∘ c ∘ i x <= i ∘ c ∘ i ∘ c ∘ i x and i ∘ c ∘ i x >= i ∘ c ∘ i ∘ c ∘ i x for all values of x. Right now I'm just working on the first inequality:

theorem T2 : ∀ (c : closure_operator α), ∀ (i : interior_operator α), ∀ x : α,
             (i.to_fun ∘ c.to_fun ∘ i.to_fun) x ≤ (i.to_fun ∘ c.to_fun ∘ i.to_fun ∘ c.to_fun ∘ i.to_fun) x

I am able to show that i ∘ c ∘ i ∘ i x <= i ∘ c ∘ i ∘ c ∘ i x as follows:

λ c, λ i, λ x,
i.to_order_hom.monotone (c.to_order_hom.monotone (i.to_order_hom.monotone (c.le_closure' (i.to_fun x))))

and now I would like to use the fact that i ∘ i x is always equal to i x to complete the proof. This is where I need the aforementioned transport-type argument. If I had a function transport that worked analogously to transport, I might do something like this:

λ c, λ i, λ x,
transport (λ y, (i.to_fun ∘ c.to_fun) y ≤ (i.to_fun ∘ c.to_fun ∘ i.to_fun ∘ c.to_fun ∘ i.to_fun) x)
          (i.idempotent' x)
          (i.to_order_hom.monotone (c.to_order_hom.monotone (i.to_order_hom.monotone (c.le_closure' (i.to_fun x)))))

Any ideas how to accomplish this?

Also, I know this code is probably hideous - I'm pretty much in the dark about any kind of shortcuts or best-practices that are usually used to make Lean code cleaner/less verbose since I kind of just jumped in the deep end with this proof. Any advice would be much appreciated. :-)

[Adam Topaz]

Can you please provide a #mwe illustrating your issue? It's a bit hard to piece together where you're running into issues with the code fragments you posted.

[Franklin Pezzuti Dyer]

Sure, sorry about that. Here's what I have right now:

import order.closure
import order.hom.basic

universe u

variables (α : Type*) {ι : Sort*} {κ : ι → Sort*}

structure interior_operator [preorder α] extends α →o α :=
(le_interior' : ∀ x, to_fun x ≤ x)
(idempotent' : ∀ x, to_fun (to_fun x) = to_fun x)

variable [preorder α]

theorem T2 : ∀ (c : closure_operator α), ∀ (i : interior_operator α), ∀ x : α,
             (i.to_fun ∘ c.to_fun ∘ i.to_fun) x ≤ (i.to_fun ∘ c.to_fun ∘ i.to_fun ∘ c.to_fun ∘ i.to_fun) x
           := λ c, λ i, λ x, sorry

[Franklin Pezzuti Dyer]

I've just gotten rid of some of the unnecessary stuff

[Matt Diamond]

@Franklin Pezzuti Dyer I assume this involves more than just the rewrite tactic?

[Yaël Dillies]

Also note that I'm unhappy with the state docs#closure_operator is in. You would have more success using docs#galois_insertion directly, and probably the lemma there already exists.

[Matt Diamond]

you might just be looking for docs#eq.subst

[Franklin Pezzuti Dyer]

ahh, yep, that is exactly what I want. It looks like the type signature of eq.subst is the same as transport pretty much! :grinning_face_with_smiling_eyes:

[Franklin Pezzuti Dyer]

hmm, I have never heard of a galois insertion, but looking at the docs, I get the impression that a galois insertion is something stronger than just an arbitrary closure operation + arbitrary interior operator? or does every pair of closure operator + interior operator give rise to a galois insertion?

[Adam Topaz]

But I don't see where you want to transport anything in your proof here...

[Yaël Dillies]

No, a closure operator is exactly the same as a Galois insertion to a subtype (of closed elements) and an interior operator is the same as a Galois coinsertion to a subtype (of open elements).

[Franklin Pezzuti Dyer]

once I get the inequality i (c (i (i x))) <= i (c (i (c (i x)))), I want to transport along the equality i (i x) = i x to yield the inequality i (c (i x)) <= i (c (i (c (i x))))

[Adam Topaz]

Note that i (i x) and i x are terms of $\alpha$. No transport necessary (in Lean)

[Yaël Dillies]

My plan is to now have closure_operator properly be a specialisation of galois_insertion to a subtype, rather than the half-baked mess I made of it a year ago.

[Franklin Pezzuti Dyer]

hmm. if no transport is needed, how would one deduce i (c (i x)) <= i (c (i (c (i x)))) from i (c (i (i x))) <= i (c (i (c (i x)))) otherwise?

[Matt Diamond]

@Adam Topaz it sounds like he wants to rewrite a Prop using an equality... wouldn't that be necessary in some cases?

[Adam Topaz]

In the original question, the context was where P is a type family, and it seemed to me that you wanted to identify the types P x and P y when x = y. This is what I usually think of as "transport". In this case, you just have terms of a type (the type is $\alpha$) and a proof that the two terms are equal. You can just rewrite with that equality.

[Matt Diamond]

@Franklin Pezzuti Dyer FYI there's a special notation for using eq.subst: ▸

[Adam Topaz]

That's why I said that you don't need to transport, because you don't need to use any identification of distinct types.

[Franklin Pezzuti Dyer]

that's just an infix version?

[Matt Diamond]

yep

[Matt Diamond]

and if you're in tactic mode, you can use the rewrite tactic (a.k.a. rw)

[Franklin Pezzuti Dyer]

oh I see what you mean. from my messing around with HoTT in Agda I know this by the name ap P

[Franklin Pezzuti Dyer]

sorry, referring back to Adam's comment, it took a sec for me to digest heh