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 :) |
| (* rfind p l = index of the last element of l satisfying p *) | ||
| (* (or -1 if there is none). *) | ||
| (* -------------------------------------------------------------------- *) | ||
| op rfind ['a] (p : 'a -> bool) (l : 'a list) : int = |
There was a problem hiding this comment.
This rfind operator should have lemmas corresponding to all existing find lemmas when possible.
This section should be next to the find section if possible.
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 :)