Commit 38ff0fc1 authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Add changes to changelog, properly reorder IsOp instance for nat

parent e68b2730
...@@ -200,6 +200,11 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -200,6 +200,11 @@ Coq development, but not every API-breaking change is listed. Changes marked
exists `heap_lang.derived_laws`. exists `heap_lang.derived_laws`.
* Remove global `Open Scope Z_scope` from `heap_lang.lang`, and leave it up to * 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. 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) 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`): (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 ...@@ -221,6 +226,8 @@ s/\blist_singletonM_included\b/list_singleton_included/g
s/\bauth_both_frac_op\b/auth_both_op/g s/\bauth_both_frac_op\b/auth_both_op/g
# inv_sep # inv_sep
s/\binv_sep\b/inv_split/g s/\binv_sep\b/inv_split/g
# mnat rename
s/\bmnat\b/max_nat/g
' $(find theories -name "*.v") ' $(find theories -name "*.v")
``` ```
......
...@@ -36,6 +36,11 @@ Section nat. ...@@ -36,6 +36,11 @@ Section nat.
intros ??; apply local_update_unital_discrete=> z _. intros ??; apply local_update_unital_discrete=> z _.
compute -[minus plus]; lia. compute -[minus plus]; lia.
Qed. 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. End nat.
(** ** Natural numbers with [max] as the operation. *) (** ** Natural numbers with [max] as the operation. *)
...@@ -130,11 +135,6 @@ Section min_nat. ...@@ -130,11 +135,6 @@ Section min_nat.
Global Instance : @IdemP min_nat (=) (). Global Instance : @IdemP min_nat (=) ().
Proof. intros [x]. rewrite min_nat_op_min. apply f_equal. lia. Qed. 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. End min_nat.
(** ** Positive integers with [Pos.add] as the operation. *) (** ** Positive integers with [Pos.add] as the operation. *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment