From 31ac77aaaa45eccf2374c5738de6d6fea4fb4a86 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= <fdupress@gmail.com>
Date: Fri, 17 Jan 2025 11:21:35 +0000
Subject: [PATCH] FMap: add lemmas on range after update

---
 theories/datatypes/FMap.ec | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/theories/datatypes/FMap.ec b/theories/datatypes/FMap.ec
index 961427d71..02ca3cffa 100644
--- a/theories/datatypes/FMap.ec
+++ b/theories/datatypes/FMap.ec
@@ -213,6 +213,23 @@ move=> x_notin_m; apply/fmap_eqP => y; rewrite remE.
 by case (y = x) => // ->>; apply/eq_sym/domNE.
 qed.
 
+(* -------------------------------------------------------------------- *)
+lemma rng_set (m : ('a, 'b) fmap) (x : 'a) (y z : 'b) :
+  rng m.[x <- y] z <=> rng (rem m x) z \/ z = y.
+proof.
+rewrite !rngE /=; split.
++ move=> [] r; rewrite get_setE; case: (r = x)=> />.
+  by move=> r_neq_x m_r; left; exists r; rewrite remE r_neq_x /= m_r.
+case=> [[] r rem_m_x_r|->>] />.
++ by exists r; move: rem_m_x_r; rewrite get_setE remE; case: (r = x).
++ by exists x; rewrite get_set_sameE.
+qed.
+
+lemma rng_set_notin (m : ('a, 'b) fmap) (x : 'a) (y z : 'b) :
+     x \notin m
+  => rng m.[x <- y] z <=> rng m z \/ z = y.
+proof. by rewrite rng_set=> /rem_id ->. qed.
+
 (* -------------------------------------------------------------------- *)
 op eq_except ['a 'b] X (m1 m2 : ('a, 'b) fmap) =
   SmtMap.eq_except X (tomap m1) (tomap m2).