## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• Nov 14 15:51

removed unused variables (in co… (compare)

• Nov 14 14:45

no nodejs in docker (compare)

• Nov 14 14:41

trying codespaces (compare)

• Nov 10 19:19
Appelcider synchronize #16
• Nov 10 18:52
Appelcider synchronize #16
• Nov 09 14:14

Definitions of Quiver and Se… Define additional structures Define 2-complexes and 35 more (compare)

• Nov 09 14:14
• Nov 09 08:27
0art0 review_requested #20
• Nov 09 08:27
0art0 opened #20
• Nov 09 07:12

0art0 on lean-update

• Nov 09 07:12

0art0 on main

• Nov 09 07:12
0art0 closed #19
• Nov 09 06:59
• Nov 09 06:57
• Nov 09 06:18
0art0 commented #17
• Nov 09 06:16

0art0 on lean-update

• Nov 08 17:35
0art0 commented #17
• Nov 08 15:04
• Nov 08 15:02

• Nov 08 14:53
My next steps are independent anway as I realized. Plus there are a couple of other things I have to do.
So there is no hurry and I am not blocked.
Anand
@0art0
I have finished setting up the basic machinery for constructing homomorphisms from Z^n to an additive group A, given a vector of elements of A of length n
I have also proved that the standard basis of Z^n maps to this vector of elements under the homomorphism (this is the lemma that I was stuck on; factoring out a few lemmas and using rewrites sorted it out).
I will next try out a concrete example and show that it holds in all Abelian groups by computing in Z^n.
Meanwhile I have made an additive tree structure. It seemed easiest to make the tree with elements in a type, and then make indices and an array. Will add methods in a few minutes to fold index trees.
This has been added too. Now the main step remaining is a theorem that shows the equality of the composition of two maps is the same as a third map.
• Assume we are given an array basis of positive size in the type α and a tree t.
• Assume that α has an additive commutative group structure (parallel for multiplicative).
• The function foldMap applied to t and the basisImages gives an element x of α.
• On the other hand, foldMap applied to t and the standard basis of the free group with generators the size of basisImages gives an element a of the free group.
• By freeness, there is a homomorphism taking the basis elements to basisElements. This maps a to an element y.
• The theorem is that x = y.
Since you are more familiar with the free group stuff, I am not trying to state or prove this. But I am happy to discuss whenever it is helpful.
Anand
@0art0
I am going through the code now. If I understand correctly, the array in the output of the indexTree function is mapping numbers occurring in the leaves of the IndexAddTree to the corresponding elements of \alpha.
Yes, that is correct (at least should be if there are no bugs).
Anand
@0art0
Thanks. I think I understand the code and what is left to be proved.
My current code is in terms of Vectors. However, I think I can try to create an "isomorphism" between the Array a and Vector a _ types, so that I can avoid reproving that the basis maps to the chosen elements of the additive group A.
With the more complicated setup that the generated tree maps to a given group element may not be reflexively true. But simpwith specific theorems should work.
By the way, if arrays are used via other slower structures one may not get efficiency.
Anand
@0art0
Thanks, I will keep that in mind. I was planning to only switch between structures for the proof that the basis elements map to the chosen group elements, and work entirely with arrays for the computation part.
That sounds good.
Anand
@0art0
The proof of soundness of the map is almost done. The remaining parts are either theorems about List.toArray or Array.get, which I will work on by looking at the definitions of these functions.
To reduce the complexity of the code, I am thinking of removing Vectors and sticking to only Lists and Arrays. Once I do this, the remaining obstacles in the proof due to indexed inductive type will disappear.
I will do this in a separate branch since I will be adding a new simp lemma about AddCommGroup.Homomorphism that may break existing code.
Anand
@0art0
That is nice to see.
Anand
@0art0
I am almost done with the proof of the soundness of compositions, but I am stuck because a rewrite that was working in the Vector formulation is now producing an error motive is not type correct.
I think it has something to do with the propositional equality that I introduced into the proofs. I will dig into it further.
Anand
@0art0
The expressions are the same even after using set_option pp.all true, which is strange.
Anand
@0art0
I found a Zulip thread which recommends using get? instead of get. I will try that.
The get method may be using a coercion which comes in the way of proofs.
Anand
@0art0
Yes, and I think a part of the problem may be Fin too (the proofs have to be specified at type level).
When working with quotients I have sometimes had to specify the motive using @fn (motive := ...). That may work here too.
Anand
@0art0
Okay, I will try that.
Anand
@0art0
I now strongly suspect that the issue is with Fin. I will also try working with a modified get' definition that uses propositional equality:
def Array.get' {α : Type _} (a : Array α) {n : ℕ} (h : a.size = n) (i : ℕ) (hi : i < n) : α :=
Array.get a ⟨i, Eq.substr h hi⟩
I was looking at your code briefly. I agree that it is the usual Fin tangle. But I had a question: is it necessary to use List at all? What stops us from using Array right through?
I see that there will be difficulties earlier. I will think through this a bit.
I am looking at the code again, and I do feel:
• unit_pow_list should first of all be camelcase as it is a definition, but also the name is cryptic. I take it this gives an element of the unit power sum from a list.
• more seriously, this is where you are using lists and this cascades; the function here should just take an Array and use results such as Array.size_pop.
I will think a little more about how to work with arrays here.
Related to this, to work with arrays one can define pow_sum to append a copy of T (though this goes against the usual right associativity). Alternatively work with vectors.
I am currently in the middle of a couple of other things, but should get to trying to modify your code later (maybe tomorrow).
One of the things is to try to work on using prompting with large language models to autoformalize. I am making notes (to double as slides) in a private Github repository which I am sharing with you. Do let me know any comments or further ideas you have.
Anand
@0art0
One reason I did not use Arrays throughout was because it is harder to prove theorems about them (such as mapcomp).
But it looks like this is causing issues in the proofs in Fin here.
unit_pow_list takes in a list of elements of the target Abelian group and gives a function from pow_sum Unit n (the direct sum of Unit with itself n times - the basis of \Z^n) to the Abelian group where each element of pow_sum Unit n maps to the corresponding entry in the list.
I will clean up the code a bit more soon and add documentation (it is currently mainly experimental).
Anand
@0art0
I am going through the notes now. I will think a bit more about some possible prompts and let you know soon.
As I thought more about it, I feel switching to appending is a bad idea as it breaks too much. But I do think we should use only arrays, and working with push, pop and size_push, size_pop.
I don't see a theorem that reversing an array preserves size, but maybe we can avoid this by reversing arrays twice.
Anand
@0art0
Okay, I will try translating a few of the List theorems to Arrays. I also want to eventually replace types such as \Z^n (pow_times \Z n with integer arrays of length n, since the final algorithm will depend heavily on the speed in which we can simplify expressions in \Z^n.
True. As we are not in a hurry now, we can try to construct Vec as a subtype of Array with given length, and just show that this is a free abelian group.
It may be worth just doing parts from scratch so we need no glue code. Maybe Array as a free abelian group with Fin n as basis.
Of course Fin n is painful.
We could also use Unit^n as a basis as we have done in the case of \Z^n. The iterated direct sum will probably not affect the efficiency since all the computations happen with the elements of the free Abelian group, and the basis type is only used in proving that the basis elements of \Z^n map to the chosen elements of the target Abelian group under the induced homomorphism.
I also had a few ideas to simplify the work of proving that Vec (the subtype of Arrays of a fixed length) with integer entries has the structure of a free Abelian group under pointwise addition
Let G be a group and let H be a type equipped with a Mul operation. Furthermore, let \phi : H -> G be a bijection between H and G such that \phi (h * h') = \phi(h) * \phi(h'). Then there is a unique group structure on H that turns \phi into a group isomorphism.
Let c : Vec \Z n -> \Z ^ n be an identification of the two types by coordinates. Once we define addition pointwise on Vec \Z n and show that c (v + v') = c(v) + c(v'), we can directly get a group structure on Vec \Z n and furthermore show that it is a free Abelian group. This bypasses proofs of associativity and so on, which might be difficult with just the Array representation.
I have a few ideas for prompts. I will write them down in a file and later make a pull request to the autoformalisation.md` file.