Decicated version of string decider for the proof mode.

This way we avoid the env_cbv tactic unfolding string related stuff
that appears in the goal and hypotheses of the proof mode.

_CoqProject

@@ -117,6 +117,7 @@ tests/barrier_client.v
 tests/list_reverse.v
 tests/tree_sum.v
 tests/counter.v
+proofmode/strings.v
 proofmode/coq_tactics.v
 proofmode/environments.v
 proofmode/intro_patterns.v

proofmode/coq_tactics.v

@@ -187,11 +187,11 @@ Proof.
   apply wand_intro_l; destruct p; simpl.
   - apply sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
-      intros j; case_decide; naive_solver.
+      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
     + by rewrite always_sep assoc.
   - apply sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
-      intros j; case_decide; naive_solver.
+      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
     + solve_sep_entails.
 Qed.
 

proofmode/environments.v

 From iris.prelude Require Export strings.
+From iris.proofmode Require Import strings.
 From iris.algebra Require Export base.
 From iris.prelude Require Import stringmap.
 
@@ -13,7 +14,7 @@ Instance: Params (@Esnoc) 1.
 Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
   match Γ with
   | Enil => None
-  | Esnoc Γ j x => if decide (i = j) then Some x else env_lookup i Γ
+  | Esnoc Γ j x => if string_beq i j then Some x else env_lookup i Γ
   end.
 
 Module env_notations.
@@ -50,7 +51,7 @@ Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) :
   match Γ with
   | Enil => None
   | Esnoc Γ j x =>
-     if decide (i = j) then env_app Γi Γ else
+     if string_beq i j then env_app Γi Γ else
      match Γi !! j with
      | None => Γ' ← env_replace i Γi Γ; Some (Esnoc Γ' j x)
      | Some _ => None
@@ -60,14 +61,14 @@ Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) :
 Fixpoint env_delete {A} (i : string) (Γ : env A) : env A :=
   match Γ with
   | Enil => Enil
-  | Esnoc Γ j x => if decide (i = j) then Γ else Esnoc (env_delete i Γ) j x
+  | Esnoc Γ j x => if string_beq i j then Γ else Esnoc (env_delete i Γ) j x
   end.
 
 Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
   match Γ with
   | Enil => None
   | Esnoc Γ j x =>
-     if decide (i = j) then Some (x,Γ)
+     if string_beq i j then Some (x,Γ)
      else '(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
   end.
 
@@ -83,7 +84,13 @@ Implicit Types i : string.
 Implicit Types x : A.
 Hint Resolve Esnoc_wf Enil_wf.
 
-Ltac simplify := repeat (case_match || simplify_option_eq).
+Ltac simplify :=
+  repeat match goal with
+  | _ => progress simplify_eq/=
+  | H : context [string_beq ?s1 ?s2] |- _ => destruct (string_beq_reflect s1 s2)
+  | |- context [string_beq ?s1 ?s2] => destruct (string_beq_reflect s1 s2)
+  | _ => case_match
+  end.
 
 Lemma env_lookup_perm Γ i x : Γ !! i = Some x → Γ ≡ₚ x :: env_delete i Γ.
 Proof.
@@ -130,10 +137,8 @@ Proof. revert Γ'. induction Γ; intros; simplify; eauto. Qed.
 Lemma env_replace_perm Γ Γi Γ' i :
   env_replace i Γi Γ = Some Γ' → Γ' ≡ₚ Γi ++ env_delete i Γ.
 Proof.
-  revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify_eq/=.
-  destruct (decide (i = j)); simplify_eq/=; auto using env_app_perm.
-  destruct (Γi !! j), (env_replace i Γi Γ) as [Γ''|] eqn:?; simplify_eq/=.
-  rewrite -Permutation_middle; f_equiv; eauto.
+  revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify; auto using env_app_perm.
+  rewrite -Permutation_middle -IH //.
 Qed.
 
 Lemma env_lookup_delete_correct Γ i :

proofmode/strings.v

+From iris.prelude Require Import strings.
+From iris.algebra Require Import base.
+From Coq Require Import Ascii.
+
+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.
+
+Definition beq (b1 b2 : bool) : bool :=
+  match b1, b2 with
+  | false, false | true, true => true
+  | _, _ => false
+  end.
+
+Definition ascii_beq (x y : ascii) : bool :=
+  let 'Ascii x1 x2 x3 x4 x5 x6 x7 x8 := x in
+  let 'Ascii y1 y2 y3 y4 y5 y6 y7 y8 := y in
+  beq x1 y1 && beq x2 y2 && beq x3 y3 && beq x4 y4 &&
+    beq x5 y5 && beq x6 y6 && beq x7 y7 && beq x8 y8.
+
+Fixpoint string_beq (s1 s2 : string) : bool :=
+  match s1, s2 with 
+  | "", "" => true
+  | String a1 s1, String a2 s2 => ascii_beq a1 a2 && string_beq s1 s2
+  | _, _ => false
+  end.
+
+Lemma beq_true b1 b2 : beq b1 b2 = true ↔ b1 = b2.
+Proof. destruct b1, b2; simpl; intuition congruence. Qed.
+
+Lemma ascii_beq_true x y : ascii_beq x y = true ↔ x = y.
+Proof.
+  destruct x, y; rewrite /= !lazy_andb_true !beq_true. intuition congruence.
+Qed.
+
+Lemma string_beq_true s1 s2 : string_beq s1 s2 = true ↔ s1 = s2.
+Proof.
+  revert s2. induction s1 as [|x s1 IH]=> -[|y s2] //=.
+  rewrite lazy_andb_true ascii_beq_true IH. intuition congruence.
+Qed.
+
+Lemma string_beq_reflect s1 s2 : reflect (s1 = s2) (string_beq s1 s2).
+Proof. apply iff_reflect. by rewrite string_beq_true. Qed.

proofmode/tactics.v

@@ -4,14 +4,11 @@ From iris.base_logic Require Export base_logic.
 From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
 From iris.prelude Require Import stringmap hlist.
+From iris.proofmode Require Import strings.
 
 Declare Reduction env_cbv := cbv [
+  beq ascii_beq string_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
-  decide (* operational classes *)
-  sumbool_rec sumbool_rect (* sumbool *)
-  bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *)
-  assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
-  string_eq_dec string_rec string_rect (* strings *)
   env_persistent env_spatial env_spatial_is_nil envs_dom
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
     envs_simple_replace envs_replace envs_split