Who wants the glory of finishing iProp?

Stream: iris-lean

[Markus de Medeiros]

iProp seems like it is pretty close to working on the rfunctors branch, however there are a couple sorry's that mainly have to do with type casts (see eg. ElemG.Bundle.ne).

I will not have much time to commit to Iris-Lean for the next little while, so if you are interested in helping, these goals are a good self-contained challenge. Finishing iProp would be a big step in this project and bring us much much closer to parity with Iris-Rocq!

[suhr]

I'll take a look.

[suhr]

Tricky stuff.

[Markus de Medeiros]

Glad I'm not the only one. Thanks for trying :)

[Zongyuan Liu]

FYI, I asked an LLM to fix the remaining sorry’s in IProp/Instance.lean (for fun). It’s almost done, except for those in iOwn_alloc_strong_dep. The proofs aren’t elegant, but they might give some clues. I’ll share more once it finishes the last ones.

[Markus de Medeiros]

Cool!!! I'm very curious to see what it ended up doing.

[Markus de Medeiros]

And I'd be interested to hear more details about the LLM and prompts as well.

[suhr]

Curious. Did you give it the proof context context with pp.all enabled? The usual view seems to lack important information, but in the same time pp.all output is not very human readable.

[Zongyuan Liu]

The LLM is stuck at the last subgoal of iOwn_alloc_strong_dep, thinking it is unprovable. The subgoal is finding a key (a Nat) of a map that is fresh AND satisfies some predicate P, given that there are infinite keys that are fresh and satisfy P, respectively. I'm not sure how to prove it either. It seems stronger than what's proven for the Rocq counterpart?

[Zongyuan Liu]

suhr said:

Curious. Did you give it the proof context context with pp.all enabled? The usual view seems to lack important information, but in the same time pp.all output is not very human readable.

I connected it to Lean LSP, not entirely sure what the LSP gives it.

[Markus de Medeiros]

Zongyuan Liu said:

I'm not sure how to prove it either. It seems stronger than what's proven for the Rocq counterpart?

It is possible that the subgoal is unprovable, the top-level statement should be identical to the Rocq one in this case.

[Markus de Medeiros]

Do you think you could commit your progress somewhere? It sounds like you solved all the hard goals, I would be happy to help finish the last one off.

[Markus de Medeiros]

Ah, I found your branch :)

[Markus de Medeiros]

The last sorry is false (take P and Q to be the sets of even and odd natural numbers) but I'm very confident that iOwn_alloc_strong_dep is provable.

[Markus de Medeiros]

I'm curious how many of the comments are yours versus the LLM?

[Markus de Medeiros]

Aha! I did not know about eq_of_heq! I can see how that can deal with all the remaining type cases. Very cool, I have learned something from the machine :robot:

[Zongyuan Liu]

Markus de Medeiros said:

I'm curious how many of the comments are yours versus the LLM?

I didn't write anything in that file - all the comments and code were written by the LLM (I haven't really got a chance to check carefully if all the generated comments make sense). I only gave it some high-level guidance.

[Michael Sammler]

Do you have a link to the file? I would be curious to see what the LLM has produced.

[Markus de Medeiros]

The file is here

[Markus de Medeiros]

Zongyuan Liu said:

I didn't write anything in that file - all the comments and code were written by the LLM (I haven't really got a chance to check carefully if all the generated comments make sense). I only gave it some high-level guidance.

Fascinating.

[Markus de Medeiros]

Today I will refactor this PR here

[Zongyuan Liu]

Markus de Medeiros said:

Today I will refactor this PR here

I'm asking the LLM to refactor it right now (didn't see your message when I started). I'll push once it finishes. Maybe I can save your time :)

[Markus de Medeiros]

Haha

[Michael Sammler]

Out of curiosity, which LLM are you using for this?

[Zongyuan Liu]

Michael Sammler said:

Out of curiosity, which LLM are you using for this?

I'm using Claude Code in VS Code, and only using it in a very basic way. I connect it to Lean LSP with https://github.com/oOo0oOo/lean-lsp-mcp, and give it the awesome prompts of https://github.com/cameronfreer/lean4-skills/tree/main. That's it. I'm sure people can easily set up similar things and try it out.

[Zongyuan Liu]

@Markus de Medeiros It's done in https://github.com/lzy0505/iris-lean/commit/a4f7441c5581a0a1483f914f490b705b6d8a71c8. Eyeballed the changes, they look reasonable.

[Markus de Medeiros]

Cool, I have some different ideas that can eliminate more code but the refactoring of the proofs looks great :)

[Remy Seassau]

Zongyuan Liu said:

Michael Sammler said:

Out of curiosity, which LLM are you using for this?

I'm using Claude Code in VS Code, and only using it in a very basic way. I connect it to Lean LSP with https://github.com/oOo0oOo/lean-lsp-mcp, and give it the awesome prompts of https://github.com/cameronfreer/lean4-skills/tree/main. That's it. I'm sure people can easily set up similar things and try it out.

Just popping in to say that I've started using this setup and it works really well, thanks Zongyuan!

[Markus de Medeiros]

iProp is sorry-free! iris-lean#97 thanks to Zongyuan!

I ended up not proving own_alloc_strong_dep and getting claude to emit a self-contained proof of iOwn_alloc_dep. I was surprised at how well it worked! We will need to revisit this for the dependencies of own_alloc_strong and own_alloc_cofinite, but the only such dependent in our near future is mono_nat.

I'll also need to refactor the code some more before it can be merged, I already did quite a bit but the code in the PR right now is not acceptable.