iris-lean
iris-lean copied to clipboard
leanprover-community
Lean 4 port of Iris, a higher-order concurrent separation logic framework
The tactic implementations need to destruct expressions (`Expr`), which is currently done by hand, i.e. using methods like `isAppOf` and `getAppArgs` in `Iris/Std/Expr.lean`. Using expression quotations would presumably simplify this...
Currently, the bidirectional entailment `⊣⊢` is defined as equality in order to use Lean's `rw` tactic to rewrite with bidirectional entailments in proofs inside the framework (e.g. in proofs of...
Currently, the proof that the length of the hypothesis mask is equal to the length of the spatial context in the implementation of `isplit` ([Tactics.lean](https://github.com/larsk21/iris-lean/blob/master/src/Iris/Proofmode/Tactics.lean)) is required to be assigned...
This MR updates the code to lean v4.10.0. This includes changing Std to Batteries and adapting the proofs. This is the first time I am working with Lean, so I...
## Summary - Add `Store` and `Heap` instances for `TreeMap K V cmp` and `ExtTreeMap K V cmp` - Add `Store`, `Heap`, `RepFunStore`, and `IsoFunStore` instances for function types -...
Implementation for issue #46 Ported the [`fixpointAB`](https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.ofe.html#fixpointAB) and [`fixpointAB_ne`](https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.ofe.html#fixpointAB_ne) sections from the Rocq implementation.
Based on #107 Add a custom version of synthInstance for the proof mode that can create and instantiate mvars. It is implemented as a simple backtracking search, reusing the standard...
Based on #108 Add support for pure specialization patterns `%h`. This subsumes the dedicated forall specialization parts of proof mode terms. TODO: decide which syntax to use for proof mode...
[Heap.lean](https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/Std/Heap.lean) contains a general interface for heap and map types. Instantiate this for the Heap types in the Lean standard library (eg. [ExtTreeMap](https://leanprover-community.github.io/mathlib4_docs/Std/Data/ExtTreeMap/Lemmas.html)).
https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/BI/Plainly.lean is not fully done, which caused some issues in https://github.com/leanprover-community/iris-lean/pull/102 It will be nice to check if we ported the most relevant lemmas and instances of the derived connectives
Metadata
Owner
Metadata
Lean 4 port of Iris, a higher-order concurrent separation logic framework