Skip to content

PORTING.md

Latest commit

 

History

History
475 lines (463 loc) · 11 KB

PORTING.md

File metadata and controls

475 lines (463 loc) · 11 KB

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
    • CMRA
    • Functors
  • auth.v
    • CMRA
    • Updates
    • Functors
  • big_op.v
    • Lists
    • Maps
    • Sets
    • Multisets
    • Homomorphisms
  • cmra.v
    • Lemmas
    • Total CMRA construction
    • CMRA Morphisms
    • Functors
    • Discrete CMRA construction
    • Resource algebra construction
    • Unit
    • Empty
    • Product
    • Option
    • Discrete
    • Isomorphisms
  • cmra_big_op.v
  • coPset.v
    • coPset definition
    • CMRA
  • cofe_solver.v
  • csum.v
    • CMRA
    • Updates
    • Functors
  • dfrac.v
    • CMRA
    • Updates
  • dyn_reservation_map.v
    • CMRA
    • Updates
  • excl.v
    • CMRA
    • Functors
  • frac.v
    • CMRA
  • functions.v (nb. contained in CMRA.lean)
    • CMRA
    • Updates
  • gmap.v (nb. generalized in Heap.lean)
    • CMRA
    • Updates
    • Functors
  • gmultiset.v
    • CMRA
    • Updates
  • gset.v
    • CMRA
    • Updates
  • list.v
    • Is this an instance of the Heap CMRA?
    • CMRA
    • Functors
  • local_updates.v
  • max_prefix_list.v
    • Lemmas
    • Functors
  • monoid.v
  • mra.v
  • numbers.v
  • ofe.v
    • Definitions
    • Contractivity tactic
    • Fixpoints
    • Mutual fixpoints
    • Unit
    • Emtpy
    • Product
    • Sum
    • Discrete
    • Leibniz
    • Option
    • Later
    • Discrete functions
    • Isomorphisms
    • 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
    • Lemmas
    • Updates
    • Isomorphisms
    • Product
    • Option
  • vector.v
    • CMRA
    • Functors
  • [] view.v
    • CMRA
    • Updates
    • Functors
  • lib/dfrac_agree.v
    • Lemmas
    • Updates
  • lib/excl_auth.v
    • Lemmas
    • Updates
    • Functors
  • lib/frac_auth.v
    • Lemmas
    • Updates
    • Functors
  • [] lib/gmap_view.v (nb. generalized in HeapView.lean)
    • CMRA
    • Updates
    • 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

  • base_logic.v
  • bi.v (nb. contained in Instances/UPred/Instance.lean)
    • BI instance
    • BI Persistently instance
    • BI Later instance
    • SBI instance
    • BUPd instance
    • Additional instances
  • bupd_alt.v (nb. contained in BI/Lib/BUpdPlain.lean)
  • derived.v
    • Modalities
  • proofmode.v
    • class instances
  • upred.v (nb. contained in Algebra/UPred.lean and Instances/UPred/Instance.lean)
    • Missing: new later_own
    • CMRA
    • Functors
    • Primitives and nonexpansivity
    • Example: SIProp embedding
    • Later lemmas
    • Update lemmas
  • lib/boxes.v
  • lib/cancelable_invariants.v
  • lib/fancy_updates.v
    • FUpd instance
    • 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
  • lib/iprop.v
    • Definition
    • subG
    • Functor solution
  • lib/later_credits.v
  • lib/mono_Z.v (nb. generalize to MonoNumbers.lean)
  • lib/mono_nat.v (nb. generalize to MonoNumbers.lean)
  • lib/na_invariants.v
  • lib/own.v
    • Missing: later_internal_eq_iRes_singleton
    • Definition
    • Updates
    • Big ops
    • Proofmode instances
    • Own/Forall lemmas
  • lib/proph_map.v
  • lib/saved_prop.v
  • lib/token.v
  • lib/wsat.v

BI

  • algebra.v
  • ascii.v
  • bi.v
  • big_op.v
    • Lists
    • Maps
    • Sets
    • Multisets
  • cmra.v
  • derived_connectives.v
  • derived_laws.v
  • derived_laws_later.v
    • Base lemmas
    • Löb induction definition
    • Löb classes
    • Except 0 lemmas
    • Timeless lemmas
    • Big Op lemmas
  • embedding.v
  • extensions.v
    • BIPureForall
  • interface.v
    • Later instances
  • internal_eq.v
  • monopred.v
    • COFE
    • BI instance
    • Extension instnaces
  • notation.v
  • plainly.v
    • plainly lemmas
    • big op lemmas
    • internal eq lemmas
  • sbi.v
  • sbi_unfold.v
  • telescopes.v
  • updates.v
    • Bupd laws
    • Fupd basic laws
    • Fupd mask change laws
    • Fupd step derived rules
    • Fupd plainly general laws
  • weakestpre.v
  • lib/atomic.v
  • lib/core.v
  • lib/counterexamples.v
  • lib/fixpoint_banach.v
  • lib/fixpoint_mono.v
    • Least fixpoints + induction
    • Greatest fixpoints + coinduction
  • lib/fractional.v
  • lib/laterable.v
  • lib/relations.v

ProofMode

  • [-] base.v (helper functions that are not necessary / different in Lean)
  • class_instances.v (Instances.lean)
    • instances for basic connectives
    • instances for telescopes
    • instances for big ops
    • MaybeCombineSepAs instances
    • CombineSepGives instances
    • FromModal instances
    • ElimModal instances
    • AddModal instances
    • ElimInv instances
  • class_instances_cmra.v
  • class_instances_embedding.v
  • class_instances_frame.v
  • class_instances_internal_eq.v
  • class_instances_later.v (InstancesLater.lean)
    • basic instances
    • FromModal
    • ElimModal
    • AddModal
    • IntoLater
  • class_instances_make.v
    • QuickAffine
    • QuickAbsorbing
    • MakeEmbed
    • MakeSep
    • MakeAnd
    • MakeOr
    • MakeAffinely
    • MakeIntuitionistically
    • MakeAbsorbingly
    • MakePersistenly
    • MakeLaterN
    • MakeExcept0
  • class_instances_plainly.v (InstancesPlainly.lean)
    • basic instances
    • FromModal
    • IntoExcept0
    • IntoLaterN
  • class_instances_updates.v (InstancesUpdates.lean)
    • Basic instances for bupd
    • Basic instances for fupd
    • FromModal bupd
    • FromModal fupd
    • ElimModal bupd
    • ElimModal fupd
    • AddModal bupd
    • AddModal fupd
    • ElimAcc bupd
    • ElimAcc fupd
  • classes.v (Classes.lean)
    • FromAssumption
    • IntoPure
    • FromPure
    • IntoInternalEq
    • IntoPersistent
    • FromModal
    • FromAffinely
    • IntoAbsorbingly
    • IntoWand
    • FromWand
    • FromImpl
    • FromSep
    • FromAnd
    • IntoAnd
    • IntoSep
    • FromOr
    • IntoOr
    • FromExist
    • IntoExist
    • IntoForall
    • FromForall
    • IsExcept0
    • CombineSepAs
    • MaybeCombineSepAs
    • CombineSepGives
    • ElimModal
    • AddModal
    • Frame
    • IntoExcept0
    • MaybeIntoLaterN / IntoLaterN
    • IntoEmbed
    • AsEmpValid
    • AsEmpValid0
    • IntoInv
    • ElimAcc
    • IntoAcc
    • ElimInv
  • classes_make.v
    • QuickAffine
    • QuickAbsorbing
    • MakeEmbed
    • MakeSep
    • MakeAnd
    • MakeOr
    • MakeAffinely
    • MakeIntuitionistically
    • MakeAbsorbingly
    • MakePersistenly
    • MakeLaterN
    • MakeExcept0
  • coq_tactics.v / ltac_tactics.v (split into the files in Tactics/)
    • iSolveSideCondition
    • iStartProof
      • basic
      • with bi specified
    • iStopProof
    • iRename
    • iClear
      • basic
      • selection patterns
    • iEval
    • iSimpl
    • iUnfold
    • iExact
    • iAssumption
    • [-] iAssumptionCoq (iassumption_lean removed in https://github.com/leanprover-community/iris-lean/commit/b02fb8306b2c66aaa336b8ee2bc5eca0cdc5c899#diff-3289e4079a39b1d9a75ba9ee8532ef1c0a855d66a8e54fc5895585d0a32d12ee can be added back if necessary)
    • iExFalso
    • iPure
      • basic
      • pure destructuring patterns (also for other tactics using ipure)
    • iEmpIntro
    • iPureIntro
    • iFrame
    • iRevert
      • basic
      • intoIH revert
      • selection patterns
    • iPoseProof (Lean: ihave _ := _)
    • iSpecialize
      • basic functionality
      • duplicate context for persistent conclusion (includes other tactics using specialization)
      • all specialization patterns (see below)
    • iApply
    • iLeft
    • iRight
    • iSplit(L/R)
    • iExists
    • iModIntro
    • iNext (with later credits)
    • iMod
    • iDestruct (Lean: icases)
      • basic
      • all destruct patterns (see below)
    • iCombine
    • iIntros
      • basic
      • all intro patterns (see below)
    • iInduction
    • iLöb
    • iAssert (Lean: ihave _ : _)
    • iRewrite
    • iInv
    • iAccu
    • rules for trivial
  • environments.v (corresponds to Hyps / Entails')
  • [-] ident_name.v (not needed)
  • intro_patterns.v (split into Patterns/CasesPattern.lean / Patterns/IntroPattern.lean)
    • IIdent
    • IFresh
    • IDrop
    • IFrame
    • IList
    • IPure
    • IIntuitionistic
    • ISpatial
    • IModalElim
    • IRewrite
    • IPureIntro
    • IModalIntro
    • ISimpl
    • IDone
    • IForall
    • IAll
    • IClear
    • IClearFrame
  • modalities.v
  • modality_instances.v
    • modality_embed
    • others
  • monpred.v
  • proofmode.v (ProofMode.lean)
  • [-] reduction.v (not necessary in Lean)
  • sel_patterns.v
  • spec_patterns.v
    • SIdent
    • SPureGoal
    • SGoal
      • Kind
      • Negate
      • Frame
      • Hyps
      • Done
    • SAutoFrame
  • [-] string_ident.v (not necessary in Lean)
  • [-] tokens.v (not necessary in Lean)

Examples

  • SI Logic

    • si_logic/siprop.v
    • si_logic/bi.v
      • BI instance
      • BI Persistently instance
      • BI Later instance

  • Program Logic

    • Final decisions about what to port from this folder have not been made yet.
    • language.v
    • ectx_language.v
    • ectxi_language.v
⚡