Add meta theorems #59
Conversation
fblanqui
left a comment
fblanqui
left a comment
There was a problem hiding this comment.
Thanks Melanie! That's nice! Just a few things to change.
| rem x s == the subsequence of s, where the first occurrence | ||
| of x has been removed (compare filter (predC1 x) s | ||
| where ALL occurrences of x are removed). | ||
| rem_idx i s == the sequence s where the element at index i has been |
There was a problem hiding this comment.
I suggest to rename it into rem_nth for consistency.
| assert ⊢ subseq eqn (42 ⸬ 4 ⸬ 51 ⸬ 3 ⸬ □) (42 ⸬ 4 ⸬ 51 ⸬ 3 ⸬ 4 ⸬ □) ≡ false; | ||
| assert ⊢ subseq eqn (42 ⸬ 4 ⸬ 51 ⸬ 3 ⸬ □) (42 ⸬ 4 ⸬ 51 ⸬ 3 ⸬ □) ≡ true; | ||
|
|
||
| // ⊆ |
There was a problem hiding this comment.
Add a more informative comment like "list inclusion"?
| with ⊆ _ □ _ ↪ true; | ||
|
|
||
| opaque symbol subset_cons_r [a] (beq : τ a → τ a → 𝔹) (x : τ a) (l m : 𝕃 a) : | ||
| π (istrue (⊆ beq l m)) → π (istrue (⊆ beq l (x ⸬ m))) ≔ |
There was a problem hiding this comment.
Since istrue is declared as a coercion from 𝔹 to Prop in Bool.lp, we do normally do not need to write it explicitly.
| // rem_idx | ||
|
|
||
| symbol rem_idx [a : Set]: 𝕃 a → ℕ → 𝕃 a; | ||
| rule rem_idx $l $n ↪ (take $n $l) ++ (drop ($n +1) $l); |
There was a problem hiding this comment.
Can't we have something more efficient by going through the list only once?
rem_nth _ [] --> []
rem_nth 0 (x :: l) --> l
rem_nth (n +1) (x :: l) --> x :: rem_nth n l
| ** Delete: | ||
| The theorem is instantiated with three lists: | ||
| 1. A list of natural numbers representing the indices of literals in the original list. |
| end; | ||
|
|
||
|
|
||
| // disj |
| // ⊆ | ||
|
|
||
| symbol ⊆ₙ ≔ ⊆ eqn; | ||
| notation ⊆ₙ infix right 30.000000; |
There was a problem hiding this comment.
already defined on line 81 with a different priority !
isn't creating an error or a warning ?
| // preserves_contents | ||
|
|
||
| symbol preserves_contents: 𝕃 nat → 𝕃 o → 𝔹; | ||
| rule preserves_contents $f $l ↪ (indexes $l) ⊆ₙ $f; |
|
|
||
| // ∨ᵢₙ | ||
| opaque symbol ∨ᵢₙ (c0 : 𝕃 o) (c1 : 𝕃 o) (c2 : 𝕃 o) : | ||
| π (disj c0) → π (disj (c0 ++ c1 ++ c2))≔ |
There was a problem hiding this comment.
Why having two lists c1 and c2? Why not having only one? Then, there are two cases: append on the left or on the right. Third case: append in the middle (replace [disj c0] by [disj c1]).
| ### Added | ||
|
|
||
| - MetaTheorems: theorems for structural operations on the level of clauses and literals | ||
| - List: ⊆, em_idx, and related theorems |
There was a problem hiding this comment.
List: add ... em_idx -> rem_nth
2 participants
No description provided.