Updated version of the Delete Theorem in Disj.LP, along with related encodings and theorems

[melanie-taprogge]

The original version of delete needs to be instantiated with two lists: one representing the indices of literals in the original clause (with identical literals sharing the same number), and another list of literal indices representing the clause after the deletion of duplicate literals. The theorem then verifies that the resulting list still contains each literal at least once. This admissibility check evaluates to ⊤ for every valid deletion and therefore has to be instantiated using ⊤ᵢ.

This PR introduces undup_first in List.lp, which deletes all but the first occurrence of each element in a list. Based on undup_first, a new convenience version of delete is defined that only needs to be instantiated with the original list of indices and automatically removes all duplicate occurrences except the first. I also proved a general theorem showing that this operation always preserves one occurrence of each literal of the original clause. As a result, it is no longer necessary to explicitly compute admissibility or to instantiate the proof with ⊤ᵢ.

In addition, several supporting theorems were added to Bool.lp, List.lp, and Nat.lp.

[fblanqui]

Thanks Melanie. The only thing I am worried about is the efficiency of undup_first. I am wondering whether we could not find something more efficient like perhaps:

undup1 acc [] --> rev acc
undup1 acc (x :: l) --> if (in beq x acc) (undup1 acc l) (undup1 (x :: acc) l)
undup_first := undup1 []

I improved the efficiency of List.rev in #61 to this end.
Perhaps we could even define undup as follows:

undup l := rev (undup_first (rev l))

Would you like to try to prove that the two definitions of undup_first and undup are equal (in a separate PR)?

[fblanqui]

Good catch! Is there any other theorem not declared as opaque?