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)

Siddhartha Gadgil
@siddhartha-gadgil
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.
Siddhartha Gadgil
@siddhartha-gadgil
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).
Siddhartha Gadgil
@siddhartha-gadgil
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⟩
Siddhartha Gadgil
@siddhartha-gadgil
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?
Siddhartha Gadgil
@siddhartha-gadgil
I see that there will be difficulties earlier. I will think through this a bit.
Siddhartha Gadgil
@siddhartha-gadgil
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.
Siddhartha Gadgil
@siddhartha-gadgil
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.
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.