Dependent type coercion with AddSemigroup structure

Stream: general

[Gaëtan Serré]

Is it possible to automatically cast an object of a dependent type to an other type that are equals because of the associativity of the addition provided by the docs#AddSemigroup structure:

import Mathlib.Algebra.Group.Defs

variable {G : Type} [AddSemigroup G] {E : G → Type*}

example : E (a + (m + d)) = E (a + m + d) := by
  rw [add_assoc]

variable {a m d : G} (p : E (a + (m + d)))

def p' : E (a + m + d) := p -- fails

I guess docs#CoeDep could do the trick but I'm struggling with it

[Kenny Lau]

@Gaëtan Serré what is the context? (i.e. what is the real value of E)? because the convention in mathlib is that for concrete values of E, there should be a cast function to transfer between equal types; e.g. Fin.cast

[Gaëtan Serré]

@Kenny Lau I'm trying to formalize Markov kernels with different arrival and departure spaces. I do not have much more information on E except that each one is a docs#MeasurableSpace.

I could create a cast function MeasurableSpace.cast?

[Kenny Lau]

well, there's always ▸ which will work right now and will put you in what's called "dependent type hell" later down the line

[Kenny Lau]

Gaëtan Serré said:

I could create a cast function MeasurableSpace.cast?

I don't think this will work, the cast function should only be on E, and not on the resulting type

[Kevin Buzzard]

use docs#cast to get a map from E (a + (m + d)) to E (a + m + d)

[Kenny Lau]

It's a bit of a miracle how we haven't run into problems yet with GradedRing

[Eric Wieser]

I don't think DTT hell is as bad as its made out to be

[Rémy Degenne]

Is what you want to implement related to that kind of kernel: ProbabilityTheory.Kernel?

[Gaëtan Serré]

well, there's always ▸ which will work right now and will put you in what's called "dependent type hell" later down the line

I don't know about it, could you send a reference?

I don't think this will work, the cast function should only be on E, and not on the resulting type

Indeed, I wrote too fast!

[Kenny Lau]

Gaëtan Serré said:

well, there's always ▸ which will work right now and will put you in what's called "dependent type hell" later down the line

I don't know about it, could you send a reference?

TPIL4:

The triangle in the second presentation is a macro built on top of Eq.subst and Eq.symm, and you can enter it by typing \t.

[Gaëtan Serré]

@Kevin Buzzard Ok nice, should I just define a function that uses docs#cast and use it whenever I need it?

[Gaëtan Serré]

@Rémy Degenne Indeed, I use the definition of docs#Kernel and the kernel composition

[Kenny Lau]

Gaëtan Serré said:

Kevin Buzzard Ok nice, should I just define a function that uses docs#cast and use it whenever I need it?

again, it probably won't work if your E is a variable

[Kenny Lau]

he's saying that you should just use cast itself

[Gaëtan Serré]

@Kenny Lau Thanks a lot!

[Gaëtan Serré]

he's saying that you should just use cast itself

Something like

def p' : E (a + m + d) := cast (...) p

?

[Kevin Buzzard]

See how

def p' : E (a + m + d) := cast (by rw [add_assoc]) p

goes. I think the idea is that if you stick with cast then hopefully simp will solve many of your problems.

[Rémy Degenne]

This file is all about dealing with the type associativity issue for kernel composition: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.html

[Gaëtan Serré]

Thank you! I'll look into ▸ out of curiosity

[Gaëtan Serré]

See how

def p' : E (a + m + d) := cast (by rw [add_assoc]) p

goes. I think the idea is that if you stick with cast then hopefully simp will solve many of your problems.

It seems to work fine, I'll see ago it goes when doing more involved stuff

[Rémy Degenne]

I don't know what you want to do so I can't tell if the technique used by @Etienne Marion for Ionescu-Tulcea would be adapted for your use case, but you might want to have a look.

[Gaëtan Serré]

This file is all about dealing with the type associativity issue for kernel composition: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.html

Ok nice thank you very much! I'll look into that as well

I don't know what you want to do so I can't tell if the technique used by @Etienne Marion for Ionescu-Tulcea would be adapted for your use case, but you might want to have a look.

For a research project, I started to try to unify definitions of Markov processes and SDE from several books. I ended up with an pretty abstract definition of transition kernels that act on different measurable spaces and depend on a probability law. I was kind of lost at some point so I started to formalize this definition. Also, I'm in a continuous time setting. I think the technique used by @Etienne Marion can be very useful for the future of my work.