Auto-prover on sequent using recursive notations

[etiennecallies]

@olaure01 suggests:

I was wondering whether it could be interesting to consider the following approach to cyclic notations: spend 2s searching for a proof without using these cyclic notations at all (just like now), spend 0.5s after a single round of unfolding of each of them, spend 0.5s for a depth 2 unfolding, then fail.

[etiennecallies]

I would have another approach: try focused prover with increasing exponential_bound and "unfolding-depth" until 3s.

What do you think?

[etiennecallies]

Also, we should not unfold all notations at each try, but part of them.

Example: A,B with A::=B^ and B::=A^.

[olaure01]

I would have another approach: try focused prover with increasing exponential_bound and "unfolding-depth" until 3s.

Good. No so different. All this is just a matter of managing some equilibrium between "exponential unfolding" and "cyclic notation unfolding". I just think priority should be given to the first one, and what I suggested is just a kind of extreme way of doing it.

[olaure01]

Also, we should not unfold all notations at each try, but part of them.

Example: A,B with A::=B^ and B::=A^.

Doing something completely fair maybe does not worth it. So I would suggest iterated parallel substitution:

• round 0: A, B gives A, B
• round 1: A, B gives B^, A^
• round 2: A, B gives A, B
• etc.

An alternative approach would be to first compile cyclic notations into equivalent ones (in particular for simple cycles). Here for example, one could compile A::=B^ and B::=A^ into A ::= A^^ and B ::= A^ (here simplified into B :: = A^ in a second step).