## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• Aug 09 02:10

• Aug 07 14:26

fun not lambdas Merge branch 'unit-conjecture' … (compare)

• Aug 07 14:25

0art0 on unit-conjecture

Change from \lambda to fun … (compare)

• Jul 29 15:11

removing unused variables (compare)

• Jul 27 13:08

0art0 on unit-conjecture

Change quotes to italics Indentation fix (compare)

• Jul 27 11:20

0art0 on unit-conjecture

Push trivial proofs out of Tor… Merge branch 'unit-conjecture' … (compare)

• Jul 27 10:35

comment tweaked (compare)

• Jul 27 10:14

tweak Merge branch 'unit-conjecture' … (compare)

• Jul 27 09:30

0art0 on unit-conjecture

Change apply Q.rec -> cases … (compare)

• Jul 27 09:04

0art0 on unit-conjecture

Improved documentation for the … Merge documentation Add more documentation and 1 more (compare)

• Jul 27 08:10

corrected silly CI (compare)

• Jul 27 08:08

FreeModule sections (compare)

• Jul 27 05:29

• Jul 27 05:22

top docs for all files, docs fo… (compare)

• Jul 27 00:47

Modify CI Modify CI further Make elan path explicit and 3 more (compare)

• Jul 27 00:42

CI tweak (compare)

• Jul 27 00:36

CI tweak Merge branch 'unit-conjecture' … (compare)

• Jul 26 17:02

0art0 on main

Try building the mathlib folder… (compare)

• Jul 26 16:51

0art0 on main

Make elan path explicit (compare)

• Jul 26 16:49

0art0 on main

Modify CI further (compare)

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.
Anand
@0art0
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
Anand
@0art0
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.
Anand
@0art0
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.
I agree that transporting the group structure may make things easier. But I feel that working slowly with Arrays only will make sure there is no leak to slower structures.
One will need to add arrays etc from scratch of course.
Anand
@0art0
That makes sense.
Is it fine if I lake init in the ATP-Project repo (on a separate prompts branch), or is the Lean code for the prompts best kept separately?
Maybe best to have a subfolder lean-code or somesuch and doit within that.
On the main branch is fine.
Anand
@0art0
I have created a few files with descriptions, but I am having trouble pushing it to the repo since lake creates another .git within the subfolder.
For the time being, I will just put the descriptions up as GitHub issues.
Anand
@0art0
I have included a few potential topics for prompts. I can work on writing a few examples of each along with plaintext descriptions.
if that is an issue just move things to root.
The sub-folder was for neatness but not worth struggling over.
By the way, we are trying to add you to a "Team". Do you have a "Teams" account?
Anand
@0art0
I don't think I do, but I will create an account now.
Once you do let me know the id or associated email
Anand
@0art0
I have created one with my IISER email ID
I added you. Do you see the chat? Can you confirm there?
Anand
@0art0
I have added the folder with the Lean files. If it is too cluttered, I can try to revert the changes and do this on a separate branch.
It is fine.
Anand
@0art0
I think I finally managed to get the proof to work (in the case of lists). I will adapt it to the case of arrays and push the final code.
I used a helper lemma:
theorem List.get_index_eq : (l l' : List α) → (hl : l = l') → (i : ℕ) → (bnd : i < l.length) → l.get ⟨i, bnd⟩ = l'.get ⟨i, hl ▸ bnd⟩
| _, _, rfl, _, _ => rfl
Excellent.
I have been focussing on the prompts for the AI stuff.
Anand
@0art0
I was planning to add some prompts related to function types and product types in the Foundations folder some time today. I will try to work on it after pushing the AddTree code.
Anand
@0art0
I was thinking of coming to IISc either tomorrow (before 10 AM, to attend the meeting from there) or on Friday.
I think I will come on Friday since there is a good chance of finishing a large portion of the AddTreecode by then. I will come in the morning at around 10:30 AM and stay for a while.