Commit e58dd720 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'last_lemma' into 'master'

Add `last_cons_Some_ne` lemma for the `last` function

See merge request iris/stdpp!361
parents 9f6f8c38 b66b5311
......@@ -1151,6 +1151,9 @@ Qed.
Lemma last_cons x l :
last (x :: l) = match last l with Some y => Some y | None => Some x end.
Proof. by apply (last_app [x]). Qed.
Lemma last_cons_Some_ne x y l :
x y last (x :: l) = Some y last l = Some y.
Proof. rewrite last_cons. destruct (last l); naive_solver. Qed.
Lemma last_lookup l : last l = l !! pred (length l).
Proof. by induction l as [| ?[]]. Qed.
Lemma last_reverse l : last (reverse l) = head l.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment