Library iris.heap_lang.lib.arith
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.prelude Require Import options.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.prelude Require Import options.
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 `{!heapGS Σ} 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 `{!heapGS Σ} 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 `{!heapGS Σ} 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 `{!heapGS Σ} 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.