feat: port bi/lib/core.v

[alvinylt]

Description

Ports bi/lib/core.v.

Addresses #279.

The theorems coreP_entails and coreP_entails' are proven in Rocq by rewriting of BI entailments. Meanwhile, I'm using two auxiliary lemma coreP_entails_aux since rw in Lean only works with equalities and ↔. Possible example to showcase the use of rw' if we can get the tactic working.

The bug in rw' is fixed (see discussions). By using rw', we are able to simplify some of the proofs (see relevant commit).

Until #1 is resolved, we can perhaps consider whether to implement Proper type class instances that are ignored in Iris-Lean as theorems with the annotation rw_mono_rule instead.

Checklist

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