Equivariant Functions

Stream: Is there code for X?

[Jorge Medina]

Hi, im new here (just downloaded LEAN last week), is there already a theorem or proof related to Equivariant functions?
this being f(g(x)) = g (f(x)). Maybe there's already a theorem about it but i haven't found it.

I want to see if i can check such a property given two functions they have such property.

[Filippo A. E. Nuccio]

Can you provide some #mwe with what you have in mind?

[Jorge Medina]

sure, something of the likes:

Sure!
something like this:

theorem Equivar (a : alfa) (h :alfa ->beta) (g : Type -> Type) : f(g(a)) =g (f (a)) :=
begin ...

--type of g, depends on whether its input is alfa o beta

so then if i define two functions, prove if they have such property
def blah : alfa -> beta := something
def bleh: type -> type := else

[Eric Wieser]

docs#function.commute?

[Eric Wieser]

Or possibly docs#function.semiconj, since it sounds like you're asking about two different gs

[Jorge Medina]

That looks just like it! Thank you!
one more question that occur to me would be, is it possible in Lean to show or prove if a particular set of functions have that property?
like:
example: fun1(fun2 x) = fun2(fun1 x) :=
like with a trivial example as:
def fun1 (x:R) := x
def fun2 (x:R):= x*0
is there tactics for that?

[Eric Wieser]

Can you write that as a #mwe with #backticks?

[Jorge Medina]

def foo (x:R):R := x
def boo (x:R) :R:= x * 0

theorem this_commutes : \all x:R , function.commute foo boo := foo boo x = boo foo x.

I think I just managed to prove it there but from my understanding of lean. To prove that two functions commute I need to be able to write f(b( x) = b (f (x)). And not write in reverse as:

def foo (x:R):R := x
def boo (x:R) :R:= x * 0

theorem this_commutes : \all x:R , foo boo x = boo foo x :=  function.commute foo boo

right? or are these two equivalent?

[Yaël Dillies]

Neither of those statements make sense. The first is saying that foo and boo commute for all x, but x isn't used anywhere! The second one is effectively the same as saying that ℕ is a natural.

[Yaël Dillies]

What you want is

theorem this_commutes : function.commute foo boo := λ x, sorry -- your proof here