Declare relations on proofmode environments to enable setoid rewriting.

proofmode/coq_tactics.v

@@ -26,6 +26,12 @@ Record envs_wf {M} (Δ : envs M) := {
 
 Coercion of_envs {M} (Δ : envs M) : uPred M :=
   (■ envs_wf Δ ★ □ Π∧ env_persistent Δ ★ Π★ env_spatial Δ)%I.
+Instance: Params (@of_envs) 1.
+
+Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
+  env_persistent_Forall2 : env_Forall2 R (env_persistent Δ1) (env_persistent Δ2);
+  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
+}.
 
 Instance envs_dom {M} : Dom (envs M) stringset := λ Δ,
   dom stringset (env_persistent Δ) ∪ dom stringset (env_spatial Δ).
@@ -252,6 +258,39 @@ Lemma envs_persistent_persistent Δ : envs_persistent Δ = true → PersistentP
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
 Hint Immediate envs_persistent_persistent : typeclass_instances.
 
+Global Instance envs_Forall2_refl (R : relation (uPred M)) :
+  Reflexive R → Reflexive (envs_Forall2 R).
+Proof. by constructor. Qed.
+Global Instance envs_Forall2_sym (R : relation (uPred M)) :
+  Symmetric R → Symmetric (envs_Forall2 R).
+Proof. intros ??? [??]; by constructor. Qed.
+Global Instance envs_Forall2_trans (R : relation (uPred M)) :
+  Transitive R → Transitive (envs_Forall2 R).
+Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
+Global Instance envs_Forall2_antisymm (R R' : relation (uPred M)) :
+  AntiSymm R R' → AntiSymm (envs_Forall2 R) (envs_Forall2 R').
+Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
+Lemma envs_Forall2_impl (R R' : relation (uPred M)) Δ1 Δ2 :
+  envs_Forall2 R Δ1 Δ2 → (∀ P Q, R P Q → R' P Q) → envs_Forall2 R' Δ1 Δ2.
+Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed.
+
+Global Instance of_envs_mono : Proper (envs_Forall2 (⊢) ==> (⊢)) (@of_envs M).
+Proof.
+  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; unfold of_envs; simpl in *.
+  apply const_elim_sep_l=>Hwf. apply sep_intro_True_l.
+  - destruct Hwf; apply const_intro; constructor;
+      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
+  - by repeat f_equiv.
+Qed.
+Global Instance of_envs_proper : Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs M).
+Proof.
+  intros Δ1 Δ2 ?; apply (anti_symm (⊢)); apply of_envs_mono;
+    eapply envs_Forall2_impl; [| |symmetry|]; eauto using equiv_entails.
+Qed.
+Global Instance Envs_mono (R : relation (uPred M)) :
+  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
+Proof. by constructor. Qed.
+
 (** * Adequacy *)
 Lemma tac_adequate P : Envs Enil Enil ⊢ P → True ⊢ P.
 Proof.

proofmode/environments.v

@@ -7,6 +7,8 @@ Inductive env (A : Type) : Type :=
   | Esnoc : env A → string → A → env A.
 Arguments Enil {_}.
 Arguments Esnoc {_} _ _%string _.
+Instance: Params (@Enil) 1.
+Instance: Params (@Esnoc) 1.
 
 Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
 Local Notation "' ( x1 , x2 ) ← y ; z" :=
@@ -28,6 +30,7 @@ Inductive env_wf {A} : env A → Prop :=
 Fixpoint env_to_list {A} (E : env A) : list A :=
   match E with Enil => [] | Esnoc Γ _ x => x :: env_to_list Γ end.
 Coercion env_to_list : env >-> list.
+Instance: Params (@env_to_list) 1.
 
 Instance env_dom {A} : Dom (env A) stringset :=
   fix go Γ := let _ : Dom _ _ := @go in
@@ -201,6 +204,32 @@ Proof. intros. apply (env_split_go_wf Enil Γ Γ1 Γ2 js); eauto. Qed.
 Lemma env_split_perm Γ Γ1 Γ2 js : env_split js Γ = Some (Γ1,Γ2) → Γ ≡ₚ Γ1 ++ Γ2.
 Proof. apply env_split_go_perm. Qed.
 
+Global Instance env_Forall2_refl (P : relation A) :
+  Reflexive P → Reflexive (env_Forall2 P).
+Proof. intros ? Γ. induction Γ; constructor; auto. Qed.
+Global Instance env_Forall2_sym (P : relation A) :
+  Symmetric P → Symmetric (env_Forall2 P).
+Proof. induction 2; constructor; auto. Qed.
+Global Instance env_Forall2_trans (P : relation A) :
+  Transitive P → Transitive (env_Forall2 P).
+Proof.
+  intros ? Γ1 Γ2 Γ3 HΓ; revert Γ3.
+  induction HΓ; inversion_clear 1; constructor; eauto.
+Qed.
+Global Instance env_Forall2_antisymm (P Q : relation A) :
+  AntiSymm P Q → AntiSymm (env_Forall2 P) (env_Forall2 Q).
+Proof. induction 2; inversion_clear 1; constructor; auto. Qed.
+Lemma env_Forall2_impl {B} (P Q : A → B → Prop) Γ Σ :
+  env_Forall2 P Γ Σ → (∀ x y, P x y → Q x y) → env_Forall2 Q Γ Σ.
+Proof. induction 1; constructor; eauto. Qed.
+
+Global Instance Esnoc_proper (P : relation A) :
+  Proper (env_Forall2 P ==> (=) ==> P ==> env_Forall2 P) Esnoc.
+Proof. intros Γ1 Γ2 HΓ i ? <-; by constructor. Qed.
+Global Instance env_to_list_proper (P : relation A) :
+  Proper (env_Forall2 P ==> Forall2 P) env_to_list.
+Proof. induction 1; constructor; auto. Qed.
+
 Lemma env_Forall2_fresh {B} (P : A → B → Prop) Γ Σ i :
   env_Forall2 P Γ Σ → Γ !! i = None → Σ !! i = None.
 Proof. by induction 1; simplify. Qed.