From ec7258e2b6e23439b21634c77a9a2af734384887 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 7 Dec 2021 12:17:58 +0100
Subject: [PATCH] Rename `(bool_)decide_iff` into `(bool_)decide_ext`.

---
 theories/decidable.v    | 6 +++---
 theories/list.v         | 4 ++--
 theories/list_numbers.v | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/decidable.v b/theories/decidable.v
index c3d94f5f..eb93b48f 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -21,7 +21,7 @@ Proof. destruct (decide P); tauto. Qed.
 Lemma decide_False {A} `{Decision P} (x y : A) :
   ¬P → (if decide P then x else y) = y.
 Proof. destruct (decide P); tauto. Qed.
-Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
+Lemma decide_ext {A} P Q `{Decision P, Decision Q} (x y : A) :
   (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
 Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
 
@@ -189,9 +189,9 @@ Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true ↔ P.
 Proof. case_bool_decide; intuition discriminate. Qed.
 Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ↔ ¬P.
 Proof. case_bool_decide; intuition discriminate. Qed.
-Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
+Lemma bool_decide_ext (P Q : Prop) `{Decision P, Decision Q} :
   (P ↔ Q) → bool_decide P = bool_decide Q.
-Proof. repeat case_bool_decide; tauto. Qed.
+Proof. apply decide_ext. Qed.
 
 Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true → P.
 Proof. apply bool_decide_eq_true. Qed.
diff --git a/theories/list.v b/theories/list.v
index 86256aa5..5341d91e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1993,7 +1993,7 @@ Lemma list_filter_filter (P1 P2 : A → Prop)
 Proof.
   induction l as [|x l IH]; [done|].
   rewrite !filter_cons. case (decide (P2 x)) as [HP2|HP2].
-  - rewrite filter_cons, IH. apply decide_iff. naive_solver.
+  - rewrite filter_cons, IH. apply decide_ext. naive_solver.
   - rewrite IH. symmetry. apply decide_False. by intros [_ ?].
 Qed.
 
@@ -3727,7 +3727,7 @@ Section find.
     list_find P l = list_find Q l.
   Proof.
     intros HPQ. induction l as [|x l IH]; simpl; [done|].
-    by rewrite (decide_iff (P x) (Q x)), IH by done.
+    by rewrite (decide_ext (P x) (Q x)), IH by done.
   Qed.
 End find.
 
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 53d88649..758f3660 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -340,7 +340,7 @@ Section Z_little_endian.
       by rewrite Z_ones_spec, bool_decide_true, andb_true_r by lia.
     - rewrite andb_false_r, orb_false_l.
       rewrite Z.shiftr_spec by lia. f_equal; [f_equal; lia|].
-      rewrite !Z_ones_spec by lia. apply bool_decide_iff. lia.
+      rewrite !Z_ones_spec by lia. apply bool_decide_ext. lia.
   Qed.
 
   Lemma Z_to_little_endian_length m n z :
-- 
GitLab