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
| 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.
There was a problem hiding this comment.
The unneeded inequalities have been removed, but the naming inconsistency is still there.
There was a problem hiding this comment.
What do you mean by naming inconsistency?
There was a problem hiding this comment.
In the last commit, I believe I have already renamed the lemma as sublist_subseq_sublist, if this is what you meant by naming inconsistency.
601f53a to
f8d6c8d
Compare
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 :)