Skip to content
Snippets Groups Projects
Commit 1657d8d0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add `Forall_reverse`.

parent 5727c9aa
No related branches found
No related tags found
No related merge requests found
......@@ -2317,6 +2317,11 @@ Section Forall_Exists.
Proof. rewrite Forall_lookup. eauto. Qed.
Lemma Forall_lookup_2 l : ( i x, l !! i = Some x P x) Forall P l.
Proof. by rewrite Forall_lookup. Qed.
Lemma Forall_reverse l : Forall P (reverse l) Forall P l.
Proof.
induction l as [|x l IH]; simpl; [done|].
rewrite reverse_cons, Forall_cons, Forall_app, Forall_singleton. naive_solver.
Qed.
Lemma Forall_tail l : Forall P l Forall P (tail l).
Proof. destruct 1; simpl; auto. Qed.
Lemma Forall_nth d l : Forall P l i, i < length l P (nth i l d).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment