From 9901a12d895027c4fc7ab4c45d6c5666ad2b0938 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 18 Dec 2019 15:11:36 +0100
Subject: [PATCH] Use &&& from lazy_bool_scope instead of redefining the &&
 notation.

---
 theories/proofmode/base.v         | 11 ++++++-----
 theories/proofmode/coq_tactics.v  |  4 +++-
 theories/proofmode/environments.v |  9 ++++-----
 3 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 45e060b66..c28fbbe9d 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -8,12 +8,13 @@ Set Default Proof Using "Type".
 (* Directions of rewrites *)
 Inductive direction := Left | Right.
 
+Local Open Scope lazy_bool_scope.
+
 (* Some specific versions of operations on strings, booleans, positive for the
 proof mode. We need those so that we can make [cbv] unfold just them, but not
 the actual operations that may appear in users' proofs. *)
-Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
-Lemma lazy_andb_true (b1 b2 : bool) : b1 && b2 = true ↔ b1 = true ∧ b2 = true.
+Lemma lazy_andb_true (b1 b2 : bool) : b1 &&& b2 = true ↔ b1 = true ∧ b2 = true.
 Proof. destruct b1, b2; intuition congruence. Qed.
 
 Fixpoint Pos_succ (x : positive) : positive :=
@@ -32,13 +33,13 @@ Definition beq (b1 b2 : bool) : bool :=
 Definition ascii_beq (x y : ascii) : bool :=
   let 'Ascii x1 x2 x3 x4 x5 x6 x7 x8 := x in
   let 'Ascii y1 y2 y3 y4 y5 y6 y7 y8 := y in
-  beq x1 y1 && beq x2 y2 && beq x3 y3 && beq x4 y4 &&
-    beq x5 y5 && beq x6 y6 && beq x7 y7 && beq x8 y8.
+  beq x1 y1 &&& beq x2 y2 &&& beq x3 y3 &&& beq x4 y4 &&&
+    beq x5 y5 &&& beq x6 y6 &&& beq x7 y7 &&& beq x8 y8.
 
 Fixpoint string_beq (s1 s2 : string) : bool :=
   match s1, s2 with
   | "", "" => true
-  | String a1 s1, String a2 s2 => ascii_beq a1 a2 && string_beq s1 s2
+  | String a1 s1, String a2 s2 => ascii_beq a1 a2 &&& string_beq s1 s2
   | _, _ => false
   end.
 
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 3018f180b..757a3b6c6 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -5,6 +5,8 @@ Set Default Proof Using "Type".
 Import bi.
 Import env_notations.
 
+Local Open Scope lazy_bool_scope.
+
 (* Coq versions of the tactics *)
 Section bi_tactics.
 Context {PROP : bi}.
@@ -269,7 +271,7 @@ Lemma tac_specialize remove_intuitionistic Δ i p j q P1 P2 R Q :
   let Δ' := envs_delete remove_intuitionistic i p Δ in
   envs_lookup j Δ' = Some (q, R) →
   IntoWand q p R P1 P2 →
-  match envs_replace j q (p && q) (Esnoc Enil j P2) Δ' with
+  match envs_replace j q (p &&& q) (Esnoc Enil j P2) Δ' with
   | Some Δ'' => envs_entails Δ'' Q
   | None => False
   end → envs_entails Δ Q.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 2ae03b1d5..25b78819c 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -24,12 +24,11 @@ Module env_notations.
   Notation "x ← y ; z" := (y ≫= λ x, z).
   Notation "' x1 .. xn ← y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. )).
   Notation "Γ !! j" := (env_lookup j Γ).
-
-  (* andb will not be simplified by pm_reduce *)
-  Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 End env_notations.
 Import env_notations.
 
+Local Open Scope lazy_bool_scope.
+
 Inductive env_wf {A} : env A → Prop :=
   | Enil_wf : env_wf Enil
   | Esnoc_wf Γ i x : Γ !! i = None → env_wf Γ → env_wf (Esnoc Γ i x).
@@ -307,7 +306,7 @@ Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
   | j :: js =>
      ''(p,P,Δ') ← envs_lookup_delete remove_intuitionistic j Δ;
      ''(q,Ps,Δ'') ← envs_lookup_delete_list remove_intuitionistic js Δ';
-     Some ((p:bool) && q, P :: Ps, Δ'')
+     Some ((p:bool) &&& q, P :: Ps, Δ'')
   end.
 
 Definition envs_snoc {PROP} (Δ : envs PROP)
@@ -545,7 +544,7 @@ Qed.
 Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps :
   envs_lookup_delete rp j Δ = Some (p1, P, Δ') →
   envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'') →
-  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ'').
+  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 &&& p2, (P :: Ps), Δ'').
 Proof. rewrite //= => -> //= -> //=. Qed.
 
 Lemma envs_lookup_delete_list_nil Δ rp :
-- 
GitLab