feat: iauintro and iaaccintro

[alvinylt]

Description

Ports iAuIntro and iAaccIntro.

Resolves #289 (i.e., the remaining items that are not included in #665).

These tactics can be used to simplify the proofs in ProgramLogic/Atomic.lean (#672).

Checklist

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

[alvinylt]

!bench

[leanprover-radar]

Benchmark results for b563fdd against 5bf8817 are in. No significant results found. @alvinylt

• 🟥 build//instructions: +5.5G (+0.28%)

Small changes (1🟥)

• 🟥 build/module/Iris.ProofMode.Expr//instructions: +1.5G (+10.92%) (reduced significance based on *//lines)

[MackieLoeffel]

I don't know these tactics very well, but from what I see, this looks fine. I guess the real test is using these tactics in #675. Can this be merged or do you still want to change something?

[MackieLoeffel]

Great, thank you!