From cac67ba39f55ea0eac6a4dffb3db5cf5789245f9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jan 2021 11:41:26 +0100
Subject: [PATCH] shorter proof by Robbert
---
iris/algebra/big_op.v | 10 +++-------
1 file changed, 3 insertions(+), 7 deletions(-)
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 39633a43d..177fb8faa 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -484,14 +484,10 @@ Section gset.
NoDup l →
([^o set] x ∈ list_to_set l, f x) ≡ [^o list] x ∈ l, f x.
Proof.
- induction l as [|x l IHl]; intros Hnodup.
+ induction 1 as [|x l ?? IHl].
- rewrite big_opS_empty //.
- - inversion Hnodup; subst; clear Hnodup.
- rewrite /= big_opS_union; last first.
- { rewrite disjoint_singleton_l.
- rewrite elem_of_list_to_set //. }
- rewrite big_opS_singleton.
- f_equiv. apply IHl; auto.
+ - rewrite /= big_opS_union; last set_solver.
+ by rewrite big_opS_singleton IHl.
Qed.
End gset.
--
GitLab