[auto-prove] Loop detection up to exchange

[olaure01]

The proof generated for ⊢ ?(A^⅋A^), ?((?1⊗⊥)⊕?(A⊗A)), ?(A⊗A), ??1 contains

⊢ ?(A⊗A), ?((?1⊗⊥)⊕?(A⊗A)), ?(A^⅋A^), ??1

thus a loop detection up to exchange would allow to compress it. I don't know how much it would cost.

[olaure01]

A similar idea is comparing sequents up to "weakening". In the automatically generated proof of ⊢ (1⅋1)⊗⊥, ?(?1⊗?1), one can find a simple proof of ⊢ ?1 and a more complex proof of ⊢ ?(?1⊗?1), ?1.

[olaure01]

This phenomenon of generating sometimes uselessly complex proofs is related to the fact that the automated prover is parametrized to try complex ?-formulas first (sorting w.r.t. whynot_height). The idea is that it could help finding complex proofs, but as a counterpart it can miss simpler ones.

[etiennecallies]

It is way better with increasing order of sort_whynot. And I can not reproduce loops, now that proofs are much simpler.

⊢ (1⅋1)⊗⊥, ?(?1⊗?1) prod ⊢ (1⅋1)⊗⊥, ?(?1⊗?1) preprod

⊢ ?(A⊗A), ?((?1⊗⊥)⊕?(A⊗A)), ?(A^⅋A^), ??1 prod ⊢ ?(A⊗A), ?((?1⊗⊥)⊕?(A⊗A)), ?(A^⅋A^), ??1 preprod

The only example which is a bit more complex is the following, but I think it's acceptable.

??1,?_ prod ??1,?_ preprod

[olaure01]

Good that proofs are simpler. The examples were designed to generate loops with the original order, so not very surprising they do not with the new one. Difficult to see whether:

remove_loop (commute_down_weakenings (remove_loop (commute_permutations proof (identity n))))

and

remove_loop (commute_down_weakenings (commute_permutations proof (identity n)))

could generate different proofs. It would require to be able to compare them.

[olaure01]

Maybe not the right place to state it, but corresponds to the version on pre-prod discussed here. auto-prove on: https://linearon.modusponens.dev/?s=%3F%21%3F%28X%7CX%5E%29%2C+%3F%21%3F%21%3F%21%28Y%7CY%5E%29%2C%3F%21%3F%21%28Y%7CY%5E%29 generates weakenings which look stuck above a promotion.

[etiennecallies]

Maybe not the right place to state it, but corresponds to the version on pre-prod discussed here. auto-prove on: https://linearon.modusponens.dev/?s=%3F%21%3F%28X%7CX%5E%29%2C+%3F%21%3F%21%3F%21%28Y%7CY%5E%29%2C%3F%21%3F%21%28Y%7CY%5E%29 generates weakenings which look stuck above a promotion.

It had to do with your previous comment. I just added back the double remove_loop and it's much simpler. Thanks!

Note: ??1,?_ is now also reduced.

[olaure01]

This one has an up-to weakening loop inside: https://linearon.modusponens.dev/?s=%3F%21%3F%21%28X%7CX%5E%29%2C+%3F%21%3F%21%3F%21%28Y%7CY%5E%29

[olaure01]

An up-to exchange loop: https://linearon.modusponens.dev/?s=A%5E%2CA%5E%2C+%3F%28%28%3F1%E2%8A%97%E2%8A%A5%29%E2%8A%95%3F%3F%28A%E2%8A%97A%29%29%2C%3F%3F%3F%28A*A%29

[etiennecallies]

An up-to exchange loop: https://linearon.modusponens.dev/?s=A%5E%2CA%5E%2C+%3F%28%28%3F1%E2%8A%97%E2%8A%A5%29%E2%8A%95%3F%3F%28A%E2%8A%97A%29%29%2C%3F%3F%3F%28A*A%29

Ok thanks, so we need to implement the loop detection with exchange. I'll do it soon.

This one has an up-to weakening loop inside: https://linearon.modusponens.dev/?s=%3F%21%3F%21%28X%7CX%5E%29%2C+%3F%21%3F%21%3F%21%28Y%7CY%5E%29

What do you mean? I see no loop in it. I agree it could be simpler: we could have a weakening directly instead of dereliction + promotion + weakening.

[olaure01]

By loop-detection up-to weakening, I mean: if a proof contains both ⊢ Γ and ⊢ Γ, ?Δ (up to permutation) with the proof of ⊢ Γ, ?Δ bigger than the proof of ⊢ Γ plus the number of formulas in Δ, then one could replace the proof of ⊢ Γ, ?Δ by the proof of ⊢ Γ followed by weakenings.

[etiennecallies]

By loop-detection up-to weakening, I mean: if a proof contains both ⊢ Γ and ⊢ Γ, ?Δ (up to exchange) with the proof of ⊢ Γ, ?Δ bigger than the proof of ⊢ Γ plus the number of formulas in Δ, then one could replace the proof of ⊢ Γ, ?Δ by the proof of ⊢ Γ followed by weakenings.

Got you! Perhaps, a bit more complex, but I'll do it.