Add some trivial but useful heaplang libraries.

_CoqProject

@@ -116,6 +116,8 @@ theories/heap_lang/lib/clairvoyant_coin.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
+theories/heap_lang/lib/diverge.v
+theories/heap_lang/lib/arith.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v

theories/heap_lang/lib/arith.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(** A library defining binary [minimum] and [maximum] functions, together with
+their expected specs. These operations come up often when working manipulating
+array indices (checking for bounds). *)
+
+Definition minimum : val :=
+  λ: "m" "n", if: "m" < "n" then "m" else "n".
+
+Definition maximum : val :=
+  λ: "m" "n", if: "m" < "n" then "n" else "m".
+
+Lemma minimum_spec `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : Z) :
+  ▷ Φ #(m `min` n) -∗
+  WP minimum #m #n @ s;E {{ Φ }}.
+Proof.
+  iIntros "HΦ". wp_lam. wp_pures. case_bool_decide; wp_pures.
+  - rewrite Z.min_l; [ done | by lia ].
+  - rewrite Z.min_r; [ done | by lia ].
+Qed.
+
+Lemma minimum_spec_nat `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : nat) :
+  ▷ Φ #(m `min` n)%nat -∗
+  WP minimum #m #n @ s;E {{ Φ }}.
+Proof. iIntros "HΦ". iApply minimum_spec. by rewrite Nat2Z.inj_min. Qed.
+
+Lemma maximum_spec `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : Z) :
+  ▷ Φ #(m `max` n) -∗
+  WP maximum #m #n @ s;E {{ Φ }}.
+Proof.
+  iIntros "HΦ". wp_lam. wp_pures. case_bool_decide; wp_pures.
+  - rewrite Z.max_r; [ done | by lia ].
+  - rewrite Z.max_l; [ done | by lia ].
+Qed.
+
+Lemma maximum_spec_nat `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : nat) :
+  ▷ Φ #(m `max` n)%nat -∗
+  WP maximum #m #n @ s;E {{ Φ }}.
+Proof. iIntros "HΦ". iApply maximum_spec. by rewrite Nat2Z.inj_max. Qed.

theories/heap_lang/lib/diverge.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(** This library provides a [diverge] function that goes into an infinite loop
+when provided with an (arbitrary) argument value. This function can be used to
+let the program diverge in corner cases that one wants to omit in proofs. This
+mechanism should be used with care and communicated clearly, obviously.
+
+Note that this mechanism only works when establishing partial correctness with
+the ordinary version of weakest preconditions, and not when establishing total
+correctness using the total version of weakest preconditions.
+
+A typical application for [diverge] is insertion functions for data structures
+having a fixed capacity. In such cases, we can choose divergence instead of an
+explicit error handling when the full capacity has already been reached. *)
+
+Definition diverge : val :=
+  rec: "diverge" "v" := "diverge" "v".
+
+Lemma wp_diverge `{!heapG Σ} s E (Φ : val → iProp Σ) (v : val) :
+  WP diverge v @ s;E {{ Φ }}%I.
+Proof.
+  iLöb as "IH". wp_lam. iApply "IH".
+Qed.