To do this, we may need to first claim that it is the fold of a particular tree. Then claim that the coordinates are the ones they are.
Within the Free Abelian group I to feel that the approach as above is fine. I am thinking of the bridge viewing an element as the image some homomorphism from this.
In principle, I think it should be possible to write meta-level code that takes a particular equality and generates all the Lean code required to prove it using free groups the universal property.
Here is a sketch of reducing (e.g. to identity) that I feel is efficient.
- Represent Free Abelian groups using
Vector. - Use a
BinTreewith leavesFin n × Boolto represent words in generators and their inverses. - Define
qmapping such a tree to the vector in the free abelian group. - Represent data for a map to the additive group
Aby aVector n A. - Define function
φmapping the data and a tree to an element ofA. - Define
ψmapping a vector to an element inA. - At meta level, associate to an element
ginAa treet(actuallynand the data are chosen after associating the element). gis definitionally equal toφ(t)which we use to prove equality.- Theorem: For a tree
tand fixed data,φ(t) = ψ(q(t))- this is a theorem at term level, so can be proved with types, using tactics etc. ; we need to prove such a theorem, as this is where the hypothesis that
Ais Abelian is used.
- this is a theorem at term level, so can be proved with types, using tactics etc. ; we need to prove such a theorem, as this is where the hypothesis that
- The reduced form
hofgish = ψ(q(t))and the above theorem showsg = h(due to reflexive equality). Both the reduction and the theorem have to be returned at meta level.
- The main part of the proof of the above theorem is exactly the statement that the standard map from the free abelian group to
Ais a homomorphism. - So the main part of the work is just constructing free abelian groups and showing that functions on the basis extend to homomorphisms.
I don't mind continuing with work at the moment and trying out a few of these ideas. I may take a break sometime next week.
I have pushed a file containing some general functions and theorems for defining the map from the free group to a given Abelian group. It is slightly different from the approach that you suggested, but it is along similar lines (I have tried to use the existing FreeAbelianGroup machinery).
On a related note, I found a tactic in mathlib3 called
assoc_rewrite, which rewrites using associativity implicitly. I haven't looked into this yet, but if this is easy to implement, we can alternatively use the idea you mentioned of fixing an order on the elements and swapping using simp.
I see it. I don't think my earlier
As you commented earlier, a similar method works for any free object. One may want to use variants of this: for example, for a commutative ring, assuming full simplification using distributivity, we can make a single list of symbols for the product terms and use the correspoding free groups. Then
simp idea is a good way. The present approach seems better. We just need some implementation of free abelian groups.As you commented earlier, a similar method works for any free object. One may want to use variants of this: for example, for a commutative ring, assuming full simplification using distributivity, we can make a single list of symbols for the product terms and use the correspoding free groups. Then
a * b - b * a should cancel.
But we can do this step by step.
It is a little harder to prove theorems about
Arrays, but there is an extensionality result, i.e., Array determined by its indices, if I am not mistaken. So any needed theorem should be derivable.
I will experiment a little (probably tomorrow) with
meta stuff starting with a term in an abelian group and trying to generate an array of symbols used and the tree corresponding to this relative to the symbols.
That makes sense. I think the main bottleneck will be in the reduction of the expression in the free Abelian group; I have modelled the free group on
n elements as Z ^ n (an iterated product), but I will try switching over to a different definition in terms of arrays after finishing the prototype that I am working on.
So there is no hurry and I am not blocked.
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.
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
basisof positive size in the typeαand a treet. - Assume that
αhas an additive commutative group structure (parallel for multiplicative). - The function
foldMapapplied totand thebasisImagesgives an elementxofα. - On the other hand,
foldMapapplied totand the standard basis of the free group with generators the size ofbasisImagesgives an elementaof the free group. - By freeness, there is a homomorphism taking the basis elements to
basisElements. This mapsato an elementy. - 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.
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.