New lemmas for List - #1072
Conversation
|
@namasikanam Did you change some lemmas? |
|
The SHA3 one could be a |
|
I didn't change any statement of existing lemmas (only update some proofs when they are not running on my machine). I coudn't find |
Maybe the sha3 dev contains rogue |
e221166 to
e211fc2
Compare
I fixed the inconsistency in docker. I couldn't reproduce the failure for SHA3. But it turned out that the failure in SHA3 gets also resolved magically :) |
|
I will always test within docker before creating a PR in the future :) |
4e5de52 to
601f53a
Compare
| => nth x (sublist s l r) m = nth x s (m + l). | ||
| proof. by move => ??; rewrite /sublist nth_drop // 1:/# nth_take /#. qed. | ||
|
|
||
| lemma sublist_subseq_sublist ['a] (s : 'a list) (m l r : int) : |
There was a problem hiding this comment.
The name should be something like sublist_cat.
| proof. by move => ??; rewrite /sublist nth_drop // 1:/# nth_take /#. qed. | ||
|
|
||
| lemma sublist_subseq_sublist ['a] (s : 'a list) (m l r : int) : | ||
| 0 <= l <= m <= r <= size s |
There was a problem hiding this comment.
You don't need 0 <= l and r <= size s.
|
|
||
| lemma sublist_subseq_sublist ['a] (s : 'a list) (m l r : int) : | ||
| 0 <= l <= m <= r <= size s | ||
| => sublist s l r = sublist s l m ++ sublist s m r. |
There was a problem hiding this comment.
Prefer putting the more complex thing (the expression with concatenation) on the left side.
| qed. | ||
|
|
||
| lemma sublistS ['a] (s : 'a list) (n m : int) : | ||
| 0 <= n < m <= size s |
There was a problem hiding this comment.
You're assuming m = n + 1 so you don't need n < m.
Maybe use n+1 directly instead of using m? Then you can drop the equality assumption as well.
| size s <= r => sublist s l r = drop l s. | ||
| proof. by move=> *; rewrite /sublist take_oversize. qed. | ||
|
|
||
| lemma sublist_subseq ['a] (s : 'a list) (l1 l2 r1 r2 : int) : |
There was a problem hiding this comment.
This one should be named sublist_subseq_sublist
| proof. by move=> *; rewrite /sublist take_oversize. qed. | ||
|
|
||
| lemma sublist_subseq ['a] (s : 'a list) (l1 l2 r1 r2 : int) : | ||
| 0 <= l1 <= l2 <= r1 <= r2 |
There was a problem hiding this comment.
You don't need l2 <= r1.
Also, the numbering on the ls and rs are inconsistent. Switch the names of l1 and l2.
There was a problem hiding this comment.
You don't need 0 <= l1 either.
4 participants
There are a few new lemmas and four new operators:
isprefix: whether one list is a prefix of the other listprefixes: the sets of all prefixes of a listinterval: a consecutive subsequence of a listrfind: reverse finding (start from the end of the list)Also, I reduced smt usage in some old proofs, as smt solving in those proof fails on my machine. I believe these updates only make proofs better :)