From 01c940bd78e9ecd530406ab893dd0d1a49ac8675 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 16 Jun 2018 23:15:16 +0200
Subject: [PATCH] remove Pos.succ from proofmode unfold list by making a copy

---
 theories/proofmode/base.v         | 13 ++++++++++---
 theories/proofmode/environments.v |  2 +-
 theories/proofmode/reduction.v    |  5 +----
 3 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 1e8dff008..2fe6e8f72 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -8,14 +8,21 @@ Set Default Proof Using "Type".
 (* Directions of rewrites *)
 Inductive direction := Left | Right.
 
-(* Some specific versions of operations on strings 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. *)
+(* 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.
 Proof. destruct b1, b2; intuition congruence. Qed.
 
+Fixpoint Pos_succ (x : positive) : positive :=
+  match x with
+  | (p~1)%positive => ((Pos_succ p)~0)%positive
+  | (p~0)%positive => (p~1)%positive
+  | 1%positive => 2%positive
+  end.
+
 Definition beq (b1 b2 : bool) : bool :=
   match b1, b2 with
   | false, false | true, true => true
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index e27df4704..cdca5f137 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -312,7 +312,7 @@ Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
   Envs Enil (env_spatial Δ) (env_counter Δ).
 
 Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos.succ (env_counter Δ)).
+  Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos_succ (env_counter Δ)).
 
 Fixpoint envs_split_go {PROP}
     (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 2133bd593..79046c3d0 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import base environments.
 Declare Reduction pm_cbv := cbv [
   (* base *)
   pm_option_bind pm_from_option pm_option_fun
-  base.beq base.ascii_beq base.string_beq base.positive_beq base.ident_beq
+  base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
   (* environments *)
   env_lookup env_lookup_delete env_delete env_app env_replace
   env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
@@ -12,9 +12,6 @@ Declare Reduction pm_cbv := cbv [
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_persistent envs_incr_counter
   envs_split_go envs_split prop_of_env
-  (* other modules. TODO: we should probably make copies of these,
-     but what will that break? *)
-  Pos.succ
 ].
 Ltac pm_eval t :=
   let u := eval pm_cbv in t in
-- 
GitLab