clone formalization

Stream: new members

[Miroslav Olšák]

Hello everybody, we tried a testing formalization of a simple proposition about clones in several ITP's for comparison. LEAN seems pretty nice so far. However, I believe that there should be a better approach to certain parts the proof (if we just knew LEAN better).
You can see the task description, together with my complains (/ TODO) under the link.
http://atrey.karlin.mff.cuni.cz/~mirecek/formal-math/clones.lean

[Johan Commelin]

@Miroslav Olšák I'm having trouble with certain symbols. I think unicode is being messed up or something. Could you post your code again with correct encoding? Maybe as a Github Gist, or something... (Don't know if you use github...)

[Bryan Gin-ge Chen]

In Firefox you can set the text encoding manually to unicode (View... Text Encoding...) and then the page displays properly. Apparently that feature no longer exists in Chrome.

[Miroslav Olšák]

All right, there it is on GitHub:
https://github.com/mirefek/clones-lean/blob/master/clones.lean
Any suggestions to the code? Is there a better way for case analysis through fin 3? Or a tactic that can do all the rewrite at the end of the code?

[Mario Carneiro]

I think you should use ternary functions rather than arrays

[Mario Carneiro]

or products, but curried will be nicer

[Miroslav Olšák]

I think you should use ternary functions rather than arrays

Definitely not. Sure, it suffices for this simple example but it does not correspond to the definition of clone at all.

[Miroslav Olšák]

or products, but curried will be nicer

Show me.

[Miroslav Olšák]

@Mario Carneiro What do you mean by curried products?

[Johan Commelin]

You can write a function X × Y → Z as X → Y → Z.

[Johan Commelin]

This is known as "currying"

[Kenny Lau]

aka product is left-adjoint of hom

[Kenny Lau]

(sorry)

[Miroslav Olšák]

I see.
But how to define the general composition for operations written like this?
I really think it is better to interpret them as functions A^n -> A, in the case of clones, as mathematicians usually do.

[Johan Commelin]

I tend to agree (I'm also a mathematician). But these CS people have really crazy operators that will do what you want.

[Johan Commelin]

And they can explain the benefits. (The disadvantage is that it no longer looks like what you are used to, although you can prove it is the same thing.)

[Abhimanyu Pallavi Sudhir]

I guess the advantage of the CS approach is that you can just give a single input and get a function.

[Johan Commelin]

I don't know what a clone is exactly, but what I saw on wiki looks like it is related operads. @Miroslav Olšák Is that right?

[Reid Barton]

nlab claims clones are analogous to operads but I think the relationship is less obvious than it looks at first glance

[Reid Barton]

The composition operation for operads takes a $k$-ary operation and $k$ operations of arity $n_1$, ..., $n_k$ and gives you an operation of arity $n_1 + \cdots + n_k$

[Reid Barton]

where the picture is that the $k$ operations each have access to disjoint subsets of the input variables

[Reid Barton]

here, each of the composed operations has access to all the input variables. I guess maybe it is the same thing as saying that you have the power to duplicate variables.

[Miroslav Olšák]

I understand the advantages of functional programming, but not in this case. If anybody feels that defining a clone by curried functions would be better, it would be nice to see such an approach.

Concerning to operads, I don't know them very well. From what I see on Wiki right now, operads are more general than abstract clones since they does not have projections (and also, operads don't glue variables). I think Reid Barton is right, just faster than me :-)

[Mario Carneiro]

The fact that you can partially apply a curried function is not actually that important in this case, it's just the way lean naturally deals with n-ary functions

[Mario Carneiro]

@Miroslav Olšák Okay, I see now. I thought that you only had to deal with ternary functions, but now I see that the statement involves membership in a clone, which involves arbitrary arity functions

[Mario Carneiro]

In this case, I will point you to nat.primrec', which is somewhat similar in needing to deal with collections of n-ary functions and n-ary composition. I use functions of type vector n A -> A, and n-ary composition is λ a, f (of_fn (λ i, g i a))

[Miroslav Olšák]

Interesting. Do you think that vectors behave in Lean better than arrays in general? (even though they are mathematically the same).