Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Aug 09 02:10

    siddhartha-gadgil on v2.0-uc

    (compare)

  • Aug 07 14:26

    siddhartha-gadgil on unit-conjecture

    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

    siddhartha-gadgil on unit-conjecture

    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

    siddhartha-gadgil on unit-conjecture

    comment tweaked (compare)

  • Jul 27 10:14

    siddhartha-gadgil on unit-conjecture

    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

    siddhartha-gadgil on unit-conjecture

    corrected silly CI (compare)

  • Jul 27 08:08

    siddhartha-gadgil on unit-conjecture

    FreeModule sections (compare)

  • Jul 27 05:29

    siddhartha-gadgil on unit-conjecture

    headings in top docs (compare)

  • Jul 27 05:22

    siddhartha-gadgil on unit-conjecture

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

  • Jul 27 00:47

    siddhartha-gadgil on unit-conjecture

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

  • Jul 27 00:42

    siddhartha-gadgil on main

    CI tweak (compare)

  • Jul 27 00:36

    siddhartha-gadgil on unit-conjecture

    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
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.
Siddhartha Gadgil
@siddhartha-gadgil
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.
Siddhartha Gadgil
@siddhartha-gadgil
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.
Siddhartha Gadgil
@siddhartha-gadgil
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.
Siddhartha Gadgil
@siddhartha-gadgil
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?
Siddhartha Gadgil
@siddhartha-gadgil
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.
Siddhartha Gadgil
@siddhartha-gadgil
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.
Siddhartha Gadgil
@siddhartha-gadgil
Once you do let me know the id or associated email
Anand
@0art0
I have created one with my IISER email ID
Siddhartha Gadgil
@siddhartha-gadgil
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.
Siddhartha Gadgil
@siddhartha-gadgil
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
Siddhartha Gadgil
@siddhartha-gadgil
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.
Siddhartha Gadgil
@siddhartha-gadgil
I have autogenerated a lot of prompts, as you may have seen. You are welcome to add manual ones, but it is also fine to wait till we discuss so you can choose those with most bang for the buck.
Let me know when you come. We can meet on Friday if you come then, to discuss the simplification tactics and a few other things. Tomorrow I will join the meeting from home, but if you are around post lunch (say 1:30 or later) we can meet then.
Anand
@0art0
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.
Siddhartha Gadgil
@siddhartha-gadgil
That sounds good.
I will meet you then.
Anand
@0art0
I have pushed a sorry-free proof of the theorem about equality of folds of the two AddTrees.
Siddhartha Gadgil
@siddhartha-gadgil
Excellent. Will look at it.