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 :) |
| lemma find_le ['a] (p : 'a -> bool) (s : 'a list) (n : int) : | ||
| 0 <= n < size s => p (nth witness s n) => find p s <= n. | ||
| proof. | ||
| move=> [ge0_n _] pn; apply/lezNgt/negP => lt_n. |
There was a problem hiding this comment.
If you're not going to use n < size s you might as well remove it from the lemma statement.
| qed. | ||
|
|
||
| lemma subseq_range (l1 l2 r1 r2 : int) : | ||
| l1 <= l2 <= r2 <= r1 => subseq (range l2 r2) (range l1 r1). |
There was a problem hiding this comment.
You don't need l2 <= r2 here.
| (* -------------------------------------------------------------------- *) | ||
| (* prefixes *) | ||
| (* -------------------------------------------------------------------- *) | ||
| op isprefix ['a] (s1 s2 : 'a list) : bool = |
There was a problem hiding this comment.
You should also expose a recursive definition through lemmas to enable induction. isprefix_nil s: isprefix [] s and isprefix_cons s1 s2 x1 x2: isprefix (x1::s1) (x2::s2) <=> (isprefix s1 s2 /\ x1 = x2)
| (* 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.
| (* interval *) | ||
| (* interval s l r = the slice s[l..r) (l included, r excluded) *) | ||
| (* -------------------------------------------------------------------- *) | ||
| op interval ['a] (s : 'a list) (l r : int) = drop l (take r s). |
There was a problem hiding this comment.
I think a name like sublist would be better. This has precedence (https://www.w3schools.com/java/ref_arraylist_sublist.asp)
| size s <= r => interval s l r = drop l s. | ||
| proof. by move=> *; rewrite /interval take_oversize. qed. | ||
|
|
||
| lemma interval_subseq ['a] (s : 'a list) (l1 l2 r1 r2 : int) : |
There was a problem hiding this comment.
I would expect a lemma with this name to prove subseq (interval s l r) s. Change the name to interval_subseq_interval
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 :)