feat: iinv

[alvinylt]

Description

Implements the iinv tactic.

Addresses #363.

This includes porting the following type classes instances of IntoAcc, ElimAcc, IntoInv and ElimInv.

Type class instance	Located in ... (Rocq)	Located in ... (Lean)	Definition ported?	Proof ported?
elim_inv_acc_without_close	class_instances.v	InstancesIris.lean	✓	✓
elim_inv_acc_with_close	class_instances.v	InstancesIris.lean	✓	✓
elim_acc_bupd	class_instances_updates.v	InstancesUpdates.lean	✓	✓
elim_acc_fupd	class_instances_updates.v	InstancesUpdates.lean	✓	✓
into_inv_inv	invariants.v	Invariants.lean	✓	✓
into_acc_inv	invariants.v	Invariants.lean	✓	✓
into_inv_cinv	cancelable_invariants.v	CInvariants.lean	✓	✓
into_acc_cinv	cancelable_invariants.v	CInvariants.lean	✓	✓
into_inv_na	na_invariants.v	NaInvariants.lean	✓	✓
into_acc_na	na_invariants.v	NaInvariants.lean	✓	✓
elim_acc_wp_atomic	weakestpre.v	WeakestPre.lean	✓	✓
elim_acc_wp_nonatomic	weakestpre.v	WeakestPre.lean	✓	✓

The following code is yet to be ported but also includes relevant type class instances.

• proofmode/monpred.v: elim_inv_embed_with_close, elim_inv_embed_without_close, elim_acc_at_None, elim_acc_at_Some
• program_logic/total_weakestpre.v: elim_acc_wp_atomic, elim_acc_wp_nonatomic
• bi/lib/atomic.v: elim_acc_aacc
• proofmode/class_instances_embedding.v: into_inv_embed

Other Changes

• Implement wandM (-∗?) in BIBase.lean, the theorem wandM_sound in DerivedLaws.lean. The related type class instances are also ported in Instances.lean, which allows us to, for example, apply iintro H given H : P -∗? Q. The outParam values obtained from type class synthesis with ElimInv may contain occurrences of wandM. The function pmReduce (similar to pm_reduce in the Rocq version) simplifies them and occurrences of Option.getD in specific propositions before using them in the new proof goals.
• Slight modifications to iSolveSidecondition in Basic.lean so that it does not fail when failOnUnsolved is set as false. Furthermore, instead of using only trivial, it now uses and_intros <;> first | trivial | simp_all so that a conjunction is broken down into smaller subgoals before trying various tactics to solve them.
• FrameResult.finishClose is made less restrictive to be consistent with the Rocq version: remove emp/True even when no progress is made with framing.
• Theorems in Pure.lean (pure_elim_spatial and pure_elim_intuitionistic) and Cases.lean (intuitionistic_elim_spatial and intuitionistic_elim_intuitionistic) are slightly modified to avoid dependency of ProofMode.Tactics on ProofMode.Instances. This enables us to use IPM tactics to complete proofs for type class instances in ProofMode.Instances without causing circular dependencies.
  • See the commit here for the relevant changes.
  • This is similar to the Rocq version where ltac_tactics.v depends on classes.v but not class_instances.v, while class_instances.v imports ltac_tactics.v.
  • There is a subtle caveat: instances of the type class AsEmpValid are used directly by ProofModeM.lean. They are moved to a separate file InstancesInit.lean, which is imported by ProofModeM.lean. Otherwise, istart fails with the error istart: <insert entailment here> is not an emp valid.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files