search

ComputerAidedLL / click-and-collect

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml
GNU Lesser General Public License v2.1
17 stars 2 forks source link

[cut elimination] explicit exchange appearing #144

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

Clicking on the red cut generates an explicit exchange. And afterwards, clicking on the green cut generates an error message:

"Bad request: invalid proof: Premises conclusion do not match expected premises conclusion after applying rule {\"rule\":\"cut\",\"formula\":{\"type\":\"whynot\",\"value\":{\"type\":\"dual\",\"value\":{\"type\":\"litt\",\"value\":\"o\"}}},\"formulaPosition\":2}}"

cut2

etiennecallies commented 3 years ago

I cannot reproduce it on https://ccll.linear-logic.org/?s=o&n=o%2C%21o+-o+o&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzl9eyXig67oHQyYTslSub4UdC6wcpw%2BxPIisUM%2FDU96uPUsSW4WGq29bgQWSkZuLsHQNlQSuJJY1%2Fwhv%2Bwj5PBMOfWTPqJjekJ%2F4AbjjPeEld4aqcgmDL6nhNhNMqIK3S%2BdlPrnNUKMTK1Vsa7N6%2BexEUxZNp%2FAVwmpL4geAqFsConAqyJfOE5zu2%2B7nywsFHyyrXVuNV0HZj%2BED0T7kEC6L0Owu72AvFoeqhBXyT1HUNQWuiC7%2FLOjs69F7KAEeB7yyCyqCB3KkOkoHg%2F77Q0PQtVk1%2Fp6GM4Vsp5WILhMteYda%2FeO3Fu1jXAEm8yn4nln1Vtre47leZYwWdvMxfgkqaY3oDB%2BGMKot2N4MY4RBYmvab0HB%2FrEy1RdOXCAqM0NqV2HwwaAR67sHUHFqaExNqRcxlqRzSG3iCLBfm%2FasD5yOuuu3QKr4%2Bcp7uukhnfe6DEg1kX4EaaKPgQfG43SiPeynJjqGakIheNkVqTGI14BnL5A188T9%2FSv7whpBqpJgG6j7Z4iXSI7ZTnJlwrSzDb%2Bo4tWQWnQ2ZE%2BeEKxUB%2F%2Bd2X%2Bw%3D&proof_transformation=1

etiennecallies commented 3 years ago

If you used the auto-prover I just pushed a commit that fixes an issue with permutation.

olaure01 commented 3 years ago

https://ccll.linear-logic.org/?s=o&n=o%2C%21o%E2%8A%B8o&proof_transformation=1&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzl9eyXig67oHQyYTslSub4UdC6wcpw%2BxPIisUM%2FDU96uPUsSW4WGq29bgQWSkZuLsHQNlQSuJJY1%2Fwhv%2Bwj5PBMOfWTPqJjekJ%2F4AbjjPeEld4aqcgmDL6nhNhNMqIK3S%2BdlPrnNUKMTK1Vsa7N6%2BexEUxZNp%2FAVwmpL4geAqFsConAqyJfOE5zu2%2B7nywsFHyyrXVuNV0HZj%2BED0T7kEC6L0Owu72AvFoeqhBXyT1HUNQWuiC7%2FLOjs69F7KAEeB7yyCyqCB3KkOkoHg%2F77Q0PQtVk1%2Fp6GM4Vsp5WILhMteYda%2FeO3Fu1jXAEm8yn4nln1Vtre47leZYwWdvMxffOXicd%2FV3Z6Ir2mMUEliMouw89fZhQVI73bekOs2J2Fadx2bL5bO8cFzjBDe8BB9XfSHwLq%2FSf0mcVfb6SVqlkHvoW5f34Wsk9Jhe3H5Ax8id8j9mlf7KtQsceUe2Lj3rJ%2FHcjKVKtO7GxERnCcyUh4MUOsPTvweR5uAg%2Bgyb97bqGoTrgGMx4aw3MOc8X0cMsW8JJdZFdnlm%2BX6%2Ff6LQ69K%2Fu7tqwBK%2F8HKIJw%3D