Prevent zify from looping

[yannl35133]

Fixes / closes rocq-prover/rocq#22093

[proux01]

@yannl35133 CI is not happy, the VST failure is known and unrelated, the metarocq one is likely unrelated too but others look like actual failures.

[proux01]

@yannl35133 the VST and metarocq failures are known and unrelated but the bedrock2 failure looks real

[yannl35133]

The first version worked well but only fixed the issue in >= 9.3.
The second version (let h1 := fresh H in let h2 := fresh H in destruct H as (h1, h2); try clear H) doesn't work because destruct H can, when H gets properly cleared, create a variable also named H, but fresh prevents this and gives different names.
So either we don't fix this for <9.3, or someone finds a way to test if a variable is a section variable (or, is cleared by destruct) in <9.3. (I don't know how to do that.)

(or we consider that omega's internals are really internals and ask bedrock maintainers to fix their proof script)

[JasonGross]

bedrock2 should not depend on variable names given by destruct in zify, I believe @andres-erbsen @samuelgruetter would agree

But if you want a backwards compat version at the cost of slowdown you can do something like:

tryif (assert_fails (
let h1 := fresh H in let h2 := fresh H destruct H as [h1 h2]; clear H))
then (* not secvar *) destruct H
else (destruct H; clear H)

Or use Ltac2 and length of Control.hyps to see whether destruct adds 1 hyp or 2 hyps net.

[SkySkimmer]

Does that work? clear in <9.3 does not fail when H is ltac bound even if destruct cleared it first

[samuelgruetter]

Or how about this version (untested):

         | [ H : 0 <= ?x < _ |- _ ] =>
           destruct H;
           lazymatch type of H with (* matching on the type of H *after* the destruct *)
           | 0 <= x => idtac (* H was not a section var, got cleared and reused, nothing to do *)
           | _ => clear H (* H was a section variable, destruct didn't clear it, which would lead to an inifinite loop *)
           end

I believe that it would be backwards-compatible even with code that relies on hypothesis names, because in the non-section-var case, it does the same as before, and in the section-var-case, we previously had an infinite loop that prevented this tactic from being used.

[JasonGross]

Does that work? clear in <9.3 does not fail when H is ltac bound even if destruct cleared it first

Use progress clear instead of clear?

Or how about this version (untested):

Presumably you need to wrap lazymatch in try or it will fail if H is unbound? Also is there a situation in which you can end up with x < _ in the variable named H, like if you have H5 : 0 <= x < _ and you are missing H4 but have all the ones before it, do you end up with H4 and H5? Or even better, swap the order

try (lazymatch type of H with (* matching on the type of H *after* the destruct *)
           | 0 <= x _ => clear H (* H was a section variable, destruct didn't clear it, which would lead to an inifinite loop *)
           | _ => idtac (* H was not a section variable *)
           end)

[proux01]

The first version worked well but only fixed the issue in >= 9.3.

I think it's fine to only fix on Rocq >= 9.3. Eventually (in about a year) the Stdlib library will require Rocq >= 9.3 and the fix will work for all supported version. As a side note, fixing only for master would be what would have been done before Stdlib became an actual library.

bedrock2 should not depend on variable names given by destruct in zify

An overlay would indeed be a solution. In that case we need a changelog entry though, to warn other users who could have done the same mistake.