From a34ad2b1041108dc619bbdc18ab6c7491b7450a5 Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Wed, 12 Feb 2025 09:13:48 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)
Co-authored-by: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
---
stdpp/list.v | 12 +++---------
1 file changed, 3 insertions(+), 9 deletions(-)
diff --git a/stdpp/list.v b/stdpp/list.v
index 108ce6e2..bd2b29d1 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -5051,15 +5051,9 @@ Section zip.
Lemma zip_nil_inv l k :
zip l k = [] → l = [] ∨ k = [].
Proof. intros. by eapply zip_with_nil_inv. Qed.
- Lemma lookup_zip_Some l k i e1 e2 :
- zip l k !! i = Some (e1, e2) ↔ l !! i = Some e1 ∧ k !! i = Some e2.
- Proof.
- rewrite lookup_zip_with_Some.
- split; first by intros (x&y&Heq&?&?); inversion Heq; subst;split.
- intros [->->].
- do 2 eexists.
- repeat split; reflexivity.
- Qed.
+ Lemma lookup_zip_Some l k i x y :
+ zip l k !! i = Some (x, y) ↔ l !! i = Some x ∧ k !! i = Some y.
+ Proof. rewrite lookup_zip_with_Some. naive_solver. Qed.
Lemma lookup_zip_None l k i :
zip l k !! i = None ↔ l !! i = None ∨ k !! i = None.
Proof. by rewrite lookup_zip_with_None. Qed.
--
GitLab