chore: proof mode directory cleanup

[alvinylt]

Description

Time to go through the entire ProofMode directory, as most of the IPM tactics have now been ported.

• A cleanup of proofs that chain transitive entailments in Instances.lean, InstancesLater.lean, InstancesPlainly.lean, InstancesUpdates.lean, InstancesFrame.lean.
• A cleanup of Tests/Tactics.lean
  • Inconsistent use of namespace and section.
  • Inconsistent section names (e.g. intro, specialize, revert vs iinv, iinduction, ieval)..
  • Inconsistent use of explicit and implicit premises (e.g. Q : PROP explicitly as a premise but P and R were not`).
• Replaces all occurrences of ϕ (\varphi) with φ (\phi): the two symbols look the same in the IDE and there were multiple occasions where they were mixed up and caused confusion.
• Updates proofmode.md
• A more descriptive reason to not port iAssumptionCoq
• A walkthrough of the tactic implementation modules (except `ispecialize).
  • Adds all missing rocq_alias annotations for theorems in rocq_tactics.v. As a principle, rocq_alias annotations are added to those directly corresponding to the Rocq counterparts. Some of the tactics are implemented with different approaches in Lean (e.g. by iteration using a mutable state to construct proofs). In such cases, items in rocq_tactics.v with no direct Lean equivalents are annotated using rocq_ignore.
  • This includes commits de2bc87, ba8b2eb, fa33749, bb9eb7b and 70630eb.
• Same task as above for ispecialize (pending feat: remaining specialisation patterns #500).
• Double-check all comments to ensure they are up to date.

Items from `rocq_tactics.v` that are ported (with `rocq_alias` annotation)

• tac_accu
• tac_and_destruct_choice
• tac_and_destruct
• tac_and_split
• tac_apply
• tac_assert
• tac_assumption
• tac_clear
• tac_combine_as_gives
• tac_combine_as
• tac_combine_gives
• tac_ex_falso
• tac_exist_destruct
• tac_exist
• tac_false_destruct
• tac_forall_intro
• tac_forall_revert
• tac_forall_specialize
• tac_frame_pure
• tac_frame
• tac_impl_intro_drop
• tac_impl_intro_intuitionistic
• tac_impl_intro
• tac_intuitionistic
• tac_modal_elim
• tac_modal_intro
• tac_or_destruct
• tac_or_l
• tac_or_r
• tac_pose_proof
• tac_pure_intro
• tac_pure_revert
• tac_pure
• tac_revert
• tac_rewrite_in
• tac_rewrite
• tac_sep_split
• tac_spatial
• tac_specialize_assert_intuitionistic
• tac_specialize_assert_pure
• tac_specialize_assert
• tac_specialize
• tac_wand_intro_intuitionistic
• tac_wand_intro

Items from `rocq_tactics.v` that are ignored (with `rocq_ignore` annotation)

• affine_env_bi
• affine_env_nil
• affine_env_snoc
• affine_env_spatial
• combine_seps_as_from_as_gives
• combine_seps_as_gives_nil
• combine_seps_as_gives_singleton
• combine_seps_gives_cons
• combine_seps_gives_of_envs
• CombineSepsAs
• CombineSepsAsGives
• into_emp_valid_forall
• into_emp_valid_here
• into_emp_valid_impl
• into_emp_valid_proj
• into_emp_valid_tforall
• into_laterN_env_sound
• into_laterN_envs
• IntoEmpValid
• tac_assumption_rocq
• tac_emp_intro
• tac_eval_in
• tac_eval
• tac_löb
• tac_pose_proof_hyp
• tac_rename
• tac_specialize_frame
• tac_specialize_intuitionistic_helper_done
• tac_specialize_intuitionistic_helper
• tac_start
• tac_stoptac_unlock
• tac_unlock_emp
• tac_unlock_True
• tac_wand_intro_drop
• transform_intuitionistic_env_nil
• transform_intuitionistic_env_snoc_not
• transform_intuitionistic_env_snoc
• transform_spatial_env_nil
• transform_spatial_env_snoc_not
• transform_spatial_env_snoc

Checklist

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

[MackieLoeffel]

Thanks for this PR! I looked over the changes and except for two small comments, everything looks fine to me.

[MackieLoeffel]

Great, this is ready to merge from my side!