arith.v 1.56 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
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.