feat: Add ihave : Q tactic

[MackieLoeffel]

Builds on #119

Add the ihave : Q tactic that allows asserting new separation logic
hypothesis

Closes #116

[MackieLoeffel]

@lzy0505 This PR is ready to review when you have time.

[lzy0505]

Looks good! I pushed some docstrings and comments. Another feature that is nice to have is destructing the asserted hypothesis. Do you think you can also add this?

[MackieLoeffel]

Another feature that is nice to have is destructing the asserted hypothesis. Do you think you can also add this?

Indeed, this is a nice feature. Lean is a bit weird since it has have x : P which does not allow destructuring and obtain <a, b> : P which allows destructuring. Should we match this in Iris Lean (i.e. have ihave x : Q that does not allow destructuring and iobtain <a, b> : Q that allows destructuring) or should we also allow destructing patterns for ihave?
(I am not sure what the best option is since I think both having less tactics to remember is good, but also consistency with the standard lean tactics.)
Also pinging @markusdemedeiros if he has an opinion.

[MackieLoeffel]

I added support for destructuring to ihave and added an alias iobtain for ihave. This means that the user can use whatever tactic / spelling they like. Let me know if you have other suggestions, otherwise I will merge this PR.

[lzy0505]

Good to go.

[markusdemedeiros]

You actually can destruct with both have and obtain, the difference is whether or not the proposition remains in the context (so spatial destruction is like obtain but intuitionistic destruction is like have). I think for this reason, we should just remove the obtain spelling.

https://live.lean-lang.org/#codez=KYDwhgtgDgNsAEBvE8Ce8Bc9CohPA6zgL6bwAqATgK4IYC88ARqgFDzwAWYAbgoBfkIARgA08APqBL8kz0QreAHsGAFzABLAHbxeqYWMl00sgLSH4KcsAiq1AZ3jr4i9ggDGctYtCKR6ACZzgtmpyirLWcuTkqEA

Otherwise, I haven't looked through it closely, but I trust Zongyuan's review and am excited to play around with it!

[MackieLoeffel]

Interesting, I thought I tried it in other settings and there have did not support destructuring patterns. But I am happy to remove the iobtain spelling, this is just one less thing to worry about.

[lzy0505]

Are we merging this?

[markusdemedeiros]

I think we're all good to go I'll just do it