Stronger `iNext` that performs arithmetic cancelation

This is WIP that fixes issue #148 (closed). Some questions:

• Where to put the canceler. Is this something more generic that should be moved to stdpp?
• Move TCIf to stdpp.
• How to name MakeIntoLaterN, it's like MakeLaterN, which is used for framing but slightly different, e.g. it does not turn ▷ True into True, but turns ▷^0 P into P and ▷^1 P into ▷ P.

changed the description

added 3 commits

• e2439195 - A simple canceler for natural numbers.
• 0ed18963 - Stronger iNext that performs arithmetic cancelation.
• 32a8c549 - Test cases for issue #148 (closed).

Compare with previous version

@jung @jjourdan Any opinions on my questions?

Not really. TBH I feel this is overkill, but then there's nothing wrong with overkill so whatever. :)

Why is there a difference between the two typeclasses?

Why is there a difference between the two typeclasses?

Which two typeclasses? The two variants of MakeLaterN?

Yes.

• MakeLaterN is used for framing, and turns ▷ True into True. That is basically to make sure that when everything under a later has been framed away, the later disappears too.
• MakeIntoLaterN is used by iNext and turns ▷^0 P into P and ▷^1 P into ▷ P. The is needed to make sure that after canceling in ▷^n we get back something nice.

Obviously, we could merge both classes, but I don't think that is nice. It makes little sense if framing would turn ▷^1 P into ▷ P, and vice versa, if iNext would turn ▷ True into just True.

Note something akin to MakeIntoLaterN could also be obtained by calling simpl on the result of iNext but I don't think we should call simpl arbitrarily, as it can change the goal in unexpected ways to the user.

I think I am going to move NatCancel to std++.

I think I am going to move NatCancel to std++.

Makes sense.

It makes little sense if framing would turn ▷^1 P into ▷ P, and vice versa, if iNext would turn ▷ True into just True.

Of course iNext should turn a hypothesis \later X into X for any X, including True... I am confused.

Where does framing have to turn things into LaterN anyway?

I suggest the version that does some sort of simpl should have Simpl in its name. Also, both typeclasses should have documentation saying what they are supposed to do and what not, Other than that, if you feel two typeclasses are needed, sure, go for it. :)

Of course iNext should turn a hypothesis \later X into X for any X, including True... I am confused.

My example was broken. iNext on a goal with a single ▷ should not turn ▷^(S n) True into True.

However, framing P in ▷^n P ∗ Q should turn the goal into Q.

I think I am going to move NatCancel to std++.

See https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/26/diffs

iNext on a goal with a single ▷ should not turn ▷^(S n) True into True.

Ah. Well, I wouldn't mind that strongly.

framing P in ▷^n P ∗ Q should turn the goal into Q.

Why does this need anything smart? Just descent below later and later^n ?

added 16 commits

• 32a8c549...4ffff895 - 14 commits from branch master
• 0414149c - Stronger iNext that performs arithmetic cancelation.
• d7041e5a - Test cases for issue #148 (closed).

Compare with previous version

marked the checklist item Where to put the canceler. Is this something more generic that should be moved to stdpp? as completed

framing P in ▷^n P ∗ Q should turn the goal into Q.

Why does this need anything smart? Just descent below later and later^n ?

The problem is that depending on whether framing in P succeeds, we need to get rid of the later ▷^n .

That's why we don't have:

Global Instance frame_laterN p n R R' P Q :
  NoBackTrack (IntoLaterN n R' R) →
  Frame p R P Q →
  Frame p R' (▷^n P) (▷^n Q).

But rather this whole MakeLaterN business.