feat: inext with later credits

[alvinylt]

Description

Implements the tactic inext n credit: H.

Addresses #239.

Similar to the Rocq implementation, once all credits are consumed (that is, H becomes £ 0), the hypothesis is discarded.

The type class AddModal and its instances have already been ported in PR #470, but are nonetheless also included in this PR so that we can use them for this tactic. Using ElimModal instead.

This tactic is unique in the sense that it is relevant only for IProp GF where InvGS GF holds. Within the ProofModeM.runTactic block, we have the generic BI instance prop. Otherwise, if we use isDefEq to unify prop and InvGS GF manually, we still run into universal level problems:

Application type mismatch: The argument
  «$GF»
has type
  BundledGFunctors.{u✝, u✝, u✝}
of sort `Type (u✝ + 1)` but is expected to have type
  BundledGFunctors.{0, 0, 0}
of sort `Type 1` in the application ...

In the implementation, we use mkAppM so that the instance InvGS GF is synthesised automatically. Resolved in commits 9056733 and 9b1963a.

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]

The latest improvement is to use the same trick for HeapLang tactics for matching IProp GF with prop, so that we can use Qq for building proofs in subsequent steps instead of inelegantly using mkApp.

Commits: 9056733 and 9b1963a

[alvinylt]

This is a test that is supposed to use intoLaterN_laterN_bool. This instance is not yet ported, so I have done so along with the addition of this test.

As mentioned in a comment in the Rocq version, it might cancel a later "too much" in the worst case, so this instance has a lower priority than intoLaterN_later and intoLaterN_laterN.

In the Rocq version, neither into_laterN_later nor into_laterN_laterN applies to this test, so into_laterN_laterN_bool applies, and we get H : P. In contrast, BIBase.laterIf is a reducible def in Lean, so ▷?p P is equivalent to laterN (Bool.toNat p) P. As a result, into_laterN_later applies (given it has a higher priority than into_laterN_laterN_bool).

I'm not sure whether this is intentional or a bug: MaybeIntoLaterN is explicitly ignored and, unlike the Rocq version, intoLaterN_later and intoLaterN_laterN does not check progress using TCIf and TCEq. Is there an intended workaround for this, or should we have ported MaybeIntoLaterN and implemented the instances faithfully?

[alvinylt]

In commit 0b7d5fb, I tried to implement the design in Rocq faithfully with TCIf introduced into Std/TC.lean and MaybeIntoLaterN being a type class. Basically, IntoLaterN is the type class that necessitates progress, whereas MaybeIntoLaterN allows a fallback option that enables propositions to remain unchanged. This is intended to avoid the lack of progress being silently accepted without trying other instances. In the example test above, the intended behaviour should be:

1. The instance intoLaterN_later has a higher priority and tried first.
2. No progress is made with intoLaterN_later, instead of leaving the H unchanged, backtrack and try other instances.
3. The instance intoLaterN_laterN_bool is tried. Progress is made, so the result of the synthesis is adopted.

This approach with the use of TCIf, however, broke the tactic as it is not an IPM type class (because it is meant to be in Std/TC.lean). With reference to the type class synthesis trace, the built-in type class synthesiser in Lean tries the applicable instances of IntoLaterN. If they all fail, the fallback option with MaybeIntoLaterN applies, and the TCIf ... instance overall succeeds. And when this propagates to the recursive type class search caller, it uses this default result of unchanged proposition directly. The search could possibly have backtracked such the recursive search had a non-default result.

In fact, there seems to be some trick for TCIf in Rocq's stdpp to avoid this:

Global Hint Extern 0 (TCIf ⇒
  first [notypeclasses refine (TCIf_true _ _ _ _ _); [tc_solve|]
        |notypeclasses refine (TCIf_false _ _ _ _)] : typeclass_instances.

So the solution is similar: instead of using TCIf, we define a wrapper type class GuardedIntoLaterN which is an IPM type class. Its two instances (guardedIntoLaterN_stuck and guardedIntoLaterN_progress) are not labelled with ipm_backtrack. Meanwhile, instances of IntoLaterN and MaybeIntoLaterN are labelled with ipm_backtrack and adjusted accordingly.

[alvinylt]

Now trying to implement IntoLaterN and NatCancel using ipm_tactic_instance.

[alvinylt]

The type classes IntoLaterN, MaybeIntoLaterN and GuardedIntoLaterN are consolidated into a single type class. A new parameter (strict) for IntoLaterN indicates whether we would like progress to made.

The tactic instance intoLaterNLater handles the work of intoLaterN_later, intoLaterN_laterN and intoLaterN_laterN_bool, using isDefEq to check whether progress is made.

See diff here.

[alvinylt]

NatCancel has now also been refactored.

• The helper type classes MakeNatAdd and MakeNatS are no longer necessary and thus removed. Instead we now have two functions to parse expressions (tryParseSucc and tryParseAdd) and break them into subexpressions.
• NatCancel is now an IPM type class. Instead of 25 type class instances, there is a single type class instance (ipm_class_instance). Nonetheless there are helper functions to help with the recursion.
• NatCancel is from stdpp, so it was originally ported in Std/TC.lean. Since it now references features in the IPM type class synthesiser, the code is now under the ProofMode directory avoid circular dependency between ProofMode and Std.

To be honest this new approach isn't really that simpler compared to the original port, especially with all the wrestling with Qq proofs, but is (hopefully) nevertheless easier to understand.

Commit: 4010144