diff --git a/Iris/PORTING.md b/Iris/PORTING.md deleted file mode 100644 index 6fc1cf89..00000000 --- a/Iris/PORTING.md +++ /dev/null @@ -1,293 +0,0 @@ -# Status of the Iris-Lean port - -This file describes the state of the Iris-Lean port relative to the Rocq implementation. -Each item in this list is organized the Rocq file containing it. -Once all tasks contained file are done, **and** once the file has been double checked for any missing lemmas, it can be marked complete. -PR's which update this list by splitting large tasks into smaller parts, or double-checking files for completeness are welcome! - -Some porting tasks will require other tasks as dependencies, the GitHub issues page lists the tasks that are accessible, and prioritised. - -## Algebra - -- [ ] `agree.v` - - [x] CMRA - - [x] Functors -- [ ] `auth.v` - - [x] CMRA - - [x] Updates - - [x] Functors -- [ ] `big_op.v` - - [x] Lists - - [x] Maps - - [x] Sets - - [ ] Multisets - - [ ] Homomorphisms -- [ ] `cmra.v` - - [x] Lemmas - - [ ] Total CMRA construction - - [x] CMRA Morphisms - - [x] Functors - - [ ] Discrete CMRA construction - - [ ] Resource algebra construction - - [x] Unit - - [x] Empty - - [x] Product - - [x] Option - - [x] Discrete - - [x] Isomorphisms -- [ ] `cmra_big_op.v` -- [ ] `coPset.v` - - [x] coPset definition - - [ ] CMRA -- [x] `cofe_solver.v` -- [x] `csum.v` - - [x] CMRA - - [x] Updates - - [x] Functors -- [ ] `dfrac.v` - - [x] CMRA - - [x] Updates -- [ ] `dyn_reservation_map.v` - - [ ] CMRA - - [ ] Updates -- [ ] `excl.v` - - [x] CMRA - - [x] Functors -- [ ] `frac.v` - - [x] CMRA -- [ ] `functions.v` (nb. contained in `CMRA.lean`) - - [x] CMRA - - [ ] Updates -- [ ] `gmap.v` (nb. generalized in `Heap.lean`) - - [x] CMRA - - [ ] Updates - - [x] Functors -- [ ] `gmultiset.v` - - [ ] CMRA - - [ ] Updates -- [ ] `gset.v` - - [x] CMRA - - [ ] Updates -- [ ] `list.v` - - Is this an instance of the `Heap` CMRA? - - [ ] CMRA - - [ ] Functors -- [x] `local_updates.v` -- [ ] `max_prefix_list.v` - - [ ] Lemmas - - [ ] Functors -- [x] `monoid.v` -- [ ] `mra.v` -- [x] `numbers.v` -- [ ] `ofe.v` - - [x] Definitions - - [ ] Contractivity tactic - - [x] Fixpoints - - [x] Mutual fixpoints - - [x] Unit - - [x] Emtpy - - [x] Product - - [x] Sum - - [x] Discrete - - [x] Leibniz - - [x] Option - - [x] Later - - [x] Discrete functions - - [x] Isomorphisms - - [x] Sigma -- [ ] `proofmode_classes.v` - - [ ] IsOp -- [ ] `reservation_map.v` - - [ ] CMRA - - [ ] Updates -- [ ] `stepindex.v` -- [ ] `stepindex_finite.v` -- [ ] `sts.v` - - [ ] CMRA - - [ ] Updates -- [ ] `ufrac.v` (nb. contained in `Frac.lean`) -- [ ] `updates.v` - - [x] Lemmas - - [x] Updates - - [x] Isomorphisms - - [x] Product - - [x] Option -- [ ] `vector.v` - - [ ] CMRA - - [ ] Functors -- [] `view.v` - - [x] CMRA - - [x] Updates - - [x] Functors -- [x] `lib/dfrac_agree.v` - - [x] Lemmas - - [x] Updates -- [x] `lib/excl_auth.v` - - [x] Lemmas - - [x] Updates - - [x] Functors -- [x] `lib/frac_auth.v` - - [x] Lemmas - - [x] Updates - - [x] Functors -- [] `lib/gmap_view.v` (nb. generalized in `HeapView.lean`) - - [x] CMRA - - [x] Updates - - [x] Functors -- [ ] `lib/gset_bij.v` -- [ ] `lib/mono_Z.v` (nb. generalize to `MonoNumbers.lean`) -- [ ] `lib/mono_list.v` - - [ ] Lemmas - - [ ] Functors -- [ ] `lib/mono_nat.v` (nb. generalize to `MonoNumbers.lean`) -- [ ] `lib/ufrac_auth.v` - - [ ] Lemmas - - [ ] Updates - - [ ] Functors - -## Base Logic -- [x] `base_logic.v` -- [x] `bi.v` (nb. contained in `Instances/UPred/Instance.lean`) - - [x] BI instance - - [x] BI Persistently instance - - [x] BI Later instance - - [x] SBI instance - - [x] BUPd instance - - [x] Additional instances -- [x] `bupd_alt.v` (nb. contained in `BI/Lib/BUpdPlain.lean`) -- [ ] `derived.v` - - [x] Modalities -- [ ] `proofmode.v` - - [ ] class instances -- [ ] `upred.v` (nb. contained in `Algebra/UPred.lean` and `Instances/UPred/Instance.lean`) - - Missing: new `later_own` - - [x] CMRA - - [x] Functors - - [x] Primitives and nonexpansivity - - Example: SIProp embedding - - [x] Later lemmas - - [x] Update lemmas -- [ ] `lib/boxes.v` -- [ ] `lib/cancelable_invariants.v` -- [ ] `lib/fancy_updates.v` - - [x] FUpd instance - - [x] Soundness - - [ ] ProofMode instances -- [ ] `lib/fancy_updates_from_vs.v` -- [ ] `lib/gen_heap.v` -- [ ] `lib/gen_inv_heap.v` -- [ ] `lib/ghost_map.v` -- [ ] `lib/ghost_var.v` -- [ ] `lib/gset_bij.v` -- [ ] `lib/invariants.v` - - [x] Lemmas - - [ ] ProofMode instances -- [ ] `lib/iprop.v` - - [x] Definition - - [ ] subG - - [x] Functor solution -- [ ] `lib/later_credits.v` - - [x] Lemmas - - [ ] ProofMode instances -- [ ] `lib/mono_Z.v` (nb. generalize to `MonoNumbers.lean`) -- [ ] `lib/mono_nat.v` (nb. generalize to `MonoNumbers.lean`) -- [ ] `lib/na_invariants.v` - - [x] Basic construction - - [ ] Proofmode classes -- [ ] `lib/own.v` - - Missing: `later_internal_eq_iRes_singleton` - - [x] Definition - - [x] Updates - - [ ] Big ops - - [ ] Proofmode instances - - [ ] Own/Forall lemmas -- [ ] `lib/proph_map.v` -- [ ] `lib/saved_prop.v` -- [x] `lib/token.v` -- [x] `lib/wsat.v` - -## BI - -- [ ] `algebra.v` - - [ ] Generic - - [ ] Map - - [ ] Excl - - [ ] List - - [x] Agree - - [ ] View - - [ ] Frag - - [x] Auth - - [x] Heap View -- `ascii.v` -- [x] `bi.v` -- [ ] `big_op.v` - - [x] Lists - - [x] Maps - - [x] Sets - - [ ] Multisets -- [ ] `cmra.v` -- [x] `derived_connectives.v` -- [ ] `derived_laws.v` -- [ ] `derived_laws_later.v` - - [x] Base lemmas - - [x] Löb induction definition - - [x] Löb classes - - [x] Except 0 lemmas - - [ ] Timeless lemmas - - [ ] Big Op lemmas -- [ ] `embedding.v` -- [x] `extensions.v` - - [x] BIPureForall -- [ ] `interface.v` - - [ ] Later instances -- [ ] `internal_eq.v` -- [ ] `monopred.v` - - [ ] COFE - - [ ] BI instance - - [ ] Extension instnaces -- [x] `notation.v` -- [ ] `plainly.v` - - [x] plainly lemmas - - [ ] big op lemmas - - [x] internal eq lemmas -- [ ] `sbi.v` -- [ ] `sbi_unfold.v` -- [ ] `telescopes.v` -- [ ] `updates.v` - - [x] Bupd laws - - [x] Fupd basic laws - - [ ] Fupd mask change laws - - [ ] Fupd step derived rules - - [ ] Fupd plainly general laws -- [x] `weakestpre.v` -- [ ] `lib/atomic.v` -- [ ] `lib/core.v` -- [ ] `lib/counterexamples.v` -- [x] `lib/fixpoint_banach.v` -- [x] `lib/fixpoint_mono.v` - - [x] Least fixpoints + induction - - [x] Greatest fixpoints + coinduction -- [ ] `lib/fractional.v` -- [ ] `lib/laterable.v` -- [ ] `lib/relations.v` - -## ProofMode - -See proofmode at https://leanprover-community.github.io/iris-lean/ - -## Examples - -- SI Logic - - [x] `si_logic/siprop.v` - - [x] `si_logic/bi.v` - - [x] BI instance - - [x] BI Persistently instance - - [x] BI Later instance - -- Program Logic - - Final decisions about what to port from this folder have not been made yet. - - [x] `language.v` - - [x] `ectx_language.v` - - [x] `ectxi_language.v` - - [x] `weakestpre.v` - - [x] `adequacy.v` diff --git a/PULL_REQUEST_TEMPLATE.md b/PULL_REQUEST_TEMPLATE.md index 9ce06d0f..6ae23494 100644 --- a/PULL_REQUEST_TEMPLATE.md +++ b/PULL_REQUEST_TEMPLATE.md @@ -5,7 +5,6 @@ Fixes # (issue number) ## Checklist * [ ] My code follows the mathlib [naming](https://leanprover-community.github.io/contribute/naming.html) and [code style](https://leanprover-community.github.io/contribute/style.html) conventions -* [ ] I have updated `PORTING.md` as appropriate * [ ] I have added my name to the `authors` section of any appropriate files ## Generative AI Guidelines