feat: port bi/lib/counterexamples.v (+ fix IntoWand instances)

[alvinylt]

Description

Ports bi/lib/counterexamples.v.

Addresses #206.

Each Module in the Rocq version corresponds to a namespace in BI/Lib/Counterexamples.lean.

• affine_em: AffineEM
• löb_em: LoebEM
• savedprop
• inv
  • inv1
  • inv2
• linear
• later_credits_plain

Fixing IntoWand Instances

There is a comment above the existing type class instances intoWand_imp_false and intoWand_imp_true:

TODO: compare this with into_wand_impl_false_false, into_wand_impl_false_true, ... in Rocq

At one point within the proof of later_anything, we come across the following proof state:

□HnotP : ¬▷ False
□IH : ▷ False
⊢ False

With the existing two instances, we are unable to use ispecialize HnotP $$ IH to solve the goal.

The instance intoWand_imp_true stipulates Affine (▷ False), which does not hold. The type class instance into_wand_impl_true_true, on the other hand, has no such requirement. The instances intoWand_impl_false_true and intoWand_impl_false_false also come with different assumptions.

The two instances are therefore replaced by those directly corresponding to the formulation in Rocq.

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]

We have to unfold laterN manually in order for imod to produce the correct hypothesis.
Might be interesting to investigate the cause.