Porting iris-tutorial

Stream: iris-lean

[suhr]

In https://github.com/suhr/iris-tutorial I started to port iris-tutorial to Lean. Here's some problems met so far:

• You can't write ⊢ P -∗ (P -∗ Q) -∗ Q as simply P -∗ (P -∗ Q) -∗ Q in iris-lean
• The tutorial needs iapply but there's no such tactic in iris-lean yet

[Mario Carneiro]

suhr said:

• You can't write ⊢ P -∗ (P -∗ Q) -∗ Q as simply P -∗ (P -∗ Q) -∗ Q in iris-lean

I think this is not likely to get better. You could get iprop(P -∗ (P -∗ Q) -∗ Q) to work but that's not really better.

[suhr]

I tired of waiting for https://github.com/leanprover-community/iris-lean/pull/80 to be merged, so I filled the rest of Basics.lean using a fork of the repo.

There are three unproven lemmas remaining, which use ⊣⊢. In the tutorial, bi-entails is split with iSplit, but in iris-lean isplit does not work for ⊣⊢.

[suhr]

But constructor works fine for ⊣⊢

[suhr]

Now I'm trying to port pure.v, but theorem eq_elm {A} (P : A → iProp σ) (x y : A) : (⌜x = y⌝ : IProp σ) -∗ P x -∗ P y := sorry gives me the following error: error: IrisTutorial/Pure.lean:39:49: elaboration function for 'Iris.BI.BIBase.«term_-∗_»' has not been implemented.

[Markus de Medeiros]

I think you should put your main goal a ⊢. Enclosing it in iprop(...) might also work.

[suhr]

Huh, I forgot about the ⊢ thing again. Thanks!

[suhr]

Now both basics.v and pure.v are ported, and the rest of tutorial requires heaplang.