From 1657d8d0e58eab24dbde98ee1a0dc05e7b47f9c4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 Apr 2019 23:30:08 +0200
Subject: [PATCH] Add `Forall_reverse`.

---
 theories/list.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index a38fc6a0..ab2bb351 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -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).
-- 
GitLab