From 9084fa771d612ca2382f211a80eb50c59264bfe9 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Thu, 18 Jun 2020 10:01:49 +0200
Subject: [PATCH] Add local update for min_nat and minor tweaks

---
 theories/algebra/numbers.v | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
index cfc0fa746..e7443c7a2 100644
--- a/theories/algebra/numbers.v
+++ b/theories/algebra/numbers.v
@@ -81,16 +81,16 @@ Section max_nat.
   Global Instance max_nat_core_id (x : max_nat) : CoreId x.
   Proof. by constructor. Qed.
 
-  Lemma max_nat_local_update (x y x' : max_natUR) :
+  Lemma max_nat_local_update (x y x' : max_nat) :
     max_nat_car x ≤ max_nat_car x' → (x,y) ~l~> (x',x').
   Proof.
-    move: x y x' => [x] [y] [y'] /= ??.
-    apply local_update_unital_discrete=> [[z]] _.
-    rewrite 2!max_nat_op_max. inversion 1.
+    move: x y x' => [x] [y] [y'] /= ?.
+    rewrite local_update_unital_discrete=> [[z]] _.
+    rewrite 2!max_nat_op_max. intros [= ?].
     split; first done. apply f_equal. lia.
   Qed.
 
-  Global Instance : @IdemP max_nat (=) (â‹…).
+  Global Instance : IdemP (=@{max_nat}) (â‹…).
   Proof. intros [x]. rewrite max_nat_op_max. apply f_equal. lia. Qed.
 End max_nat.
 
@@ -127,13 +127,22 @@ Section min_nat.
   Global Instance min_nat_core_id (x : min_nat) : CoreId x.
   Proof. by constructor. Qed.
 
+  Lemma min_nat_local_update (x y x' : min_nat) :
+    min_nat_car x' ≤ min_nat_car x → (x,y) ~l~> (x',x').
+  Proof.
+    move: x y x' => [x] [y] [x'] /= ?.
+    rewrite local_update_discrete. move=> [[z]|] _ /=; last done.
+    rewrite 2!min_nat_op_min. intros [= ?].
+    split; first done. apply f_equal. lia.
+  Qed.
+
   Global Instance : LeftAbsorb (=) (MinNat 0) (â‹…).
   Proof. done. Qed.
 
   Global Instance : RightAbsorb (=) (MinNat 0) (â‹…).
   Proof. intros [x]. by rewrite min_nat_op_min Min.min_0_r. Qed.
 
-  Global Instance : @IdemP min_nat (=) (â‹…).
+  Global Instance : IdemP (=@{min_nat}) (â‹…).
   Proof. intros [x]. rewrite min_nat_op_min. apply f_equal. lia. Qed.
 End min_nat.
 
-- 
GitLab