From 1f85ff2485552c9a646de126b9cc1f5321267946 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 8 Oct 2020 17:25:13 +0200
Subject: [PATCH] add IsOp instances for addition and min/max

---
 theories/algebra/frac.v    |  7 ++++++-
 theories/algebra/numbers.v | 15 ++++++++++++++-
 2 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 85543266d..4fea0470c 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -55,5 +55,10 @@ Proof. done. Qed.
 Lemma frac_valid' (p : Qp) : ✓ p ↔ (p ≤ 1%Qp)%Qc.
 Proof. done. Qed.
 
-Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
+Global Instance frac_is_op_half q : IsOp' q (q/2)%Qp (q/2)%Qp.
 Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.
+
+(* This one has a higher precendence than [is_op_op] so we get a [+] instead
+   of an [â‹…]. *)
+Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2.
+Proof. done. Qed.
diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
index b83e36f23..25893ec9d 100644
--- a/theories/algebra/numbers.v
+++ b/theories/algebra/numbers.v
@@ -40,7 +40,7 @@ Section nat.
 
   (* This one has a higher precendence than [is_op_op] so we get a [+] instead
      of an [â‹…]. *)
-  Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
+  Global Instance nat_is_op (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
   Proof. done. Qed.
 End nat.
 
@@ -93,6 +93,10 @@ Section max_nat.
 
   Global Instance : IdemP (=@{max_nat}) (â‹…).
   Proof. intros [x]. rewrite max_nat_op_max. apply f_equal. lia. Qed.
+
+  Global Instance max_nat_is_op (x y : nat) :
+    IsOp (MaxNat (x `max` y)) (MaxNat x) (MaxNat y).
+  Proof. done. Qed.
 End max_nat.
 
 (** ** Natural numbers with [min] as the operation. *)
@@ -145,6 +149,10 @@ Section min_nat.
 
   Global Instance : IdemP (=@{min_nat}) (â‹…).
   Proof. intros [x]. rewrite min_nat_op_min. apply f_equal. lia. Qed.
+
+  Global Instance min_nat_is_op (x y : nat) :
+    IsOp (MinNat (x `min` y)) (MinNat x) (MinNat y).
+  Proof. done. Qed.
 End min_nat.
 
 (** ** Positive integers with [Pos.add] as the operation. *)
@@ -175,4 +183,9 @@ Section positive.
     intros y ??. apply (Pos.add_no_neutral x y). rewrite Pos.add_comm.
     by apply leibniz_equiv.
   Qed.
+
+  (* This one has a higher precendence than [is_op_op] so we get a [+] instead
+     of an [â‹…]. *)
+  Global Instance pos_is_op (x y : positive) : IsOp (x + y)%positive x y.
+  Proof. done. Qed.
 End positive.
-- 
GitLab