From 3bdeb62fca5042f24deb6ec574311bcdc45a80bb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Mar 2017 19:33:28 +0100
Subject: [PATCH] Shorten a lemma.

---
 theories/base_logic/big_op.v | 29 +++++++++++------------------
 1 file changed, 11 insertions(+), 18 deletions(-)

diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 4c263b62a..215568a46 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -320,25 +320,18 @@ Section list2.
   (* Some lemmas depend on the generalized versions of the above ones. *)
 
   Lemma big_sepL_zip_with {B C} Φ f (l1 : list B) (l2 : list C) :
-    ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l1, ∀ y, ⌜l2 !! k = Some y⌝ → Φ k (f x y)).
+    ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x)
+    ⊣⊢ ([∗ list] k↦x ∈ l1, ∀ y, ⌜l2 !! k = Some y⌝ → Φ k (f x y)).
   Proof.
-    revert Φ l2; induction l1; intros Φ l2; first by rewrite /= big_sepL_nil.
-    destruct l2; simpl.
-    { rewrite big_sepL_nil. apply (anti_symm _); last exact: True_intro.
-      (* TODO: Can this be done simpler? *)
-      rewrite -(big_sepL_mono (λ _ _, True%I)).
-      - rewrite big_sepL_forall. apply forall_intro=>k. apply forall_intro=>b.
-        apply impl_intro_r. apply True_intro.
-      - intros k b _. apply forall_intro=>c. apply impl_intro_l. rewrite right_id.
-        apply pure_elim'. done.
-    }
-    rewrite !big_sepL_cons. apply sep_proper; last exact: IHl1.
-    apply (anti_symm _).
-    - apply forall_intro=>c'. simpl. apply impl_intro_r.
-      eapply pure_elim; first exact: and_elim_r. intros [=->].
-      apply and_elim_l.
-    - rewrite (forall_elim c). simpl. eapply impl_elim; first done.
-      apply pure_intro. done.
+    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2]//=.
+    - rewrite big_sepL_nil. apply (anti_symm _), True_intro.
+      trans ([∗ list] _↦_ ∈ x :: l1, True : uPred M)%I.
+      + rewrite big_sepL_forall. auto using forall_intro, impl_intro_l, True_intro.
+      + apply big_sepL_mono=> k y _. apply forall_intro=> z.
+        by apply impl_intro_l, pure_elim_l.
+    - rewrite !big_sepL_cons IH. apply sep_proper=> //. apply (anti_symm _).
+      + apply forall_intro=>z /=. by apply impl_intro_r, pure_elim_r=>-[->].
+      + rewrite (forall_elim y) /=. by eapply impl_elim, pure_intro.
   Qed.
 End list2.
 
-- 
GitLab