From 38ff0fc1d8f806c955c81cf097a76382296b1263 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Wed, 17 Jun 2020 14:00:40 +0200
Subject: [PATCH] Add changes to changelog, properly reorder IsOp instance for
nat
---
CHANGELOG.md | 7 +++++++
theories/algebra/numbers.v | 10 +++++-----
2 files changed, 12 insertions(+), 5 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index edb16a12d..b7958f09c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -200,6 +200,11 @@ Coq development, but not every API-breaking change is listed. Changes marked
exists `heap_lang.derived_laws`.
* Remove global `Open Scope Z_scope` from `heap_lang.lang`, and leave it up to
reverse dependencies if they want to `Open Scope Z_scope` or not.
+* Add `min_nat`, a RA for natural numbers with `min` as the operation.
+* Rename `mnat` to `max_nat` and "box" it by creating a separate type for it.
+* Move the RAs for `nat` and `positive` and the `mnat` RA into a separate
+ module. They must now be imported from `From iris.algebra Require Import
+ numbers`.
The following `sed` script should perform most of the renaming (FIXME: incomplete)
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -221,6 +226,8 @@ s/\blist_singletonM_included\b/list_singleton_included/g
s/\bauth_both_frac_op\b/auth_both_op/g
# inv_sep
s/\binv_sep\b/inv_split/g
+# mnat rename
+s/\bmnat\b/max_nat/g
' $(find theories -name "*.v")
```
diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
index d1f65b46a..cfc0fa746 100644
--- a/theories/algebra/numbers.v
+++ b/theories/algebra/numbers.v
@@ -36,6 +36,11 @@ Section nat.
intros ??; apply local_update_unital_discrete=> z _.
compute -[minus plus]; lia.
Qed.
+
+ (* 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.
+ Proof. done. Qed.
End nat.
(** ** Natural numbers with [max] as the operation. *)
@@ -130,11 +135,6 @@ Section min_nat.
Global Instance : @IdemP min_nat (=) (â‹…).
Proof. intros [x]. rewrite min_nat_op_min. apply f_equal. lia. Qed.
-
- (* 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.
- Proof. done. Qed.
End min_nat.
(** ** Positive integers with [Pos.add] as the operation. *)
--
GitLab