Heaplang

Stream: iris-lean

[Shreyas Srinivas]

I am porting heaplang right now. I noticed that in Rocq they use prefixes in constructors. We don't need them because our constructors are namespaced by the name of the type.

[Shreyas Srinivas]

I am currently making judicious use of this namespacing and removing these prefixes. Is that fine? CC : @Mario Carneiro

[Mario Carneiro]

yes

[Shreyas Srinivas]

And can I use Std.Hashmap for the state?

[Mario Carneiro]

probably, I don't know all of the context but if you need a hashmap that is one

[Mario Carneiro]

and it has a fair number of theorems proved about it when it comes to that

[Shreyas Srinivas]

There is also a bunch of "Countable" instances. Should I copy mathlib's countable class into this file?

[Mario Carneiro]

I think you won't need those, just leave them out and reconsider them in context

[Shreyas Srinivas]

How does one derive DecidableEq instances for mutual inductives? Nvm : Mutual def

[Shreyas Srinivas]

Could someone help me shorten the proofs of the DecidableEq instances for Expr and Val?

[Shreyas Srinivas]

https://github.com/leanprover-community/iris-lean/pull/93

[Shreyas Srinivas]

Basically each explicit case arm corresponds to two Vals/Exprs of the same constructor*. Then I by_cases on the equality of each corresponding argument and call decide_tactic. Surely there has to be a simpler way to do this.

*big_decide_tactic takes care of the rest.

[Shreyas Srinivas]

Help : Some of the definitions for bitwise operations are in mathlib. I can't seem to find the equivalent definitions in core: https://github.com/leanprover-community/mathlib4/blob/dd5e2a555841a8e2d5d0440b785c1f1b4efe5bab/Mathlib/Data/Int/Bitwise.lean#L231-L242

[Shreyas Srinivas]

Should I just create a subfolder "FromMathlib" and transfer as many definitions as necessary from there?

[Markus de Medeiros]

Go for it, though in my opinion HeapLang should be in a separate project than Iris anyhow.

[Markus de Medeiros]

Re. countability: A lot of those come from the HeapLang semantics using gmaps, which may or may not be the case anymore.

[Shreyas Srinivas]

Currently if heaplang lived separately, it would have to be upstream of iris or a third repository using iris and heaplang. Making it depend on mathlib will effectively introduce the dependency in all Iris projects

[Markus de Medeiros]

No. What I'm saying is that nothing in the core Iris library depends on HeapLang; not all Iris projects use HeapLang. Anyways, it's fine to develop in in the Iris repository for now, we can revisit this when there's more code written.

[Shreyas Srinivas]

That's fair. But my motivation for working on heap lang right now is that I keenly missed being able to show some heaplang proofs to Derek and group in my talk, because me and many others attended Derek's Iris semantics course

[Shreyas Srinivas]

It would have been really cool to show the lean counterpart of some of the course material. It would have been much simpler to have it in one repo